Proofgold Asset

Param nat_p^nat_p : ι → ο
Param ordsucc^ordsucc : ι → ι
Known nat_ordsucc^nat_ordsucc : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc x0)
Known nat_12^nat_12 : nat_p 12
Theorem nat_13^nat_13 : nat_p 13 (proof)
Theorem nat_14^nat_14 : nat_p 14 (proof)
Theorem nat_15^nat_15 : nat_p 15 (proof)
Theorem nat_16^nat_16 : nat_p 16 (proof)
Theorem nat_17^nat_17 : nat_p 17 (proof)
Param add_nat^add_nat : ι → ι → ι
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 ordsuccI2^ordsuccI2 : ∀ x0 . x0 ∈ ordsucc x0
Known add_nat_SR^add_nat_SR : ∀ x0 x1 . nat_p x1 ⟶ add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Known ordsuccI1^ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
Theorem d8085.. : ∀ x0 x1 . nat_p x1 ⟶ x0 ∈ ordsucc (add_nat x0 x1) (proof)
Known nat_0^nat_0 : nat_p 0
Theorem b76af.. : add_nat 23 1 = 24 (proof)
Known nat_1^nat_1 : nat_p 1
Theorem 86ab5.. : add_nat 23 2 = 25 (proof)
Known nat_2^nat_2 : nat_p 2
Theorem da65f.. : add_nat 23 3 = 26 (proof)
Known nat_3^nat_3 : nat_p 3
Theorem 92918.. : add_nat 23 4 = 27 (proof)
Known nat_4^nat_4 : nat_p 4
Theorem 1505b.. : add_nat 23 5 = 28 (proof)
Known nat_5^nat_5 : nat_p 5
Theorem 9d5e3.. : add_nat 23 6 = 29 (proof)
Known nat_6^nat_6 : nat_p 6
Theorem a1411.. : add_nat 23 7 = 30 (proof)
Known nat_7^nat_7 : nat_p 7
Theorem 2e090.. : add_nat 23 8 = 31 (proof)
Known nat_8^nat_8 : nat_p 8
Theorem e4564.. : 23 ∈ 32 (proof)
Theorem 1f5db.. : add_nat 24 1 = 25 (proof)
Theorem e90e1.. : add_nat 24 2 = 26 (proof)
Theorem fe07b.. : add_nat 24 3 = 27 (proof)
Theorem de55b.. : add_nat 24 4 = 28 (proof)
Theorem 14e96.. : add_nat 24 5 = 29 (proof)
Theorem 2a2ab.. : add_nat 24 6 = 30 (proof)
Theorem 6ba1d.. : add_nat 24 7 = 31 (proof)
Theorem be3fd.. : 24 ∈ 32 (proof)