Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrRJn../14bc2..
PUVFS../e8186..
vout
PrRJn../f351f.. 9.70 bars
TMU2c../2aaae.. ownership of 1129e.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMTQV../aa1b5.. ownership of 1bc37.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMcxe../0e5c1.. ownership of 9bd18.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMbgN../afdda.. ownership of 8d3f6.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMK3o../db89b.. ownership of a3726.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMRjf../4fd3d.. ownership of 33dd3.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMcyg../ecb48.. ownership of af26f.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMGpp../7db8b.. ownership of db57c.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMLC2../edfee.. ownership of 9dc41.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMb2p../292ec.. ownership of 3729f.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMafg../653c8.. ownership of 4e2fe.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMRhs../25807.. ownership of acded.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMXZR../5c043.. ownership of 16680.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMVt6../91fcb.. ownership of baf75.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMaSw../1cb16.. ownership of a96cd.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMSfw../b7850.. ownership of ae2a4.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMPX9../deded.. ownership of 9a5d6.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMb46../1d4bd.. ownership of c1ba1.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMYA6../8df82.. ownership of 3899c.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMWgt../3ac39.. ownership of dd587.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMQj6../1b2a9.. ownership of a0cc9.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMXt4../117f9.. ownership of 1f574.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMTfG../90b3f.. ownership of a297e.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMbQJ../01f5a.. ownership of 68b6f.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMSyf../51bf5.. ownership of 2326d.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMbrY../68882.. ownership of 50a15.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMaz4../fae17.. ownership of d07df.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMKck../0e812.. ownership of 5e30a.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMWom../46708.. ownership of 22c84.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMF9Q../aeaa2.. ownership of 011f9.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMKAZ../c1d72.. ownership of 63bfe.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMLLc../43330.. ownership of b7aa6.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMJfK../2ede6.. ownership of 33475.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMUym../89a46.. ownership of bfe38.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMJZt../a58d8.. ownership of b6e18.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMLTL../f3424.. ownership of 89e73.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMWvj../1d8f1.. ownership of 10be6.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMFNo../976bf.. ownership of b9f76.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMWJn../acc11.. ownership of 03b8a.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMcPA../add95.. ownership of 28d72.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMSZa../81fd1.. ownership of c1cc5.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMcTq../22f0c.. ownership of c8e82.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMdyY../037ab.. ownership of b4d9c.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMThc../e7ed5.. ownership of 0058e.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMZ76../380e0.. ownership of 81ebf.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMTZd../ee65d.. ownership of 8ec44.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMK1Y../94b8e.. ownership of ad387.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMLi8../79a54.. ownership of 18419.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMQi4../8294b.. ownership of 5d96a.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMJ3U../a13e5.. ownership of 611f8.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMJad../b309a.. ownership of 1c3ee.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMGxR../f2cb3.. ownership of acfe9.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMW2X../bed17.. ownership of 586cf.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMNxV../d0967.. ownership of b7d52.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMWg8../75d57.. ownership of d59a0.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMZWt../789da.. ownership of 0d6a0.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMNk6../05489.. ownership of eaa26.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMP8g../9c83f.. ownership of 0572f.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMRVv../c724a.. ownership of 71c93.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMHjN../e4f47.. ownership of 8739d.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMUcd../1c9a8.. ownership of 168aa.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMSuo../e837a.. ownership of f77d4.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMcXm../dd506.. ownership of 05ecb.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMRqa../4a06e.. ownership of 3e6f6.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
PUQQ9../456e5.. doc published by PrQUS..
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Definition injinj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3x0x2 x3x1) (∀ x3 . x3x0∀ x4 . x4x0x2 x3 = x2 x4x3 = x4)
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Theorem 71c93..injI : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . x3x0x2 x3x1)(∀ x3 . x3x0∀ x4 . x4x0x2 x3 = x2 x4x3 = x4)inj x0 x1 x2 (proof)
Param nat_pnat_p : ιο
Param add_natadd_nat : ιιι
Known add_nat_comadd_nat_com : ∀ x0 . nat_p x0∀ x1 . nat_p x1add_nat x0 x1 = add_nat x1 x0
Known nat_p_transnat_p_trans : ∀ x0 . nat_p x0∀ x1 . x1x0nat_p x1
Known 85b3a..add_nat_In_R : ∀ x0 . nat_p x0∀ x1 . x1x0∀ x2 . nat_p x2add_nat x1 x2add_nat x0 x2
Theorem eaa26..add_nat_In_L : ∀ x0 . nat_p x0∀ x1 . nat_p x1∀ x2 . x2x1add_nat x0 x2add_nat x0 x1 (proof)
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Param ordinalordinal : ιο
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
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 nat_transnat_trans : ∀ x0 . nat_p x0∀ x1 . x1x0x1x0
Known add_nat_padd_nat_p : ∀ x0 . nat_p x0∀ x1 . nat_p x1nat_p (add_nat x0 x1)
Known set_extset_ext : ∀ x0 x1 . x0x1x1x0x0 = x1
Known Subq_refSubq_ref : ∀ x0 . x0x0
Theorem d59a0..add_nat_Subq_R : ∀ x0 . nat_p x0∀ x1 . nat_p x1x0x1∀ x2 . nat_p x2add_nat x0 x2add_nat x1 x2 (proof)
Theorem 586cf..add_nat_Subq_L : ∀ x0 . nat_p x0∀ x1 . nat_p x1∀ x2 . nat_p x2x1x2add_nat x0 x1add_nat x0 x2 (proof)
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 add_nat_SRadd_nat_SR : ∀ x0 x1 . nat_p x1add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known ordsucc_injordsucc_inj : ∀ x0 x1 . ordsucc x0 = ordsucc x1x0 = x1
Theorem 1c3ee..add_nat_cancel_R : ∀ x0 . nat_p x0∀ x1 . nat_p x1∀ x2 . nat_p x2add_nat x0 x2 = add_nat x1 x2x0 = x1 (proof)
Param mul_natmul_nat : ιιι
Known nat_inv_imprednat_inv_impred : ∀ x0 : ι → ο . x0 0(∀ x1 . nat_p x1x0 (ordsucc x1))∀ x1 . nat_p x1x0 x1
Definition FalseFalse := ∀ x0 : ο . x0
Known FalseEFalseE : False∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Definition nInnIn := λ x0 x1 . not (x0x1)
Known EmptyEEmptyE : ∀ x0 . nIn x0 0
Known In_no2cycleIn_no2cycle : ∀ x0 x1 . x0x1x1x0False
Known In_0_1In_0_1 : 01
Known In_irrefIn_irref : ∀ x0 . nIn x0 x0
Known mul_nat_SRmul_nat_SR : ∀ x0 x1 . nat_p x1mul_nat x0 (ordsucc x1) = add_nat x0 (mul_nat x0 x1)
Known nat_ordsuccnat_ordsucc : ∀ x0 . nat_p x0nat_p (ordsucc x0)
Known mul_nat_pmul_nat_p : ∀ x0 . nat_p x0∀ x1 . nat_p x1nat_p (mul_nat x0 x1)
Known mul_nat_SLmul_nat_SL : ∀ x0 . nat_p x0∀ x1 . nat_p x1mul_nat (ordsucc x0) x1 = add_nat (mul_nat x0 x1) x1
Known nat_0_in_ordsuccnat_0_in_ordsucc : ∀ x0 . nat_p x00ordsucc x0
Theorem 5d96a..mul_nat_0m_1n_In : ∀ x0 . nat_p x0∀ x1 . nat_p x10x01x1x0mul_nat x0 x1 (proof)
Known Subq_traSubq_tra : ∀ x0 x1 x2 . x0x1x1x2x0x2
Known df9cc..mul_nat_Subq_L : ∀ x0 x1 . nat_p x0nat_p x1x0x1∀ x2 . nat_p x2mul_nat x2 x0mul_nat x2 x1
Known 4324d..mul_nat_Subq_R : ∀ x0 x1 . nat_p x0nat_p x1x0x1∀ x2 . nat_p x2mul_nat x0 x2mul_nat x1 x2
Theorem ad387.. : ∀ x0 x1 . nat_p x0nat_p x1x0x1mul_nat x0 x0mul_nat x1 x1 (proof)
Param exp_natexp_nat : ιιι
Known caaf4..exp_nat_S : ∀ x0 x1 . nat_p x1exp_nat x0 (ordsucc x1) = mul_nat x0 (exp_nat x0 x1)
Known nat_1nat_1 : nat_p 1
Known 3e9f7..exp_nat_1 : ∀ x0 . exp_nat x0 1 = x0
Theorem 81ebf.. : ∀ x0 . exp_nat x0 2 = mul_nat x0 x0 (proof)
Definition bijbij := λ x0 x1 . λ x2 : ι → ι . and (and (∀ x3 . x3x0x2 x3x1) (∀ x3 . x3x0∀ x4 . x4x0x2 x3 = x2 x4x3 = x4)) (∀ x3 . x3x1∀ x4 : ο . (∀ x5 . and (x5x0) (x2 x5 = x3)x4)x4)
Definition equipequip := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . bij x0 x1 x3x2)x2
Known equip_0_Emptyequip_0_Empty : ∀ x0 . equip x0 0x0 = 0
Known 856b4..exp_nat_0 : ∀ x0 . exp_nat x0 0 = 1
Param SingSing : ιι
Known Power_0_Sing_0Power_0_Sing_0 : prim4 0 = Sing 0
Known eq_1_Sing0eq_1_Sing0 : 1 = Sing 0
Known equip_refequip_ref : ∀ x0 . equip x0 x0
Known mul_nat_commul_nat_com : ∀ x0 . nat_p x0∀ x1 . nat_p x1mul_nat x0 x1 = mul_nat x1 x0
Known nat_2nat_2 : nat_p 2
Known add_nat_1_1_2add_nat_1_1_2 : add_nat 1 1 = 2
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 mul_nat_1Rmul_nat_1R : ∀ x0 . mul_nat x0 1 = x0
Known equip_symequip_sym : ∀ x0 x1 . equip x0 x1equip x1 x0
Known ordsuccI2ordsuccI2 : ∀ x0 . x0ordsucc x0
Param setminussetminus : ιιι
Known 9c223..equip_ordsucc_remove1 : ∀ x0 x1 x2 . x2x0equip x0 (ordsucc x1)equip (setminus x0 (Sing x2)) x1
Param If_iIf_i : οιιι
Known bijIbijI : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . x3x0x2 x3x1)(∀ x3 . x3x0∀ x4 . x4x0x2 x3 = x2 x4x3 = x4)(∀ x3 . x3x1∀ x4 : ο . (∀ x5 . and (x5x0) (x2 x5 = x3)x4)x4)bij x0 x1 x2
Known xmxm : ∀ x0 : ο . or x0 (not x0)
Known If_i_1If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0If_i x0 x1 x2 = x1
Known PowerIPowerI : ∀ x0 x1 . x1x0x1prim4 x0
Known setminusEsetminusE : ∀ x0 x1 x2 . x2setminus x0 x1and (x2x0) (nIn x2 x1)
Known setminusIsetminusI : ∀ x0 x1 x2 . x2x0nIn x2 x1x2setminus x0 x1
Known PowerEPowerE : ∀ x0 x1 . x1prim4 x0x1x0
Known If_i_0If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0If_i x0 x1 x2 = x2
Known add_nat_Subq_Ladd_nat_Subq_R : ∀ x0 . nat_p x0∀ x1 . nat_p x1x0add_nat x0 x1
Known SingESingE : ∀ x0 x1 . x1Sing x0x1 = x0
Known setminusE1setminusE1 : ∀ x0 x1 x2 . x2setminus x0 x1x2x0
Known setminusE2setminusE2 : ∀ x0 x1 x2 . x2setminus x0 x1nIn x2 x1
Known SingISingI : ∀ x0 . x0Sing x0
Known nat_Subq_add_exnat_Subq_add_ex : ∀ x0 . nat_p x0∀ x1 . nat_p x1x0x1∀ x2 : ο . (∀ x3 . and (nat_p x3) (x1 = add_nat x3 x0)x2)x2
Param binunionbinunion : ιιι
Known binunion_Subq_minbinunion_Subq_min : ∀ x0 x1 x2 . x0x2x1x2binunion x0 x1x2
Known setminus_Subqsetminus_Subq : ∀ x0 x1 . setminus x0 x1x0
Known binunionI2binunionI2 : ∀ x0 x1 x2 . x2x1x2binunion x0 x1
Known binunionEbinunionE : ∀ x0 x1 x2 . x2binunion x0 x1or (x2x0) (x2x1)
Known binunionI1binunionI1 : ∀ x0 x1 x2 . x2x0x2binunion x0 x1
Known 4f402..exp_nat_p : ∀ x0 . nat_p x0∀ x1 . nat_p x1nat_p (exp_nat x0 x1)
Theorem b4d9c..equip_finite_Power : ∀ x0 . nat_p x0∀ x1 . equip x1 x0equip (prim4 x1) (exp_nat 2 x0) (proof)
Param infiniteinfinite : ιο
Param omegaomega : ι
Known and3Iand3I : ∀ x0 x1 x2 : ο . x0x1x2and (and x0 x1) x2
Known ordinal_trichotomy_or_impredordinal_trichotomy_or_impred : ∀ x0 x1 . ordinal x0ordinal x1∀ x2 : ο . (x0x1x2)(x0 = x1x2)(x1x0x2)x2
Known omega_nat_pomega_nat_p : ∀ x0 . x0omeganat_p x0
Known omega_ordsuccomega_ordsucc : ∀ x0 . x0omegaordsucc x0omega
Known nat_p_omeganat_p_omega : ∀ x0 . nat_p x0x0omega
Known ordinal_ordsucc_In_Subqordinal_ordsucc_In_Subq : ∀ x0 . ordinal x0∀ x1 . x1x0ordsucc x1x0
Theorem c1cc5..infiniteRamsey_lem : ∀ x0 . ∀ x1 x2 x3 : ι → ι . infinite x0(∀ x4 . x4x0infinite x4and (x1 x4x4) (infinite (x1 x4)))(∀ x4 . x4x0infinite x4and (x2 x4x4) (nIn (x2 x4) (x1 x4)))x3 0 = x1 x0(∀ x4 . nat_p x4x3 (ordsucc x4) = x1 (x3 x4))and (and (∀ x4 . nat_p x4and (x3 x4x0) (infinite (x3 x4))) (∀ x4 . x4omega∀ x5 . x5omegax4x5x3 x5x3 x4)) (∀ x4 . x4omega∀ x5 . x5omegax2 (x3 x4) = x2 (x3 x5)x4 = x5) (proof)
Param SNoSNo : ιο
Param intint : ι
Param mul_SNomul_SNo : ιιι
Definition divides_intdivides_int := λ x0 x1 . and (and (x0int) (x1int)) (∀ x2 : ο . (∀ x3 . and (x3int) (mul_SNo x0 x3 = x1)x2)x2)
Param add_SNoadd_SNo : ιιι
Param minus_SNominus_SNo : ιι
Known add_SNo_comadd_SNo_com : ∀ x0 x1 . SNo x0SNo x1add_SNo x0 x1 = add_SNo x1 x0
Known SNo_minus_SNoSNo_minus_SNo : ∀ x0 . SNo x0SNo (minus_SNo x0)
Known minus_SNo_involminus_SNo_invol : ∀ x0 . SNo x0minus_SNo (minus_SNo x0) = x0
Known minus_add_SNo_distrminus_add_SNo_distr : ∀ x0 x1 . SNo x0SNo x1minus_SNo (add_SNo x0 x1) = add_SNo (minus_SNo x0) (minus_SNo x1)
Known divides_int_minus_SNodivides_int_minus_SNo : ∀ x0 x1 . divides_int x0 x1divides_int x0 (minus_SNo x1)
Theorem 03b8a.. : ∀ x0 x1 x2 . SNo x1SNo x2divides_int x0 (add_SNo x1 (minus_SNo x2))divides_int x0 (add_SNo x2 (minus_SNo x1)) (proof)
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))
Param SNoLtSNoLt : ιιο
Known SNoLt_irrefSNoLt_irref : ∀ x0 . not (SNoLt x0 x0)
Param SNoLeSNoLe : ιιο
Known SNoLtLe_traSNoLtLe_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x0 x1SNoLe x1 x2SNoLt x0 x2
Known SNo_1SNo_1 : SNo 1
Known nat_p_SNonat_p_SNo : ∀ x0 . nat_p x0SNo x0
Known ordinal_In_SNoLtordinal_In_SNoLt : ∀ x0 . ordinal x0∀ x1 . x1x0SNoLt x1 x0
Known divides_int_pos_Ledivides_int_pos_Le : ∀ x0 x1 . divides_int x0 x1SNoLt 0 x1SNoLe x0 x1
Known SNoLt_0_1SNoLt_0_1 : SNoLt 0 1
Theorem 10be6..prime_not_divides_int_1 : ∀ x0 . prime_nat x0not (divides_int x0 1) (proof)
Param nat_primrecnat_primrec : ι(ιιι) → ιι
Definition 05ecb..Pi_SNo := λ x0 : ι → ι . nat_primrec 1 (λ x1 x2 . mul_SNo x2 (x0 x1))
Known nat_primrec_0nat_primrec_0 : ∀ x0 . ∀ x1 : ι → ι → ι . nat_primrec x0 x1 0 = x0
Theorem b6e18..Pi_SNo_0 : ∀ x0 : ι → ι . 05ecb.. x0 0 = 1 (proof)
Known nat_primrec_Snat_primrec_S : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . nat_p x2nat_primrec x0 x1 (ordsucc x2) = x1 x2 (nat_primrec x0 x1 x2)
Theorem 33475..Pi_SNo_S : ∀ x0 : ι → ι . ∀ x1 . nat_p x105ecb.. x0 (ordsucc x1) = mul_SNo (05ecb.. x0 x1) (x0 x1) (proof)
Known mul_SNo_In_omegamul_SNo_In_omega : ∀ x0 . x0omega∀ x1 . x1omegamul_SNo x0 x1omega
Known ordsuccI1ordsuccI1 : ∀ x0 . x0ordsucc x0
Theorem 63bfe..Pi_SNo_In_omega : ∀ x0 : ι → ι . ∀ x1 . nat_p x1(∀ x2 . x2x1x0 x2omega)05ecb.. x0 x1omega (proof)
Known Subq_omega_intSubq_omega_int : omegaint
Known int_mul_SNoint_mul_SNo : ∀ x0 . x0int∀ x1 . x1intmul_SNo x0 x1int
Theorem 22c84..Pi_SNo_In_int : ∀ x0 : ι → ι . ∀ x1 . nat_p x1(∀ x2 . x2x1x0 x2int)05ecb.. x0 x1int (proof)
Known divides_int_divides_natdivides_int_divides_nat : ∀ x0 . x0omega∀ x1 . x1omegadivides_int x0 x1divides_nat x0 x1
Theorem d07df..divides_int_prime_nat_eq : ∀ x0 x1 . prime_nat x0prime_nat x1divides_int x0 x1x0 = x1 (proof)
Known Euclid_lemmaEuclid_lemma : ∀ x0 . prime_nat x0∀ x1 . x1int∀ x2 . x2intdivides_int x0 (mul_SNo x1 x2)or (divides_int x0 x1) (divides_int x0 x2)
Theorem 2326d..Euclid_lemma_Pi_SNo : ∀ x0 : ι → ι . ∀ x1 . prime_nat x1∀ x2 . nat_p x2(∀ x3 . x3x2x0 x3int)divides_int x1 (05ecb.. x0 x2)∀ x3 : ο . (∀ x4 . and (x4x2) (divides_int x1 (x0 x4))x3)x3 (proof)
Known mul_nat_mul_SNomul_nat_mul_SNo : ∀ x0 . x0omega∀ x1 . x1omegamul_nat x0 x1 = mul_SNo x0 x1
Theorem a297e..divides_nat_mul_SNo_R : ∀ x0 . x0omega∀ x1 . x1omegadivides_nat x0 (mul_SNo x0 x1) (proof)
Known mul_SNo_commul_SNo_com : ∀ x0 x1 . SNo x0SNo x1mul_SNo x0 x1 = mul_SNo x1 x0
Known omega_SNoomega_SNo : ∀ x0 . x0omegaSNo x0
Theorem a0cc9..divides_nat_mul_SNo_L : ∀ x0 . x0omega∀ x1 . x1omegadivides_nat x1 (mul_SNo x0 x1) (proof)
Known ordsuccEordsuccE : ∀ x0 x1 . x1ordsucc x0or (x1x0) (x1 = x0)
Known e4e38..divides_nat_tra : ∀ x0 x1 x2 . divides_nat x0 x1divides_nat x1 x2divides_nat x0 x2
Theorem 3899c..Pi_SNo_divides : ∀ x0 : ι → ι . ∀ x1 . nat_p x1(∀ x2 . x2x1x0 x2omega)∀ x2 . x2x1divides_nat (x0 x2) (05ecb.. x0 x1) (proof)
Theorem 9a5d6..Pi_SNo_eq : ∀ x0 x1 : ι → ι . ∀ x2 . nat_p x2(∀ x3 . x3x2x0 x3 = x1 x3)05ecb.. x0 x2 = 05ecb.. x1 x2 (proof)
Definition 168aa..nonincrfinseq := λ x0 : ι → ο . λ x1 . λ x2 : ι → ι . ∀ x3 . x3x1and (x0 (x2 x3)) (∀ x4 . x4x3SNoLe (x2 x3) (x2 x4))
Known nat_complete_indnat_complete_ind : ∀ x0 : ι → ο . (∀ x1 . nat_p x1(∀ x2 . x2x1x0 x2)x0 x1)∀ x1 . nat_p x1x0 x1
Known nat_0nat_0 : nat_p 0
Known Empty_eqEmpty_eq : ∀ x0 . (∀ x1 . nIn x1 x0)x0 = 0
Known divides_nat_divides_intdivides_nat_divides_int : ∀ x0 x1 . divides_nat x0 x1divides_int x0 x1
Known least_ordinal_exleast_ordinal_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . and (ordinal x2) (x0 x2)x1)x1)∀ x1 : ο . (∀ x2 . and (and (ordinal x2) (x0 x2)) (∀ x3 . x3x2not (x0 x3))x1)x1
Known prime_nat_divisor_exprime_nat_divisor_ex : ∀ x0 . nat_p x01x0∀ x1 : ο . (∀ x2 . and (prime_nat x2) (divides_nat x2 x0)x1)x1
Known cases_1cases_1 : ∀ x0 . x01∀ x1 : ι → ο . x1 0x1 x0
Known ordinal_SNoLt_Inordinal_SNoLt_In : ∀ x0 x1 . ordinal x0ordinal x1SNoLt x0 x1x0x1
Known mul_SNo_oneRmul_SNo_oneR : ∀ x0 . SNo x0mul_SNo x0 1 = x0
Known pos_mul_SNo_Ltpos_mul_SNo_Lt : ∀ x0 x1 x2 . SNo x0SNoLt 0 x0SNo x1SNo x2SNoLt x1 x2SNoLt (mul_SNo x0 x1) (mul_SNo x0 x2)
Known ordinal_Emptyordinal_Empty : ordinal 0
Known SNoLtLe_orSNoLtLe_or : ∀ x0 x1 . SNo x0SNo x1or (SNoLt x0 x1) (SNoLe x1 x0)
Known nat_invnat_inv : ∀ x0 . nat_p x0or (x0 = 0) (∀ x1 : ο . (∀ x2 . and (nat_p x2) (x0 = ordsucc x2)x1)x1)
Known mul_SNo_nonzero_cancelmul_SNo_nonzero_cancel_L : ∀ x0 x1 x2 . SNo x0(x0 = 0∀ x3 : ο . x3)SNo x1SNo x2mul_SNo x0 x1 = mul_SNo x0 x2x1 = x2
Known SNoLt_traSNoLt_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x0 x1SNoLt x1 x2SNoLt x0 x2
Known SNo_0SNo_0 : SNo 0
Known SNoLt_trichotomy_or_impredSNoLt_trichotomy_or_impred : ∀ x0 x1 . SNo x0SNo x1∀ x2 : ο . (SNoLt x0 x1x2)(x0 = x1x2)(SNoLt x1 x0x2)x2
Known SNoLeESNoLeE : ∀ x0 x1 . SNo x0SNo x1SNoLe x0 x1or (SNoLt x0 x1) (x0 = x1)
Known omega_nonnegomega_nonneg : ∀ x0 . x0omegaSNoLe 0 x0
Known mul_SNo_zeroRmul_SNo_zeroR : ∀ x0 . SNo x0mul_SNo x0 0 = 0
Theorem a96cd..prime_factorization_ex_uniq : ∀ x0 . nat_p x00x0∀ x1 : ο . (∀ x2 . and (x2omega) (∀ x3 : ο . (∀ x4 : ι → ι . and (and (168aa.. prime_nat x2 x4) (05ecb.. x4 x2 = x0)) (∀ x5 . x5omega∀ x6 : ι → ι . 168aa.. prime_nat x5 x605ecb.. x6 x5 = x0and (x5 = x2) (∀ x7 . x7x2x6 x7 = x4 x7))x3)x3)x1)x1 (proof)
Known orILorIL : ∀ x0 x1 : ο . x0or x0 x1
Known orIRorIR : ∀ x0 x1 : ο . x1or x0 x1
Known nat_ordsucc_in_ordsuccnat_ordsucc_in_ordsucc : ∀ x0 . nat_p x0∀ x1 . x1x0ordsucc x1ordsucc x0
Theorem 16680..nat_le2_cases : ∀ x0 . nat_p x0x02or (or (x0 = 0) (x0 = 1)) (x0 = 2) (proof)
Known 2bbf0..mul_nat_0_or_Subq : ∀ x0 . nat_p x0∀ x1 . nat_p x1or (x1 = 0) (x0mul_nat x0 x1)
Known neq_2_0neq_2_0 : 2 = 0∀ x0 : ο . x0
Known mul_nat_0Rmul_nat_0R : ∀ x0 . mul_nat x0 0 = 0
Known mul_nat_0Lmul_nat_0L : ∀ x0 . nat_p x0mul_nat 0 x0 = 0
Theorem 4e2fe..prime_nat_2_lem : ∀ x0 . nat_p x0∀ x1 . nat_p x1mul_nat x0 x1 = 2or (x0 = 1) (x0 = 2) (proof)
Known In_1_2In_1_2 : 12
Theorem 9dc41..prime_nat_2 : prime_nat 2 (proof)
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_2SNo_2 : SNo 2
Known int_SNoint_SNo : ∀ x0 . x0intSNo 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 add_SNo_cancel_Ladd_SNo_cancel_L : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2add_SNo x0 x1 = add_SNo x0 x2x1 = x2
Known SNo_add_SNoSNo_add_SNo : ∀ x0 x1 . SNo x0SNo x1SNo (add_SNo x0 x1)
Known add_SNo_rotate_3_1add_SNo_rotate_3_1 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2add_SNo x0 (add_SNo x1 x2) = add_SNo x2 (add_SNo x0 x1)
Known add_SNo_minus_L2add_SNo_minus_L2 : ∀ x0 x1 . SNo x0SNo x1add_SNo (minus_SNo x0) (add_SNo x0 x1) = x1
Known divides_int_mul_SNo_Ldivides_int_mul_SNo_L : ∀ x0 x1 x2 . x2intdivides_int x0 x1divides_int x0 (mul_SNo x1 x2)
Known int_add_SNoint_add_SNo : ∀ x0 . x0int∀ x1 . x1intadd_SNo x0 x1int
Known int_minus_SNoint_minus_SNo : ∀ x0 . x0intminus_SNo x0int
Known divides_int_refdivides_int_ref : ∀ x0 . x0intdivides_int x0 x0
Known SNo_mul_SNoSNo_mul_SNo : ∀ x0 x1 . SNo x0SNo x1SNo (mul_SNo x0 x1)
Theorem af26f..not_eq_2m_2n1 : ∀ x0 . x0int∀ x1 . x1intmul_SNo 2 x0 = add_SNo (mul_SNo 2 x1) 1∀ x2 : ο . x2 (proof)
Param div_SNodiv_SNo : ιιι
Known div_SNo_0_denumdiv_SNo_0_denum : ∀ x0 . SNo x0div_SNo x0 0 = 0
Known SNo_div_SNoSNo_div_SNo : ∀ x0 x1 . SNo x0SNo x1SNo (div_SNo x0 x1)
Known mul_div_SNo_invRmul_div_SNo_invR : ∀ x0 x1 . SNo x0SNo x1(x1 = 0∀ x2 : ο . x2)mul_SNo x1 (div_SNo x0 x1) = x0
Theorem a3726..divides_int_div_SNo_int : ∀ x0 x1 . divides_int x0 x1div_SNo x1 x0int (proof)
Known div_SNo_pos_LtLdiv_SNo_pos_LtL : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt 0 x1SNoLt x0 (mul_SNo x2 x1)SNoLt (div_SNo x0 x1) x2
Known SNoLt_0_2SNoLt_0_2 : SNoLt 0 2
Known add_SNo_Lt1_canceladd_SNo_Lt1_cancel : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt (add_SNo x0 x1) (add_SNo x2 x1)SNoLt x0 x2
Known add_SNo_minus_SNo_rinvadd_SNo_minus_SNo_rinv : ∀ x0 . SNo x0add_SNo x0 (minus_SNo x0) = 0
Known add_SNo_1_1_2add_SNo_1_1_2 : add_SNo 1 1 = 2
Known add_SNo_minus_R2add_SNo_minus_R2 : ∀ x0 x1 . SNo x0SNo x1add_SNo (add_SNo x0 x1) (minus_SNo x1) = x0
Known aa7e8..nonneg_int_nat_p : ∀ x0 . x0intSNoLe 0 x0nat_p 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 mul_div_SNo_Lmul_div_SNo_L : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2mul_SNo x2 (div_SNo x0 x1) = div_SNo (mul_SNo x2 x0) x1
Known div_mul_SNo_invLdiv_mul_SNo_invL : ∀ x0 x1 . SNo x0SNo x1(x1 = 0∀ x2 : ο . x2)div_SNo (mul_SNo x0 x1) x1 = x0
Known SNoLtLeSNoLtLe : ∀ x0 x1 . SNoLt x0 x1SNoLe x0 x1
Known div_SNo_pos_posdiv_SNo_pos_pos : ∀ x0 x1 . SNo x0SNo x1SNoLt 0 x0SNoLt 0 x1SNoLt 0 (div_SNo x0 x1)
Known mul_div_SNo_bothmul_div_SNo_both : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3mul_SNo (div_SNo x0 x1) (div_SNo x2 x3) = div_SNo (mul_SNo x0 x2) (mul_SNo x1 x3)
Known mul_SNo_pos_posmul_SNo_pos_pos : ∀ x0 x1 . SNo x0SNo x1SNoLt 0 x0SNoLt 0 x1SNoLt 0 (mul_SNo x0 x1)
Theorem 9bd18..form100_1_lem1 : ∀ x0 . nat_p x0∀ x1 . nat_p x1mul_SNo x0 x0 = mul_SNo 2 (mul_SNo x1 x1)x1 = 0 (proof)
Theorem 1129e..form100_1_lem2 : ∀ x0 . x0omega∀ x1 . x1setminus omega 1mul_SNo x0 x0 = mul_SNo 2 (mul_SNo x1 x1)∀ x2 : ο . x2 (proof)