Search for blocks/addresses/...

Proofgold Asset

asset id
70edb82b4d52aedb12b8971f69d5229b8e1cee1639c0ec2df48a911884c6812b
asset hash
bc961801d70181c57f098e5770b5c4db4ef66756fd25b98742fe0d639f0ae638
bday / block
27290
tx
007b5..
preasset
doc published by Pr5Zc..
Param nat_pnat_p : ιο
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Param add_natadd_nat : ιιι
Param ordsuccordsucc : ιι
Known nat_indnat_ind : ∀ x0 : ι → ο . x0 0(∀ x1 . nat_p x1x0 x1x0 (ordsucc x1))∀ x1 . nat_p x1x0 x1
Known add_nat_0Radd_nat_0R : ∀ x0 . add_nat x0 0 = x0
Known Subq_refSubq_ref : ∀ x0 . x0x0
Known add_nat_SRadd_nat_SR : ∀ x0 x1 . nat_p x1add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known Subq_traSubq_tra : ∀ x0 x1 x2 . x0x1x1x2x0x2
Known ordsuccI1ordsuccI1 : ∀ x0 . x0ordsucc x0
Theorem 4d87b.. : ∀ x0 x1 . nat_p x1x0add_nat x0 x1 (proof)
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Param mul_natmul_nat : ιιι
Known orILorIL : ∀ x0 x1 : ο . x0or x0 x1
Known orIRorIR : ∀ x0 x1 : ο . x1or x0 x1
Known mul_nat_SRmul_nat_SR : ∀ x0 x1 . nat_p x1mul_nat x0 (ordsucc x1) = add_nat x0 (mul_nat x0 x1)
Known mul_nat_pmul_nat_p : ∀ x0 . nat_p x0∀ x1 . nat_p x1nat_p (mul_nat x0 x1)
Theorem 2bbf0..mul_nat_0_or_Subq : ∀ x0 . nat_p x0∀ x1 . nat_p x1or (x1 = 0) (x0mul_nat x0 x1) (proof)
Theorem nat_inv_imprednat_inv_impred : ∀ x0 : ι → ο . x0 0(∀ x1 . nat_p x1x0 (ordsucc x1))∀ x1 . nat_p x1x0 x1 (proof)
Theorem 7be16.. : ∀ x0 : ι → ο . x0 0x0 1(∀ x1 . nat_p x1x0 (ordsucc (ordsucc x1)))∀ x1 . nat_p x1x0 x1 (proof)
Theorem 054a4.. : ∀ x0 : ι → ο . x0 0x0 1x0 2(∀ x1 . nat_p x1x0 (ordsucc (ordsucc (ordsucc x1))))∀ x1 . nat_p x1x0 x1 (proof)
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Definition FalseFalse := ∀ x0 : ο . x0
Known FalseEFalseE : False∀ x0 : ο . x0
Known neq_ordsucc_0neq_ordsucc_0 : ∀ x0 . ordsucc x0 = 0∀ x1 : ο . x1
Theorem 3fa1a.. : ∀ x0 x1 . nat_p x1add_nat x0 x1 = 0and (x0 = 0) (x1 = 0) (proof)
Known ordsucc_injordsucc_inj : ∀ x0 x1 . ordsucc x0 = ordsucc x1x0 = x1
Theorem c89ba.. : ∀ x0 x1 . nat_p x1add_nat x0 x1 = x1x0 = 0 (proof)
Known mul_nat_0Rmul_nat_0R : ∀ x0 . mul_nat x0 0 = 0
Known nat_ordsuccnat_ordsucc : ∀ x0 . nat_p x0nat_p (ordsucc x0)
Known add_nat_comadd_nat_com : ∀ x0 . nat_p x0∀ x1 . nat_p x1add_nat x0 x1 = add_nat x1 x0
Known add_nat_padd_nat_p : ∀ x0 . nat_p x0∀ x1 . nat_p x1nat_p (add_nat x0 x1)
Theorem 75048.. : ∀ x0 . nat_p x0∀ x1 . nat_p x1mul_nat x1 x0 = x1(x1 = 0∀ x2 : ο . x2)x0 = 1 (proof)
Param omegaomega : ι
Definition notnot := λ x0 : ο . x0False
Definition divides_natdivides_nat := λ x0 x1 . and (and (x0omega) (x1omega)) (∀ x2 : ο . (∀ x3 . and (x3omega) (mul_nat x0 x3 = x1)x2)x2)
Definition prime_natprime_nat := λ x0 . and (and (x0omega) (1x0)) (∀ x1 . x1omegadivides_nat x1 x0or (x1 = 1) (x1 = x0))
Known dnegdneg : ∀ x0 : ο . not (not x0)x0
Known and3Iand3I : ∀ x0 x1 x2 : ο . x0x1x2and (and x0 x1) x2
Param ordinalordinal : ιο
Known ordinal_In_Or_Subqordinal_In_Or_Subq : ∀ x0 x1 . ordinal x0ordinal x1or (x0x1) (x1x0)
Known nat_p_ordinalnat_p_ordinal : ∀ x0 . nat_p x0ordinal x0
Known omega_nat_pomega_nat_p : ∀ x0 . x0omeganat_p x0
Definition nInnIn := λ x0 x1 . not (x0x1)
Known In_irrefIn_irref : ∀ x0 . nIn x0 x0
Known mul_nat_commul_nat_com : ∀ x0 . nat_p x0∀ x1 . nat_p x1mul_nat x0 x1 = mul_nat x1 x0
Known set_extset_ext : ∀ x0 x1 . x0x1x1x0x0 = x1
Known mul_nat_1Rmul_nat_1R : ∀ x0 . mul_nat x0 1 = x0
Known ordinal_ordsucc_Inordinal_ordsucc_In : ∀ x0 . ordinal x0∀ x1 . x1x0ordsucc x1ordsucc x0
Known nat_0_in_ordsuccnat_0_in_ordsucc : ∀ x0 . nat_p x00ordsucc x0
Known ordinal_trichotomy_or_impredordinal_trichotomy_or_impred : ∀ x0 x1 . ordinal x0ordinal x1∀ x2 : ο . (x0x1x2)(x0 = x1x2)(x1x0x2)x2
Known ordinal_1ordinal_1 : ordinal 1
Known cases_1cases_1 : ∀ x0 . x01∀ x1 : ι → ο . x1 0x1 x0
Known ordinal_Emptyordinal_Empty : ordinal 0
Known Empty_Subq_eqEmpty_Subq_eq : ∀ x0 . x00x0 = 0
Known mul_nat_0Lmul_nat_0L : ∀ x0 . nat_p x0mul_nat 0 x0 = 0
Known EmptyEEmptyE : ∀ x0 . nIn x0 0
Theorem b8d2f.. : ∀ x0 . x0omeganot (prime_nat x0)1x0∀ x1 : ο . (∀ x2 . x2x0∀ x3 . x3x01x21x3x0 = mul_nat x2 x3x1)x1 (proof)
Param SNoSNo : ιο
Param SNoLtSNoLt : ιιο
Known ordinal_SNoLt_Inordinal_SNoLt_In : ∀ x0 x1 . ordinal x0ordinal x1SNoLt x0 x1x0x1
Param mul_SNomul_SNo : ιιι
Known mul_nat_mul_SNomul_nat_mul_SNo : ∀ x0 . x0omega∀ x1 . x1omegamul_nat x0 x1 = mul_SNo x0 x1
Known nat_p_omeganat_p_omega : ∀ x0 . nat_p x0x0omega
Param add_SNoadd_SNo : ιιι
Known add_SNo_0Ladd_SNo_0L : ∀ x0 . SNo x0add_SNo 0 x0 = x0
Param minus_SNominus_SNo : ιι
Known add_SNo_minus_Lt2add_SNo_minus_Lt2 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x2 (add_SNo x0 (minus_SNo x1))SNoLt (add_SNo x2 x1) x0
Known SNo_mul_SNoSNo_mul_SNo : ∀ x0 x1 . SNo x0SNo x1SNo (mul_SNo x0 x1)
Known SNo_0SNo_0 : SNo 0
Known mul_SNo_oneRmul_SNo_oneR : ∀ x0 . SNo x0mul_SNo x0 1 = x0
Known mul_SNo_minus_distrRmul_minus_SNo_distrR : ∀ x0 x1 . SNo x0SNo x1mul_SNo x0 (minus_SNo x1) = minus_SNo (mul_SNo x0 x1)
Known SNo_1SNo_1 : SNo 1
Known mul_SNo_distrLmul_SNo_distrL : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2mul_SNo x0 (add_SNo x1 x2) = add_SNo (mul_SNo x0 x1) (mul_SNo x0 x2)
Known SNo_minus_SNoSNo_minus_SNo : ∀ x0 . SNo x0SNo (minus_SNo x0)
Known mul_SNo_pos_posmul_SNo_pos_pos : ∀ x0 x1 . SNo x0SNo x1SNoLt 0 x0SNoLt 0 x1SNoLt 0 (mul_SNo x0 x1)
Known SNo_add_SNoSNo_add_SNo : ∀ x0 x1 . SNo x0SNo x1SNo (add_SNo x0 x1)
Known add_SNo_minus_Lt2badd_SNo_minus_Lt2b : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt (add_SNo x2 x1) x0SNoLt x2 (add_SNo x0 (minus_SNo x1))
Known ordinal_In_SNoLtordinal_In_SNoLt : ∀ x0 . ordinal x0∀ x1 . x1x0SNoLt x1 x0
Known ordinal_SNoordinal_SNo : ∀ x0 . ordinal x0SNo x0
Theorem 58a75.. : ∀ x0 x1 . nat_p x0nat_p x10x01x1x0mul_nat x0 x1 (proof)
Known nat_transnat_trans : ∀ x0 . nat_p x0∀ x1 . x1x0x1x0
Known In_0_1In_0_1 : 01
Theorem 7d1f8.. : ∀ x0 x1 . nat_p x0nat_p x11x01x1and (x0mul_nat x0 x1) (x1mul_nat x0 x1) (proof)
Known 25618.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))∀ x2 x3 x4 x5 . x0 x2x0 x3x0 x4x0 x5x0 (x1 x2 (x1 x3 (x1 x4 x5)))
Known 88d93.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 . x0 x3x0 x4x0 (x2 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x1 x3 (x1 x4 x5) = x1 x4 (x1 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x1 (x1 x3 x4) x5 = x1 x3 (x1 x4 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 : ι → ι . (∀ x4 . x0 x4x3 x4 = x2 x4 x4)∀ x4 : ι → ι . (∀ x5 . x0 x5x0 (x4 x5))(∀ x5 . x0 x5x4 (x4 x5) = x5)(∀ x5 x6 . x0 x5x0 x6x1 (x4 x5) (x1 x5 x6) = x6)(∀ x5 x6 . x0 x5x0 x6x1 x5 (x1 (x4 x5) x6) = x6)(∀ x5 x6 . x0 x5x0 x6x2 (x4 x5) x6 = x4 (x2 x5 x6))(∀ x5 x6 . x0 x5x0 x6x2 x5 (x4 x6) = x4 (x2 x5 x6))(∀ x5 x6 . x0 x5x0 x6x2 x5 x6 = x2 x6 x5)(∀ x5 x6 x7 x8 . x0 x5x0 x6x0 x7x0 x8x2 (x2 x5 x6) (x2 x7 x8) = x2 (x2 x5 x7) (x2 x6 x8))∀ x5 x6 x7 x8 x9 x10 x11 x12 . x0 x5x0 x6x0 x7x0 x8x0 x9x0 x10x0 x11x0 x12x2 (x1 (x3 x5) (x1 (x3 x6) (x1 (x3 x7) (x3 x8)))) (x1 (x3 x9) (x1 (x3 x10) (x1 (x3 x11) (x3 x12)))) = x1 (x3 (x1 (x2 x5 x10) (x1 (x2 x6 x9) (x1 (x2 x7 x12) (x4 (x2 x8 x11)))))) (x1 (x3 (x1 (x2 x5 x11) (x1 (x4 (x2 x6 x12)) (x1 (x2 x7 x9) (x2 x8 x10))))) (x1 (x3 (x1 (x2 x5 x12) (x1 (x2 x6 x11) (x1 (x4 (x2 x7 x10)) (x2 x8 x9))))) (x3 (x1 (x2 x5 x9) (x1 (x4 (x2 x6 x10)) (x1 (x4 (x2 x7 x11)) (x4 (x2 x8 x12))))))))
Theorem 41130.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 . x0 x3x0 x4x0 (x2 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x1 x3 (x1 x4 x5) = x1 x4 (x1 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x1 (x1 x3 x4) x5 = x1 x3 (x1 x4 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 : ι → ι . (∀ x4 . x0 x4x3 x4 = x2 x4 x4)∀ x4 : ι → ι . (∀ x5 . x0 x5x0 (x4 x5))(∀ x5 . x0 x5x4 (x4 x5) = x5)(∀ x5 x6 . x0 x5x0 x6x1 (x4 x5) (x1 x5 x6) = x6)(∀ x5 x6 . x0 x5x0 x6x1 x5 (x1 (x4 x5) x6) = x6)(∀ x5 x6 . x0 x5x0 x6x2 (x4 x5) x6 = x4 (x2 x5 x6))(∀ x5 x6 . x0 x5x0 x6x2 x5 (x4 x6) = x4 (x2 x5 x6))(∀ x5 x6 . x0 x5x0 x6x2 x5 x6 = x2 x6 x5)(∀ x5 x6 x7 x8 . x0 x5x0 x6x0 x7x0 x8x2 (x2 x5 x6) (x2 x7 x8) = x2 (x2 x5 x7) (x2 x6 x8))∀ x5 x6 . x0 x5x0 x6∀ x7 x8 x9 x10 . x0 x7x0 x8x0 x9x0 x10x5 = x1 (x3 x7) (x1 (x3 x8) (x1 (x3 x9) (x3 x10)))∀ x11 x12 x13 x14 . x0 x11x0 x12x0 x13x0 x14x6 = x1 (x3 x11) (x1 (x3 x12) (x1 (x3 x13) (x3 x14)))∀ x15 : ο . (∀ x16 x17 x18 x19 . x0 x16x0 x17x0 x18x0 x19x2 x5 x6 = x1 (x3 x16) (x1 (x3 x17) (x1 (x3 x18) (x3 x19)))x15)x15 (proof)
Theorem 277a1.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 . x0 x3x0 x4x0 (x2 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x1 x3 (x1 x4 x5) = x1 x4 (x1 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x1 (x1 x3 x4) x5 = x1 x3 (x1 x4 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 : ι → ι . (∀ x4 . x0 x4x3 x4 = x2 x4 x4)∀ x4 : ι → ι . (∀ x5 . x0 x5x0 (x4 x5))(∀ x5 . x0 x5x4 (x4 x5) = x5)(∀ x5 x6 . x0 x5x0 x6x1 (x4 x5) (x1 x5 x6) = x6)(∀ x5 x6 . x0 x5x0 x6x1 x5 (x1 (x4 x5) x6) = x6)(∀ x5 x6 . x0 x5x0 x6x2 (x4 x5) x6 = x4 (x2 x5 x6))(∀ x5 x6 . x0 x5x0 x6x2 x5 (x4 x6) = x4 (x2 x5 x6))(∀ x5 x6 . x0 x5x0 x6x2 x5 x6 = x2 x6 x5)(∀ x5 x6 x7 x8 . x0 x5x0 x6x0 x7x0 x8x2 (x2 x5 x6) (x2 x7 x8) = x2 (x2 x5 x7) (x2 x6 x8))∀ x5 : ι → ο . (∀ x6 . x0 x6∀ x7 : ο . (∀ x8 . and (x5 x8) (x3 x8 = x3 x6)x7)x7)∀ x6 x7 . x0 x6x0 x7∀ x8 x9 x10 x11 . x0 x8x0 x9x0 x10x0 x11x6 = x1 (x3 x8) (x1 (x3 x9) (x1 (x3 x10) (x3 x11)))∀ x12 x13 x14 x15 . x0 x12x0 x13x0 x14x0 x15x7 = x1 (x3 x12) (x1 (x3 x13) (x1 (x3 x14) (x3 x15)))∀ x16 : ο . (∀ x17 x18 x19 x20 . x5 x17x5 x18x5 x19x5 x20x2 x6 x7 = x1 (x3 x17) (x1 (x3 x18) (x1 (x3 x19) (x3 x20)))x16)x16 (proof)
Known add_SNo_com_3_0_1add_SNo_com_3_0_1 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2add_SNo x0 (add_SNo x1 x2) = add_SNo x1 (add_SNo x0 x2)
Known mul_SNo_distrRmul_SNo_distrR : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2mul_SNo (add_SNo x0 x1) x2 = add_SNo (mul_SNo x0 x2) (mul_SNo x1 x2)
Known minus_SNo_involminus_SNo_invol : ∀ x0 . SNo x0minus_SNo (minus_SNo x0) = x0
Known add_SNo_minus_L2add_SNo_minus_L2 : ∀ x0 x1 . SNo x0SNo x1add_SNo (minus_SNo x0) (add_SNo x0 x1) = x1
Known add_SNo_minus_SNo_prop2add_SNo_minus_SNo_prop2 : ∀ x0 x1 . SNo x0SNo x1add_SNo x0 (add_SNo (minus_SNo x0) x1) = x1
Known mul_SNo_minus_distrLmul_SNo_minus_distrL : ∀ x0 x1 . SNo x0SNo x1mul_SNo (minus_SNo x0) x1 = minus_SNo (mul_SNo x0 x1)
Known mul_SNo_commul_SNo_com : ∀ x0 x1 . SNo x0SNo x1mul_SNo x0 x1 = mul_SNo x1 x0
Known mul_SNo_assocmul_SNo_assoc : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2mul_SNo x0 (mul_SNo x1 x2) = mul_SNo (mul_SNo x0 x1) x2
Known add_SNo_assocadd_SNo_assoc : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2add_SNo x0 (add_SNo x1 x2) = add_SNo (add_SNo x0 x1) x2
Theorem 634fb.. : ∀ x0 x1 . SNo x0SNo x1∀ x2 x3 x4 x5 . SNo x2SNo x3SNo x4SNo x5x0 = add_SNo (mul_SNo x2 x2) (add_SNo (mul_SNo x3 x3) (add_SNo (mul_SNo x4 x4) (mul_SNo x5 x5)))∀ x6 x7 x8 x9 . SNo x6SNo x7SNo x8SNo x9x1 = add_SNo (mul_SNo x6 x6) (add_SNo (mul_SNo x7 x7) (add_SNo (mul_SNo x8 x8) (mul_SNo x9 x9)))∀ x10 : ο . (∀ x11 x12 x13 x14 . SNo x11SNo x12SNo x13SNo x14mul_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 (proof)
Param intint : ι
Known int_add_SNoint_add_SNo : ∀ x0 . x0int∀ x1 . x1intadd_SNo x0 x1int
Known int_mul_SNoint_mul_SNo : ∀ x0 . x0int∀ x1 . x1intmul_SNo x0 x1int
Known int_minus_SNoint_minus_SNo : ∀ x0 . x0intminus_SNo x0int
Known int_SNoint_SNo : ∀ x0 . x0intSNo x0
Theorem d6e7f.. : ∀ 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 . x11int∀ x12 . x12int∀ x13 . x13int∀ x14 . x14intmul_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 (proof)
Known int_SNo_casesint_SNo_cases : ∀ x0 : ι → ο . (∀ x1 . x1omegax0 x1)(∀ x1 . x1omegax0 (minus_SNo x1))∀ x1 . x1intx0 x1
Known omega_SNoomega_SNo : ∀ x0 . x0omegaSNo x0
Theorem 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 (proof)