Search for blocks/addresses/...

Proofgold Address

address
PURxq7vEGY4QbFR5cPrrZJMND61ztPi75yd
total
0
mg
-
conjpub
-
current assets
57f1e../23349.. bday: 28153 doc published by Pr5Zc..
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Param omegaomega : ι
Param mul_natmul_nat : ιιι
Param ordsuccordsucc : ιι
Definition even_nateven_nat := λ x0 . and (x0omega) (∀ x1 : ο . (∀ x2 . and (x2omega) (x0 = mul_nat 2 x2)x1)x1)
Definition divides_natdivides_nat := λ x0 x1 . and (and (x0omega) (x1omega)) (∀ x2 : ο . (∀ x3 . and (x3omega) (mul_nat x0 x3 = x1)x2)x2)
Known and3Iand3I : ∀ x0 x1 x2 : ο . x0x1x2and (and x0 x1) x2
Param nat_pnat_p : ιο
Known nat_p_omeganat_p_omega : ∀ x0 . nat_p x0x0omega
Known nat_2nat_2 : nat_p 2
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Theorem b2900.. : ∀ x0 . even_nat x0divides_nat 2 x0 (proof)
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Definition prime_natprime_nat := λ x0 . and (and (x0omega) (1x0)) (∀ x1 . x1omegadivides_nat x1 x0or (x1 = 1) (x1 = x0))
Definition FalseFalse := ∀ x0 : ο . x0
Known FalseEFalseE : False∀ x0 : ο . x0
Known neq_2_1neq_2_1 : 2 = 1∀ x0 : ο . x0
Theorem 447ce.. : ∀ x0 . prime_nat x0even_nat x0x0 = 2 (proof)
Param intint : ι
Param add_SNoadd_SNo : ιιι
Param mul_SNomul_SNo : ιιι
Known c6211.. : ∀ x0 . x0int∀ x1 . x1int∀ x2 . x2int∀ x3 . x3int∀ x4 . x4int∀ x5 . x5intx0 = add_SNo (mul_SNo x2 x2) (add_SNo (mul_SNo x3 x3) (add_SNo (mul_SNo x4 x4) (mul_SNo x5 x5)))∀ x6 . x6int∀ x7 . x7int∀ x8 . x8int∀ x9 . x9intx1 = add_SNo (mul_SNo x6 x6) (add_SNo (mul_SNo x7 x7) (add_SNo (mul_SNo x8 x8) (mul_SNo x9 x9)))∀ x10 : ο . (∀ x11 . x11omega∀ x12 . x12omega∀ x13 . x13omega∀ x14 . x14omegamul_SNo x0 x1 = add_SNo (mul_SNo x11 x11) (add_SNo (mul_SNo x12 x12) (add_SNo (mul_SNo x13 x13) (mul_SNo x14 x14)))x10)x10
Param odd_natodd_nat : ιο
Known omega_nat_pomega_nat_p : ∀ x0 . x0omeganat_p x0
Known nat_complete_indnat_complete_ind : ∀ x0 : ι → ο . (∀ x1 . nat_p x1(∀ x2 . x2x1x0 x2)x0 x1)∀ x1 . nat_p x1x0 x1
Known 054a4.. : ∀ x0 : ι → ο . x0 0x0 1x0 2(∀ x1 . nat_p x1x0 (ordsucc (ordsucc (ordsucc x1))))∀ x1 . nat_p x1x0 x1
Known nat_0nat_0 : nat_p 0
Param SNoSNo : ιο
Known mul_SNo_zeroRmul_SNo_zeroR : ∀ x0 . SNo x0mul_SNo x0 0 = 0
Known SNo_0SNo_0 : SNo 0
Known add_SNo_0Ladd_SNo_0L : ∀ x0 . SNo x0add_SNo 0 x0 = x0
Known nat_1nat_1 : nat_p 1
Known mul_SNo_oneRmul_SNo_oneR : ∀ x0 . SNo x0mul_SNo x0 1 = x0
Known SNo_1SNo_1 : SNo 1
Known add_SNo_1_1_2add_SNo_1_1_2 : add_SNo 1 1 = 2
Known SNo_2SNo_2 : SNo 2
Definition notnot := λ x0 : ο . x0False
Known xmxm : ∀ x0 : ο . or x0 (not x0)
Known even_nat_or_odd_nateven_nat_or_odd_nat : ∀ x0 . nat_p x0or (even_nat x0) (odd_nat x0)
Known neq_ordsucc_0neq_ordsucc_0 : ∀ x0 . ordsucc x0 = 0∀ x1 : ο . x1
Known ordsucc_injordsucc_inj : ∀ x0 x1 . ordsucc x0 = ordsucc x1x0 = x1
Known b8d2f.. : ∀ x0 . x0omeganot (prime_nat x0)1x0∀ x1 : ο . (∀ x2 . x2x0∀ x3 . x3x01x21x3x0 = mul_nat x2 x3x1)x1
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Known mul_nat_mul_SNomul_nat_mul_SNo : ∀ x0 . x0omega∀ x1 . x1omegamul_nat x0 x1 = mul_SNo x0 x1
Known Subq_omega_intSubq_omega_int : omegaint
Known nat_p_transnat_p_trans : ∀ x0 . nat_p x0∀ x1 . x1x0nat_p x1
Known nat_ordsucc_in_ordsuccnat_ordsucc_in_ordsucc : ∀ x0 . nat_p x0∀ x1 . x1x0ordsucc x1ordsucc x0
Known nat_0_in_ordsuccnat_0_in_ordsucc : ∀ x0 . nat_p x00ordsucc x0
Known nat_ordsuccnat_ordsucc : ∀ x0 . nat_p x0nat_p (ordsucc x0)
Theorem 8ff04.. : (∀ x0 . prime_nat x0odd_nat x0∀ x1 : ο . (∀ x2 . and (x2omega) (∀ x3 : ο . (∀ x4 . and (x4omega) (∀ x5 : ο . (∀ x6 . and (x6omega) (∀ x7 : ο . (∀ x8 . and (x8omega) (x0 = add_SNo (mul_SNo x2 x2) (add_SNo (mul_SNo x4 x4) (add_SNo (mul_SNo x6 x6) (mul_SNo x8 x8))))x7)x7)x5)x5)x3)x3)x1)x1)∀ x0 . x0omega∀ x1 : ο . (∀ x2 . and (x2omega) (∀ x3 : ο . (∀ x4 . and (x4omega) (∀ x5 : ο . (∀ x6 . and (x6omega) (∀ x7 : ο . (∀ x8 . and (x8omega) (x0 = add_SNo (mul_SNo x2 x2) (add_SNo (mul_SNo x4 x4) (add_SNo (mul_SNo x6 x6) (mul_SNo x8 x8))))x7)x7)x5)x5)x3)x3)x1)x1 (proof)

previous assets