Proofgold Address

Definition c3e2e.. := λ x0 x1 . λ x2 : ι → ι . λ x3 . λ x4 : ι → ι → ι . λ x5 x6 . ∀ x7 : ι → ι → ο . x7 x1 x3 ⟶ (∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x7 x8 x9 ⟶ x7 (x2 x8) (x4 x8 x9)) ⟶ x7 x5 x6
Param explicit_Nats^{explicit_Nats} : ι → ι → (ι → ι) → ο
Known explicit_Nats_ind^{explicit_Nats_ind} : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x3 : ι → ο . x3 x1 ⟶ (∀ x4 . x4 ∈ x0 ⟶ x3 x4 ⟶ x3 (x2 x4)) ⟶ ∀ x4 . x4 ∈ x0 ⟶ x3 x4
Theorem e9411.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 . ∀ x4 : ι → ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 : ο . (∀ x7 . c3e2e.. x0 x1 x2 x3 x4 x5 x7 ⟶ x6) ⟶ x6 (proof)
Known explicit_Nats_E^{explicit_Nats_E} : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ο . (explicit_Nats x0 x1 x2 ⟶ x1 ∈ x0 ⟶ (∀ x4 . x4 ∈ x0 ⟶ x2 x4 ∈ x0) ⟶ (∀ x4 . x4 ∈ x0 ⟶ x2 x4 = x1 ⟶ ∀ x5 : ο . x5) ⟶ (∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ x2 x4 = x2 x5 ⟶ x4 = x5) ⟶ (∀ x4 : ι → ο . x4 x1 ⟶ (∀ x5 . x4 x5 ⟶ x4 (x2 x5)) ⟶ ∀ x5 . x5 ∈ x0 ⟶ x4 x5) ⟶ x3) ⟶ explicit_Nats x0 x1 x2 ⟶ x3
Definition False^False := ∀ x0 : ο . x0
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Theorem 451aa.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 . ∀ x4 : ι → ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x5 . c3e2e.. x0 x1 x2 x3 x4 x1 x5 ⟶ x5 = x3 (proof)
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem 19ff6.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 . ∀ x4 : ι → ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . c3e2e.. x0 x1 x2 x3 x4 (x2 x5) x6 ⟶ ∀ x7 : ο . (∀ x8 . and (x6 = x4 x5 x8) (c3e2e.. x0 x1 x2 x3 x4 x5 x8) ⟶ x7) ⟶ x7 (proof)
Theorem 766cf.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 . ∀ x4 : ι → ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 x7 . c3e2e.. x0 x1 x2 x3 x4 x5 x6 ⟶ c3e2e.. x0 x1 x2 x3 x4 x5 x7 ⟶ x6 = x7 (proof)
Definition explicit_Nats_primrec^{explicit_Nats_primrec} := λ x0 x1 . λ x2 : ι → ι . λ x3 . λ x4 : ι → ι → ι . λ x5 . prim0 (c3e2e.. x0 x1 x2 x3 x4 x5)
Known Eps_i_ex^Eps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (prim0 x0)
Theorem 31431.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 . ∀ x4 : ι → ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x5 . x5 ∈ x0 ⟶ c3e2e.. x0 x1 x2 x3 x4 x5 (explicit_Nats_primrec x0 x1 x2 x3 x4 x5) (proof)
Theorem explicit_Nats_primrec_base^{explicit_Nats_primrec_base} : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 . ∀ x4 : ι → ι → ι . explicit_Nats x0 x1 x2 ⟶ explicit_Nats_primrec x0 x1 x2 x3 x4 x1 = x3 (proof)
Theorem explicit_Nats_primrec_S^{explicit_Nats_primrec_S} : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 . ∀ x4 : ι → ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x5 . x5 ∈ x0 ⟶ explicit_Nats_primrec x0 x1 x2 x3 x4 (x2 x5) = x4 x5 (explicit_Nats_primrec x0 x1 x2 x3 x4 x5) (proof)
Definition explicit_Nats_zero_plus^{explicit_Nats_zero_plus} := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 . explicit_Nats_primrec x0 x1 x2 x4 (λ x5 . x2) x3
Definition explicit_Nats_zero_mult^{explicit_Nats_zero_mult} := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 . explicit_Nats_primrec x0 x1 x2 x1 (λ x5 . explicit_Nats_zero_plus x0 x1 x2 x4) x3
Theorem explicit_Nats_zero_plus_0L^{explicit_Nats_zero_plus_0L} : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x3 . x3 ∈ x0 ⟶ explicit_Nats_zero_plus x0 x1 x2 x1 x3 = x3 (proof)
Theorem explicit_Nats_zero_plus_SL^{explicit_Nats_zero_plus_SL} : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ explicit_Nats_zero_plus x0 x1 x2 (x2 x3) x4 = x2 (explicit_Nats_zero_plus x0 x1 x2 x3 x4) (proof)
Theorem explicit_Nats_zero_mult_0L^{explicit_Nats_zero_mult_0L} : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x3 . x3 ∈ x0 ⟶ explicit_Nats_zero_mult x0 x1 x2 x1 x3 = x1 (proof)
Theorem explicit_Nats_zero_mult_SL^{explicit_Nats_zero_mult_SL} : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ explicit_Nats_zero_mult x0 x1 x2 (x2 x3) x4 = explicit_Nats_zero_plus x0 x1 x2 x4 (explicit_Nats_zero_mult x0 x1 x2 x3 x4) (proof)
Definition explicit_Nats_one_plus^{explicit_Nats_one_plus} := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 . explicit_Nats_primrec x0 x1 x2 (x2 x4) (λ x5 . x2) x3
Definition explicit_Nats_one_mult^{explicit_Nats_one_mult} := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 . explicit_Nats_primrec x0 x1 x2 x4 (λ x5 . explicit_Nats_one_plus x0 x1 x2 x4) x3
Definition explicit_Nats_one_exp^{explicit_Nats_one_exp} := λ x0 x1 . λ x2 : ι → ι . λ x3 . explicit_Nats_primrec x0 x1 x2 x3 (λ x4 . explicit_Nats_one_mult x0 x1 x2 x3)
Theorem explicit_Nats_one_plus_1L^{explicit_Nats_one_plus_1L} : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x3 . x3 ∈ x0 ⟶ explicit_Nats_one_plus x0 x1 x2 x1 x3 = x2 x3 (proof)
Theorem explicit_Nats_one_plus_SL^{explicit_Nats_one_plus_SL} : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ explicit_Nats_one_plus x0 x1 x2 (x2 x3) x4 = x2 (explicit_Nats_one_plus x0 x1 x2 x3 x4) (proof)
Theorem explicit_Nats_one_mult_1L^{explicit_Nats_one_mult_1L} : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x3 . x3 ∈ x0 ⟶ explicit_Nats_one_mult x0 x1 x2 x1 x3 = x3 (proof)
Theorem explicit_Nats_one_mult_SL^{explicit_Nats_one_mult_SL} : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ explicit_Nats_one_mult x0 x1 x2 (x2 x3) x4 = explicit_Nats_one_plus x0 x1 x2 x4 (explicit_Nats_one_mult x0 x1 x2 x3 x4) (proof)
Theorem explicit_Nats_one_exp_1L^{explicit_Nats_one_exp_1L} : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x3 . x3 ∈ x0 ⟶ explicit_Nats_one_exp x0 x1 x2 x3 x1 = x3 (proof)
Theorem explicit_Nats_one_exp_SL^{explicit_Nats_one_exp_SL} : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ explicit_Nats_one_exp x0 x1 x2 x3 (x2 x4) = explicit_Nats_one_mult x0 x1 x2 x3 (explicit_Nats_one_exp x0 x1 x2 x3 x4) (proof)