Proofgold Address

Param 0fc90.. : ι → (ι → ι) → ι
Param 4ae4a.. : ι → ι
Param 4a7ef.. : ι
Param f482f.. : ι → ι → ι
Param If_i : ο → ι → ι → ι
Known 7e4c2.. : ∀ x0 . ∀ x1 : ι → ι . 0fc90.. x0 (f482f.. (0fc90.. x0 x1)) = 0fc90.. x0 x1
Theorem 3f4b4.. : ∀ x0 x1 x2 . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) x1 x2)))) = 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) x1 x2)) (proof)
Theorem 2c4f9.. : ∀ x0 x1 x2 x3 . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) x1 (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 x3))))) = 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) x1 (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 x3))) (proof)
Known f22ec.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ f482f.. (0fc90.. x0 x1) x2 = x1 x2
Known 72f77.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))
Known If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Theorem 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 (proof)
Known c60fe.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))
Definition False := ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Known If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Known 5c667.. : 4ae4a.. 4a7ef.. = 4a7ef.. ⟶ ∀ x0 : ο . x0
Theorem 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 (proof)
Known 2eaee.. : prim1 (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))
Known 3a2b6.. : 4ae4a.. (4ae4a.. 4a7ef..) = 4a7ef.. ⟶ ∀ x0 : ο . x0
Known f9d2f.. : 4ae4a.. (4ae4a.. 4a7ef..) = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0
Theorem 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 (proof)
Known 77d87.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem 9f6be.. : ∀ x0 x1 x2 x3 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) x1 (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 x3)))) 4a7ef.. = x0 (proof)
Known 42824.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem 8a328.. : ∀ x0 x1 x2 x3 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) x1 (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 x3)))) (4ae4a.. 4a7ef..) = x1 (proof)
Known 68d02.. : prim1 (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem 142e6.. : ∀ x0 x1 x2 x3 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) x1 (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 x3)))) (4ae4a.. (4ae4a.. 4a7ef..)) = x2 (proof)
Known 778cc.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))
Known 57b7e.. : 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) = 4a7ef.. ⟶ ∀ x0 : ο . x0
Known daead.. : 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0
Known 0c325.. : 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) = 4ae4a.. (4ae4a.. 4a7ef..) ⟶ ∀ x0 : ο . x0
Theorem 62a6b.. : ∀ x0 x1 x2 x3 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) x1 (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 x3)))) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) = x3 (proof)
Param 3097a.. : ι → (ι → ι) → ι
Definition b5c9f.. := λ x0 x1 . 3097a.. x1 (λ x2 . x0)
Known 27474.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) (x1 x3)) ⟶ prim1 (0fc90.. x0 x2) (3097a.. x0 x1)
Known b1d09.. : ∀ x0 . prim1 x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ ∀ x1 : ι → ο . x1 4a7ef.. ⟶ x1 (4ae4a.. 4a7ef..) ⟶ x1 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ x1 x0
Theorem 29def.. : ∀ x0 x1 x2 x3 . prim1 x0 x3 ⟶ prim1 x1 x3 ⟶ prim1 x2 x3 ⟶ prim1 (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) x1 x2))) (b5c9f.. x3 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Param bij : ι → ι → (ι → ι) → ο
Param ba9d8.. : ι → ο
Known aa4b6.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) x0) ⟶ (∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) ⟶ bij x0 x0 x1
Known 2fbbc.. : ∀ x0 . ba9d8.. x0 ⟶ ba9d8.. (4ae4a.. x0)
Known d7fe6.. : ba9d8.. (4ae4a.. (4ae4a.. 4a7ef..))
Theorem 530f4.. : ∀ x0 x1 x2 . prim1 x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ prim1 x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ prim1 x2 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ (x0 = x1 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ bij (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x3 . If_i (x3 = 4a7ef..) x0 (If_i (x3 = 4ae4a.. 4a7ef..) x1 x2)))) (proof)
Known aeaf9.. : ∀ x0 . prim1 x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ ∀ x1 : ι → ο . x1 4a7ef.. ⟶ x1 (4ae4a.. 4a7ef..) ⟶ x1 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ x1 x0
Theorem 794ec.. : ∀ x0 x1 x2 x3 x4 . prim1 x0 x4 ⟶ prim1 x1 x4 ⟶ prim1 x2 x4 ⟶ prim1 x3 x4 ⟶ prim1 (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) x1 (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 x3)))) (b5c9f.. x4 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Theorem 81723.. : ∀ x0 x1 x2 x3 . prim1 x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ prim1 x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ prim1 x2 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ prim1 x3 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ (x0 = x1 ⟶ ∀ x4 : ο . x4) ⟶ (x0 = x2 ⟶ ∀ x4 : ο . x4) ⟶ (x0 = x3 ⟶ ∀ x4 : ο . x4) ⟶ (x1 = x2 ⟶ ∀ x4 : ο . x4) ⟶ (x1 = x3 ⟶ ∀ x4 : ο . x4) ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ bij (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) x1 (If_i (x4 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 x3))))) (proof)