Search for blocks/addresses/...

Proofgold Address

address
PUVEYgknVTPAXWKm6riNQFpsraHq1kwsMbn
total
0
mg
-
conjpub
-
current assets
a40a0../bf7c8.. bday: 2902 doc published by PrGxv..
Param 0fc90.. : ι(ιι) → ι
Param 4ae4a.. : ιι
Param 4a7ef.. : ι
Param If_i : οιιι
Param d2155.. : ι(ιιο) → ι
Param 1216a.. : ι(ιο) → ι
Definition 81367.. := λ x0 . λ x1 : ι → ι . λ x2 : ι → ι → ο . λ x3 : ι → ο . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) (0fc90.. x0 x1) (If_i (x4 = 4ae4a.. (4ae4a.. 4a7ef..)) (d2155.. x0 x2) (1216a.. x0 x3))))
Param f482f.. : ιιι
Known 9f6be.. : ∀ x0 x1 x2 x3 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) x1 (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 x3)))) 4a7ef.. = x0
Theorem c51b5.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . x0 = 81367.. x1 x2 x3 x4x1 = f482f.. x0 4a7ef.. (proof)
Theorem 3a064.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . x0 = f482f.. (81367.. x0 x1 x2 x3) 4a7ef.. (proof)
Known 8a328.. : ∀ x0 x1 x2 x3 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) x1 (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 x3)))) (4ae4a.. 4a7ef..) = x1
Known f22ec.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0f482f.. (0fc90.. x0 x1) x2 = x1 x2
Theorem 1a110.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . x0 = 81367.. x1 x2 x3 x4∀ x5 . prim1 x5 x1x2 x5 = f482f.. (f482f.. x0 (4ae4a.. 4a7ef..)) x5 (proof)
Theorem 2e323.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . prim1 x4 x0x1 x4 = f482f.. (f482f.. (81367.. x0 x1 x2 x3) (4ae4a.. 4a7ef..)) x4 (proof)
Param 2b2e3.. : ιιιο
Known 142e6.. : ∀ x0 x1 x2 x3 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) x1 (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 x3)))) (4ae4a.. (4ae4a.. 4a7ef..)) = x2
Known 67416.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 . prim1 x2 x0∀ x3 . prim1 x3 x02b2e3.. (d2155.. x0 x1) x2 x3 = x1 x2 x3
Theorem 65b5f.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . x0 = 81367.. x1 x2 x3 x4∀ x5 . prim1 x5 x1∀ x6 . prim1 x6 x1x3 x5 x6 = 2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6 (proof)
Theorem 9fe37.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . prim1 x4 x0∀ x5 . prim1 x5 x0x2 x4 x5 = 2b2e3.. (f482f.. (81367.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. 4a7ef..))) x4 x5 (proof)
Param decode_p : ιιο
Known 62a6b.. : ∀ x0 x1 x2 x3 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) x1 (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 x3)))) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) = x3
Known 931fe.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0decode_p (1216a.. x0 x1) x2 = x1 x2
Theorem 32c95.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . x0 = 81367.. x1 x2 x3 x4∀ x5 . prim1 x5 x1x4 x5 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5 (proof)
Theorem f5ffc.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . prim1 x4 x0x3 x4 = decode_p (f482f.. (81367.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 (proof)
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Known and4I : ∀ x0 x1 x2 x3 : ο . x0x1x2x3and (and (and x0 x1) x2) x3
Theorem c5aab.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ο . ∀ x6 x7 : ι → ο . 81367.. x0 x2 x4 x6 = 81367.. x1 x3 x5 x7and (and (and (x0 = x1) (∀ x8 . prim1 x8 x0x2 x8 = x3 x8)) (∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0x4 x8 x9 = x5 x8 x9)) (∀ x8 . prim1 x8 x0x6 x8 = x7 x8) (proof)
Param iff : οοο
Known ee7ef.. : ∀ x0 . ∀ x1 x2 : ι → ο . (∀ x3 . prim1 x3 x0iff (x1 x3) (x2 x3))1216a.. x0 x1 = 1216a.. x0 x2
Known 62ef7.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . (∀ x3 . prim1 x3 x0∀ x4 . prim1 x4 x0iff (x1 x3 x4) (x2 x3 x4))d2155.. x0 x1 = d2155.. x0 x2
Known 4402a.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0x1 x3 = x2 x3)0fc90.. x0 x1 = 0fc90.. x0 x2
Theorem f9c4e.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 : ι → ι → ο . ∀ x5 x6 : ι → ο . (∀ x7 . prim1 x7 x0x1 x7 = x2 x7)(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0iff (x3 x7 x8) (x4 x7 x8))(∀ x7 . prim1 x7 x0iff (x5 x7) (x6 x7))81367.. x0 x1 x3 x5 = 81367.. x0 x2 x4 x6 (proof)
Definition 86f84.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι . (∀ x4 . prim1 x4 x2prim1 (x3 x4) x2)∀ x4 : ι → ι → ο . ∀ x5 : ι → ο . x1 (81367.. x2 x3 x4 x5))x1 x0
Theorem d85c0.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0prim1 (x1 x2) x0)∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . 86f84.. (81367.. x0 x1 x2 x3) (proof)
Theorem cd0a3.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . 86f84.. (81367.. x0 x1 x2 x3)∀ x4 . prim1 x4 x0prim1 (x1 x4) x0 (proof)
Known iff_refl : ∀ x0 : ο . iff x0 x0
Theorem 81349.. : ∀ x0 . 86f84.. x0x0 = 81367.. (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Definition 3e28b.. := λ x0 . λ x1 : ι → (ι → ι)(ι → ι → ο)(ι → ο) → ι . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem dff40.. : ∀ x0 : ι → (ι → ι)(ι → ι → ο)(ι → ο) → ι . ∀ x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . (∀ x5 : ι → ι . (∀ x6 . prim1 x6 x1x2 x6 = x5 x6)∀ x6 : ι → ι → ο . (∀ x7 . prim1 x7 x1∀ x8 . prim1 x8 x1iff (x3 x7 x8) (x6 x7 x8))∀ x7 : ι → ο . (∀ x8 . prim1 x8 x1iff (x4 x8) (x7 x8))x0 x1 x5 x6 x7 = x0 x1 x2 x3 x4)3e28b.. (81367.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition 7d7bf.. := λ x0 . λ x1 : ι → (ι → ι)(ι → ι → ο)(ι → ο) → ο . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 90754.. : ∀ x0 : ι → (ι → ι)(ι → ι → ο)(ι → ο) → ο . ∀ x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . (∀ x5 : ι → ι . (∀ x6 . prim1 x6 x1x2 x6 = x5 x6)∀ x6 : ι → ι → ο . (∀ x7 . prim1 x7 x1∀ x8 . prim1 x8 x1iff (x3 x7 x8) (x6 x7 x8))∀ x7 : ι → ο . (∀ x8 . prim1 x8 x1iff (x4 x8) (x7 x8))x0 x1 x5 x6 x7 = x0 x1 x2 x3 x4)7d7bf.. (81367.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition 1bcc7.. := λ x0 . λ x1 : ι → ι . λ x2 : ι → ι → ο . λ x3 . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) (0fc90.. x0 x1) (If_i (x4 = 4ae4a.. (4ae4a.. 4a7ef..)) (d2155.. x0 x2) x3)))
Theorem 12274.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 . x0 = 1bcc7.. x1 x2 x3 x4x1 = f482f.. x0 4a7ef.. (proof)
Theorem f7360.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 . x0 = f482f.. (1bcc7.. x0 x1 x2 x3) 4a7ef.. (proof)
Theorem 72790.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 . x0 = 1bcc7.. x1 x2 x3 x4∀ x5 . prim1 x5 x1x2 x5 = f482f.. (f482f.. x0 (4ae4a.. 4a7ef..)) x5 (proof)
Theorem b995b.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 . prim1 x4 x0x1 x4 = f482f.. (f482f.. (1bcc7.. x0 x1 x2 x3) (4ae4a.. 4a7ef..)) x4 (proof)
Theorem 13468.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 . x0 = 1bcc7.. x1 x2 x3 x4∀ x5 . prim1 x5 x1∀ x6 . prim1 x6 x1x3 x5 x6 = 2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6 (proof)
Theorem fe79a.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 . prim1 x4 x0∀ x5 . prim1 x5 x0x2 x4 x5 = 2b2e3.. (f482f.. (1bcc7.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. 4a7ef..))) x4 x5 (proof)
Theorem 1502a.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 . x0 = 1bcc7.. x1 x2 x3 x4x4 = f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem 915b7.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 . x3 = f482f.. (1bcc7.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem 1b17b.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ι → ο . ∀ x6 x7 . 1bcc7.. x0 x2 x4 x6 = 1bcc7.. x1 x3 x5 x7and (and (and (x0 = x1) (∀ x8 . prim1 x8 x0x2 x8 = x3 x8)) (∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0x4 x8 x9 = x5 x8 x9)) (x6 = x7) (proof)
Theorem e4331.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 : ι → ι → ο . ∀ x5 . (∀ x6 . prim1 x6 x0x1 x6 = x2 x6)(∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0iff (x3 x6 x7) (x4 x6 x7))1bcc7.. x0 x1 x3 x5 = 1bcc7.. x0 x2 x4 x5 (proof)
Definition 6100b.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι . (∀ x4 . prim1 x4 x2prim1 (x3 x4) x2)∀ x4 : ι → ι → ο . ∀ x5 . prim1 x5 x2x1 (1bcc7.. x2 x3 x4 x5))x1 x0
Theorem 39190.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0prim1 (x1 x2) x0)∀ x2 : ι → ι → ο . ∀ x3 . prim1 x3 x06100b.. (1bcc7.. x0 x1 x2 x3) (proof)
Theorem f7341.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 . 6100b.. (1bcc7.. x0 x1 x2 x3)∀ x4 . prim1 x4 x0prim1 (x1 x4) x0 (proof)
Theorem 5041b.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 . 6100b.. (1bcc7.. x0 x1 x2 x3)prim1 x3 x0 (proof)
Theorem 6f356.. : ∀ x0 . 6100b.. x0x0 = 1bcc7.. (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Definition 79719.. := λ x0 . λ x1 : ι → (ι → ι)(ι → ι → ο)ι → ι . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem 33e73.. : ∀ x0 : ι → (ι → ι)(ι → ι → ο)ι → ι . ∀ x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 . (∀ x5 : ι → ι . (∀ x6 . prim1 x6 x1x2 x6 = x5 x6)∀ x6 : ι → ι → ο . (∀ x7 . prim1 x7 x1∀ x8 . prim1 x8 x1iff (x3 x7 x8) (x6 x7 x8))x0 x1 x5 x6 x4 = x0 x1 x2 x3 x4)79719.. (1bcc7.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition 7557e.. := λ x0 . λ x1 : ι → (ι → ι)(ι → ι → ο)ι → ο . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem 3e25e.. : ∀ x0 : ι → (ι → ι)(ι → ι → ο)ι → ο . ∀ x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 . (∀ x5 : ι → ι . (∀ x6 . prim1 x6 x1x2 x6 = x5 x6)∀ x6 : ι → ι → ο . (∀ x7 . prim1 x7 x1∀ x8 . prim1 x8 x1iff (x3 x7 x8) (x6 x7 x8))x0 x1 x5 x6 x4 = x0 x1 x2 x3 x4)7557e.. (1bcc7.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition 1cd8e.. := λ x0 . λ x1 : ι → ι . λ x2 : ι → ο . λ x3 . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) (0fc90.. x0 x1) (If_i (x4 = 4ae4a.. (4ae4a.. 4a7ef..)) (1216a.. x0 x2) x3)))
Theorem 47259.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 . x0 = 1cd8e.. x1 x2 x3 x4x1 = f482f.. x0 4a7ef.. (proof)
Theorem 9db4b.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . ∀ x3 . x0 = f482f.. (1cd8e.. x0 x1 x2 x3) 4a7ef.. (proof)
Theorem 59148.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 . x0 = 1cd8e.. x1 x2 x3 x4∀ x5 . prim1 x5 x1x2 x5 = f482f.. (f482f.. x0 (4ae4a.. 4a7ef..)) x5 (proof)
Theorem 02a4b.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . ∀ x3 x4 . prim1 x4 x0x1 x4 = f482f.. (f482f.. (1cd8e.. x0 x1 x2 x3) (4ae4a.. 4a7ef..)) x4 (proof)
Theorem dadc3.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 . x0 = 1cd8e.. x1 x2 x3 x4∀ x5 . prim1 x5 x1x3 x5 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x5 (proof)
Theorem 13aa7.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . ∀ x3 x4 . prim1 x4 x0x2 x4 = decode_p (f482f.. (1cd8e.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. 4a7ef..))) x4 (proof)
Theorem 72e88.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 . x0 = 1cd8e.. x1 x2 x3 x4x4 = f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem 42ff4.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . ∀ x3 . x3 = f482f.. (1cd8e.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem c9420.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 x5 : ι → ο . ∀ x6 x7 . 1cd8e.. x0 x2 x4 x6 = 1cd8e.. x1 x3 x5 x7and (and (and (x0 = x1) (∀ x8 . prim1 x8 x0x2 x8 = x3 x8)) (∀ x8 . prim1 x8 x0x4 x8 = x5 x8)) (x6 = x7) (proof)
Theorem 6a79a.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 : ι → ο . ∀ x5 . (∀ x6 . prim1 x6 x0x1 x6 = x2 x6)(∀ x6 . prim1 x6 x0iff (x3 x6) (x4 x6))1cd8e.. x0 x1 x3 x5 = 1cd8e.. x0 x2 x4 x5 (proof)
Definition 49e31.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι . (∀ x4 . prim1 x4 x2prim1 (x3 x4) x2)∀ x4 : ι → ο . ∀ x5 . prim1 x5 x2x1 (1cd8e.. x2 x3 x4 x5))x1 x0
Theorem b756b.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0prim1 (x1 x2) x0)∀ x2 : ι → ο . ∀ x3 . prim1 x3 x049e31.. (1cd8e.. x0 x1 x2 x3) (proof)
Theorem 42fa4.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . ∀ x3 . 49e31.. (1cd8e.. x0 x1 x2 x3)∀ x4 . prim1 x4 x0prim1 (x1 x4) x0 (proof)
Theorem c70df.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . ∀ x3 . 49e31.. (1cd8e.. x0 x1 x2 x3)prim1 x3 x0 (proof)
Theorem da228.. : ∀ x0 . 49e31.. x0x0 = 1cd8e.. (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Definition 68d20.. := λ x0 . λ x1 : ι → (ι → ι)(ι → ο)ι → ι . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem b8cba.. : ∀ x0 : ι → (ι → ι)(ι → ο)ι → ι . ∀ x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 . (∀ x5 : ι → ι . (∀ x6 . prim1 x6 x1x2 x6 = x5 x6)∀ x6 : ι → ο . (∀ x7 . prim1 x7 x1iff (x3 x7) (x6 x7))x0 x1 x5 x6 x4 = x0 x1 x2 x3 x4)68d20.. (1cd8e.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition 4ea01.. := λ x0 . λ x1 : ι → (ι → ι)(ι → ο)ι → ο . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem 36171.. : ∀ x0 : ι → (ι → ι)(ι → ο)ι → ο . ∀ x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ο . ∀ x4 . (∀ x5 : ι → ι . (∀ x6 . prim1 x6 x1x2 x6 = x5 x6)∀ x6 : ι → ο . (∀ x7 . prim1 x7 x1iff (x3 x7) (x6 x7))x0 x1 x5 x6 x4 = x0 x1 x2 x3 x4)4ea01.. (1cd8e.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition 3bbe6.. := λ x0 . λ x1 x2 : ι → ι → ο . λ x3 : ι → ο . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) (d2155.. x0 x1) (If_i (x4 = 4ae4a.. (4ae4a.. 4a7ef..)) (d2155.. x0 x2) (1216a.. x0 x3))))
Theorem 04e59.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 : ι → ο . x0 = 3bbe6.. x1 x2 x3 x4x1 = f482f.. x0 4a7ef.. (proof)
Theorem 3a341.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 : ι → ο . x0 = f482f.. (3bbe6.. x0 x1 x2 x3) 4a7ef.. (proof)
Theorem 42b73.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 : ι → ο . x0 = 3bbe6.. x1 x2 x3 x4∀ x5 . prim1 x5 x1∀ x6 . prim1 x6 x1x2 x5 x6 = 2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..)) x5 x6 (proof)
Theorem f2271.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . prim1 x4 x0∀ x5 . prim1 x5 x0x1 x4 x5 = 2b2e3.. (f482f.. (3bbe6.. x0 x1 x2 x3) (4ae4a.. 4a7ef..)) x4 x5 (proof)
Theorem 2ef07.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 : ι → ο . x0 = 3bbe6.. x1 x2 x3 x4∀ x5 . prim1 x5 x1∀ x6 . prim1 x6 x1x3 x5 x6 = 2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6 (proof)
Theorem 9bb3e.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . prim1 x4 x0∀ x5 . prim1 x5 x0x2 x4 x5 = 2b2e3.. (f482f.. (3bbe6.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. 4a7ef..))) x4 x5 (proof)
Theorem aacc9.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 : ι → ο . x0 = 3bbe6.. x1 x2 x3 x4∀ x5 . prim1 x5 x1x4 x5 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5 (proof)
Theorem 0b18c.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . prim1 x4 x0x3 x4 = decode_p (f482f.. (3bbe6.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 (proof)
Theorem 6adab.. : ∀ x0 x1 . ∀ x2 x3 x4 x5 : ι → ι → ο . ∀ x6 x7 : ι → ο . 3bbe6.. x0 x2 x4 x6 = 3bbe6.. x1 x3 x5 x7and (and (and (x0 = x1) (∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0x2 x8 x9 = x3 x8 x9)) (∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0x4 x8 x9 = x5 x8 x9)) (∀ x8 . prim1 x8 x0x6 x8 = x7 x8) (proof)
Theorem 827c4.. : ∀ x0 . ∀ x1 x2 x3 x4 : ι → ι → ο . ∀ x5 x6 : ι → ο . (∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0iff (x1 x7 x8) (x2 x7 x8))(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0iff (x3 x7 x8) (x4 x7 x8))(∀ x7 . prim1 x7 x0iff (x5 x7) (x6 x7))3bbe6.. x0 x1 x3 x5 = 3bbe6.. x0 x2 x4 x6 (proof)
Definition 0b60a.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 x4 : ι → ι → ο . ∀ x5 : ι → ο . x1 (3bbe6.. x2 x3 x4 x5))x1 x0
Theorem e65f7.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 : ι → ο . 0b60a.. (3bbe6.. x0 x1 x2 x3) (proof)
Theorem dc474.. : ∀ x0 . 0b60a.. x0x0 = 3bbe6.. (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Definition ed32f.. := λ x0 . λ x1 : ι → (ι → ι → ο)(ι → ι → ο)(ι → ο) → ι . x1 (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 33736.. : ∀ x0 : ι → (ι → ι → ο)(ι → ι → ο)(ι → ο) → ι . ∀ x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 : ι → ο . (∀ x5 : ι → ι → ο . (∀ x6 . prim1 x6 x1∀ x7 . prim1 x7 x1iff (x2 x6 x7) (x5 x6 x7))∀ x6 : ι → ι → ο . (∀ x7 . prim1 x7 x1∀ x8 . prim1 x8 x1iff (x3 x7 x8) (x6 x7 x8))∀ x7 : ι → ο . (∀ x8 . prim1 x8 x1iff (x4 x8) (x7 x8))x0 x1 x5 x6 x7 = x0 x1 x2 x3 x4)ed32f.. (3bbe6.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition 29e37.. := λ x0 . λ x1 : ι → (ι → ι → ο)(ι → ι → ο)(ι → ο) → ο . x1 (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 53bce.. : ∀ x0 : ι → (ι → ι → ο)(ι → ι → ο)(ι → ο) → ο . ∀ x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 : ι → ο . (∀ x5 : ι → ι → ο . (∀ x6 . prim1 x6 x1∀ x7 . prim1 x7 x1iff (x2 x6 x7) (x5 x6 x7))∀ x6 : ι → ι → ο . (∀ x7 . prim1 x7 x1∀ x8 . prim1 x8 x1iff (x3 x7 x8) (x6 x7 x8))∀ x7 : ι → ο . (∀ x8 . prim1 x8 x1iff (x4 x8) (x7 x8))x0 x1 x5 x6 x7 = x0 x1 x2 x3 x4)29e37.. (3bbe6.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition 1f7e2.. := λ x0 . λ x1 x2 : ι → ι → ο . λ x3 . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) (d2155.. x0 x1) (If_i (x4 = 4ae4a.. (4ae4a.. 4a7ef..)) (d2155.. x0 x2) x3)))
Theorem 56e41.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 . x0 = 1f7e2.. x1 x2 x3 x4x1 = f482f.. x0 4a7ef.. (proof)
Theorem d8aec.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 . x0 = f482f.. (1f7e2.. x0 x1 x2 x3) 4a7ef.. (proof)
Theorem a72d5.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 . x0 = 1f7e2.. x1 x2 x3 x4∀ x5 . prim1 x5 x1∀ x6 . prim1 x6 x1x2 x5 x6 = 2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..)) x5 x6 (proof)
Theorem 45188.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 x4 . prim1 x4 x0∀ x5 . prim1 x5 x0x1 x4 x5 = 2b2e3.. (f482f.. (1f7e2.. x0 x1 x2 x3) (4ae4a.. 4a7ef..)) x4 x5 (proof)
Theorem 39d3e.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 . x0 = 1f7e2.. x1 x2 x3 x4∀ x5 . prim1 x5 x1∀ x6 . prim1 x6 x1x3 x5 x6 = 2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6 (proof)
Theorem b362f.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 x4 . prim1 x4 x0∀ x5 . prim1 x5 x0x2 x4 x5 = 2b2e3.. (f482f.. (1f7e2.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. 4a7ef..))) x4 x5 (proof)
Theorem c3fd7.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 . x0 = 1f7e2.. x1 x2 x3 x4x4 = f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem d2b0c.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 . x3 = f482f.. (1f7e2.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem 1d1cc.. : ∀ x0 x1 . ∀ x2 x3 x4 x5 : ι → ι → ο . ∀ x6 x7 . 1f7e2.. x0 x2 x4 x6 = 1f7e2.. x1 x3 x5 x7and (and (and (x0 = x1) (∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0x2 x8 x9 = x3 x8 x9)) (∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0x4 x8 x9 = x5 x8 x9)) (x6 = x7) (proof)
Theorem ca557.. : ∀ x0 . ∀ x1 x2 x3 x4 : ι → ι → ο . ∀ x5 . (∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0iff (x1 x6 x7) (x2 x6 x7))(∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0iff (x3 x6 x7) (x4 x6 x7))1f7e2.. x0 x1 x3 x5 = 1f7e2.. x0 x2 x4 x5 (proof)
Definition d97ab.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 x4 : ι → ι → ο . ∀ x5 . prim1 x5 x2x1 (1f7e2.. x2 x3 x4 x5))x1 x0
Theorem a0ca8.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 . prim1 x3 x0d97ab.. (1f7e2.. x0 x1 x2 x3) (proof)
Theorem 2b61f.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 . d97ab.. (1f7e2.. x0 x1 x2 x3)prim1 x3 x0 (proof)
Theorem 75acf.. : ∀ x0 . d97ab.. x0x0 = 1f7e2.. (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Definition 85b48.. := λ x0 . λ x1 : ι → (ι → ι → ο)(ι → ι → ο)ι → ι . x1 (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem 46416.. : ∀ x0 : ι → (ι → ι → ο)(ι → ι → ο)ι → ι . ∀ x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 . (∀ x5 : ι → ι → ο . (∀ x6 . prim1 x6 x1∀ x7 . prim1 x7 x1iff (x2 x6 x7) (x5 x6 x7))∀ x6 : ι → ι → ο . (∀ x7 . prim1 x7 x1∀ x8 . prim1 x8 x1iff (x3 x7 x8) (x6 x7 x8))x0 x1 x5 x6 x4 = x0 x1 x2 x3 x4)85b48.. (1f7e2.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition 16053.. := λ x0 . λ x1 : ι → (ι → ι → ο)(ι → ι → ο)ι → ο . x1 (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem 6f4cb.. : ∀ x0 : ι → (ι → ι → ο)(ι → ι → ο)ι → ο . ∀ x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 . (∀ x5 : ι → ι → ο . (∀ x6 . prim1 x6 x1∀ x7 . prim1 x7 x1iff (x2 x6 x7) (x5 x6 x7))∀ x6 : ι → ι → ο . (∀ x7 . prim1 x7 x1∀ x8 . prim1 x8 x1iff (x3 x7 x8) (x6 x7 x8))x0 x1 x5 x6 x4 = x0 x1 x2 x3 x4)16053.. (1f7e2.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)

previous assets