Proofgold Address

Param ordsucc^ordsucc : ι → ι
Param nat_p^nat_p : ι → ο
Known nat_0_in_ordsucc^{nat_0_in_ordsucc} : ∀ x0 . nat_p x0 ⟶ 0 ∈ ordsucc x0
Known nat_13^nat_13 : nat_p 13
Theorem d209c.. : 0 ∈ 14
Known nat_ordsucc_in_ordsucc^{nat_ordsucc_in_ordsucc} : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ ordsucc x1 ∈ ordsucc x0
Known cc8e9.. : 0 ∈ 13
Theorem df543.. : 1 ∈ 14
Known ab386.. : 1 ∈ 13
Theorem 12aa9.. : 2 ∈ 14
Known a582b.. : 2 ∈ 13
Theorem 19652.. : 3 ∈ 14
Known c03b3.. : 3 ∈ 13
Theorem 48239.. : 4 ∈ 14
Known 39abb.. : 4 ∈ 13
Theorem 37ac1.. : 5 ∈ 14
Known 88508.. : 5 ∈ 13
Theorem 21515.. : 6 ∈ 14
Known 827a1.. : 6 ∈ 13
Theorem b0eb6.. : 7 ∈ 14
Known 4039c.. : 7 ∈ 13
Theorem 77742.. : 8 ∈ 14
Known 17545.. : 8 ∈ 13
Theorem bfb05.. : 9 ∈ 14
Known e5d7b.. : 9 ∈ 13
Theorem 5c550.. : 10 ∈ 14
Known 74a33.. : 10 ∈ 13
Theorem 63273.. : 11 ∈ 14
Known 925e4.. : 11 ∈ 13
Theorem d80fe.. : 12 ∈ 14
Known f6a92.. : 12 ∈ 13
Theorem 3ef99.. : 13 ∈ 14
Known nat_14^nat_14 : nat_p 14
Theorem 2708c.. : 0 ∈ 15
Theorem 26f84.. : 1 ∈ 15
Theorem ba15b.. : 2 ∈ 15
Theorem 88998.. : 3 ∈ 15
Theorem 78026.. : 4 ∈ 15
Theorem 144e3.. : 5 ∈ 15
Theorem 7b7a1.. : 6 ∈ 15
Theorem c208d.. : 7 ∈ 15
Theorem 39ad4.. : 8 ∈ 15
Theorem 099a7.. : 9 ∈ 15
Theorem f7113.. : 10 ∈ 15
Theorem 9c224.. : 11 ∈ 15
Theorem ce1d0.. : 12 ∈ 15
Theorem 53185.. : 13 ∈ 15
Theorem 2e90c.. : 14 ∈ 15
Known nat_15^nat_15 : nat_p 15
Theorem 2c104.. : 0 ∈ 16
Theorem 6ec80.. : 1 ∈ 16
Theorem b34ab.. : 2 ∈ 16
Theorem f312e.. : 3 ∈ 16
Theorem add3d.. : 4 ∈ 16
Theorem fe610.. : 5 ∈ 16
Theorem 6d5be.. : 6 ∈ 16
Theorem 64265.. : 7 ∈ 16
Theorem 98f71.. : 8 ∈ 16
Theorem fdaf0.. : 9 ∈ 16
Theorem 662c8.. : 10 ∈ 16
Theorem 2039c.. : 11 ∈ 16
Theorem be924.. : 12 ∈ 16
Theorem e0b58.. : 13 ∈ 16
Theorem d4076.. : 14 ∈ 16
Theorem 0e6a7.. : 15 ∈ 16
Param add_nat^add_nat : ι → ι → ι
Known add_nat_SR^add_nat_SR : ∀ x0 x1 . nat_p x1 ⟶ add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known 22701.. : add_nat 16 13 = 29
Theorem b70e6.. : add_nat 16 14 = 30
Theorem d9ae8.. : add_nat 16 15 = 31
Theorem 35002.. : add_nat 16 16 = 32
Param mul_nat^mul_nat : ι → ι → ι
Known 1521b.. : add_nat 8 8 = 16
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 nat_2^nat_2 : nat_p 2
Known nat_8^nat_8 : nat_p 8
Known af7b1.. : mul_nat 2 8 = 16
Theorem 12f85.. : mul_nat 2 16 = 32
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_4^nat_4 : nat_p 4
Known db1de.. : exp_nat 2 4 = 16
Theorem e089c.. : exp_nat 2 5 = 32
Known 4f402..^exp_nat_p : ∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ nat_p (exp_nat x0 x1)
Known nat_5^nat_5 : nat_p 5
Theorem 1f846.. : nat_p 32
Known d9442.. : ∀ x0 . nat_p x0 ⟶ ordsucc (exp_nat 2 (ordsucc x0)) ∈ exp_nat 2 (ordsucc (ordsucc x0))
Known nat_3^nat_3 : nat_p 3
Theorem 8ad73.. : 17 ∈ 32