Search for blocks/addresses/...

Proofgold Asset

asset id
607c67699101ddcd4e70d1f9972e0d637bc90ace1da2c96825e69987f63484f0
asset hash
c25223dc2980962937339a03e98d3b7a56b597bf05475989244650c4cd4345c1
bday / block
15396
tx
68efb..
preasset
doc published by Pr4zB..
Param ordsuccordsucc : ιι
Param nat_pnat_p : ιο
Known nat_0_in_ordsuccnat_0_in_ordsucc : ∀ x0 . nat_p x00ordsucc x0
Known nat_13nat_13 : nat_p 13
Theorem d209c.. : 014 (proof)
Known nat_ordsucc_in_ordsuccnat_ordsucc_in_ordsucc : ∀ x0 . nat_p x0∀ x1 . x1x0ordsucc x1ordsucc x0
Known cc8e9.. : 013
Theorem df543.. : 114 (proof)
Known ab386.. : 113
Theorem 12aa9.. : 214 (proof)
Known a582b.. : 213
Theorem 19652.. : 314 (proof)
Known c03b3.. : 313
Theorem 48239.. : 414 (proof)
Known 39abb.. : 413
Theorem 37ac1.. : 514 (proof)
Known 88508.. : 513
Theorem 21515.. : 614 (proof)
Known 827a1.. : 613
Theorem b0eb6.. : 714 (proof)
Known 4039c.. : 713
Theorem 77742.. : 814 (proof)
Known 17545.. : 813
Theorem bfb05.. : 914 (proof)
Known e5d7b.. : 913
Theorem 5c550.. : 1014 (proof)
Known 74a33.. : 1013
Theorem 63273.. : 1114 (proof)
Known 925e4.. : 1113
Theorem d80fe.. : 1214 (proof)
Known f6a92.. : 1213
Theorem 3ef99.. : 1314 (proof)
Known nat_14nat_14 : nat_p 14
Theorem 2708c.. : 015 (proof)
Theorem 26f84.. : 115 (proof)
Theorem ba15b.. : 215 (proof)
Theorem 88998.. : 315 (proof)
Theorem 78026.. : 415 (proof)
Theorem 144e3.. : 515 (proof)
Theorem 7b7a1.. : 615 (proof)
Theorem c208d.. : 715 (proof)
Theorem 39ad4.. : 815 (proof)
Theorem 099a7.. : 915 (proof)
Theorem f7113.. : 1015 (proof)
Theorem 9c224.. : 1115 (proof)
Theorem ce1d0.. : 1215 (proof)
Theorem 53185.. : 1315 (proof)
Theorem 2e90c.. : 1415 (proof)
Known nat_15nat_15 : nat_p 15
Theorem 2c104.. : 016 (proof)
Theorem 6ec80.. : 116 (proof)
Theorem b34ab.. : 216 (proof)
Theorem f312e.. : 316 (proof)
Theorem add3d.. : 416 (proof)
Theorem fe610.. : 516 (proof)
Theorem 6d5be.. : 616 (proof)
Theorem 64265.. : 716 (proof)
Theorem 98f71.. : 816 (proof)
Theorem fdaf0.. : 916 (proof)
Theorem 662c8.. : 1016 (proof)
Theorem 2039c.. : 1116 (proof)
Theorem be924.. : 1216 (proof)
Theorem e0b58.. : 1316 (proof)
Theorem d4076.. : 1416 (proof)
Theorem 0e6a7.. : 1516 (proof)
Param add_natadd_nat : ιιι
Known add_nat_SRadd_nat_SR : ∀ x0 x1 . nat_p x1add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known 22701.. : add_nat 16 13 = 29
Theorem b70e6.. : add_nat 16 14 = 30 (proof)
Theorem d9ae8.. : add_nat 16 15 = 31 (proof)
Theorem 35002.. : add_nat 16 16 = 32 (proof)
Param mul_natmul_nat : ιιι
Known 1521b.. : add_nat 8 8 = 16
Known mul_add_nat_distrLmul_add_nat_distrL : ∀ x0 . nat_p x0∀ x1 . nat_p x1∀ x2 . nat_p x2mul_nat x0 (add_nat x1 x2) = add_nat (mul_nat x0 x1) (mul_nat x0 x2)
Known nat_2nat_2 : nat_p 2
Known nat_8nat_8 : nat_p 8
Known af7b1.. : mul_nat 2 8 = 16
Theorem 12f85.. : mul_nat 2 16 = 32 (proof)
Param nat_primrecnat_primrec : ι(ιιι) → ιι
Definition exp_natexp_nat := λ x0 . nat_primrec 1 (λ x1 . mul_nat x0)
Known nat_primrec_Snat_primrec_S : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . nat_p x2nat_primrec x0 x1 (ordsucc x2) = x1 x2 (nat_primrec x0 x1 x2)
Known nat_4nat_4 : nat_p 4
Known db1de.. : exp_nat 2 4 = 16
Theorem e089c.. : exp_nat 2 5 = 32 (proof)
Known 4f402..exp_nat_p : ∀ x0 . nat_p x0∀ x1 . nat_p x1nat_p (exp_nat x0 x1)
Known nat_5nat_5 : nat_p 5
Theorem 1f846.. : nat_p 32 (proof)
Known d9442.. : ∀ x0 . nat_p x0ordsucc (exp_nat 2 (ordsucc x0))exp_nat 2 (ordsucc (ordsucc x0))
Known nat_3nat_3 : nat_p 3
Theorem 8ad73.. : 1732 (proof)