Proofgold Address

Param add_nat^add_nat : ι → ι → ι
Param ordsucc^ordsucc : ι → ι
Param nat_p^nat_p : ι → ο
Known add_nat_SR^add_nat_SR : ∀ x0 x1 . nat_p x1 ⟶ add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known nat_0^nat_0 : nat_p 0
Known add_nat_0R^add_nat_0R : ∀ x0 . add_nat x0 0 = x0
Theorem 893fe.. : add_nat 4 1 = 5 (proof)
Known nat_1^nat_1 : nat_p 1
Theorem f3bb6.. : add_nat 4 2 = 6 (proof)
Known nat_2^nat_2 : nat_p 2
Theorem 54790.. : add_nat 4 3 = 7 (proof)
Known nat_3^nat_3 : nat_p 3
Theorem 36602.. : add_nat 4 4 = 8 (proof)
Theorem 9dea5.. : add_nat 8 1 = 9 (proof)
Theorem 118d3.. : add_nat 8 2 = 10 (proof)
Theorem cd2cb.. : add_nat 8 3 = 11 (proof)
Theorem 69b67..^add_nat_8_4 : add_nat 8 4 = 12 (proof)
Known nat_4^nat_4 : nat_p 4
Theorem 5f9b2.. : add_nat 8 5 = 13 (proof)
Known nat_5^nat_5 : nat_p 5
Theorem 70d6d.. : add_nat 8 6 = 14 (proof)
Known nat_6^nat_6 : nat_p 6
Theorem e1175.. : add_nat 8 7 = 15 (proof)
Known nat_7^nat_7 : nat_p 7
Theorem 1521b.. : add_nat 8 8 = 16 (proof)
Theorem 4ff4f.. : add_nat 11 1 = 12 (proof)
Theorem cef3c.. : add_nat 11 2 = 13 (proof)
Theorem 336f0.. : add_nat 11 3 = 14 (proof)
Theorem 62dd3.. : add_nat 11 4 = 15 (proof)
Theorem 525d1.. : add_nat 11 5 = 16 (proof)
Theorem 91a85.. : add_nat 11 6 = 17 (proof)
Theorem a918d.. : add_nat 11 7 = 18 (proof)
Theorem 50bed.. : add_nat 11 8 = 19 (proof)
Known nat_8^nat_8 : nat_p 8
Theorem 45540.. : add_nat 11 9 = 20 (proof)
Known nat_9^nat_9 : nat_p 9
Theorem 2e174.. : add_nat 11 10 = 21 (proof)
Known nat_10^nat_10 : nat_p 10
Theorem d5f37.. : add_nat 11 11 = 22 (proof)
Known nat_11^nat_11 : nat_p 11
Theorem 90194.. : add_nat 11 12 = 23 (proof)
Param mul_nat^mul_nat : ι → ι → ι
Known add_nat_1_1_2^{add_nat_1_1_2} : add_nat 1 1 = 2
Known mul_add_nat_distrL^{mul_add_nat_distrL} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 . nat_p x2 ⟶ mul_nat x0 (add_nat x1 x2) = add_nat (mul_nat x0 x1) (mul_nat x0 x2)
Known mul_nat_1R^mul_nat_1R : ∀ x0 . mul_nat x0 1 = x0
Known 256ca.. : add_nat 2 2 = 4
Theorem c3da7.. : mul_nat 2 2 = 4 (proof)
Theorem 5712d.. : mul_nat 2 4 = 8 (proof)
Theorem af7b1.. : mul_nat 2 8 = 16 (proof)
Theorem a9609.. : add_nat 6 1 = 7 (proof)
Theorem a16a6.. : add_nat 6 2 = 8 (proof)
Theorem c3434.. : add_nat 6 3 = 9 (proof)
Theorem 2cf95.. : add_nat 6 4 = 10 (proof)
Theorem 3df8e.. : add_nat 16 1 = 17 (proof)
Theorem 019e3.. : add_nat 16 2 = 18 (proof)
Theorem dc79e.. : add_nat 16 3 = 19 (proof)
Theorem f956d.. : add_nat 16 4 = 20 (proof)
Theorem ba5ba.. : add_nat 16 5 = 21 (proof)
Theorem f5339.. : add_nat 16 6 = 22 (proof)
Theorem 07f4e.. : add_nat 16 7 = 23 (proof)
Theorem 816bd.. : add_nat 16 8 = 24 (proof)
Theorem a3f6a.. : add_nat 16 9 = 25 (proof)
Theorem d085c.. : add_nat 16 10 = 26 (proof)
Theorem fa3b7.. : add_nat 16 11 = 27 (proof)
Theorem fbe6e.. : add_nat 16 12 = 28 (proof)
Known nat_12^nat_12 : nat_p 12
Theorem 22701.. : add_nat 16 13 = 29 (proof)
Param nat_primrec^nat_primrec : ι → (ι → ι → ι) → ι → ι
Definition exp_nat^exp_nat := λ x0 . nat_primrec 1 (λ x1 . mul_nat x0)
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)
Known nat_primrec_0^{nat_primrec_0} : ∀ x0 . ∀ x1 : ι → ι → ι . nat_primrec x0 x1 0 = x0
Theorem 3e9f7..^exp_nat_1 : ∀ x0 . exp_nat x0 1 = x0 (proof)
Theorem a8f07.. : exp_nat 2 2 = 4 (proof)
Known nat_ind^nat_ind : ∀ x0 : ι → ο . x0 0 ⟶ (∀ x1 . nat_p x1 ⟶ x0 x1 ⟶ x0 (ordsucc x1)) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1
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 EmptyE^EmptyE : ∀ x0 . nIn x0 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 add_nat_SL^add_nat_SL : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ add_nat (ordsucc x0) x1 = ordsucc (add_nat x0 x1)
Known mul_nat_p^mul_nat_p : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (mul_nat x0 x1)
Known add_nat_0L^add_nat_0L : ∀ x0 . nat_p x0 ⟶ add_nat 0 x0 = x0
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known ordsuccE^ordsuccE : ∀ x0 x1 . x1 ∈ ordsucc x0 ⟶ or (x1 ∈ x0) (x1 = x0)
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Known ordsuccI1^ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
Known ordsuccI2^ordsuccI2 : ∀ x0 . x0 ∈ ordsucc x0
Theorem 95d11.. : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ordsucc (mul_nat 2 x1) ∈ mul_nat 2 x0 (proof)
Known In_3_4^In_3_4 : 3 ∈ 4
Known nat_ordsucc^nat_ordsucc : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc x0)
Known nat_trans^nat_trans : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ x1 ⊆ x0
Known 4f402..^exp_nat_p : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (exp_nat x0 x1)
Theorem d9442.. : ∀ x0 . nat_p x0 ⟶ ordsucc (exp_nat 2 (ordsucc x0)) ∈ exp_nat 2 (ordsucc (ordsucc x0)) (proof)
Theorem adab1.. : exp_nat 2 3 = 8 (proof)
Theorem db1de.. : exp_nat 2 4 = 16 (proof)