Proofgold Address

Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Param c4def.. : ι
Param 6b90c.. : ι → ι → ι
Param 5e331.. : ι
Param a3eb9.. : ι → ι → ι
Param bf68c.. : ι → ι → ι
Param c9248.. : ι
Param a6e19.. : ι → ι
Param 2fe34.. : ι → ι
Param 3e00e.. : ι → ι → ι
Param f9341.. : ι → ι → ι
Param 1fa6d.. : ι → ι
Param 3a365.. : ι → ι
Definition False := ∀ x0 : ο . x0
Known 92e6a.. : ∀ x0 : ι → ι . ∀ x1 x2 . prim1 x0 = prim0 x1 x2 ⟶ False
Known 50787.. : ∀ x0 x1 x2 x3 . prim0 x0 x1 = prim0 x2 x3 ⟶ x0 = x2
Known 8b073.. : ∀ x0 x1 x2 . prim0 (prim1 (λ x4 . prim1 (λ x5 . prim0 (prim0 (prim0 x5 x4) (prim0 x4 x5)) (prim0 (prim0 x5 x5) (prim0 x4 x4))))) x0 = prim0 (prim0 (prim1 (λ x4 . prim1 (λ x5 . prim0 (prim0 (prim0 x5 x4) (prim0 x4 x5)) (prim0 (prim0 x5 x5) (prim0 x4 x4))))) x1) x2 ⟶ ∀ x3 : ο . x3
Known 6641d.. : ∀ x0 x1 x2 . prim0 (prim0 (prim1 (λ x4 . prim1 (λ x5 . prim0 (prim0 (prim0 x5 x4) (prim0 x4 x5)) (prim0 (prim0 x5 x5) (prim0 x4 x4))))) x1) x2 = prim0 (prim1 (λ x4 . prim1 (λ x5 . prim0 (prim0 (prim0 x5 x4) (prim0 x4 x5)) (prim0 (prim0 x5 x5) (prim0 x4 x4))))) x0 ⟶ ∀ x3 : ο . x3
Known 9ec26.. : ∀ x0 x1 . 5e331.. = a3eb9.. x0 x1 ⟶ ∀ x2 : ο . x2
Known 59f91.. : ∀ x0 x1 . 5e331.. = bf68c.. x0 x1 ⟶ ∀ x2 : ο . x2
Param 236c6.. : ι
Known f558c.. : ∀ x0 x1 . 236c6.. = prim0 x0 x1 ⟶ ∀ x2 : ο . x2
Known 93754.. : ∀ x0 x1 x2 x3 . prim0 x0 x1 = prim0 x2 x3 ⟶ x1 = x3
Known db6fe.. : ∀ x0 x1 : ι → ι . ∀ x2 . prim1 x0 = prim1 x1 ⟶ x0 x2 = x1 x2
Known a8e2e.. : ∀ x0 x1 x2 x3 . a3eb9.. x0 x1 = bf68c.. x2 x3 ⟶ ∀ x4 : ο . x4
Known 128d8.. : ∀ x0 x1 x2 x3 . prim0 x0 x1 = prim0 x2 x3 ⟶ ∀ x4 : ο . (x0 = x2 ⟶ x1 = x3 ⟶ x4) ⟶ x4
Known 5e750.. : ∀ x0 x1 x2 x3 . a3eb9.. x0 x1 = a3eb9.. x2 x3 ⟶ and (x0 = x2) (x1 = x3)
Known 2f86f.. : ∀ x0 x1 x2 x3 . bf68c.. x0 x1 = bf68c.. x2 x3 ⟶ and (x0 = x2) (x1 = x3)
Known a3634.. : ∀ x0 x1 . c4def.. = 6b90c.. x0 x1 ⟶ ∀ x2 : ο . x2
Known 0286c.. : ∀ x0 x1 . prim0 x0 x1 = 236c6.. ⟶ False
Known 5e60e.. : c4def.. = c9248.. ⟶ ∀ x0 : ο . x0
Known dc5ae.. : ∀ x0 x1 . 6b90c.. x0 x1 = c9248.. ⟶ ∀ x2 : ο . x2
Known 924dd.. : ∀ x0 . c4def.. = a6e19.. x0 ⟶ ∀ x1 : ο . x1
Known a9278.. : ∀ x0 x1 x2 . 6b90c.. x0 x1 = a6e19.. x2 ⟶ ∀ x3 : ο . x3
Known 84bad.. : ∀ x0 . c9248.. = a6e19.. x0 ⟶ ∀ x1 : ο . x1
Known 0cc7e.. : ∀ x0 . c4def.. = 2fe34.. x0 ⟶ ∀ x1 : ο . x1
Known dabcf.. : ∀ x0 x1 x2 . 6b90c.. x0 x1 = 2fe34.. x2 ⟶ ∀ x3 : ο . x3
Known 1832c.. : ∀ x0 . c9248.. = 2fe34.. x0 ⟶ ∀ x1 : ο . x1
Known 7241c.. : ∀ x0 x1 . a6e19.. x0 = 2fe34.. x1 ⟶ ∀ x2 : ο . x2
Known 91964.. : ∀ x0 x1 . c4def.. = 3e00e.. x0 x1 ⟶ ∀ x2 : ο . x2
Known 07fb9.. : ∀ x0 x1 x2 x3 . 6b90c.. x0 x1 = 3e00e.. x2 x3 ⟶ ∀ x4 : ο . x4
Known 77b59.. : ∀ x0 x1 . c9248.. = 3e00e.. x0 x1 ⟶ ∀ x2 : ο . x2
Known 62a09.. : ∀ x0 x1 x2 . a6e19.. x0 = 3e00e.. x1 x2 ⟶ ∀ x3 : ο . x3
Known a0ec1.. : ∀ x0 x1 x2 . 2fe34.. x0 = 3e00e.. x1 x2 ⟶ ∀ x3 : ο . x3
Known a14cf.. : ∀ x0 x1 . c4def.. = f9341.. x0 x1 ⟶ ∀ x2 : ο . x2
Known 72b8e.. : ∀ x0 x1 x2 x3 . 6b90c.. x0 x1 = f9341.. x2 x3 ⟶ ∀ x4 : ο . x4
Known b728e.. : ∀ x0 x1 . c9248.. = f9341.. x0 x1 ⟶ ∀ x2 : ο . x2
Known cec81.. : ∀ x0 x1 x2 . a6e19.. x0 = f9341.. x1 x2 ⟶ ∀ x3 : ο . x3
Known becdb.. : ∀ x0 x1 x2 . 2fe34.. x0 = f9341.. x1 x2 ⟶ ∀ x3 : ο . x3
Known a1a1b.. : ∀ x0 x1 x2 x3 . 3e00e.. x0 x1 = f9341.. x2 x3 ⟶ ∀ x4 : ο . x4
Known b8b08.. : ∀ x0 . c4def.. = 1fa6d.. x0 ⟶ ∀ x1 : ο . x1
Known 0a32f.. : ∀ x0 x1 x2 . 6b90c.. x0 x1 = 1fa6d.. x2 ⟶ ∀ x3 : ο . x3
Known 0482c.. : ∀ x0 . c9248.. = 1fa6d.. x0 ⟶ ∀ x1 : ο . x1
Known 4bdb9.. : ∀ x0 x1 . a6e19.. x0 = 1fa6d.. x1 ⟶ ∀ x2 : ο . x2
Known a5def.. : ∀ x0 x1 . 2fe34.. x0 = 1fa6d.. x1 ⟶ ∀ x2 : ο . x2
Known 54459.. : ∀ x0 x1 x2 . 3e00e.. x0 x1 = 1fa6d.. x2 ⟶ ∀ x3 : ο . x3
Known 38968.. : ∀ x0 x1 x2 . f9341.. x0 x1 = 1fa6d.. x2 ⟶ ∀ x3 : ο . x3
Known f9749.. : ∀ x0 . c4def.. = 3a365.. x0 ⟶ ∀ x1 : ο . x1
Known ff84b.. : ∀ x0 x1 x2 . 6b90c.. x0 x1 = 3a365.. x2 ⟶ ∀ x3 : ο . x3
Known 36b24.. : ∀ x0 . c9248.. = 3a365.. x0 ⟶ ∀ x1 : ο . x1
Known 62476.. : ∀ x0 x1 . a6e19.. x0 = 3a365.. x1 ⟶ ∀ x2 : ο . x2
Known cdd8a.. : ∀ x0 x1 . 2fe34.. x0 = 3a365.. x1 ⟶ ∀ x2 : ο . x2
Known fb77a.. : ∀ x0 x1 x2 . 3e00e.. x0 x1 = 3a365.. x2 ⟶ ∀ x3 : ο . x3
Known 6774e.. : ∀ x0 x1 x2 . f9341.. x0 x1 = 3a365.. x2 ⟶ ∀ x3 : ο . x3
Known 9f429.. : ∀ x0 x1 . 1fa6d.. x0 = 3a365.. x1 ⟶ ∀ x2 : ο . x2
Known ffc37.. : ∀ x0 x1 x2 x3 . 6b90c.. x0 x1 = 6b90c.. x2 x3 ⟶ and (x0 = x2) (x1 = x3)
Known ffefa.. : ∀ x0 x1 x2 x3 . 6b90c.. x0 x1 = 6b90c.. x2 x3 ⟶ x0 = x2
Known af84e.. : ∀ x0 x1 x2 x3 . 6b90c.. x0 x1 = 6b90c.. x2 x3 ⟶ x1 = x3
Known 84af1.. : ∀ x0 x1 . a6e19.. x0 = a6e19.. x1 ⟶ x0 = x1
Known 2eb6f.. : ∀ x0 x1 . 2fe34.. x0 = 2fe34.. x1 ⟶ x0 = x1
Known 42e43.. : ∀ x0 x1 x2 x3 . 3e00e.. x0 x1 = 3e00e.. x2 x3 ⟶ and (x0 = x2) (x1 = x3)
Known ee7eb.. : ∀ x0 x1 x2 x3 . 3e00e.. x0 x1 = 3e00e.. x2 x3 ⟶ x0 = x2
Known 67376.. : ∀ x0 x1 x2 x3 . 3e00e.. x0 x1 = 3e00e.. x2 x3 ⟶ x1 = x3
Known 063ac.. : ∀ x0 x1 x2 x3 . f9341.. x0 x1 = f9341.. x2 x3 ⟶ and (x0 = x2) (x1 = x3)
Known 9efcd.. : ∀ x0 x1 x2 x3 . f9341.. x0 x1 = f9341.. x2 x3 ⟶ x0 = x2
Known 2b512.. : ∀ x0 x1 x2 x3 . f9341.. x0 x1 = f9341.. x2 x3 ⟶ x1 = x3
Known a1c68.. : ∀ x0 x1 . 1fa6d.. x0 = 1fa6d.. x1 ⟶ x0 = x1
Known f684d.. : ∀ x0 x1 . 3a365.. x0 = 3a365.. x1 ⟶ x0 = x1
Param 74e69.. : ι → ο
Known e5778.. : 74e69.. 5e331..
Known c4252.. : ∀ x0 x1 . 74e69.. x0 ⟶ 74e69.. x1 ⟶ 74e69.. (a3eb9.. x0 x1)
Known fbf8c.. : ∀ x0 x1 . 74e69.. x0 ⟶ 74e69.. x1 ⟶ 74e69.. (bf68c.. x0 x1)
Known facf7.. : ∀ x0 : ι → ο . x0 5e331.. ⟶ (∀ x1 x2 . 74e69.. x1 ⟶ x0 x1 ⟶ 74e69.. x2 ⟶ x0 x2 ⟶ x0 (a3eb9.. x1 x2)) ⟶ (∀ x1 x2 . 74e69.. x1 ⟶ x0 x1 ⟶ 74e69.. x2 ⟶ x0 x2 ⟶ x0 (bf68c.. x1 x2)) ⟶ ∀ x1 . 74e69.. x1 ⟶ x0 x1
Known FalseE : False ⟶ ∀ x0 : ο . x0
Known 75262.. : ∀ x0 x1 . 74e69.. (a3eb9.. x0 x1) ⟶ and (74e69.. x0) (74e69.. x1)
Known 826e0.. : ∀ x0 x1 . 74e69.. (bf68c.. x0 x1) ⟶ and (74e69.. x0) (74e69.. x1)
Param e05e6.. : ι → ο
Known b24e2.. : e05e6.. c4def..
Known 05df6.. : ∀ x0 x1 . e05e6.. x0 ⟶ e05e6.. x1 ⟶ e05e6.. (6b90c.. x0 x1)
Known 9dc64.. : e05e6.. c9248..
Known 82f14.. : ∀ x0 . e05e6.. x0 ⟶ e05e6.. (a6e19.. x0)
Known 6d5ea.. : ∀ x0 . e05e6.. x0 ⟶ e05e6.. (2fe34.. x0)
Known 1a774.. : ∀ x0 x1 . e05e6.. x0 ⟶ e05e6.. x1 ⟶ e05e6.. (3e00e.. x0 x1)
Known 6891d.. : ∀ x0 x1 . e05e6.. x0 ⟶ e05e6.. x1 ⟶ e05e6.. (f9341.. x0 x1)
Known 96df8.. : ∀ x0 . e05e6.. x0 ⟶ e05e6.. (1fa6d.. x0)
Known b6c01.. : ∀ x0 . e05e6.. x0 ⟶ e05e6.. (3a365.. x0)
Definition 762f0.. := λ x0 x1 x2 . ∀ x3 : ι → ι → ι → ο . (∀ x4 . 74e69.. x4 ⟶ x3 c4def.. x4 x4) ⟶ (∀ x4 x5 x6 x7 x8 . x3 x7 x4 x5 ⟶ x3 x8 x5 x6 ⟶ x3 (6b90c.. x7 x8) x4 x6) ⟶ (∀ x4 . 74e69.. x4 ⟶ x3 c9248.. x4 5e331..) ⟶ (∀ x4 x5 x6 x7 . 74e69.. x6 ⟶ x3 x7 x4 x5 ⟶ x3 (a6e19.. x7) x4 (a3eb9.. x5 x6)) ⟶ (∀ x4 x5 x6 x7 . 74e69.. x5 ⟶ x3 x7 x4 x6 ⟶ x3 (2fe34.. x7) x4 (a3eb9.. x5 x6)) ⟶ (∀ x4 x5 x6 x7 x8 x9 . x3 x8 (bf68c.. x4 x6) x7 ⟶ x3 x9 (bf68c.. x5 x6) x7 ⟶ x3 (3e00e.. x8 x9) (bf68c.. (a3eb9.. x4 x5) x6) x7) ⟶ (∀ x4 x5 x6 x7 x8 . x3 x7 x4 x5 ⟶ x3 x8 x4 x6 ⟶ x3 (f9341.. x7 x8) x4 (bf68c.. x5 x6)) ⟶ (∀ x4 x5 x6 x7 . 74e69.. x5 ⟶ x3 x7 x4 x6 ⟶ x3 (1fa6d.. x7) (bf68c.. x4 x5) x6) ⟶ (∀ x4 x5 x6 x7 . 74e69.. x4 ⟶ x3 x7 x5 x6 ⟶ x3 (3a365.. x7) (bf68c.. x4 x5) x6) ⟶ x3 x0 x1 x2
Theorem 010e7.. : ∀ x0 . 74e69.. x0 ⟶ 762f0.. c4def.. x0 x0 (proof)
Theorem 0333b.. : ∀ x0 x1 x2 x3 x4 . 762f0.. x3 x0 x1 ⟶ 762f0.. x4 x1 x2 ⟶ 762f0.. (6b90c.. x3 x4) x0 x2 (proof)
Theorem ead5a.. : ∀ x0 . 74e69.. x0 ⟶ 762f0.. c9248.. x0 5e331.. (proof)
Theorem 80667.. : ∀ x0 x1 x2 x3 . 74e69.. x2 ⟶ 762f0.. x3 x0 x1 ⟶ 762f0.. (a6e19.. x3) x0 (a3eb9.. x1 x2) (proof)
Theorem f5f14.. : ∀ x0 x1 x2 x3 . 74e69.. x1 ⟶ 762f0.. x3 x0 x2 ⟶ 762f0.. (2fe34.. x3) x0 (a3eb9.. x1 x2) (proof)
Theorem 8353a.. : ∀ x0 x1 x2 x3 x4 x5 . 762f0.. x4 (bf68c.. x0 x2) x3 ⟶ 762f0.. x5 (bf68c.. x1 x2) x3 ⟶ 762f0.. (3e00e.. x4 x5) (bf68c.. (a3eb9.. x0 x1) x2) x3 (proof)
Theorem ba8a3.. : ∀ x0 x1 x2 x3 x4 . 762f0.. x3 x0 x1 ⟶ 762f0.. x4 x0 x2 ⟶ 762f0.. (f9341.. x3 x4) x0 (bf68c.. x1 x2) (proof)
Theorem b8429.. : ∀ x0 x1 x2 x3 . 74e69.. x1 ⟶ 762f0.. x3 x0 x2 ⟶ 762f0.. (1fa6d.. x3) (bf68c.. x0 x1) x2 (proof)
Theorem 383fe.. : ∀ x0 x1 x2 x3 . 74e69.. x0 ⟶ 762f0.. x3 x1 x2 ⟶ 762f0.. (3a365.. x3) (bf68c.. x0 x1) x2 (proof)
Theorem 4eb50.. : ∀ x0 : ι → ι → ι → ο . (∀ x1 . 74e69.. x1 ⟶ x0 c4def.. x1 x1) ⟶ (∀ x1 x2 x3 x4 x5 . 762f0.. x4 x1 x2 ⟶ x0 x4 x1 x2 ⟶ 762f0.. x5 x2 x3 ⟶ x0 x5 x2 x3 ⟶ x0 (6b90c.. x4 x5) x1 x3) ⟶ (∀ x1 . 74e69.. x1 ⟶ x0 c9248.. x1 5e331..) ⟶ (∀ x1 x2 x3 x4 . 74e69.. x3 ⟶ 762f0.. x4 x1 x2 ⟶ x0 x4 x1 x2 ⟶ x0 (a6e19.. x4) x1 (a3eb9.. x2 x3)) ⟶ (∀ x1 x2 x3 x4 . 74e69.. x2 ⟶ 762f0.. x4 x1 x3 ⟶ x0 x4 x1 x3 ⟶ x0 (2fe34.. x4) x1 (a3eb9.. x2 x3)) ⟶ (∀ x1 x2 x3 x4 x5 x6 . 762f0.. x5 (bf68c.. x1 x3) x4 ⟶ x0 x5 (bf68c.. x1 x3) x4 ⟶ 762f0.. x6 (bf68c.. x2 x3) x4 ⟶ x0 x6 (bf68c.. x2 x3) x4 ⟶ x0 (3e00e.. x5 x6) (bf68c.. (a3eb9.. x1 x2) x3) x4) ⟶ (∀ x1 x2 x3 x4 x5 . 762f0.. x4 x1 x2 ⟶ x0 x4 x1 x2 ⟶ 762f0.. x5 x1 x3 ⟶ x0 x5 x1 x3 ⟶ x0 (f9341.. x4 x5) x1 (bf68c.. x2 x3)) ⟶ (∀ x1 x2 x3 x4 . 74e69.. x2 ⟶ 762f0.. x4 x1 x3 ⟶ x0 x4 x1 x3 ⟶ x0 (1fa6d.. x4) (bf68c.. x1 x2) x3) ⟶ (∀ x1 x2 x3 x4 . 74e69.. x1 ⟶ 762f0.. x4 x2 x3 ⟶ x0 x4 x2 x3 ⟶ x0 (3a365.. x4) (bf68c.. x1 x2) x3) ⟶ ∀ x1 x2 x3 . 762f0.. x1 x2 x3 ⟶ x0 x1 x2 x3 (proof)
Theorem beff0.. : ∀ x0 x1 x2 . 762f0.. x0 x1 x2 ⟶ and (and (e05e6.. x0) (74e69.. x1)) (74e69.. x2) (proof)