Proofgold Address

Param In_rec_ii^In_rec_ii : (ι → (ι → ι → ι) → ι → ι) → ι → ι → ι
Param If_ii^If_ii : ο → (ι → ι) → (ι → ι) → ι → ι
Definition nat_primrec_ii := λ x0 : ι → ι . λ x1 : ι → (ι → ι) → ι → ι . In_rec_ii (λ x2 . λ x3 : ι → ι → ι . If_ii (prim3 x2 ∈ x2) (x1 (prim3 x2) (x3 (prim3 x2))) x0)
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Known xm^xm : ∀ x0 : ο . or x0 (not x0)
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known If_ii_0^If_ii_0 : ∀ x0 : ο . ∀ x1 x2 : ι → ι . not x0 ⟶ If_ii x0 x1 x2 = x2
Theorem fe983.. : ∀ x0 : ι → ι . ∀ x1 : ι → (ι → ι) → ι → ι . ∀ x2 . ∀ x3 x4 : ι → ι → ι . (∀ x5 . x5 ∈ x2 ⟶ x3 x5 = x4 x5) ⟶ If_ii (prim3 x2 ∈ x2) (x1 (prim3 x2) (x3 (prim3 x2))) x0 = If_ii (prim3 x2 ∈ x2) (x1 (prim3 x2) (x4 (prim3 x2))) x0 (proof)
Known In_rec_ii_eq^In_rec_ii_eq : ∀ x0 : ι → (ι → ι → ι) → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_ii x0 x1 = x0 x1 (In_rec_ii x0)
Known EmptyE^EmptyE : ∀ x0 . nIn x0 0
Theorem 496a9.. : ∀ x0 : ι → ι . ∀ x1 : ι → (ι → ι) → ι → ι . nat_primrec_ii x0 x1 0 = x0 (proof)
Param nat_p^nat_p : ι → ο
Param ordsucc^ordsucc : ι → ι
Known Union_ordsucc_eq^{Union_ordsucc_eq} : ∀ x0 . nat_p x0 ⟶ prim3 (ordsucc x0) = x0
Known If_ii_1^If_ii_1 : ∀ x0 : ο . ∀ x1 x2 : ι → ι . x0 ⟶ If_ii x0 x1 x2 = x1
Known ordsuccI2^ordsuccI2 : ∀ x0 . x0 ∈ ordsucc x0
Theorem 8092f.. : ∀ x0 : ι → ι . ∀ x1 : ι → (ι → ι) → ι → ι . ∀ x2 . nat_p x2 ⟶ nat_primrec_ii x0 x1 (ordsucc x2) = x1 x2 (nat_primrec_ii x0 x1 x2) (proof)
Param In_rec_iii^In_rec_iii : (ι → (ι → ι → ι → ι) → ι → ι → ι) → ι → ι → ι → ι
Param If_iii^If_iii : ο → (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι
Definition nat_primrec_iii := λ x0 : ι → ι → ι . λ x1 : ι → (ι → ι → ι) → ι → ι → ι . In_rec_iii (λ x2 . λ x3 : ι → ι → ι → ι . If_iii (prim3 x2 ∈ x2) (x1 (prim3 x2) (x3 (prim3 x2))) x0)
Known If_iii_0^If_iii_0 : ∀ x0 : ο . ∀ x1 x2 : ι → ι → ι . not x0 ⟶ If_iii x0 x1 x2 = x2
Theorem 3d3bd.. : ∀ x0 : ι → ι → ι . ∀ x1 : ι → (ι → ι → ι) → ι → ι → ι . ∀ x2 . ∀ x3 x4 : ι → ι → ι → ι . (∀ x5 . x5 ∈ x2 ⟶ x3 x5 = x4 x5) ⟶ If_iii (prim3 x2 ∈ x2) (x1 (prim3 x2) (x3 (prim3 x2))) x0 = If_iii (prim3 x2 ∈ x2) (x1 (prim3 x2) (x4 (prim3 x2))) x0 (proof)
Known In_rec_iii_eq^{In_rec_iii_eq} : ∀ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ι . (∀ x4 . x4 ∈ x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_iii x0 x1 = x0 x1 (In_rec_iii x0)
Theorem c3d57.. : ∀ x0 : ι → ι → ι . ∀ x1 : ι → (ι → ι → ι) → ι → ι → ι . nat_primrec_iii x0 x1 0 = x0 (proof)
Known If_iii_1^If_iii_1 : ∀ x0 : ο . ∀ x1 x2 : ι → ι → ι . x0 ⟶ If_iii x0 x1 x2 = x1
Theorem 50acb.. : ∀ x0 : ι → ι → ι . ∀ x1 : ι → (ι → ι → ι) → ι → ι → ι . ∀ x2 . nat_p x2 ⟶ nat_primrec_iii x0 x1 (ordsucc x2) = x1 x2 (nat_primrec_iii x0 x1 x2) (proof)
Known nat_ind^nat_ind : ∀ x0 : ι → ο . x0 0 ⟶ (∀ x1 . nat_p x1 ⟶ x0 x1 ⟶ x0 (ordsucc x1)) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1
Theorem a0d40.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ (∀ x2 . nat_p x2 ⟶ x1 (ordsucc x2)) ⟶ x1 x0 (proof)
Param omega^omega : ι
Known omega_nat_p^omega_nat_p : ∀ x0 . x0 ∈ omega ⟶ nat_p x0
Known nat_p_omega^nat_p_omega : ∀ x0 . nat_p x0 ⟶ x0 ∈ omega
Theorem b767b.. : ∀ x0 : ι → ο . x0 0 ⟶ (∀ x1 . x1 ∈ omega ⟶ x0 x1 ⟶ x0 (ordsucc x1)) ⟶ ∀ x1 . x1 ∈ omega ⟶ x0 x1 (proof)
Theorem 3c0c7.. : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 : ι → ο . x1 0 ⟶ (∀ x2 . x2 ∈ omega ⟶ x1 (ordsucc x2)) ⟶ x1 x0 (proof)
Param lam^Sigma : ι → (ι → ι) → ι
Param If_i^If_i : ο → ι → ι → ι
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known lamE2^lamE2 : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . and (x4 ∈ x0) (∀ x5 : ο . (∀ x6 . and (x6 ∈ x1 x4) (x2 = lam 2 (λ x8 . If_i (x8 = 0) x4 x6)) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3
Theorem f0163.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ lam x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x1 x4 ⟶ x2 = lam 2 (λ x7 . If_i (x7 = 0) x4 x5) ⟶ x3) ⟶ x3 (proof)
Param ap^ap : ι → ι → ι
Known ap_const_0^ap_const_0 : ∀ x0 . ap 0 x0 = 0
Theorem a3ed9.. : ∀ x0 x1 x2 . ap x0 x1 = x2 ⟶ (x2 = 0 ⟶ ∀ x3 : ο . x3) ⟶ x0 = 0 ⟶ ∀ x3 : ο . x3 (proof)
Known nat_0^nat_0 : nat_p 0
Theorem e4648.. : 0 ∈ omega (proof)
Known omega_ordsucc^{omega_ordsucc} : ∀ x0 . x0 ∈ omega ⟶ ordsucc x0 ∈ omega
Theorem fded7.. : 1 ∈ omega (proof)
Theorem 74a82.. : 2 ∈ omega (proof)
Theorem 973f5.. : 3 ∈ omega (proof)
Theorem a590d.. : 4 ∈ omega (proof)
Theorem 1cf06.. : 5 ∈ omega (proof)
Theorem bacd6.. : 6 ∈ omega (proof)
Theorem 1328b.. : 7 ∈ omega (proof)
Theorem 315a5.. : 8 ∈ omega (proof)
Theorem ee345.. : 9 ∈ omega (proof)
Param nat_primrec^nat_primrec : ι → (ι → ι → ι) → ι → ι
Definition 4ec03.. := λ x0 x1 . lam omega (nat_primrec x0 (λ x2 x3 . ap x1 x2))
Known beta^beta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ap (lam x0 x1) x2 = x1 x2
Known nat_primrec_0^{nat_primrec_0} : ∀ x0 . ∀ x1 : ι → ι → ι . nat_primrec x0 x1 0 = x0
Theorem 46adb.. : ∀ x0 x1 . ap (4ec03.. x0 x1) 0 = x0 (proof)
Known nat_primrec_S^{nat_primrec_S} : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . nat_p x2 ⟶ nat_primrec x0 x1 (ordsucc x2) = x1 x2 (nat_primrec x0 x1 x2)
Theorem 5bda7.. : ∀ x0 x1 x2 . x2 ∈ omega ⟶ ap (4ec03.. x0 x1) (ordsucc x2) = ap x1 x2 (proof)
Theorem cc413.. : ∀ x0 x1 x2 x3 . x3 ∈ omega ⟶ ap x1 x3 = x2 ⟶ ap (4ec03.. x0 x1) (ordsucc x3) = x2 (proof)
Definition 84af2.. := λ x0 . x0 = lam omega (ap x0)
Known encode_u_ext^encode_u_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ lam x0 x1 = lam x0 x2
Theorem 70867.. : ∀ x0 x1 . 84af2.. (4ec03.. x0 x1) (proof)
Known tuple_2_Sigma^{tuple_2_Sigma} : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x1 x2 ⟶ lam 2 (λ x4 . If_i (x4 = 0) x2 x3) ∈ lam x0 x1
Theorem aee79.. : ∀ x0 . 84af2.. x0 ⟶ ∀ x1 . x1 ∈ omega ⟶ ∀ x2 . x2 ∈ ap x0 x1 ⟶ lam 2 (λ x3 . If_i (x3 = 0) x1 x2) ∈ x0 (proof)
Theorem 3a762.. : ∀ x0 x1 x2 . x2 ∈ omega ⟶ ∀ x3 . x3 ∈ ap (4ec03.. x0 x1) x2 ⟶ lam 2 (λ x4 . If_i (x4 = 0) x2 x3) ∈ 4ec03.. x0 x1 (proof)
Theorem e0bc1.. : ∀ x0 . 84af2.. x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 : ο . (∀ x3 . x3 ∈ omega ⟶ ∀ x4 . x4 ∈ ap x0 x3 ⟶ x1 = lam 2 (λ x6 . If_i (x6 = 0) x3 x4) ⟶ x2) ⟶ x2 (proof)
Theorem d9636.. : ∀ x0 x1 x2 . x2 ∈ 4ec03.. x0 x1 ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ omega ⟶ ∀ x5 . x5 ∈ ap (4ec03.. x0 x1) x4 ⟶ x2 = lam 2 (λ x7 . If_i (x7 = 0) x4 x5) ⟶ x3) ⟶ x3 (proof)
Theorem 89569.. : ∀ x0 x1 x2 x3 . 4ec03.. x0 x1 = 4ec03.. x2 x3 ⟶ x0 = x2 (proof)
Theorem 4bd46.. : ∀ x0 x1 x2 x3 . 4ec03.. x0 x1 = 4ec03.. x2 x3 ⟶ lam omega (ap x1) = lam omega (ap x3) (proof)
Theorem 9adfe.. : ∀ x0 x1 x2 x3 . 84af2.. x1 ⟶ 84af2.. x3 ⟶ 4ec03.. x0 x1 = 4ec03.. x2 x3 ⟶ x1 = x3 (proof)
Known tuple_2_eta^tuple_2_eta : ∀ x0 x1 . lam 2 (ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1))) = lam 2 (λ x3 . If_i (x3 = 0) x0 x1)
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Known set_ext^set_ext : ∀ x0 x1 . x0 ⊆ x1 ⟶ x1 ⊆ x0 ⟶ x0 = x1
Known cases_2^cases_2 : ∀ x0 . x0 ∈ 2 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 x0
Known tuple_2_0_eq^tuple_2_0_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 0 = x0
Known tuple_2_1_eq^tuple_2_1_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 1 = x1
Known In_0_2^In_0_2 : 0 ∈ 2
Known In_1_2^In_1_2 : 1 ∈ 2
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Theorem 2b117.. : ∀ x0 x1 . lam 2 (λ x3 . If_i (x3 = 0) x0 x1) = 4ec03.. x0 (4ec03.. x1 0) (proof)
Known tuple_3_eta^tuple_3_eta : ∀ x0 x1 x2 . lam 3 (ap (lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2)))) = lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2))
Known cases_3^cases_3 : ∀ x0 . x0 ∈ 3 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 x0
Known tuple_3_0_eq^tuple_3_0_eq : ∀ x0 x1 x2 . ap (lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2))) 0 = x0
Known tuple_3_1_eq^tuple_3_1_eq : ∀ x0 x1 x2 . ap (lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2))) 1 = x1
Known tuple_3_2_eq^tuple_3_2_eq : ∀ x0 x1 x2 . ap (lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2))) 2 = x2
Known In_0_3^In_0_3 : 0 ∈ 3
Known In_1_3^In_1_3 : 1 ∈ 3
Known In_2_3^In_2_3 : 2 ∈ 3
Theorem ed696.. : ∀ x0 x1 x2 . lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2)) = 4ec03.. x0 (4ec03.. x1 (4ec03.. x2 0)) (proof)
Known tuple_4_eta^tuple_4_eta : ∀ x0 x1 x2 x3 . lam 4 (ap (lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3))))) = lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3)))
Known cases_4^cases_4 : ∀ x0 . x0 ∈ 4 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 2 ⟶ x1 3 ⟶ x1 x0
Known tuple_4_0_eq^tuple_4_0_eq : ∀ x0 x1 x2 x3 . ap (lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3)))) 0 = x0
Known tuple_4_1_eq^tuple_4_1_eq : ∀ x0 x1 x2 x3 . ap (lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3)))) 1 = x1
Known tuple_4_2_eq^tuple_4_2_eq : ∀ x0 x1 x2 x3 . ap (lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3)))) 2 = x2
Known tuple_4_3_eq^tuple_4_3_eq : ∀ x0 x1 x2 x3 . ap (lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3)))) 3 = x3
Known In_0_4^In_0_4 : 0 ∈ 4
Known In_1_4^In_1_4 : 1 ∈ 4
Known In_2_4^In_2_4 : 2 ∈ 4
Known In_3_4^In_3_4 : 3 ∈ 4
Theorem a1414.. : ∀ x0 x1 x2 x3 . lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3))) = 4ec03.. x0 (4ec03.. x1 (4ec03.. x2 (4ec03.. x3 0))) (proof)
Definition stream_rest := λ x0 . lam omega (λ x1 . ap x0 (ordsucc x1))
Theorem ed853.. : ∀ x0 . 84af2.. (stream_rest x0) (proof)
Theorem 64afd.. : ∀ x0 x1 . 84af2.. x1 ⟶ stream_rest (4ec03.. x0 x1) = x1 (proof)
Definition b38a5.. := λ x0 x1 x2 . nat_primrec_ii (λ x3 . x2) (λ x3 . λ x4 : ι → ι . λ x5 . 4ec03.. (ap x5 0) (x4 (stream_rest x5))) x0 x1
Theorem d959a.. : ∀ x0 x1 . b38a5.. 0 x0 x1 = x1 (proof)
Theorem 8242e.. : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 x2 . b38a5.. (ordsucc x0) x1 x2 = 4ec03.. (ap x1 0) (b38a5.. x0 (stream_rest x1) x2) (proof)
Definition df9be.. := nat_primrec_iii (λ x0 x1 . 0) (λ x0 . λ x1 : ι → ι → ι . λ x2 x3 . b38a5.. (ap x2 0) (ap x3 0) (x1 (stream_rest x2) (stream_rest x3)))
Theorem 87bb6.. : ∀ x0 x1 . df9be.. 0 x0 x1 = 0 (proof)
Theorem 1f5be.. : ∀ x0 . x0 ∈ omega ⟶ ∀ x1 x2 . df9be.. (ordsucc x0) x1 x2 = b38a5.. (ap x1 0) (ap x2 0) (df9be.. x0 (stream_rest x1) (stream_rest x2)) (proof)