Proofgold Address

Definition 8e91b.. := λ x0 : ι → ι → ο . λ x1 x2 . ∀ x3 : ι → ι → ο . (∀ x4 x5 . x0 x4 x5 ⟶ x3 x4 x5) ⟶ (∀ x4 x5 x6 . x3 x4 x5 ⟶ x3 x5 x6 ⟶ x3 x4 x6) ⟶ x3 x1 x2
Theorem 94d41.. : ∀ x0 x1 : ι → ι → ο . (∀ x2 x3 . x0 x2 x3 ⟶ x1 x2 x3) ⟶ ∀ x2 x3 . 8e91b.. x0 x2 x3 ⟶ 8e91b.. x1 x2 x3 (proof)
Definition 236c6.. := prim1 (λ x0 . x0)
Definition 6915e.. := prim1 (λ x0 . 236c6..)
Definition 32d20.. := prim1 (λ x0 . prim1 (λ x1 . x0))
Known 148f8.. : ∀ x0 : ι → ι → ι . 236c6.. = prim1 (λ x2 . prim1 (x0 x2)) ⟶ ∀ x1 : ο . x1
Theorem 61590.. : 236c6.. = 6915e.. ⟶ ∀ x0 : ο . x0 (proof)
Theorem b916f.. : 236c6.. = 32d20.. ⟶ ∀ x0 : ο . x0 (proof)
Known b4755.. : ∀ x0 x1 : ι → ι . prim1 x0 = prim1 x1 ⟶ x0 = x1
Theorem 63d4e.. : 6915e.. = 32d20.. ⟶ ∀ x0 : ο . x0 (proof)
Definition 57d6a.. := λ x0 x1 . prim0 236c6.. (prim0 x0 x1)
Definition bcddf.. := λ x0 . λ x1 : ι → ι . prim0 6915e.. (prim0 x0 (prim1 x1))
Definition d7cf0.. := λ x0 . λ x1 : ι → ι . prim0 32d20.. (prim0 x0 (prim1 x1))
Definition 91fd5.. := λ x0 x1 . d7cf0.. x0 (λ x2 . x1)
Definition 051a7.. := λ x0 : ι → ι → ο . λ x1 x2 . ∀ x3 : ι → ι → ο . (∀ x4 x5 . x0 x4 x5 ⟶ x3 x4 x5) ⟶ (∀ x4 . x3 x4 x4) ⟶ (∀ x4 x5 x6 x7 . x3 x4 x5 ⟶ x3 x6 x7 ⟶ x3 (57d6a.. x4 x6) (57d6a.. x5 x7)) ⟶ (∀ x4 x5 . ∀ x6 x7 : ι → ι . x3 x4 x5 ⟶ (∀ x8 . x3 (x6 x8) (x7 x8)) ⟶ x3 (bcddf.. x4 x6) (bcddf.. x5 x7)) ⟶ (∀ x4 x5 . ∀ x6 x7 : ι → ι . x3 x4 x5 ⟶ (∀ x8 . x3 (x6 x8) (x7 x8)) ⟶ x3 (d7cf0.. x4 x6) (d7cf0.. x5 x7)) ⟶ x3 x1 x2
Theorem 0a05d.. : ∀ x0 x1 : ι → ι → ο . (∀ x2 x3 . x0 x2 x3 ⟶ x1 x2 x3) ⟶ ∀ x2 x3 . 051a7.. x0 x2 x3 ⟶ 051a7.. x1 x2 x3 (proof)
Definition 1ca3e.. := λ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . ∀ x4 : ι → ι . ∀ x5 . x2 (bcddf.. x3 x4) (x4 x5)) ⟶ x2 x0 x1
Definition 93971.. := λ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 x4 . x2 (bcddf.. x3 (57d6a.. x4)) x4) ⟶ x2 x0 x1
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Definition d3ec1.. := λ x0 : ι → ι → ο . 8e91b.. (051a7.. (λ x1 x2 . or (x0 x1 x2) (1ca3e.. x1 x2)))
Definition 13ace.. := λ x0 : ι → ι → ο . 8e91b.. (051a7.. (λ x1 x2 . or (or (x0 x1 x2) (1ca3e.. x1 x2)) (93971.. x1 x2)))
Known orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Theorem 74efc.. : ∀ x0 x1 : ι → ι → ο . (∀ x2 x3 . x0 x2 x3 ⟶ x1 x2 x3) ⟶ ∀ x2 x3 . d3ec1.. x0 x2 x3 ⟶ d3ec1.. x1 x2 x3 (proof)
Definition False := ∀ x0 : ο . x0
Definition 5c39b.. := λ x0 x1 . False
Param and : ο → ο → ο
Definition a603a.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 . or (x0 x3 x4) (and (x3 = x1) (x4 = x2))
Theorem 87e44.. : ∀ x0 x1 : ι → ι → ο . ∀ x2 x3 . (∀ x4 x5 . x0 x4 x5 ⟶ x1 x4 x5) ⟶ ∀ x4 x5 . a603a.. x0 x2 x3 x4 x5 ⟶ a603a.. x1 x2 x3 x4 x5 (proof)
Definition f6435.. := λ x0 . or (x0 = 32d20..) (x0 = 6915e..)
Theorem 02f21.. : f6435.. 32d20.. (proof)
Theorem 40b47.. : f6435.. 6915e.. (proof)
Definition 6fe8d.. := λ x0 x1 x2 : ι → ι → ο . λ x3 x4 . ∀ x5 : (ι → ι → ο) → ι → ι → ο . (∀ x6 : ι → ι → ο . ∀ x7 x8 . x0 x7 x8 ⟶ x5 x6 x7 x8) ⟶ (∀ x6 : ι → ι → ο . ∀ x7 x8 . x6 x7 x8 ⟶ x5 x6 x7 x8) ⟶ (∀ x6 : ι → ι → ο . x5 x6 32d20.. 6915e..) ⟶ (∀ x6 : ι → ι → ο . ∀ x7 x8 . ∀ x9 : ι → ι . f6435.. x7 ⟶ x5 x6 x8 32d20.. ⟶ (∀ x10 . x5 (a603a.. x6 x10 x8) (x9 x10) x7) ⟶ x5 x6 (d7cf0.. x8 x9) x7) ⟶ (∀ x6 : ι → ι → ο . ∀ x7 x8 x9 . ∀ x10 : ι → ι . x5 x6 x7 (d7cf0.. x9 x10) ⟶ x5 x6 x8 x9 ⟶ x5 x6 (57d6a.. x7 x8) (x10 x8)) ⟶ (∀ x6 : ι → ι → ο . ∀ x7 x8 . ∀ x9 x10 : ι → ι . f6435.. x7 ⟶ x5 x6 (d7cf0.. x8 x10) x7 ⟶ (∀ x11 . x5 (a603a.. x6 x11 x8) (x9 x11) (x10 x11)) ⟶ x5 x6 (bcddf.. 236c6.. x9) (d7cf0.. x8 x10)) ⟶ (∀ x6 : ι → ι → ο . ∀ x7 x8 . ∀ x9 x10 : ι → ι . f6435.. x7 ⟶ x5 x6 (d7cf0.. x8 x10) x7 ⟶ (∀ x11 . x5 (a603a.. x6 x11 x8) (x9 x11) (x10 x11)) ⟶ x5 x6 (bcddf.. x8 x9) (d7cf0.. x8 x10)) ⟶ (∀ x6 : ι → ι → ο . ∀ x7 x8 x9 x10 x11 . f6435.. x7 ⟶ x5 x6 x8 x9 ⟶ x5 x6 x10 x7 ⟶ d3ec1.. x1 x9 x11 ⟶ d3ec1.. x1 x10 x11 ⟶ x5 x6 x8 x10) ⟶ x5 x2 x3 x4
Theorem c1535.. : ∀ x0 x1 x2 : ι → ι → ο . ∀ x3 x4 . x0 x3 x4 ⟶ 6fe8d.. x0 x1 x2 x3 x4 (proof)
Theorem f0743.. : ∀ x0 x1 x2 : ι → ι → ο . ∀ x3 x4 . x2 x3 x4 ⟶ 6fe8d.. x0 x1 x2 x3 x4 (proof)
Theorem 7d6ad.. : ∀ x0 x1 x2 : ι → ι → ο . 6fe8d.. x0 x1 x2 32d20.. 6915e.. (proof)
Theorem 798c1.. : ∀ x0 x1 x2 : ι → ι → ο . ∀ x3 x4 . ∀ x5 : ι → ι . f6435.. x3 ⟶ 6fe8d.. x0 x1 x2 x4 32d20.. ⟶ (∀ x6 . 6fe8d.. x0 x1 (a603a.. x2 x6 x4) (x5 x6) x3) ⟶ 6fe8d.. x0 x1 x2 (d7cf0.. x4 x5) x3 (proof)
Theorem dfeb0.. : ∀ x0 x1 x2 : ι → ι → ο . ∀ x3 x4 x5 . ∀ x6 : ι → ι . 6fe8d.. x0 x1 x2 x3 (d7cf0.. x5 x6) ⟶ 6fe8d.. x0 x1 x2 x4 x5 ⟶ 6fe8d.. x0 x1 x2 (57d6a.. x3 x4) (x6 x4) (proof)
Theorem d69a1.. : ∀ x0 x1 x2 : ι → ι → ο . ∀ x3 x4 . ∀ x5 x6 : ι → ι . f6435.. x3 ⟶ 6fe8d.. x0 x1 x2 (d7cf0.. x4 x6) x3 ⟶ (∀ x7 . 6fe8d.. x0 x1 (a603a.. x2 x7 x4) (x5 x7) (x6 x7)) ⟶ 6fe8d.. x0 x1 x2 (bcddf.. 236c6.. x5) (d7cf0.. x4 x6) (proof)
Theorem 64513.. : ∀ x0 x1 x2 : ι → ι → ο . ∀ x3 x4 . ∀ x5 x6 : ι → ι . f6435.. x3 ⟶ 6fe8d.. x0 x1 x2 (d7cf0.. x4 x6) x3 ⟶ (∀ x7 . 6fe8d.. x0 x1 (a603a.. x2 x7 x4) (x5 x7) (x6 x7)) ⟶ 6fe8d.. x0 x1 x2 (bcddf.. x4 x5) (d7cf0.. x4 x6) (proof)
Theorem b8a80.. : ∀ x0 x1 x2 : ι → ι → ο . ∀ x3 x4 x5 x6 x7 . f6435.. x3 ⟶ 6fe8d.. x0 x1 x2 x4 x5 ⟶ 6fe8d.. x0 x1 x2 x6 x3 ⟶ d3ec1.. x1 x5 x7 ⟶ d3ec1.. x1 x6 x7 ⟶ 6fe8d.. x0 x1 x2 x4 x6 (proof)
Theorem 913b8.. : ∀ x0 x1 x2 x3 x4 : ι → ι → ο . (∀ x5 x6 . x0 x5 x6 ⟶ x2 x5 x6) ⟶ (∀ x5 x6 . x1 x5 x6 ⟶ x3 x5 x6) ⟶ ∀ x5 x6 . 6fe8d.. x0 x1 x4 x5 x6 ⟶ 6fe8d.. x2 x3 x4 x5 x6 (proof)
Theorem f4e4d.. : ∀ x0 x1 x2 : ι → ι → ο . ∀ x3 x4 . 6fe8d.. x0 x1 x2 x3 x4 ⟶ ∀ x5 : ι → ι → ο . (∀ x6 x7 . x2 x6 x7 ⟶ x5 x6 x7) ⟶ 6fe8d.. x0 x1 x5 x3 x4 (proof)
Theorem b581d.. : ∀ x0 x1 x2 : ι → ι → ο . ∀ x3 x4 x5 . f6435.. x3 ⟶ 6fe8d.. x0 x1 x2 x4 32d20.. ⟶ 6fe8d.. x0 x1 x2 x5 x3 ⟶ 6fe8d.. x0 x1 x2 (91fd5.. x4 x5) x3 (proof)
Theorem 09e09.. : ∀ x0 x1 x2 : ι → ι → ο . ∀ x3 x4 . 6fe8d.. x0 x1 x2 x3 32d20.. ⟶ 6fe8d.. x0 x1 x2 x4 32d20.. ⟶ 6fe8d.. x0 x1 x2 (91fd5.. x3 x4) 32d20.. (proof)
Definition ee912.. := λ x0 : ι → ι → ο . ∀ x1 x2 x3 . x0 x1 x2 ⟶ x0 x1 x3 ⟶ x2 = x3
Definition d478c.. := λ x0 x1 : ι → ι → ο . λ x2 . or (6fe8d.. x0 x1 5c39b.. x2 6915e..) (6fe8d.. x0 x1 5c39b.. x2 32d20..)
Theorem 9df63.. : ∀ x0 x1 : ι → ι → ο . ∀ x2 . 6fe8d.. x0 x1 5c39b.. x2 6915e.. ⟶ d478c.. x0 x1 x2 (proof)
Theorem a63fb.. : ∀ x0 x1 : ι → ι → ο . ∀ x2 . 6fe8d.. x0 x1 5c39b.. x2 32d20.. ⟶ d478c.. x0 x1 x2 (proof)