Proofgold Asset

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 x4 ⟶ x1 = 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 x0 ⟶ f482f.. (0fc90.. x0 x1) x2 = x1 x2
Theorem 1a110.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . x0 = 81367.. x1 x2 x3 x4 ⟶ ∀ x5 . prim1 x5 x1 ⟶ x2 x5 = f482f.. (f482f.. x0 (4ae4a.. 4a7ef..)) x5 (proof)
Theorem 2e323.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . prim1 x4 x0 ⟶ x1 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 x0 ⟶ 2b2e3.. (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 x1 ⟶ x3 x5 x6 = 2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6 (proof)
Theorem 9fe37.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x2 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 x0 ⟶ decode_p (1216a.. x0 x1) x2 = x1 x2
Theorem 32c95.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . x0 = 81367.. x1 x2 x3 x4 ⟶ ∀ x5 . prim1 x5 x1 ⟶ x4 x5 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5 (proof)
Theorem f5ffc.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . prim1 x4 x0 ⟶ x3 x4 = decode_p (f482f.. (81367.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 (proof)
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known and4I : ∀ x0 x1 x2 x3 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ and (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 x7 ⟶ and (and (and (x0 = x1) (∀ x8 . prim1 x8 x0 ⟶ x2 x8 = x3 x8)) (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x4 x8 x9 = x5 x8 x9)) (∀ x8 . prim1 x8 x0 ⟶ x6 x8 = x7 x8) (proof)
Param iff : ο → ο → ο
Known ee7ef.. : ∀ x0 . ∀ x1 x2 : ι → ο . (∀ x3 . prim1 x3 x0 ⟶ iff (x1 x3) (x2 x3)) ⟶ 1216a.. x0 x1 = 1216a.. x0 x2
Known 62ef7.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ iff (x1 x3 x4) (x2 x3 x4)) ⟶ d2155.. x0 x1 = d2155.. x0 x2
Known 4402a.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ x1 x3 = x2 x3) ⟶ 0fc90.. x0 x1 = 0fc90.. x0 x2
Theorem f9c4e.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 : ι → ι → ο . ∀ x5 x6 : ι → ο . (∀ x7 . prim1 x7 x0 ⟶ x1 x7 = x2 x7) ⟶ (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ iff (x3 x7 x8) (x4 x7 x8)) ⟶ (∀ x7 . prim1 x7 x0 ⟶ iff (x5 x7) (x6 x7)) ⟶ 81367.. x0 x1 x3 x5 = 81367.. x0 x2 x4 x6 (proof)
Definition 86f84.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι . (∀ x4 . prim1 x4 x2 ⟶ prim1 (x3 x4) x2) ⟶ ∀ x4 : ι → ι → ο . ∀ x5 : ι → ο . x1 (81367.. x2 x3 x4 x5)) ⟶ x1 x0
Theorem d85c0.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0 ⟶ prim1 (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 x0 ⟶ prim1 (x1 x4) x0 (proof)
Known iff_refl : ∀ x0 : ο . iff x0 x0
Theorem 81349.. : ∀ x0 . 86f84.. x0 ⟶ x0 = 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 x1 ⟶ x2 x6 = x5 x6) ⟶ ∀ x6 : ι → ι → ο . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ iff (x3 x7 x8) (x6 x7 x8)) ⟶ ∀ x7 : ι → ο . (∀ x8 . prim1 x8 x1 ⟶ iff (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 x1 ⟶ x2 x6 = x5 x6) ⟶ ∀ x6 : ι → ι → ο . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ iff (x3 x7 x8) (x6 x7 x8)) ⟶ ∀ x7 : ι → ο . (∀ x8 . prim1 x8 x1 ⟶ iff (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 x4 ⟶ x1 = 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 x1 ⟶ x2 x5 = f482f.. (f482f.. x0 (4ae4a.. 4a7ef..)) x5 (proof)
Theorem b995b.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 . prim1 x4 x0 ⟶ x1 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 x1 ⟶ x3 x5 x6 = 2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6 (proof)
Theorem fe79a.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x2 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 x4 ⟶ x4 = 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 x7 ⟶ and (and (and (x0 = x1) (∀ x8 . prim1 x8 x0 ⟶ x2 x8 = x3 x8)) (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x4 x8 x9 = x5 x8 x9)) (x6 = x7) (proof)
Theorem e4331.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 : ι → ι → ο . ∀ x5 . (∀ x6 . prim1 x6 x0 ⟶ x1 x6 = x2 x6) ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ iff (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 x2 ⟶ prim1 (x3 x4) x2) ⟶ ∀ x4 : ι → ι → ο . ∀ x5 . prim1 x5 x2 ⟶ x1 (1bcc7.. x2 x3 x4 x5)) ⟶ x1 x0
Theorem 39190.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) x0) ⟶ ∀ x2 : ι → ι → ο . ∀ x3 . prim1 x3 x0 ⟶ 6100b.. (1bcc7.. x0 x1 x2 x3) (proof)
Theorem f7341.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 . 6100b.. (1bcc7.. x0 x1 x2 x3) ⟶ ∀ x4 . prim1 x4 x0 ⟶ prim1 (x1 x4) x0 (proof)
Theorem 5041b.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 . 6100b.. (1bcc7.. x0 x1 x2 x3) ⟶ prim1 x3 x0 (proof)
Theorem 6f356.. : ∀ x0 . 6100b.. x0 ⟶ x0 = 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 x1 ⟶ x2 x6 = x5 x6) ⟶ ∀ x6 : ι → ι → ο . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ iff (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 x1 ⟶ x2 x6 = x5 x6) ⟶ ∀ x6 : ι → ι → ο . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ iff (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 x4 ⟶ x1 = 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 x1 ⟶ x2 x5 = f482f.. (f482f.. x0 (4ae4a.. 4a7ef..)) x5 (proof)
Theorem 02a4b.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . ∀ x3 x4 . prim1 x4 x0 ⟶ x1 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 x1 ⟶ x3 x5 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x5 (proof)
Theorem 13aa7.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . ∀ x3 x4 . prim1 x4 x0 ⟶ x2 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 x4 ⟶ x4 = 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 x7 ⟶ and (and (and (x0 = x1) (∀ x8 . prim1 x8 x0 ⟶ x2 x8 = x3 x8)) (∀ x8 . prim1 x8 x0 ⟶ x4 x8 = x5 x8)) (x6 = x7) (proof)
Theorem 6a79a.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 : ι → ο . ∀ x5 . (∀ x6 . prim1 x6 x0 ⟶ x1 x6 = x2 x6) ⟶ (∀ x6 . prim1 x6 x0 ⟶ iff (x3 x6) (x4 x6)) ⟶ 1cd8e.. x0 x1 x3 x5 = 1cd8e.. x0 x2 x4 x5 (proof)
Definition 49e31.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι . (∀ x4 . prim1 x4 x2 ⟶ prim1 (x3 x4) x2) ⟶ ∀ x4 : ι → ο . ∀ x5 . prim1 x5 x2 ⟶ x1 (1cd8e.. x2 x3 x4 x5)) ⟶ x1 x0
Theorem b756b.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) x0) ⟶ ∀ x2 : ι → ο . ∀ x3 . prim1 x3 x0 ⟶ 49e31.. (1cd8e.. x0 x1 x2 x3) (proof)
Theorem 42fa4.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . ∀ x3 . 49e31.. (1cd8e.. x0 x1 x2 x3) ⟶ ∀ x4 . prim1 x4 x0 ⟶ prim1 (x1 x4) x0 (proof)
Theorem c70df.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ο . ∀ x3 . 49e31.. (1cd8e.. x0 x1 x2 x3) ⟶ prim1 x3 x0 (proof)
Theorem da228.. : ∀ x0 . 49e31.. x0 ⟶ x0 = 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 x1 ⟶ x2 x6 = x5 x6) ⟶ ∀ x6 : ι → ο . (∀ x7 . prim1 x7 x1 ⟶ iff (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 x1 ⟶ x2 x6 = x5 x6) ⟶ ∀ x6 : ι → ο . (∀ x7 . prim1 x7 x1 ⟶ iff (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 x4 ⟶ x1 = 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 x1 ⟶ x2 x5 x6 = 2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..)) x5 x6 (proof)
Theorem f2271.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x1 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 x1 ⟶ x3 x5 x6 = 2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6 (proof)
Theorem 9bb3e.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x2 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 x1 ⟶ x4 x5 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5 (proof)
Theorem 0b18c.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . prim1 x4 x0 ⟶ x3 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 x7 ⟶ and (and (and (x0 = x1) (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x2 x8 x9 = x3 x8 x9)) (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x4 x8 x9 = x5 x8 x9)) (∀ x8 . prim1 x8 x0 ⟶ x6 x8 = x7 x8) (proof)
Theorem 827c4.. : ∀ x0 . ∀ x1 x2 x3 x4 : ι → ι → ο . ∀ x5 x6 : ι → ο . (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ iff (x1 x7 x8) (x2 x7 x8)) ⟶ (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ iff (x3 x7 x8) (x4 x7 x8)) ⟶ (∀ x7 . prim1 x7 x0 ⟶ iff (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.. x0 ⟶ x0 = 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 x1 ⟶ iff (x2 x6 x7) (x5 x6 x7)) ⟶ ∀ x6 : ι → ι → ο . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ iff (x3 x7 x8) (x6 x7 x8)) ⟶ ∀ x7 : ι → ο . (∀ x8 . prim1 x8 x1 ⟶ iff (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 x1 ⟶ iff (x2 x6 x7) (x5 x6 x7)) ⟶ ∀ x6 : ι → ι → ο . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ iff (x3 x7 x8) (x6 x7 x8)) ⟶ ∀ x7 : ι → ο . (∀ x8 . prim1 x8 x1 ⟶ iff (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 x4 ⟶ x1 = 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 x1 ⟶ x2 x5 x6 = 2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..)) x5 x6 (proof)
Theorem 45188.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x1 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 x1 ⟶ x3 x5 x6 = 2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6 (proof)
Theorem b362f.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x2 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 x4 ⟶ x4 = 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 x7 ⟶ and (and (and (x0 = x1) (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x2 x8 x9 = x3 x8 x9)) (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x4 x8 x9 = x5 x8 x9)) (x6 = x7) (proof)
Theorem ca557.. : ∀ x0 . ∀ x1 x2 x3 x4 : ι → ι → ο . ∀ x5 . (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ iff (x1 x6 x7) (x2 x6 x7)) ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ iff (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 x2 ⟶ x1 (1f7e2.. x2 x3 x4 x5)) ⟶ x1 x0
Theorem a0ca8.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 . prim1 x3 x0 ⟶ d97ab.. (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.. x0 ⟶ x0 = 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 x1 ⟶ iff (x2 x6 x7) (x5 x6 x7)) ⟶ ∀ x6 : ι → ι → ο . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ iff (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 x1 ⟶ iff (x2 x6 x7) (x5 x6 x7)) ⟶ ∀ x6 : ι → ι → ο . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ iff (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)