Proofgold Address

Param nat_p^nat_p : ι → ο
Param add_nat^add_nat : ι → ι → ι
Param ordsucc^ordsucc : ι → ι
Known nat_ind^nat_ind : ∀ x0 : ι → ο . x0 0 ⟶ (∀ x1 . nat_p x1 ⟶ x0 x1 ⟶ x0 (ordsucc x1)) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1
Known add_nat_0R^add_nat_0R : ∀ x0 . add_nat x0 0 = x0
Known add_nat_SR^add_nat_SR : ∀ x0 x1 . nat_p x1 ⟶ add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known nat_ordsucc_in_ordsucc^{nat_ordsucc_in_ordsucc} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ordsucc x1 ∈ ordsucc x0
Known add_nat_p^add_nat_p : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (add_nat x0 x1)
Theorem 85b3a..^add_nat_In_R : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . nat_p x2 ⟶ add_nat x1 x2 ∈ add_nat x0 x2 (proof)
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Param ordinal^ordinal : ι → ο
Known ordinal_trichotomy_or_impred^{ordinal_trichotomy_or_impred} : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x2 : ο . (x0 ∈ x1 ⟶ x2) ⟶ (x0 = x1 ⟶ x2) ⟶ (x1 ∈ x0 ⟶ x2) ⟶ x2
Known nat_p_ordinal^{nat_p_ordinal} : ∀ x0 . nat_p x0 ⟶ ordinal x0
Known nat_trans^nat_trans : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ x1 ⊆ x0
Known Subq_ref^Subq_ref : ∀ x0 . x0 ⊆ x0
Definition False^False := ∀ x0 : ο . x0
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known In_irref^In_irref : ∀ x0 . nIn x0 x0
Theorem 116d8.. : ∀ x0 x1 . nat_p x0 ⟶ nat_p x1 ⟶ x0 ⊆ x1 ⟶ ∀ x2 . nat_p x2 ⟶ add_nat x0 x2 ⊆ add_nat x1 x2 (proof)
Known add_nat_com^add_nat_com : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ add_nat x0 x1 = add_nat x1 x0
Theorem abb9e.. : ∀ x0 x1 . nat_p x0 ⟶ nat_p x1 ⟶ x0 ⊆ x1 ⟶ ∀ x2 . nat_p x2 ⟶ add_nat x2 x0 ⊆ add_nat x2 x1 (proof)
Param mul_nat^mul_nat : ι → ι → ι
Known mul_nat_0R^mul_nat_0R : ∀ x0 . mul_nat x0 0 = 0
Known mul_nat_SR^mul_nat_SR : ∀ x0 x1 . nat_p x1 ⟶ mul_nat x0 (ordsucc x1) = add_nat x0 (mul_nat x0 x1)
Known Subq_tra^Subq_tra : ∀ x0 x1 x2 . x0 ⊆ x1 ⟶ x1 ⊆ x2 ⟶ x0 ⊆ x2
Known mul_nat_p^mul_nat_p : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (mul_nat x0 x1)
Theorem 4324d..^{mul_nat_Subq_R} : ∀ x0 x1 . nat_p x0 ⟶ nat_p x1 ⟶ x0 ⊆ x1 ⟶ ∀ x2 . nat_p x2 ⟶ mul_nat x0 x2 ⊆ mul_nat x1 x2 (proof)
Param nat_primrec^nat_primrec : ι → (ι → ι → ι) → ι → ι
Definition Sigma_nat := λ x0 . λ x1 : ι → ι . nat_primrec 0 (λ x2 x3 . add_nat x3 (x1 x2)) x0
Known nat_primrec_0^{nat_primrec_0} : ∀ x0 . ∀ x1 : ι → ι → ι . nat_primrec x0 x1 0 = x0
Theorem bbccf.. : ∀ x0 : ι → ι . Sigma_nat 0 x0 = 0 (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 492bc.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 : ι → ι . Sigma_nat (ordsucc x0) x1 = add_nat (Sigma_nat x0 x1) (x1 x0) (proof)
Known nat_0^nat_0 : nat_p 0
Known ordsuccI1^ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
Known ordsuccI2^ordsuccI2 : ∀ x0 . x0 ∈ ordsucc x0
Theorem 330aa.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ nat_p (x1 x2)) ⟶ nat_p (Sigma_nat x0 x1) (proof)
Definition exp_nat^exp_nat := λ x0 . nat_primrec 1 (λ x1 . mul_nat x0)
Known In_0_1^In_0_1 : 0 ∈ 1
Known mul_nat_SL^mul_nat_SL : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ mul_nat (ordsucc x0) x1 = add_nat (mul_nat x0 x1) x1
Known 4f402..^exp_nat_p : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (exp_nat x0 x1)
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known ordsuccE^ordsuccE : ∀ x0 x1 . x1 ∈ ordsucc x0 ⟶ or (x1 ∈ x0) (x1 = x0)
Known nat_p_trans^nat_p_trans : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ nat_p x1
Known nat_ordsucc^nat_ordsucc : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc x0)
Theorem 45039.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x1 ⟶ x2 x3 ∈ ordsucc x0) ⟶ Sigma_nat x1 (λ x3 . mul_nat (x2 x3) (exp_nat (ordsucc x0) x3)) ∈ exp_nat (ordsucc x0) x1 (proof)
Known nat_1^nat_1 : nat_p 1
Theorem bdfcb.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ 2) ⟶ Sigma_nat x0 (λ x2 . mul_nat (x1 x2) (exp_nat 2 x2)) ∈ exp_nat 2 x0 (proof)
Theorem 7a596.. : add_nat 32 1 = 33 (proof)
Theorem ef922.. : add_nat 32 2 = 34 (proof)
Known nat_2^nat_2 : nat_p 2
Theorem e6aba.. : add_nat 32 3 = 35 (proof)
Known nat_3^nat_3 : nat_p 3
Theorem 4470a.. : add_nat 32 4 = 36 (proof)
Known nat_4^nat_4 : nat_p 4
Theorem 834ba.. : add_nat 32 5 = 37 (proof)
Known nat_5^nat_5 : nat_p 5
Theorem 777a2.. : add_nat 32 6 = 38 (proof)
Known nat_6^nat_6 : nat_p 6
Theorem 15f5b.. : add_nat 32 7 = 39 (proof)
Known nat_7^nat_7 : nat_p 7
Theorem 8b5c1.. : add_nat 32 8 = 40 (proof)
Known nat_8^nat_8 : nat_p 8
Theorem c828e.. : add_nat 32 9 = 41 (proof)
Param ap^ap : ι → ι → ι
Param lam^Sigma : ι → (ι → ι) → ι
Param If_i^If_i : ο → ι → ι → ι
Known tuple_6_5_eq^tuple_6_5_eq : ∀ x0 x1 x2 x3 x4 x5 . ap (lam 6 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 (If_i (x7 = 3) x3 (If_i (x7 = 4) x4 x5)))))) 5 = x5
Known f11bb.. : ∀ x0 . nat_p x0 ⟶ mul_nat 1 x0 = x0
Known tuple_6_4_eq^tuple_6_4_eq : ∀ x0 x1 x2 x3 x4 x5 . ap (lam 6 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 (If_i (x7 = 3) x3 (If_i (x7 = 4) x4 x5)))))) 4 = x4
Known mul_nat_0L^mul_nat_0L : ∀ x0 . nat_p x0 ⟶ mul_nat 0 x0 = 0
Known tuple_6_3_eq^tuple_6_3_eq : ∀ x0 x1 x2 x3 x4 x5 . ap (lam 6 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 (If_i (x7 = 3) x3 (If_i (x7 = 4) x4 x5)))))) 3 = x3
Known tuple_6_2_eq^tuple_6_2_eq : ∀ x0 x1 x2 x3 x4 x5 . ap (lam 6 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 (If_i (x7 = 3) x3 (If_i (x7 = 4) x4 x5)))))) 2 = x2
Known tuple_6_1_eq^tuple_6_1_eq : ∀ x0 x1 x2 x3 x4 x5 . ap (lam 6 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 (If_i (x7 = 3) x3 (If_i (x7 = 4) x4 x5)))))) 1 = x1
Known tuple_6_0_eq^tuple_6_0_eq : ∀ x0 x1 x2 x3 x4 x5 . ap (lam 6 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 (If_i (x7 = 3) x3 (If_i (x7 = 4) x4 x5)))))) 0 = x0
Known adab1.. : exp_nat 2 3 = 8
Known e089c.. : exp_nat 2 5 = 32
Known add_nat_0L^add_nat_0L : ∀ x0 . nat_p x0 ⟶ add_nat 0 x0 = x0
Known 9dea5.. : add_nat 8 1 = 9
Known nat_9^nat_9 : nat_p 9
Known 1f846.. : nat_p 32
Theorem 0c734.. : Sigma_nat 6 (λ x1 . mul_nat (ap (lam 6 (λ x2 . If_i (x2 = 0) 1 (If_i (x2 = 1) 0 (If_i (x2 = 2) 0 (If_i (x2 = 3) 1 (If_i (x2 = 4) 0 1)))))) x1) (exp_nat 2 x1)) = 41 (proof)