Proofgold Address

Param ordsucc^ordsucc : ι → ι
Known neq_2_0^neq_2_0 : 2 = 0 ⟶ ∀ x0 : ο . x0
Param omega^omega : ι
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known EmptyE^EmptyE : ∀ x0 . nIn x0 0
Param nat_p^nat_p : ι → ο
Known nat_p_omega^nat_p_omega : ∀ x0 . nat_p x0 ⟶ x0 ∈ omega
Known nat_0^nat_0 : nat_p 0
Theorem b2bdc.. : omega = 0 ⟶ ∀ x0 : ο . x0
Param If_i^If_i : ο → ι → ι → ι
Known If_i_1^If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Known In_0_1^In_0_1 : 0 ∈ 1
Theorem 9348e.. : ∀ x0 : ο . x0 ⟶ 0 ∈ If_i x0 1 0
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known xm^xm : ∀ x0 : ο . or x0 (not x0)
Known If_i_0^If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Theorem 9bd39.. : ∀ x0 : ο . 0 ∈ If_i x0 1 0 ⟶ x0
Param lam^Sigma : ι → (ι → ι) → ι
Definition 9ca4f.. := λ x0 . lam x0 (λ x1 . lam x0 (λ x2 . If_i (x1 = x2) 1 0))
Param Pi^Pi : ι → (ι → ι) → ι
Definition setexp^setexp := λ x0 x1 . Pi x1 (λ x2 . x0)
Known lam_Pi^lam_Pi : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1 x3) ⟶ lam x0 x2 ∈ Pi x0 x1
Known If_i_or^If_i_or : ∀ x0 : ο . ∀ x1 x2 . or (If_i x0 x1 x2 = x1) (If_i x0 x1 x2 = x2)
Known In_1_2^In_1_2 : 1 ∈ 2
Known In_0_2^In_0_2 : 0 ∈ 2
Theorem 4488c.. : ∀ x0 . 9ca4f.. x0 ∈ setexp (setexp 2 x0) x0
Param ap^ap : ι → ι → ι
Known beta^beta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ap (lam x0 x1) x2 = x1 x2
Theorem 2d60a.. : ∀ x0 x1 . x1 ∈ x0 ⟶ 0 ∈ ap (ap (9ca4f.. x0) x1) x1
Theorem 17684.. : ∀ x0 x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ 0 ∈ ap (ap (9ca4f.. x0) x1) x2 ⟶ x1 = x2
Theorem ad55a.. : ∀ x0 . x0 ∈ 2 ⟶ ∀ x1 . x1 ∈ 2 ⟶ 0 ∈ ap (ap (9ca4f.. 2) x0) x1 ⟶ 0 ∈ x0 ⟶ 0 ∈ x1
Known cases_2^cases_2 : ∀ x0 . x0 ∈ 2 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 x0
Theorem 5ab41.. : ∀ x0 . x0 ∈ 2 ⟶ ∀ x1 . x1 ∈ 2 ⟶ (0 ∈ x0 ⟶ 0 ∈ x1) ⟶ (0 ∈ x1 ⟶ 0 ∈ x0) ⟶ 0 ∈ ap (ap (9ca4f.. 2) x0) x1
Theorem 70484.. : ∀ x0 x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ 0 ∈ ap (ap (9ca4f.. x0) x1) x2 ⟶ 0 ∈ ap (ap (9ca4f.. x0) x2) x3 ⟶ 0 ∈ ap (ap (9ca4f.. x0) x1) x3
Known ap_Pi^ap_Pi : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2 ∈ Pi x0 x1 ⟶ x3 ∈ x0 ⟶ ap x2 x3 ∈ x1 x3
Theorem a94a5.. : ∀ x0 x1 x2 . x2 ∈ setexp x1 x0 ⟶ ∀ x3 . x3 ∈ setexp x1 x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ 0 ∈ ap (ap (9ca4f.. (setexp x1 x0)) x2) x3 ⟶ 0 ∈ ap (ap (9ca4f.. x0) x4) x5 ⟶ 0 ∈ ap (ap (9ca4f.. x1) (ap x2 x4)) (ap x3 x5)
Known encode_u_ext^encode_u_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ lam x0 x1 = lam x0 x2
Theorem 7e67a.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . (∀ x4 . x4 ∈ x0 ⟶ x2 x4 ∈ x1) ⟶ (∀ x4 . x4 ∈ x0 ⟶ x3 x4 ∈ x1) ⟶ (∀ x4 . x4 ∈ x0 ⟶ 0 ∈ ap (ap (9ca4f.. x1) (x2 x4)) (x3 x4)) ⟶ 0 ∈ ap (ap (9ca4f.. (setexp x1 x0)) (lam x0 x2)) (lam x0 x3)
Definition 8d6e5.. := ap (ap (9ca4f.. (setexp 2 2)) (lam 2 (λ x0 . x0))) (lam 2 (λ x0 . x0))
Theorem 18dc3.. : 8d6e5.. ∈ 2
Theorem a497c.. : 0 ∈ ap (ap (9ca4f.. 2) 8d6e5..) (ap (ap (9ca4f.. (setexp 2 2)) (lam 2 (λ x0 . x0))) (lam 2 (λ x0 . x0)))
Theorem e7067.. : 0 ∈ 8d6e5..
Definition 9de32.. := lam 2 (λ x0 . lam 2 (λ x1 . ap (ap (9ca4f.. (setexp 2 (setexp (setexp 2 2) 2))) (lam (setexp (setexp 2 2) 2) (λ x2 . ap (ap x2 x0) x1))) (lam (setexp (setexp 2 2) 2) (λ x2 . ap (ap x2 8d6e5..) 8d6e5..))))
Theorem b2e87.. : 9de32.. ∈ setexp (setexp 2 2) 2
Theorem e0fb0.. : 0 ∈ ap (ap (9ca4f.. (setexp (setexp 2 2) 2)) 9de32..) (lam 2 (λ x0 . lam 2 (λ x1 . ap (ap (9ca4f.. (setexp 2 (setexp (setexp 2 2) 2))) (lam (setexp (setexp 2 2) 2) (λ x2 . ap (ap x2 x0) x1))) (lam (setexp (setexp 2 2) 2) (λ x2 . ap (ap x2 8d6e5..) 8d6e5..)))))
Definition 90e5f.. := lam 2 (λ x0 . lam 2 (λ x1 . ap (ap (9ca4f.. 2) (ap (ap 9de32.. x0) x1)) x0))
Theorem 0b79f.. : 90e5f.. ∈ setexp (setexp 2 2) 2
Theorem ec419.. : 0 ∈ ap (ap (9ca4f.. (setexp (setexp 2 2) 2)) 90e5f..) (lam 2 (λ x0 . lam 2 (λ x1 . ap (ap (9ca4f.. 2) (ap (ap 9de32.. x0) x1)) x0)))
Definition 1c786.. := λ x0 . lam (setexp 2 x0) (λ x1 . ap (ap (9ca4f.. (setexp 2 x0)) x1) (lam x0 (λ x2 . 8d6e5..)))
Theorem 72e0b.. : ∀ x0 . (x0 = 0 ⟶ ∀ x1 : ο . x1) ⟶ 1c786.. x0 ∈ setexp 2 (setexp 2 x0)
Theorem 897f1.. : ∀ x0 . (x0 = 0 ⟶ ∀ x1 : ο . x1) ⟶ 0 ∈ ap (ap (9ca4f.. (setexp 2 (setexp 2 x0))) (1c786.. x0)) (lam (setexp 2 x0) (λ x1 . ap (ap (9ca4f.. (setexp 2 x0)) x1) (lam x0 (λ x2 . 8d6e5..))))
Definition 82c61.. := λ x0 . lam (setexp 2 x0) (λ x1 . ap (1c786.. 2) (lam 2 (λ x2 . ap (ap 90e5f.. (ap (1c786.. x0) (lam x0 (λ x3 . ap (ap 90e5f.. (ap x1 x3)) x2)))) x2)))
Theorem 05c85.. : ∀ x0 . (x0 = 0 ⟶ ∀ x1 : ο . x1) ⟶ 82c61.. x0 ∈ setexp 2 (setexp 2 x0)
Theorem cee69.. : ∀ x0 . (x0 = 0 ⟶ ∀ x1 : ο . x1) ⟶ 0 ∈ ap (ap (9ca4f.. (setexp 2 (setexp 2 x0))) (82c61.. x0)) (lam (setexp 2 x0) (λ x1 . ap (1c786.. 2) (lam 2 (λ x2 . ap (ap 90e5f.. (ap (1c786.. x0) (lam x0 (λ x3 . ap (ap 90e5f.. (ap x1 x3)) x2)))) x2))))
Definition 8a736.. := lam 2 (λ x0 . lam 2 (λ x1 . ap (1c786.. 2) (lam 2 (λ x2 . ap (ap 90e5f.. (ap (ap 90e5f.. x0) x2)) (ap (ap 90e5f.. (ap (ap 90e5f.. x1) x2)) x2)))))
Theorem 7c7c0.. : 8a736.. ∈ setexp (setexp 2 2) 2
Theorem 18a89.. : 0 ∈ ap (ap (9ca4f.. (setexp (setexp 2 2) 2)) 8a736..) (lam 2 (λ x0 . lam 2 (λ x1 . ap (1c786.. 2) (lam 2 (λ x2 . ap (ap 90e5f.. (ap (ap 90e5f.. x0) x2)) (ap (ap 90e5f.. (ap (ap 90e5f.. x1) x2)) x2))))))
Definition 497c5.. := ap (1c786.. 2) (lam 2 (λ x0 . x0))
Theorem eed34.. : 497c5.. ∈ 2
Theorem b131f.. : 0 ∈ ap (ap (9ca4f.. 2) 497c5..) (ap (1c786.. 2) (lam 2 (λ x0 . x0)))
Definition d8d8a.. := lam 2 (λ x0 . ap (ap 90e5f.. x0) 497c5..)
Theorem 07b96.. : d8d8a.. ∈ setexp 2 2
Theorem 1391d.. : 0 ∈ ap (ap (9ca4f.. (setexp 2 2)) d8d8a..) (lam 2 (λ x0 . ap (ap 90e5f.. x0) 497c5..))