Proofgold Address

Param 0fc90.. : ι → (ι → ι) → ι
Param 4ae4a.. : ι → ι
Param 4a7ef.. : ι
Param If_i : ο → ι → ι → ι
Param 1216a.. : ι → (ι → ο) → ι
Definition 2c81e.. := λ x0 . λ x1 x2 : ι → ο . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x3 . If_i (x3 = 4a7ef..) x0 (If_i (x3 = 4ae4a.. 4a7ef..) (1216a.. x0 x1) (1216a.. x0 x2)))
Param f482f.. : ι → ι → ι
Known 52da6.. : ∀ x0 x1 x2 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) x1 x2))) 4a7ef.. = x0
Theorem cd612.. : ∀ x0 x1 . ∀ x2 x3 : ι → ο . x0 = 2c81e.. x1 x2 x3 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem bafbc.. : ∀ x0 . ∀ x1 x2 : ι → ο . x0 = f482f.. (2c81e.. x0 x1 x2) 4a7ef.. (proof)
Param decode_p : ι → ι → ο
Known c2bca.. : ∀ x0 x1 x2 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) x1 x2))) (4ae4a.. 4a7ef..) = x1
Known 931fe.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0 ⟶ decode_p (1216a.. x0 x1) x2 = x1 x2
Theorem 46d9c.. : ∀ x0 x1 . ∀ x2 x3 : ι → ο . x0 = 2c81e.. x1 x2 x3 ⟶ ∀ x4 . prim1 x4 x1 ⟶ x2 x4 = decode_p (f482f.. x0 (4ae4a.. 4a7ef..)) x4 (proof)
Theorem 64120.. : ∀ x0 . ∀ x1 x2 : ι → ο . ∀ x3 . prim1 x3 x0 ⟶ x1 x3 = decode_p (f482f.. (2c81e.. x0 x1 x2) (4ae4a.. 4a7ef..)) x3 (proof)
Known 11d6d.. : ∀ x0 x1 x2 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) x1 x2))) (4ae4a.. (4ae4a.. 4a7ef..)) = x2
Theorem 8ef96.. : ∀ x0 x1 . ∀ x2 x3 : ι → ο . x0 = 2c81e.. x1 x2 x3 ⟶ ∀ x4 . prim1 x4 x1 ⟶ x3 x4 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x4 (proof)
Theorem bef21.. : ∀ x0 . ∀ x1 x2 : ι → ο . ∀ x3 . prim1 x3 x0 ⟶ x2 x3 = decode_p (f482f.. (2c81e.. x0 x1 x2) (4ae4a.. (4ae4a.. 4a7ef..))) x3 (proof)
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Theorem 348e6.. : ∀ x0 x1 . ∀ x2 x3 x4 x5 : ι → ο . 2c81e.. x0 x2 x4 = 2c81e.. x1 x3 x5 ⟶ and (and (x0 = x1) (∀ x6 . prim1 x6 x0 ⟶ x2 x6 = x3 x6)) (∀ x6 . prim1 x6 x0 ⟶ x4 x6 = x5 x6) (proof)
Param iff : ο → ο → ο
Known ee7ef.. : ∀ x0 . ∀ x1 x2 : ι → ο . (∀ x3 . prim1 x3 x0 ⟶ iff (x1 x3) (x2 x3)) ⟶ 1216a.. x0 x1 = 1216a.. x0 x2
Theorem ed007.. : ∀ x0 . ∀ x1 x2 x3 x4 : ι → ο . (∀ x5 . prim1 x5 x0 ⟶ iff (x1 x5) (x2 x5)) ⟶ (∀ x5 . prim1 x5 x0 ⟶ iff (x3 x5) (x4 x5)) ⟶ 2c81e.. x0 x1 x3 = 2c81e.. x0 x2 x4 (proof)
Definition 3d9b3.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 x4 : ι → ο . x1 (2c81e.. x2 x3 x4)) ⟶ x1 x0
Theorem abc60.. : ∀ x0 . ∀ x1 x2 : ι → ο . 3d9b3.. (2c81e.. x0 x1 x2) (proof)
Known iff_refl : ∀ x0 : ο . iff x0 x0
Theorem fc35f.. : ∀ x0 . 3d9b3.. x0 ⟶ x0 = 2c81e.. (f482f.. x0 4a7ef..) (decode_p (f482f.. x0 (4ae4a.. 4a7ef..))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Definition ec96a.. := λ x0 . λ x1 : ι → (ι → ο) → (ι → ο) → ι . x1 (f482f.. x0 4a7ef..) (decode_p (f482f.. x0 (4ae4a.. 4a7ef..))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem d859a.. : ∀ x0 : ι → (ι → ο) → (ι → ο) → ι . ∀ x1 . ∀ x2 x3 : ι → ο . (∀ x4 : ι → ο . (∀ x5 . prim1 x5 x1 ⟶ iff (x2 x5) (x4 x5)) ⟶ ∀ x5 : ι → ο . (∀ x6 . prim1 x6 x1 ⟶ iff (x3 x6) (x5 x6)) ⟶ x0 x1 x4 x5 = x0 x1 x2 x3) ⟶ ec96a.. (2c81e.. x1 x2 x3) x0 = x0 x1 x2 x3 (proof)
Definition 04a04.. := λ x0 . λ x1 : ι → (ι → ο) → (ι → ο) → ο . x1 (f482f.. x0 4a7ef..) (decode_p (f482f.. x0 (4ae4a.. 4a7ef..))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem 4dbf2.. : ∀ x0 : ι → (ι → ο) → (ι → ο) → ο . ∀ x1 . ∀ x2 x3 : ι → ο . (∀ x4 : ι → ο . (∀ x5 . prim1 x5 x1 ⟶ iff (x2 x5) (x4 x5)) ⟶ ∀ x5 : ι → ο . (∀ x6 . prim1 x6 x1 ⟶ iff (x3 x6) (x5 x6)) ⟶ x0 x1 x4 x5 = x0 x1 x2 x3) ⟶ 04a04.. (2c81e.. x1 x2 x3) x0 = x0 x1 x2 x3 (proof)
Definition 5f5a0.. := λ x0 . λ x1 : ι → ο . λ x2 . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x3 . If_i (x3 = 4a7ef..) x0 (If_i (x3 = 4ae4a.. 4a7ef..) (1216a.. x0 x1) x2))
Theorem e81f9.. : ∀ x0 x1 . ∀ x2 : ι → ο . ∀ x3 . x0 = 5f5a0.. x1 x2 x3 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 47994.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x0 = f482f.. (5f5a0.. x0 x1 x2) 4a7ef.. (proof)
Theorem 06fa1.. : ∀ x0 x1 . ∀ x2 : ι → ο . ∀ x3 . x0 = 5f5a0.. x1 x2 x3 ⟶ ∀ x4 . prim1 x4 x1 ⟶ x2 x4 = decode_p (f482f.. x0 (4ae4a.. 4a7ef..)) x4 (proof)
Theorem 32b36.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 x3 . prim1 x3 x0 ⟶ x1 x3 = decode_p (f482f.. (5f5a0.. x0 x1 x2) (4ae4a.. 4a7ef..)) x3 (proof)
Theorem 04553.. : ∀ x0 x1 . ∀ x2 : ι → ο . ∀ x3 . x0 = 5f5a0.. x1 x2 x3 ⟶ x3 = f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)) (proof)
Theorem d7c95.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 = f482f.. (5f5a0.. x0 x1 x2) (4ae4a.. (4ae4a.. 4a7ef..)) (proof)
Theorem 87020.. : ∀ x0 x1 . ∀ x2 x3 : ι → ο . ∀ x4 x5 . 5f5a0.. x0 x2 x4 = 5f5a0.. x1 x3 x5 ⟶ and (and (x0 = x1) (∀ x6 . prim1 x6 x0 ⟶ x2 x6 = x3 x6)) (x4 = x5) (proof)
Theorem 96513.. : ∀ x0 . ∀ x1 x2 : ι → ο . ∀ x3 . (∀ x4 . prim1 x4 x0 ⟶ iff (x1 x4) (x2 x4)) ⟶ 5f5a0.. x0 x1 x3 = 5f5a0.. x0 x2 x3 (proof)
Definition b0e4a.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ο . ∀ x4 . prim1 x4 x2 ⟶ x1 (5f5a0.. x2 x3 x4)) ⟶ x1 x0
Theorem 5c907.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0 ⟶ b0e4a.. (5f5a0.. x0 x1 x2) (proof)
Theorem d2c56.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . b0e4a.. (5f5a0.. x0 x1 x2) ⟶ prim1 x2 x0 (proof)
Theorem 75fde.. : ∀ x0 . b0e4a.. x0 ⟶ x0 = 5f5a0.. (f482f.. x0 4a7ef..) (decode_p (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Definition 42c37.. := λ x0 . λ x1 : ι → (ι → ο) → ι → ι . x1 (f482f.. x0 4a7ef..) (decode_p (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))
Theorem ad064.. : ∀ x0 : ι → (ι → ο) → ι → ι . ∀ x1 . ∀ x2 : ι → ο . ∀ x3 . (∀ x4 : ι → ο . (∀ x5 . prim1 x5 x1 ⟶ iff (x2 x5) (x4 x5)) ⟶ x0 x1 x4 x3 = x0 x1 x2 x3) ⟶ 42c37.. (5f5a0.. x1 x2 x3) x0 = x0 x1 x2 x3 (proof)
Definition b6337.. := λ x0 . λ x1 : ι → (ι → ο) → ι → ο . x1 (f482f.. x0 4a7ef..) (decode_p (f482f.. x0 (4ae4a.. 4a7ef..))) (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))
Theorem c4dd8.. : ∀ x0 : ι → (ι → ο) → ι → ο . ∀ x1 . ∀ x2 : ι → ο . ∀ x3 . (∀ x4 : ι → ο . (∀ x5 . prim1 x5 x1 ⟶ iff (x2 x5) (x4 x5)) ⟶ x0 x1 x4 x3 = x0 x1 x2 x3) ⟶ b6337.. (5f5a0.. x1 x2 x3) x0 = x0 x1 x2 x3 (proof)
Definition 59c41.. := λ x0 x1 x2 . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x3 . If_i (x3 = 4a7ef..) x0 (If_i (x3 = 4ae4a.. 4a7ef..) x1 x2))
Theorem 6cc5b.. : ∀ x0 x1 x2 x3 . x0 = 59c41.. x1 x2 x3 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem ced17.. : ∀ x0 x1 x2 . x0 = f482f.. (59c41.. x0 x1 x2) 4a7ef.. (proof)
Theorem 4d620.. : ∀ x0 x1 x2 x3 . x0 = 59c41.. x1 x2 x3 ⟶ x2 = f482f.. x0 (4ae4a.. 4a7ef..) (proof)
Theorem b8922.. : ∀ x0 x1 x2 . x1 = f482f.. (59c41.. x0 x1 x2) (4ae4a.. 4a7ef..) (proof)
Theorem 40a41.. : ∀ x0 x1 x2 x3 . x0 = 59c41.. x1 x2 x3 ⟶ x3 = f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)) (proof)
Theorem 5a5f5.. : ∀ x0 x1 x2 . x2 = f482f.. (59c41.. x0 x1 x2) (4ae4a.. (4ae4a.. 4a7ef..)) (proof)
Theorem 67a86.. : ∀ x0 x1 x2 x3 x4 x5 . 59c41.. x0 x2 x4 = 59c41.. x1 x3 x5 ⟶ and (and (x0 = x1) (x2 = x3)) (x4 = x5) (proof)
Definition 5c3a8.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 x3 . prim1 x3 x2 ⟶ ∀ x4 . prim1 x4 x2 ⟶ x1 (59c41.. x2 x3 x4)) ⟶ x1 x0
Theorem b14a4.. : ∀ x0 x1 . prim1 x1 x0 ⟶ ∀ x2 . prim1 x2 x0 ⟶ 5c3a8.. (59c41.. x0 x1 x2) (proof)
Theorem 13449.. : ∀ x0 x1 x2 . 5c3a8.. (59c41.. x0 x1 x2) ⟶ prim1 x1 x0 (proof)
Theorem b7feb.. : ∀ x0 x1 x2 . 5c3a8.. (59c41.. x0 x1 x2) ⟶ prim1 x2 x0 (proof)
Theorem 24ae7.. : ∀ x0 . 5c3a8.. x0 ⟶ x0 = 59c41.. (f482f.. x0 4a7ef..) (f482f.. x0 (4ae4a.. 4a7ef..)) (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Definition a7889.. := λ x0 . λ x1 : ι → ι → ι → ι . x1 (f482f.. x0 4a7ef..) (f482f.. x0 (4ae4a.. 4a7ef..)) (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))
Theorem b27b9.. : ∀ x0 : ι → ι → ι → ι . ∀ x1 x2 x3 . a7889.. (59c41.. x1 x2 x3) x0 = x0 x1 x2 x3 (proof)
Definition a35ef.. := λ x0 . λ x1 : ι → ι → ι → ο . x1 (f482f.. x0 4a7ef..) (f482f.. x0 (4ae4a.. 4a7ef..)) (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))
Theorem 17ee4.. : ∀ x0 : ι → ι → ι → ο . ∀ x1 x2 x3 . a35ef.. (59c41.. x1 x2 x3) x0 = x0 x1 x2 x3 (proof)