Proofgold Address

Definition a813b.. := λ x0 x1 . λ x2 : ι → ι . λ x3 . λ x4 : ι → ι → ι . λ x5 x6 . ∀ x7 : ι → ι → ο . x7 x1 x3 ⟶ (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . x7 x8 x9 ⟶ x7 (x2 x8) (x4 x8 x9)) ⟶ x7 x5 x6
Param explicit_Nats : ι → ι → (ι → ι) → ο
Known explicit_Nats_ind : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x3 : ι → ο . x3 x1 ⟶ (∀ x4 . prim1 x4 x0 ⟶ x3 x4 ⟶ x3 (x2 x4)) ⟶ ∀ x4 . prim1 x4 x0 ⟶ x3 x4
Theorem 89666.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 . ∀ x4 : ι → ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 : ο . (∀ x7 . a813b.. x0 x1 x2 x3 x4 x5 x7 ⟶ x6) ⟶ x6 (proof)
Known explicit_Nats_E : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ο . (explicit_Nats x0 x1 x2 ⟶ prim1 x1 x0 ⟶ (∀ x4 . prim1 x4 x0 ⟶ prim1 (x2 x4) x0) ⟶ (∀ x4 . prim1 x4 x0 ⟶ x2 x4 = x1 ⟶ ∀ x5 : ο . x5) ⟶ (∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x2 x4 = x2 x5 ⟶ x4 = x5) ⟶ (∀ x4 : ι → ο . x4 x1 ⟶ (∀ x5 . x4 x5 ⟶ x4 (x2 x5)) ⟶ ∀ x5 . prim1 x5 x0 ⟶ x4 x5) ⟶ x3) ⟶ explicit_Nats x0 x1 x2 ⟶ x3
Definition False := ∀ x0 : ο . x0
Known FalseE : False ⟶ ∀ x0 : ο . x0
Theorem 45784.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 . ∀ x4 : ι → ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x5 . a813b.. x0 x1 x2 x3 x4 x1 x5 ⟶ x5 = x3 (proof)
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem 0bfdd.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 . ∀ x4 : ι → ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . a813b.. x0 x1 x2 x3 x4 (x2 x5) x6 ⟶ ∀ x7 : ο . (∀ x8 . and (x6 = x4 x5 x8) (a813b.. x0 x1 x2 x3 x4 x5 x8) ⟶ x7) ⟶ x7 (proof)
Theorem f1675.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 . ∀ x4 : ι → ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 x7 . a813b.. x0 x1 x2 x3 x4 x5 x6 ⟶ a813b.. x0 x1 x2 x3 x4 x5 x7 ⟶ x6 = x7 (proof)
Definition explicit_Nats_primrec := λ x0 x1 . λ x2 : ι → ι . λ x3 . λ x4 : ι → ι → ι . λ x5 . prim0 (a813b.. x0 x1 x2 x3 x4 x5)
Theorem 89666.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 . ∀ x4 : ι → ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 : ο . (∀ x7 . a813b.. x0 x1 x2 x3 x4 x5 x7 ⟶ x6) ⟶ x6 (proof)
Known Eps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (prim0 x0)
Theorem 1347b.. : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 . ∀ x4 : ι → ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x5 . prim1 x5 x0 ⟶ a813b.. x0 x1 x2 x3 x4 x5 (explicit_Nats_primrec x0 x1 x2 x3 x4 x5) (proof)
Theorem 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 : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 . ∀ x4 : ι → ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x5 . prim1 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 := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 . explicit_Nats_primrec x0 x1 x2 x4 (λ x5 . x2) x3
Definition 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 : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x3 . prim1 x3 x0 ⟶ explicit_Nats_zero_plus x0 x1 x2 x1 x3 = x3 (proof)
Theorem explicit_Nats_zero_plus_SL : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 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 : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x3 . prim1 x3 x0 ⟶ explicit_Nats_zero_mult x0 x1 x2 x1 x3 = x1 (proof)
Theorem explicit_Nats_zero_mult_SL : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 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 := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 . explicit_Nats_primrec x0 x1 x2 (x2 x4) (λ x5 . x2) x3
Definition 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 := λ 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 : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x3 . prim1 x3 x0 ⟶ explicit_Nats_one_plus x0 x1 x2 x1 x3 = x2 x3 (proof)
Theorem explicit_Nats_one_plus_SL : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 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 : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x3 . prim1 x3 x0 ⟶ explicit_Nats_one_mult x0 x1 x2 x1 x3 = x3 (proof)
Theorem explicit_Nats_one_mult_SL : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 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 : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x3 . prim1 x3 x0 ⟶ explicit_Nats_one_exp x0 x1 x2 x3 x1 = x3 (proof)
Theorem explicit_Nats_one_exp_SL : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2 ⟶ ∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 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)