Proofgold Address

Param ap^ap : ι → ι → ι
Param lam^Sigma : ι → (ι → ι) → ι
Param ordsucc^ordsucc : ι → ι
Param If_i^If_i : ο → ι → ι → ι
Definition u17_to_Church17 := λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . ap (lam 17 (λ x18 . If_i (x18 = 0) x1 (If_i (x18 = 1) x2 (If_i (x18 = 2) x3 (If_i (x18 = 3) x4 (If_i (x18 = 4) x5 (If_i (x18 = 5) x6 (If_i (x18 = 6) x7 (If_i (x18 = 7) x8 (If_i (x18 = 8) x9 (If_i (x18 = 9) x10 (If_i (x18 = 10) x11 (If_i (x18 = 11) x12 (If_i (x18 = 12) x13 (If_i (x18 = 13) x14 (If_i (x18 = 14) x15 (If_i (x18 = 15) x16 x17))))))))))))))))) x0
Known 192ab.. : (∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 . x3 ∈ x1 ⟶ ap (lam x1 (λ x5 . If_i (x5 = x3) x0 (x2 (ordsucc x3) x5))) x3 = x0) ⟶ (∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 x4 . (x4 = x3 ⟶ ∀ x5 : ο . x5) ⟶ ap (lam x1 (λ x6 . If_i (x6 = x3) x0 (x2 (ordsucc x3) x6))) x4 = ap (lam x1 (x2 (ordsucc x3))) x4) ⟶ ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . ap (lam 17 (λ x18 . If_i (x18 = 0) x0 (If_i (x18 = 1) x1 (If_i (x18 = 2) x2 (If_i (x18 = 3) x3 (If_i (x18 = 4) x4 (If_i (x18 = 5) x5 (If_i (x18 = 6) x6 (If_i (x18 = 7) x7 (If_i (x18 = 8) x8 (If_i (x18 = 9) x9 (If_i (x18 = 10) x10 (If_i (x18 = 11) x11 (If_i (x18 = 12) x12 (If_i (x18 = 13) x13 (If_i (x18 = 14) x14 (If_i (x18 = 15) x15 x16))))))))))))))))) 0 = x0
Known 48efb.. : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 . x3 ∈ x1 ⟶ ap (lam x1 (λ x5 . If_i (x5 = x3) x0 (x2 (ordsucc x3) x5))) x3 = x0
Known d21a1.. : ∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 x4 . (x4 = x3 ⟶ ∀ x5 : ο . x5) ⟶ ap (lam x1 (λ x6 . If_i (x6 = x3) x0 (x2 (ordsucc x3) x6))) x4 = ap (lam x1 (x2 (ordsucc x3))) x4
Theorem 631b4.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . ap (lam 17 (λ x18 . If_i (x18 = 0) x0 (If_i (x18 = 1) x1 (If_i (x18 = 2) x2 (If_i (x18 = 3) x3 (If_i (x18 = 4) x4 (If_i (x18 = 5) x5 (If_i (x18 = 6) x6 (If_i (x18 = 7) x7 (If_i (x18 = 8) x8 (If_i (x18 = 9) x9 (If_i (x18 = 10) x10 (If_i (x18 = 11) x11 (If_i (x18 = 12) x12 (If_i (x18 = 13) x13 (If_i (x18 = 14) x14 (If_i (x18 = 15) x15 x16))))))))))))))))) 0 = x0 (proof)
Param u1 : ι
Known 74e99.. : (∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 . x3 ∈ x1 ⟶ ap (lam x1 (λ x5 . If_i (x5 = x3) x0 (x2 (ordsucc x3) x5))) x3 = x0) ⟶ (∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 x4 . (x4 = x3 ⟶ ∀ x5 : ο . x5) ⟶ ap (lam x1 (λ x6 . If_i (x6 = x3) x0 (x2 (ordsucc x3) x6))) x4 = ap (lam x1 (x2 (ordsucc x3))) x4) ⟶ ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . ap (lam 17 (λ x18 . If_i (x18 = 0) x0 (If_i (x18 = 1) x1 (If_i (x18 = 2) x2 (If_i (x18 = 3) x3 (If_i (x18 = 4) x4 (If_i (x18 = 5) x5 (If_i (x18 = 6) x6 (If_i (x18 = 7) x7 (If_i (x18 = 8) x8 (If_i (x18 = 9) x9 (If_i (x18 = 10) x10 (If_i (x18 = 11) x11 (If_i (x18 = 12) x12 (If_i (x18 = 13) x13 (If_i (x18 = 14) x14 (If_i (x18 = 15) x15 x16))))))))))))))))) u1 = x1
Theorem a6778.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . ap (lam 17 (λ x18 . If_i (x18 = 0) x0 (If_i (x18 = 1) x1 (If_i (x18 = 2) x2 (If_i (x18 = 3) x3 (If_i (x18 = 4) x4 (If_i (x18 = 5) x5 (If_i (x18 = 6) x6 (If_i (x18 = 7) x7 (If_i (x18 = 8) x8 (If_i (x18 = 9) x9 (If_i (x18 = 10) x10 (If_i (x18 = 11) x11 (If_i (x18 = 12) x12 (If_i (x18 = 13) x13 (If_i (x18 = 14) x14 (If_i (x18 = 15) x15 x16))))))))))))))))) u1 = x1 (proof)
Param u2 : ι
Known c7cd7.. : (∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 . x3 ∈ x1 ⟶ ap (lam x1 (λ x5 . If_i (x5 = x3) x0 (x2 (ordsucc x3) x5))) x3 = x0) ⟶ (∀ x0 x1 . ∀ x2 : ι → ι → ι . ∀ x3 x4 . (x4 = x3 ⟶ ∀ x5 : ο . x5) ⟶ ap (lam x1 (λ x6 . If_i (x6 = x3) x0 (x2 (ordsucc x3) x6))) x4 = ap (lam x1 (x2 (ordsucc x3))) x4) ⟶ ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . ap (lam 17 (λ x18 . If_i (x18 = 0) x0 (If_i (x18 = 1) x1 (If_i (x18 = 2) x2 (If_i (x18 = 3) x3 (If_i (x18 = 4) x4 (If_i (x18 = 5) x5 (If_i (x18 = 6) x6 (If_i (x18 = 7) x7 (If_i (x18 = 8) x8 (If_i (x18 = 9) x9 (If_i (x18 = 10) x10 (If_i (x18 = 11) x11 (If_i (x18 = 12) x12 (If_i (x18 = 13) x13 (If_i (x18 = 14) x14 (If_i (x18 = 15) x15 x16))))))))))))))))) u2 = x2
Theorem 02ffe.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . ap (lam 17 (λ x18 . If_i (x18 = 0) x0 (If_i (x18 = 1) x1 (If_i (x18 = 2) x2 (If_i (x18 = 3) x3 (If_i (x18 = 4) x4 (If_i (x18 = 5) x5 (If_i (x18 = 6) x6 (If_i (x18 = 7) x7 (If_i (x18 = 8) x8 (If_i (x18 = 9) x9 (If_i (x18 = 10) x10 (If_i (x18 = 11) x11 (If_i (x18 = 12) x12 (If_i (x18 = 13) x13 (If_i (x18 = 14) x14 (If_i (x18 = 15) x15 x16))))))))))))))))) u2 = x2 (proof)
Known aa7c9.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . ∀ x1 . ∀ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . (∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x0 x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 = x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19) ⟶ x0 x1 = x2
Theorem c5926.. : u17_to_Church17 0 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x1 (proof)
Theorem b0ce1.. : u17_to_Church17 u1 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x2 (proof)
Theorem e8ec5.. : u17_to_Church17 u2 = λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x3 (proof)