Proofgold Address

Param 762f0.. : ι → ι → ι → ο
Param 858ff.. : ι → (ι → ο) → ο
Param d7d78.. : ι → ι → ι → ο
Param 74e69.. : ι → ο
Param c4def.. : ι
Param 6b90c.. : ι → ι → ι
Param c9248.. : ι
Param 5e331.. : ι
Param a6e19.. : ι → ι
Param a3eb9.. : ι → ι → ι
Param 2fe34.. : ι → ι
Param bf68c.. : ι → ι → ι
Param 3e00e.. : ι → ι → ι
Param f9341.. : ι → ι → ι
Param 1fa6d.. : ι → ι
Param 3a365.. : ι → ι
Known 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
Known b316e.. : ∀ x0 x1 . d7d78.. c4def.. x0 x1 ⟶ x0 = x1
Known e3e6f.. : ∀ x0 . ∀ x1 x2 : ι → ο . 858ff.. x0 x1 ⟶ 858ff.. x0 x2 ⟶ x1 = x2
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Param e05e6.. : ι → ο
Known beff0.. : ∀ x0 x1 x2 . 762f0.. x0 x1 x2 ⟶ and (and (e05e6.. x0) (74e69.. x1)) (74e69.. x2)
Known 41bc1.. : ∀ x0 . 74e69.. x0 ⟶ ∀ x1 : ο . (∀ x2 : ι → ο . 858ff.. x0 x2 ⟶ x1) ⟶ x1
Known 8b3a5.. : ∀ x0 x1 x2 x3 . d7d78.. (6b90c.. x0 x1) x2 x3 ⟶ ∀ x4 : ο . (∀ x5 . and (d7d78.. x0 x2 x5) (d7d78.. x1 x5 x3) ⟶ x4) ⟶ x4
Param 236c6.. : ι
Definition 07017.. := λ x0 . x0 = 236c6..
Known 84f7f.. : ∀ x0 x1 . d7d78.. c9248.. x0 x1 ⟶ x1 = 236c6..
Known fb7af.. : 858ff.. 5e331.. 07017..
Param 0b8ef.. : ι → ι
Known aca1a.. : ∀ x0 x1 x2 . d7d78.. (a6e19.. x0) x1 x2 ⟶ ∀ x3 : ο . (∀ x4 . and (d7d78.. x0 x1 x4) (x2 = 0b8ef.. x4) ⟶ x3) ⟶ x3
Param c0709.. : (ι → ο) → (ι → ο) → ι → ο
Known b4c82.. : ∀ x0 x1 . ∀ x2 : ι → ο . 858ff.. (a3eb9.. x0 x1) x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → ο . (∀ x5 : ο . (∀ x6 : ι → ο . and (and (858ff.. x0 x4) (858ff.. x1 x6)) (x2 = c0709.. x4 x6) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3
Known 5c8d7.. : ∀ x0 x1 : ι → ο . ∀ x2 . x0 x2 ⟶ c0709.. x0 x1 (0b8ef.. x2)
Param 6c5f4.. : ι → ι
Known 42fd0.. : ∀ x0 x1 x2 . d7d78.. (2fe34.. x0) x1 x2 ⟶ ∀ x3 : ο . (∀ x4 . and (d7d78.. x0 x1 x4) (x2 = 6c5f4.. x4) ⟶ x3) ⟶ x3
Known f3d9f.. : ∀ x0 x1 : ι → ο . ∀ x2 . x1 x2 ⟶ c0709.. x0 x1 (6c5f4.. x2)
Param 6e020.. : (ι → ο) → (ι → ο) → ι → ο
Known 2156c.. : ∀ x0 x1 . ∀ x2 : ι → ο . 858ff.. (bf68c.. x0 x1) x2 ⟶ ∀ x3 : ο . (∀ x4 : ι → ο . (∀ x5 : ο . (∀ x6 : ι → ο . and (and (858ff.. x0 x4) (858ff.. x1 x6)) (x2 = 6e020.. x4 x6) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Param cfc98.. : ι → ι → ι
Known b4261.. : ∀ x0 x1 x2 x3 . d7d78.. (3e00e.. x0 x1) x2 x3 ⟶ or (∀ x4 : ο . (∀ x5 . (∀ x6 : ο . (∀ x7 . and (x2 = cfc98.. (0b8ef.. x5) x7) (d7d78.. x0 (cfc98.. x5 x7) x3) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4) (∀ x4 : ο . (∀ x5 . (∀ x6 : ο . (∀ x7 . and (x2 = cfc98.. (6c5f4.. x5) x7) (d7d78.. x1 (cfc98.. x5 x7) x3) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4)
Known 024d1.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 . x0 x2 ⟶ x1 x3 ⟶ 6e020.. x0 x1 (cfc98.. x2 x3)
Known 78238.. : ∀ x0 x1 : ι → ο . ∀ x2 . 6e020.. x0 x1 x2 ⟶ ∀ x3 : ι → ο . (∀ x4 x5 . x0 x4 ⟶ x1 x5 ⟶ x3 (cfc98.. x4 x5)) ⟶ x3 x2
Known 8b44a.. : ∀ x0 x1 : ι → ο . ∀ x2 . c0709.. x0 x1 x2 ⟶ ∀ x3 : ι → ο . (∀ x4 . x0 x4 ⟶ x3 (0b8ef.. x4)) ⟶ (∀ x4 . x1 x4 ⟶ x3 (6c5f4.. x4)) ⟶ x3 x2
Known 3a4f6.. : ∀ x0 x1 x2 x3 . cfc98.. x0 x1 = cfc98.. x2 x3 ⟶ and (x0 = x2) (x1 = x3)
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known 3a245.. : ∀ x0 x1 . 0b8ef.. x0 = 0b8ef.. x1 ⟶ x0 = x1
Definition False := ∀ x0 : ο . x0
Known FalseE : False ⟶ ∀ x0 : ο . x0
Known 88d35.. : ∀ x0 x1 . 0b8ef.. x0 = 6c5f4.. x1 ⟶ ∀ x2 : ο . x2
Known cc192.. : ∀ x0 x1 . 6c5f4.. x0 = 6c5f4.. x1 ⟶ x0 = x1
Known 57d3c.. : ∀ x0 x1 . ∀ x2 x3 : ι → ο . 858ff.. x0 x2 ⟶ 858ff.. x1 x3 ⟶ 858ff.. (bf68c.. x0 x1) (6e020.. x2 x3)
Known 3f6f9.. : ∀ x0 x1 x2 x3 . d7d78.. (f9341.. x0 x1) x2 x3 ⟶ ∀ x4 : ο . (∀ x5 . (∀ x6 : ο . (∀ x7 . and (and (d7d78.. x0 x2 x5) (d7d78.. x1 x2 x7)) (x3 = cfc98.. x5 x7) ⟶ x6) ⟶ x6) ⟶ x4) ⟶ x4
Known 17be7.. : ∀ x0 x1 x2 . d7d78.. (1fa6d.. x0) x1 x2 ⟶ ∀ x3 : ο . (∀ x4 . (∀ x5 : ο . (∀ x6 . and (x1 = cfc98.. x4 x6) (d7d78.. x0 x4 x2) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3
Known efdff.. : ∀ x0 x1 x2 . d7d78.. (3a365.. x0) x1 x2 ⟶ ∀ x3 : ο . (∀ x4 . (∀ x5 : ο . (∀ x6 . and (x1 = cfc98.. x4 x6) (d7d78.. x0 x6 x2) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3
Theorem 085db.. : ∀ x0 x1 x2 . 762f0.. x0 x1 x2 ⟶ ∀ x3 x4 : ι → ο . 858ff.. x1 x3 ⟶ 858ff.. x2 x4 ⟶ ∀ x5 x6 . x3 x5 ⟶ d7d78.. x0 x5 x6 ⟶ x4 x6 (proof)
Definition 5dc8b.. := λ x0 x1 . and (∀ x2 . x0 = 0b8ef.. x2 ⟶ x1 = 6c5f4.. x2) (∀ x2 . x0 = 6c5f4.. x2 ⟶ x1 = 0b8ef.. x2)
Known 0333b.. : ∀ x0 x1 x2 x3 x4 . 762f0.. x3 x0 x1 ⟶ 762f0.. x4 x1 x2 ⟶ 762f0.. (6b90c.. x3 x4) x0 x2
Known ba8a3.. : ∀ x0 x1 x2 x3 x4 . 762f0.. x3 x0 x1 ⟶ 762f0.. x4 x0 x2 ⟶ 762f0.. (f9341.. x3 x4) x0 (bf68c.. x1 x2)
Known 010e7.. : ∀ x0 . 74e69.. x0 ⟶ 762f0.. c4def.. x0 x0
Known ead5a.. : ∀ x0 . 74e69.. x0 ⟶ 762f0.. c9248.. x0 5e331..
Known 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
Known b8429.. : ∀ x0 x1 x2 x3 . 74e69.. x1 ⟶ 762f0.. x3 x0 x2 ⟶ 762f0.. (1fa6d.. x3) (bf68c.. x0 x1) x2
Known e5778.. : 74e69.. 5e331..
Known f5f14.. : ∀ x0 x1 x2 x3 . 74e69.. x1 ⟶ 762f0.. x3 x0 x2 ⟶ 762f0.. (2fe34.. x3) x0 (a3eb9.. x1 x2)
Known 80667.. : ∀ x0 x1 x2 x3 . 74e69.. x2 ⟶ 762f0.. x3 x0 x1 ⟶ 762f0.. (a6e19.. x3) x0 (a3eb9.. x1 x2)
Known 3e6f8.. : ∀ x0 x1 x2 x3 x4 . d7d78.. x0 x2 x3 ⟶ d7d78.. x1 x3 x4 ⟶ d7d78.. (6b90c.. x0 x1) x2 x4
Known 092f4.. : ∀ x0 x1 x2 x3 x4 . d7d78.. x0 x2 x3 ⟶ d7d78.. x1 x2 x4 ⟶ d7d78.. (f9341.. x0 x1) x2 (cfc98.. x3 x4)
Known 4a83c.. : ∀ x0 . d7d78.. c4def.. x0 x0
Known b6648.. : ∀ x0 . d7d78.. c9248.. x0 236c6..
Known 547ca.. : ∀ x0 x1 x2 x3 x4 . e05e6.. x1 ⟶ d7d78.. x0 (cfc98.. x2 x3) x4 ⟶ d7d78.. (3e00e.. x0 x1) (cfc98.. (0b8ef.. x2) x3) x4
Known 96df8.. : ∀ x0 . e05e6.. x0 ⟶ e05e6.. (1fa6d.. x0)
Known 82f14.. : ∀ x0 . e05e6.. x0 ⟶ e05e6.. (a6e19.. x0)
Known b24e2.. : e05e6.. c4def..
Known d0180.. : ∀ x0 x1 x2 x3 . d7d78.. x0 x1 x3 ⟶ d7d78.. (1fa6d.. x0) (cfc98.. x1 x2) x3
Known ca73c.. : ∀ x0 x1 x2 . d7d78.. x0 x1 x2 ⟶ d7d78.. (2fe34.. x0) x1 (6c5f4.. x2)
Known 2011d.. : ∀ x0 x1 x2 x3 x4 . e05e6.. x0 ⟶ d7d78.. x1 (cfc98.. x2 x3) x4 ⟶ d7d78.. (3e00e.. x0 x1) (cfc98.. (6c5f4.. x2) x3) x4
Known 6d5ea.. : ∀ x0 . e05e6.. x0 ⟶ e05e6.. (2fe34.. x0)
Known c8e20.. : ∀ x0 x1 x2 . d7d78.. x0 x1 x2 ⟶ d7d78.. (a6e19.. x0) x1 (0b8ef.. x2)
Known c4252.. : ∀ x0 x1 . 74e69.. x0 ⟶ 74e69.. x1 ⟶ 74e69.. (a3eb9.. x0 x1)
Theorem 181f2.. : ∀ x0 . 74e69.. x0 ⟶ ∀ x1 : ο . (∀ x2 . and (762f0.. x2 (a3eb9.. x0 x0) (a3eb9.. x0 x0)) (∀ x3 : ι → ο . 858ff.. x0 x3 ⟶ ∀ x4 x5 . c0709.. x3 x3 x4 ⟶ 5dc8b.. x4 x5 ⟶ d7d78.. x2 x4 x5) ⟶ x1) ⟶ x1 (proof)