Param 0fc90.. : ι → (ι → ι) → ι
Param 4ae4a.. : ι → ι
Param 4a7ef.. : ι
Param If_i : ο → ι → ι → ι
Definition 11e73.. := λ x0 x1 . 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x2 . If_i (x2 = 4a7ef..) x0 x1)
Param f482f.. : ι → ι → ι
Known 6f2e8.. : ∀ x0 x1 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) x0 x1)) 4a7ef.. = x0
Theorem e7c20.. : ∀ x0 x1 x2 . x0 = 11e73.. x1 x2 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem f25e9.. : ∀ x0 x1 . x0 = f482f.. (11e73.. x0 x1) 4a7ef.. (proof)
Known 15d37.. : ∀ x0 x1 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) x0 x1)) (4ae4a.. 4a7ef..) = x1
Theorem 1fa74.. : ∀ x0 x1 x2 . x0 = 11e73.. x1 x2 ⟶ x2 = f482f.. x0 (4ae4a.. 4a7ef..) (proof)
Theorem 10197.. : ∀ x0 x1 . x1 = f482f.. (11e73.. x0 x1) (4ae4a.. 4a7ef..) (proof)
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem 54ffc.. : ∀ x0 x1 x2 x3 . 11e73.. x0 x2 = 11e73.. x1 x3 ⟶ and (x0 = x1) (x2 = x3) (proof)
Definition c40a6.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 x3 . prim1 x3 x2 ⟶ x1 (11e73.. x2 x3)) ⟶ x1 x0
Theorem 9e478.. : ∀ x0 x1 . prim1 x1 x0 ⟶ c40a6.. (11e73.. x0 x1) (proof)
Theorem f73e5.. : ∀ x0 x1 . c40a6.. (11e73.. x0 x1) ⟶ prim1 x1 x0 (proof)
Theorem d26db.. : ∀ x0 . c40a6.. x0 ⟶ x0 = 11e73.. (f482f.. x0 4a7ef..) (f482f.. x0 (4ae4a.. 4a7ef..)) (proof)
Definition fcf68.. := λ x0 . λ x1 : ι → ι → ι . x1 (f482f.. x0 4a7ef..) (f482f.. x0 (4ae4a.. 4a7ef..))
Theorem 148e7.. : ∀ x0 : ι → ι → ι . ∀ x1 x2 . fcf68.. (11e73.. x1 x2) x0 = x0 x1 x2 (proof)
Definition 3aee2.. := λ x0 . λ x1 : ι → ι → ο . x1 (f482f.. x0 4a7ef..) (f482f.. x0 (4ae4a.. 4a7ef..))
Theorem 42688.. : ∀ x0 : ι → ι → ο . ∀ x1 x2 . 3aee2.. (11e73.. x1 x2) x0 = x0 x1 x2 (proof)
Definition c0301.. := λ x0 . λ x1 : ι → ι . 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x2 . If_i (x2 = 4a7ef..) x0 (0fc90.. x0 x1))
Theorem 2bd96.. : ∀ x0 x1 . ∀ x2 : ι → ι . x0 = c0301.. x1 x2 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 03207.. : ∀ x0 . ∀ x1 : ι → ι . x0 = f482f.. (c0301.. x0 x1) 4a7ef.. (proof)
Known f22ec.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ f482f.. (0fc90.. x0 x1) x2 = x1 x2
Theorem f9c17.. : ∀ x0 x1 . ∀ x2 : ι → ι . x0 = c0301.. x1 x2 ⟶ ∀ x3 . prim1 x3 x1 ⟶ x2 x3 = f482f.. (f482f.. x0 (4ae4a.. 4a7ef..)) x3 (proof)
Theorem 6793f.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ x1 x2 = f482f.. (f482f.. (c0301.. x0 x1) (4ae4a.. 4a7ef..)) x2 (proof)
Theorem 1b8bb.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . c0301.. x0 x2 = c0301.. x1 x3 ⟶ and (x0 = x1) (∀ x4 . prim1 x4 x0 ⟶ x2 x4 = x3 x4) (proof)
Known 4402a.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ x1 x3 = x2 x3) ⟶ 0fc90.. x0 x1 = 0fc90.. x0 x2
Theorem 68a3f.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ x1 x3 = x2 x3) ⟶ c0301.. x0 x1 = c0301.. x0 x2 (proof)
Definition f4ccf.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι . (∀ x4 . prim1 x4 x2 ⟶ prim1 (x3 x4) x2) ⟶ x1 (c0301.. x2 x3)) ⟶ x1 x0
Theorem 70745.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) x0) ⟶ f4ccf.. (c0301.. x0 x1) (proof)
Theorem 01ef5.. : ∀ x0 . ∀ x1 : ι → ι . f4ccf.. (c0301.. x0 x1) ⟶ ∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) x0 (proof)
Theorem 9903d.. : ∀ x0 . f4ccf.. x0 ⟶ x0 = c0301.. (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..))) (proof)
Definition 027cf.. := λ x0 . λ x1 : ι → (ι → ι) → ι . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..)))
Theorem 27e2e.. : ∀ x0 : ι → (ι → ι) → ι . ∀ x1 . ∀ x2 : ι → ι . (∀ x3 : ι → ι . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ 027cf.. (c0301.. x1 x2) x0 = x0 x1 x2 (proof)
Definition 4de1f.. := λ x0 . λ x1 : ι → (ι → ι) → ο . x1 (f482f.. x0 4a7ef..) (f482f.. (f482f.. x0 (4ae4a.. 4a7ef..)))
Theorem 74d25.. : ∀ x0 : ι → (ι → ι) → ο . ∀ x1 . ∀ x2 : ι → ι . (∀ x3 : ι → ι . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ 4de1f.. (c0301.. x1 x2) x0 = x0 x1 x2 (proof)
Param eb53d.. : ι → CT2 ι
Definition 987b2.. := λ x0 . λ x1 : ι → ι → ι . 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x2 . If_i (x2 = 4a7ef..) x0 (eb53d.. x0 x1))
Theorem 2ce64.. : ∀ x0 x1 . ∀ x2 : ι → ι → ι . x0 = 987b2.. x1 x2 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem f26a7.. : ∀ x0 . ∀ x1 : ι → ι → ι . x0 = f482f.. (987b2.. x0 x1) 4a7ef.. (proof)
Param e3162.. : ι → ι → ι → ι
Known 35054.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ e3162.. (eb53d.. x0 x1) x2 x3 = x1 x2 x3
Theorem ad438.. : ∀ x0 x1 . ∀ x2 : ι → ι → ι . x0 = 987b2.. x1 x2 ⟶ ∀ x3 . prim1 x3 x1 ⟶ ∀ x4 . prim1 x4 x1 ⟶ x2 x3 x4 = e3162.. (f482f.. x0 (4ae4a.. 4a7ef..)) x3 x4 (proof)
Theorem 88494.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ x1 x2 x3 = e3162.. (f482f.. (987b2.. x0 x1) (4ae4a.. 4a7ef..)) x2 x3 (proof)
Theorem 31c9d.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . 987b2.. x0 x2 = 987b2.. x1 x3 ⟶ and (x0 = x1) (∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x2 x4 x5 = x3 x4 x5) (proof)
Known 8fdaf.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x1 x3 x4 = x2 x3 x4) ⟶ eb53d.. x0 x1 = eb53d.. x0 x2
Theorem a90ae.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x1 x3 x4 = x2 x3 x4) ⟶ 987b2.. x0 x1 = 987b2.. x0 x2 (proof)
Definition 30750.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . prim1 x4 x2 ⟶ ∀ x5 . prim1 x5 x2 ⟶ prim1 (x3 x4 x5) x2) ⟶ x1 (987b2.. x2 x3)) ⟶ x1 x0
Theorem b6770.. : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ prim1 (x1 x2 x3) x0) ⟶ 30750.. (987b2.. x0 x1) (proof)
Theorem 4e11f.. : ∀ x0 . ∀ x1 : ι → ι → ι . 30750.. (987b2.. x0 x1) ⟶ ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ prim1 (x1 x2 x3) x0 (proof)
Theorem 6eef1.. : ∀ x0 . 30750.. x0 ⟶ x0 = 987b2.. (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (proof)
Definition 19c2c.. := λ x0 . λ x1 : ι → (ι → ι → ι) → ι . x1 (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..)))
Theorem 0ccad.. : ∀ x0 : ι → (ι → ι → ι) → ι . ∀ x1 . ∀ x2 : ι → ι → ι . (∀ x3 : ι → ι → ι . (∀ x4 . prim1 x4 x1 ⟶ ∀ x5 . prim1 x5 x1 ⟶ x2 x4 x5 = x3 x4 x5) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ 19c2c.. (987b2.. x1 x2) x0 = x0 x1 x2 (proof)
Definition 93c99.. := λ x0 . λ x1 : ι → (ι → ι → ι) → ο . x1 (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..)))
Theorem 7dd3b.. : ∀ x0 : ι → (ι → ι → ι) → ο . ∀ x1 . ∀ x2 : ι → ι → ι . (∀ x3 : ι → ι → ι . (∀ x4 . prim1 x4 x1 ⟶ ∀ x5 . prim1 x5 x1 ⟶ x2 x4 x5 = x3 x4 x5) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ 93c99.. (987b2.. x1 x2) x0 = x0 x1 x2 (proof)
Param 1216a.. : ι → (ι → ο) → ι
Definition 81bb1.. := λ x0 . λ x1 : ι → ο . 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x2 . If_i (x2 = 4a7ef..) x0 (1216a.. x0 x1))
Theorem 6ca5c.. : ∀ x0 x1 . ∀ x2 : ι → ο . x0 = 81bb1.. x1 x2 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem a4354.. : ∀ x0 . ∀ x1 : ι → ο . x0 = f482f.. (81bb1.. x0 x1) 4a7ef.. (proof)
Param decode_p : ι → ι → ο
Known 931fe.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0 ⟶ decode_p (1216a.. x0 x1) x2 = x1 x2
Theorem d3d68.. : ∀ x0 x1 . ∀ x2 : ι → ο . x0 = 81bb1.. x1 x2 ⟶ ∀ x3 . prim1 x3 x1 ⟶ x2 x3 = decode_p (f482f.. x0 (4ae4a.. 4a7ef..)) x3 (proof)
Theorem 73cce.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0 ⟶ x1 x2 = decode_p (f482f.. (81bb1.. x0 x1) (4ae4a.. 4a7ef..)) x2 (proof)
Theorem 14896.. : ∀ x0 x1 . ∀ x2 x3 : ι → ο . 81bb1.. x0 x2 = 81bb1.. x1 x3 ⟶ and (x0 = x1) (∀ x4 . prim1 x4 x0 ⟶ x2 x4 = x3 x4) (proof)
Param iff : ο → ο → ο
Known ee7ef.. : ∀ x0 . ∀ x1 x2 : ι → ο . (∀ x3 . prim1 x3 x0 ⟶ iff (x1 x3) (x2 x3)) ⟶ 1216a.. x0 x1 = 1216a.. x0 x2
Theorem 6deec.. : ∀ x0 . ∀ x1 x2 : ι → ο . (∀ x3 . prim1 x3 x0 ⟶ iff (x1 x3) (x2 x3)) ⟶ 81bb1.. x0 x1 = 81bb1.. x0 x2 (proof)
Definition ec553.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ο . x1 (81bb1.. x2 x3)) ⟶ x1 x0
Theorem 0f4de.. : ∀ x0 . ∀ x1 : ι → ο . ec553.. (81bb1.. x0 x1) (proof)
Known iff_refl : ∀ x0 : ο . iff x0 x0
Theorem b0c07.. : ∀ x0 . ec553.. x0 ⟶ x0 = 81bb1.. (f482f.. x0 4a7ef..) (decode_p (f482f.. x0 (4ae4a.. 4a7ef..))) (proof)
Definition 013da.. := λ x0 . λ x1 : ι → (ι → ο) → ι . x1 (f482f.. x0 4a7ef..) (decode_p (f482f.. x0 (4ae4a.. 4a7ef..)))
Theorem 4b446.. : ∀ x0 : ι → (ι → ο) → ι . ∀ x1 . ∀ x2 : ι → ο . (∀ x3 : ι → ο . (∀ x4 . prim1 x4 x1 ⟶ iff (x2 x4) (x3 x4)) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ 013da.. (81bb1.. x1 x2) x0 = x0 x1 x2 (proof)
Definition 23a1a.. := λ x0 . λ x1 : ι → (ι → ο) → ο . x1 (f482f.. x0 4a7ef..) (decode_p (f482f.. x0 (4ae4a.. 4a7ef..)))
Theorem 8f348.. : ∀ x0 : ι → (ι → ο) → ο . ∀ x1 . ∀ x2 : ι → ο . (∀ x3 : ι → ο . (∀ x4 . prim1 x4 x1 ⟶ iff (x2 x4) (x3 x4)) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ 23a1a.. (81bb1.. x1 x2) x0 = x0 x1 x2 (proof)
Param d2155.. : ι → (ι → ι → ο) → ι
Definition 35983.. := λ x0 . λ x1 : ι → ι → ο . 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x2 . If_i (x2 = 4a7ef..) x0 (d2155.. x0 x1))
Theorem d1955.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . x0 = 35983.. x1 x2 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 7c7b1.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . x2 x0 (f482f.. (35983.. x0 x1) 4a7ef..) ⟶ x2 (f482f.. (35983.. x0 x1) 4a7ef..) x0 (proof)
Param 2b2e3.. : ι → ι → ι → ο
Known 67416.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ 2b2e3.. (d2155.. x0 x1) x2 x3 = x1 x2 x3
Theorem d8839.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . x0 = 35983.. x1 x2 ⟶ ∀ x3 . prim1 x3 x1 ⟶ ∀ x4 . prim1 x4 x1 ⟶ x2 x3 x4 = 2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..)) x3 x4 (proof)
Theorem 8e7c5.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ x1 x2 x3 = 2b2e3.. (f482f.. (35983.. x0 x1) (4ae4a.. 4a7ef..)) x2 x3 (proof)
Theorem 33e65.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . 35983.. x0 x2 = 35983.. x1 x3 ⟶ and (x0 = x1) (∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x2 x4 x5 = x3 x4 x5) (proof)
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
Theorem e7504.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ iff (x1 x3 x4) (x2 x3 x4)) ⟶ 35983.. x0 x1 = 35983.. x0 x2 (proof)
Definition 36093.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ο . x1 (35983.. x2 x3)) ⟶ x1 x0
Theorem 19215.. : ∀ x0 . ∀ x1 : ι → ι → ο . 36093.. (35983.. x0 x1) (proof)
Theorem cf13a.. : ∀ x0 . 36093.. x0 ⟶ x0 = 35983.. (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..))) (proof)
Definition 56080.. := λ x0 . λ x1 : ι → (ι → ι → ο) → ι . x1 (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..)))
Theorem 55955.. : ∀ x0 : ι → (ι → ι → ο) → ι . ∀ x1 . ∀ x2 : ι → ι → ο . (∀ x3 : ι → ι → ο . (∀ x4 . prim1 x4 x1 ⟶ ∀ x5 . prim1 x5 x1 ⟶ iff (x2 x4 x5) (x3 x4 x5)) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ 56080.. (35983.. x1 x2) x0 = x0 x1 x2 (proof)
Definition e0700.. := λ x0 . λ x1 : ι → (ι → ι → ο) → ο . x1 (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..)))
Theorem 4f8ca.. : ∀ x0 : ι → (ι → ι → ο) → ο . ∀ x1 . ∀ x2 : ι → ι → ο . (∀ x3 : ι → ι → ο . (∀ x4 . prim1 x4 x1 ⟶ ∀ x5 . prim1 x5 x1 ⟶ iff (x2 x4 x5) (x3 x4 x5)) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ e0700.. (35983.. x1 x2) x0 = x0 x1 x2 (proof)
Param e0e40.. : ι → ((ι → ο) → ο) → ι
Definition 35104.. := λ x0 . λ x1 : (ι → ο) → ο . 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x2 . If_i (x2 = 4a7ef..) x0 (e0e40.. x0 x1))
Theorem 01155.. : ∀ x0 x1 . ∀ x2 : (ι → ο) → ο . x0 = 35104.. x1 x2 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem f00b6.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . x0 = f482f.. (35104.. x0 x1) 4a7ef.. (proof)
Param decode_c : ι → (ι → ο) → ο
Known 81500.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ο . (∀ x3 . x2 x3 ⟶ prim1 x3 x0) ⟶ decode_c (e0e40.. x0 x1) x2 = x1 x2
Theorem 1efa9.. : ∀ x0 x1 . ∀ x2 : (ι → ο) → ο . x0 = 35104.. x1 x2 ⟶ ∀ x3 : ι → ο . (∀ x4 . x3 x4 ⟶ prim1 x4 x1) ⟶ x2 x3 = decode_c (f482f.. x0 (4ae4a.. 4a7ef..)) x3 (proof)
Theorem b2596.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ο . (∀ x3 . x2 x3 ⟶ prim1 x3 x0) ⟶ x1 x2 = decode_c (f482f.. (35104.. x0 x1) (4ae4a.. 4a7ef..)) x2 (proof)
Theorem d08e9.. : ∀ x0 x1 . ∀ x2 x3 : (ι → ο) → ο . 35104.. x0 x2 = 35104.. x1 x3 ⟶ and (x0 = x1) (∀ x4 : ι → ο . (∀ x5 . x4 x5 ⟶ prim1 x5 x0) ⟶ x2 x4 = x3 x4) (proof)
Known fe043.. : ∀ x0 . ∀ x1 x2 : (ι → ο) → ο . (∀ x3 : ι → ο . (∀ x4 . x3 x4 ⟶ prim1 x4 x0) ⟶ iff (x1 x3) (x2 x3)) ⟶ e0e40.. x0 x1 = e0e40.. x0 x2
Theorem fc6d0.. : ∀ x0 . ∀ x1 x2 : (ι → ο) → ο . (∀ x3 : ι → ο . (∀ x4 . x3 x4 ⟶ prim1 x4 x0) ⟶ iff (x1 x3) (x2 x3)) ⟶ 35104.. x0 x1 = 35104.. x0 x2 (proof)
Definition 87ddc.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : (ι → ο) → ο . x1 (35104.. x2 x3)) ⟶ x1 x0
Theorem 8f88b.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . 87ddc.. (35104.. x0 x1) (proof)
Theorem 7efe5.. : ∀ x0 . 87ddc.. x0 ⟶ x0 = 35104.. (f482f.. x0 4a7ef..) (decode_c (f482f.. x0 (4ae4a.. 4a7ef..))) (proof)
Definition 5e74a.. := λ x0 . λ x1 : ι → ((ι → ο) → ο) → ι . x1 (f482f.. x0 4a7ef..) (decode_c (f482f.. x0 (4ae4a.. 4a7ef..)))
Theorem 7210f.. : ∀ x0 : ι → ((ι → ο) → ο) → ι . ∀ x1 . ∀ x2 : (ι → ο) → ο . (∀ x3 : (ι → ο) → ο . (∀ x4 : ι → ο . (∀ x5 . x4 x5 ⟶ prim1 x5 x1) ⟶ iff (x2 x4) (x3 x4)) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ 5e74a.. (35104.. x1 x2) x0 = x0 x1 x2 (proof)
Definition a146d.. := λ x0 . λ x1 : ι → ((ι → ο) → ο) → ο . x1 (f482f.. x0 4a7ef..) (decode_c (f482f.. x0 (4ae4a.. 4a7ef..)))
Theorem 0b20d.. : ∀ x0 : ι → ((ι → ο) → ο) → ο . ∀ x1 . ∀ x2 : (ι → ο) → ο . (∀ x3 : (ι → ο) → ο . (∀ x4 : ι → ο . (∀ x5 . x4 x5 ⟶ prim1 x5 x1) ⟶ iff (x2 x4) (x3 x4)) ⟶ x0 x1 x3 = x0 x1 x2) ⟶ a146d.. (35104.. x1 x2) x0 = x0 x1 x2 (proof)

Proofgold Address