Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrFKo../70e94..
PUNjt../a21c0..
vout
PrFKo../0f8b1.. 99.86 bars
TMMjp../e57a9.. ownership of 47d21.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMb5S../9485e.. ownership of 742df.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMPDK../da6ae.. ownership of 09f1b.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMG4B../5c7e2.. ownership of 513c0.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMcof../f0a9f.. ownership of f673c.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMPUE../3d4f7.. ownership of 9edf9.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMWG6../673f4.. ownership of 12389.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMK5J../ef8be.. ownership of 2f6be.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMJaZ../ec76a.. ownership of d3d9f.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMY2U../feada.. ownership of 7f59a.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMdFk../73b15.. ownership of 2d187.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMFmx../179b9.. ownership of 786cc.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMa9L../c550b.. ownership of bd5ca.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMM64../cea83.. ownership of 97f14.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMN8a../6f866.. ownership of 55103.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMNiM../121da.. ownership of 66895.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMR1q../34cd8.. ownership of 59ab3.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMdjG../24a97.. ownership of 596ad.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMLAk../25da7.. ownership of c8949.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMVHE../5cb3b.. ownership of bec30.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMVqF../3cbcf.. ownership of ee3a2.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMSjs../cd64a.. ownership of 4a0a3.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMam9../2db2b.. ownership of 826f0.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMZq8../7ab22.. ownership of fb5c0.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMMZG../f5293.. ownership of 8c422.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMNrF../7e92d.. ownership of 99a3c.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMJDq../ceda8.. ownership of f495c.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMYak../0d94a.. ownership of 87c96.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TML3C../124d2.. ownership of b106b.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMTUH../401cc.. ownership of de46f.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMFEv../01e09.. ownership of 9112b.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMcVD../0c8ab.. ownership of 92549.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMRsr../db364.. ownership of 64b8f.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMN5j../cc06f.. ownership of b8495.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMYf6../f3316.. ownership of b82e6.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMTgv../5c0e4.. ownership of 5638b.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMGmX../39c85.. ownership of ac69f.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMcUH../625f6.. ownership of 0b6bf.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMMFS../7ed0b.. ownership of aff59.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMYct../4e386.. ownership of 32031.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMLtH../36901.. ownership of fe2c2.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMbxh../56bbf.. ownership of 92c0a.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMSvi../447c6.. ownership of b889a.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMGkj../09244.. ownership of ea9c6.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMKfi../8f4cc.. ownership of a52ed.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMV7j../39267.. ownership of 7a57e.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMcJG../c037a.. ownership of 87731.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMJgR../b2c74.. ownership of ee483.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMNno../a03ef.. ownership of a7fcd.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMQU4../783ac.. ownership of 1942f.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMLRk../027ab.. ownership of 75e74.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMMWH../759df.. ownership of adfc5.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMHdJ../d99ca.. ownership of 9f06e.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMUgU../2fb73.. ownership of dbfbb.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMFfX../592a7.. ownership of be839.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMXEm../e56c3.. ownership of c1f47.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMWBh../54cb9.. ownership of 4f733.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMcWV../bedd1.. ownership of 72d12.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMSAr../da734.. ownership of 96eca.. as obj with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMV86../08d72.. ownership of 07ba8.. as obj with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
Pr5Zc../ef9b8.. 200.00 bars
PrBQv../b608e.. 100.00 bars
PUTs8../a81bf.. doc published by Pr5Zc..
Theorem 4f733.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))∀ x3 x4 x5 x6 . x0 x3x0 x4x0 x5x0 x6x2 (x1 x3 x4) (x1 x5 x6) = x1 (x1 (x2 x3 x5) (x2 x3 x6)) (x1 (x2 x4 x5) (x2 x4 x6)) (proof)
Theorem be839.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 . x0 x3x0 x4x0 (x2 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x1 (x1 x3 x4) x5 = x1 x3 (x1 x4 x5))∀ x3 x4 x5 x6 . x0 x3x0 x4x0 x5x0 x6x2 (x1 x3 x4) (x1 x5 x6) = x1 (x2 x3 x5) (x1 (x2 x3 x6) (x1 (x2 x4 x5) (x2 x4 x6))) (proof)
Param ordsuccordsucc : ιι
Theorem 9f06e.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))(∀ x3 x4 . x0 x3x0 x4x0 (x2 x3 x4))(∀ x3 x4 . x0 x3x0 x4x2 x3 x4 = x2 x4 x3)(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x1 (x1 x3 x4) (x1 x4 x5) = x1 x3 (x1 (x2 2 x4) x5))∀ x3 x4 . x0 x3x0 x4x2 (x1 x3 x4) (x1 x3 x4) = x1 (x2 x3 x3) (x1 (x2 2 (x2 x3 x4)) (x2 x4 x4)) (proof)
Theorem 75e74.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5))∀ x3 : ι → ι . (∀ x4 . x0 x4x0 (x3 x4))(∀ x4 x5 . x0 x4x0 x5x0 (x2 x4 x5))(∀ x4 x5 . x0 x4x0 x5x2 x4 x5 = x2 x5 x4)(∀ x4 x5 . x0 x4x0 x5x2 x4 (x3 x5) = x3 (x2 x4 x5))(∀ x4 x5 x6 . x0 x4x0 x5x0 x6x1 (x1 x4 (x3 x5)) (x1 x5 x6) = x1 x4 x6)∀ x4 x5 . x0 x4x0 x5x2 (x1 x4 x5) (x1 x4 (x3 x5)) = x1 (x2 x4 x4) (x3 (x2 x5 x5)) (proof)
Param nat_pnat_p : ιο
Param add_natadd_nat : ιιι
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
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
Definition FalseFalse := ∀ x0 : ο . x0
Known FalseEFalseE : False∀ x0 : ο . x0
Known neq_ordsucc_0neq_ordsucc_0 : ∀ x0 . ordsucc x0 = 0∀ x1 : ο . x1
Known add_nat_SRadd_nat_SR : ∀ x0 x1 . nat_p x1add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known add_nat_SLadd_nat_SL : ∀ x0 . nat_p x0∀ x1 . nat_p x1add_nat (ordsucc x0) x1 = ordsucc (add_nat x0 x1)
Known 7be16.. : ∀ x0 : ι → ο . x0 0x0 1(∀ x1 . nat_p x1x0 (ordsucc (ordsucc x1)))∀ x1 . nat_p x1x0 x1
Known neq_0_ordsuccneq_0_ordsucc : ∀ x0 . 0 = ordsucc x0∀ x1 : ο . x1
Known ordsucc_injordsucc_inj : ∀ x0 x1 . ordsucc x0 = ordsucc x1x0 = x1
Known orIRorIR : ∀ x0 x1 : ο . x1or x0 x1
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Known nat_invnat_inv : ∀ x0 . nat_p x0or (x0 = 0) (∀ x1 : ο . (∀ x2 . and (nat_p x2) (x0 = ordsucc x2)x1)x1)
Known orILorIL : ∀ x0 x1 : ο . x0or x0 x1
Param ordinalordinal : ιο
Known ordinal_ordsucc_Inordinal_ordsucc_In : ∀ x0 . ordinal x0∀ x1 . x1x0ordsucc x1ordsucc x0
Known nat_p_ordinalnat_p_ordinal : ∀ x0 . nat_p x0ordinal x0
Known nat_ordsuccnat_ordsucc : ∀ x0 . nat_p x0nat_p (ordsucc x0)
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Known ordsuccI1ordsuccI1 : ∀ x0 . x0ordsucc x0
Known In_2_3In_2_3 : 23
Theorem a7fcd.. : ∀ x0 . nat_p x0∀ x1 . nat_p x1ordsucc x1 = add_nat x0 x0or (x0x1) (and (x1 = 1) (x0 = 1)) (proof)
Param mul_natmul_nat : ιιι
Known mul_nat_SRmul_nat_SR : ∀ x0 x1 . nat_p x1mul_nat x0 (ordsucc x1) = add_nat x0 (mul_nat x0 x1)
Known nat_1nat_1 : nat_p 1
Known mul_nat_1Rmul_nat_1R : ∀ x0 . mul_nat x0 1 = x0
Known nat_0nat_0 : nat_p 0
Known cases_2cases_2 : ∀ x0 . x02∀ x1 : ι → ο . x1 0x1 1x1 x0
Known mul_nat_0Rmul_nat_0R : ∀ x0 . mul_nat x0 0 = 0
Known In_1_4In_1_4 : 14
Known In_2_4In_2_4 : 24
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 ordsuccEordsuccE : ∀ x0 x1 . x1ordsucc x0or (x1x0) (x1 = x0)
Known add_nat_Subq_Ladd_nat_Subq_R : ∀ x0 . nat_p x0∀ x1 . nat_p x1x0add_nat x0 x1
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)
Known ordsuccI2ordsuccI2 : ∀ x0 . x0ordsucc x0
Known mul_nat_pmul_nat_p : ∀ x0 . nat_p x0∀ x1 . nat_p x1nat_p (mul_nat x0 x1)
Theorem 87731.. : ∀ x0 . nat_p x0∀ x1 . x1ordsucc (ordsucc x0)ordsucc (mul_nat x1 x1)mul_nat (ordsucc (ordsucc x0)) (ordsucc (ordsucc x0)) (proof)
Definition notnot := λ x0 : ο . x0False
Definition nInnIn := λ x0 x1 . not (x0x1)
Known EmptyEEmptyE : ∀ x0 . nIn x0 0
Known Subq_traSubq_tra : ∀ x0 x1 x2 . x0x1x1x2x0x2
Known f0633.. : ∀ x0 x1 . ordinal x0ordinal x1x0x1ordsucc x0ordsucc x1
Theorem a52ed.. : ∀ x0 . nat_p x0∀ x1 . x1x0ordsucc (mul_nat x1 x1)mul_nat x0 x0 (proof)
Theorem b889a.. : ∀ x0 . nat_p x0(x0 = 1∀ x1 : ο . x1)∀ x1 . x1x0ordsucc (mul_nat x1 x1)mul_nat x0 x0 (proof)
Known nat_ordsucc_in_ordsuccnat_ordsucc_in_ordsucc : ∀ x0 . nat_p x0∀ x1 . x1x0ordsucc x1ordsucc x0
Theorem 85b3a..add_nat_In_R : ∀ x0 . nat_p x0∀ x1 . x1x0∀ x2 . nat_p x2add_nat x1 x2add_nat x0 x2 (proof)
Known nat_inv_imprednat_inv_impred : ∀ x0 : ι → ο . x0 0(∀ x1 . nat_p x1x0 (ordsucc x1))∀ x1 . nat_p x1x0 x1
Theorem fe2c2.. : ∀ x0 . nat_p x0∀ x1 . nat_p x1∀ x2 . nat_p x2add_nat x0 x1 = ordsucc x2∀ x3 . x3x0∀ x4 . x4x1add_nat x3 x4x2 (proof)
Param nat_primrecnat_primrec : ι(ιιι) → ιι
Param If_iIf_i : οιιι
Definition 96eca.. := λ x0 . nat_primrec 0 (λ x1 x2 . If_i (ordsucc x2x0) (ordsucc x2) 0)
Known nat_primrec_0nat_primrec_0 : ∀ x0 . ∀ x1 : ι → ι → ι . nat_primrec x0 x1 0 = x0
Theorem aff59.. : ∀ x0 . 96eca.. x0 0 = 0 (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)
Known If_i_1If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0If_i x0 x1 x2 = x1
Theorem ac69f.. : ∀ x0 x1 . nat_p x1ordsucc (96eca.. x0 x1)x096eca.. x0 (ordsucc x1) = ordsucc (96eca.. x0 x1) (proof)
Known If_i_0If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0If_i x0 x1 x2 = x2
Theorem b82e6.. : ∀ x0 x1 . nat_p x1nIn (ordsucc (96eca.. x0 x1)) x096eca.. x0 (ordsucc x1) = 0 (proof)
Param setminussetminus : ιιι
Param omegaomega : ι
Param SingSing : ιι
Known setminusEsetminusE : ∀ x0 x1 x2 . x2setminus x0 x1and (x2x0) (nIn x2 x1)
Known xmxm : ∀ x0 : ο . or x0 (not x0)
Known SingISingI : ∀ x0 . x0Sing x0
Known nat_0_in_ordsuccnat_0_in_ordsucc : ∀ x0 . nat_p x00ordsucc x0
Known omega_nat_pomega_nat_p : ∀ x0 . x0omeganat_p x0
Theorem 64b8f.. : ∀ x0 . x0setminus omega (Sing 0)∀ x1 . nat_p x196eca.. x0 x1x0 (proof)
Param SNoSNo : ιο
Param minus_SNominus_SNo : ιι
Param add_SNoadd_SNo : ιιι
Known minus_add_SNo_distr_3minus_add_SNo_distr_3 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2minus_SNo (add_SNo x0 (add_SNo x1 x2)) = add_SNo (minus_SNo x0) (add_SNo (minus_SNo x1) (minus_SNo x2))
Known SNo_add_SNoSNo_add_SNo : ∀ x0 x1 . SNo x0SNo x1SNo (add_SNo x0 x1)
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)
Theorem 9112b.. : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3minus_SNo (add_SNo x0 (add_SNo x1 (add_SNo x2 x3))) = add_SNo (minus_SNo x0) (add_SNo (minus_SNo x1) (add_SNo (minus_SNo x2) (minus_SNo x3))) (proof)
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)
Known minus_SNo_0minus_SNo_0 : minus_SNo 0 = 0
Known add_SNo_0Ladd_SNo_0L : ∀ x0 . SNo x0add_SNo 0 x0 = x0
Known SNo_0SNo_0 : SNo 0
Known divides_int_0divides_int_0 : ∀ x0 . x0intdivides_int x0 0
Known nat_p_intnat_p_int : ∀ x0 . nat_p x0x0int
Known add_SNo_0Radd_SNo_0R : ∀ x0 . SNo x0add_SNo x0 0 = x0
Known add_SNo_minus_R2'add_SNo_minus_R2 : ∀ x0 x1 . SNo x0SNo x1add_SNo (add_SNo x0 (minus_SNo x1)) x1 = x0
Known nat_p_SNonat_p_SNo : ∀ x0 . nat_p x0SNo x0
Known divides_int_add_SNodivides_int_add_SNo : ∀ x0 x1 x2 . divides_int x0 x1divides_int x0 x2divides_int x0 (add_SNo x1 x2)
Known ordinal_ordsucc_In_eqordinal_ordsucc_In_eq : ∀ x0 x1 . ordinal x0x1x0or (ordsucc x1x0) (x0 = ordsucc x1)
Known divides_int_refdivides_int_ref : ∀ x0 . x0intdivides_int x0 x0
Known ordinal_ordsucc_SNo_eqordinal_ordsucc_SNo_eq : ∀ x0 . ordinal x0ordsucc x0 = add_SNo 1 x0
Known SNo_1SNo_1 : SNo 1
Known add_SNo_com_4_inner_midadd_SNo_com_4_inner_mid : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3add_SNo (add_SNo x0 x1) (add_SNo x2 x3) = add_SNo (add_SNo x0 x2) (add_SNo x1 x3)
Known SNo_minus_SNoSNo_minus_SNo : ∀ x0 . SNo x0SNo (minus_SNo x0)
Known add_SNo_minus_SNo_rinvadd_SNo_minus_SNo_rinv : ∀ x0 . SNo x0add_SNo x0 (minus_SNo x0) = 0
Known ordinal_SNoordinal_SNo : ∀ x0 . ordinal x0SNo x0
Known ordinal_Heredordinal_Hered : ∀ x0 . ordinal x0∀ x1 . x1x0ordinal x1
Theorem b106b.. : ∀ x0 . x0setminus omega (Sing 0)∀ x1 . nat_p x1divides_int x0 (add_SNo x1 (minus_SNo (96eca.. x0 x1))) (proof)
Theorem f495c.. : ∀ x0 . x0setminus omega (Sing 0)∀ x1 . nat_p x196eca.. x0 x1 = 0divides_int x0 x1 (proof)
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
Known add_SNo_minus_L2add_SNo_minus_L2 : ∀ x0 x1 . SNo x0SNo x1add_SNo (minus_SNo x0) (add_SNo x0 x1) = x1
Theorem 8c422.. : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2add_SNo (add_SNo x0 (minus_SNo x1)) (add_SNo x1 x2) = add_SNo x0 x2 (proof)
Known divides_int_diff_SNo_rev : ∀ x0 x1 . x1int∀ x2 . x2intdivides_int x0 (add_SNo x1 (minus_SNo x2))divides_int x0 (add_SNo x2 (minus_SNo x1))
Known nat_p_transnat_p_trans : ∀ x0 . nat_p x0∀ x1 . x1x0nat_p x1
Theorem 826f0.. : ∀ x0 . x0setminus omega (Sing 0)∀ x1 x2 . nat_p x1nat_p x296eca.. x0 x1 = 96eca.. x0 x2divides_int x0 (add_SNo x1 (minus_SNo x2)) (proof)
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 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_mul_SNoSNo_mul_SNo : ∀ x0 x1 . SNo x0SNo x1SNo (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_minus_distrRmul_minus_SNo_distrR : ∀ x0 x1 . SNo x0SNo x1mul_SNo x0 (minus_SNo x1) = minus_SNo (mul_SNo x0 x1)
Theorem ee3a2.. : ∀ x0 x1 . SNo x0SNo x1mul_SNo (add_SNo x0 x1) (add_SNo x0 (minus_SNo x1)) = add_SNo (mul_SNo x0 x0) (minus_SNo (mul_SNo x1 x1)) (proof)
Param SNoLtSNoLt : ιιο
Known SNoLt_trichotomy_or_impredSNoLt_trichotomy_or_impred : ∀ x0 x1 . SNo x0SNo x1∀ x2 : ο . (SNoLt x0 x1x2)(x0 = x1x2)(SNoLt x1 x0x2)x2
Known SNoLt_irrefSNoLt_irref : ∀ x0 . not (SNoLt x0 x0)
Known mul_SNo_neg_negmul_SNo_neg_neg : ∀ x0 x1 . SNo x0SNo x1SNoLt x0 0SNoLt x1 0SNoLt 0 (mul_SNo x0 x1)
Known mul_SNo_neg_posmul_SNo_neg_pos : ∀ x0 x1 . SNo x0SNo x1SNoLt x0 0SNoLt 0 x1SNoLt (mul_SNo x0 x1) 0
Known mul_SNo_pos_negmul_SNo_pos_neg : ∀ x0 x1 . SNo x0SNo x1SNoLt 0 x0SNoLt x1 0SNoLt (mul_SNo x0 x1) 0
Known mul_SNo_pos_posmul_SNo_pos_pos : ∀ x0 x1 . SNo x0SNo x1SNoLt 0 x0SNoLt 0 x1SNoLt 0 (mul_SNo x0 x1)
Theorem c8949.. : ∀ x0 x1 . SNo x0SNo x1mul_SNo x0 x1 = 0or (x0 = 0) (x1 = 0) (proof)
Param divides_natdivides_nat : ιιο
Definition prime_natprime_nat := λ x0 . and (and (x0omega) (1x0)) (∀ x1 . x1omegadivides_nat x1 x0or (x1 = 1) (x1 = x0))
Known setminusIsetminusI : ∀ x0 x1 x2 . x2x0nIn x2 x1x2setminus x0 x1
Known In_no2cycleIn_no2cycle : ∀ x0 x1 . x0x1x1x0False
Known SingESingE : ∀ x0 x1 . x1Sing x0x1 = x0
Known In_0_1In_0_1 : 01
Theorem 59ab3.. : ∀ x0 . prime_nat x0x0setminus omega (Sing 0) (proof)
Param PNoLtPNoLt : ι(ιο) → ι(ιο) → ο
Param PNoEq_PNoEq_ : ι(ιο) → (ιο) → ο
Definition PNoLePNoLe := λ x0 . λ x1 : ι → ο . λ x2 . λ x3 : ι → ο . or (PNoLt x0 x1 x2 x3) (and (x0 = x2) (PNoEq_ x0 x1 x3))
Param SNoLevSNoLev : ιι
Definition SNoLeSNoLe := λ x0 x1 . PNoLe (SNoLev x0) (λ x2 . x2x0) (SNoLev x1) (λ x2 . x2x1)
Known SNoLe_traSNoLe_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x0 x1SNoLe x1 x2SNoLe x0 x2
Known nonneg_mul_SNo_Lenonneg_mul_SNo_Le : ∀ x0 x1 x2 . SNo x0SNoLe 0 x0SNo x1SNo x2SNoLe x1 x2SNoLe (mul_SNo x0 x1) (mul_SNo x0 x2)
Theorem 55103.. : ∀ x0 x1 x2 x3 . SNo x0SNoLe 0 x0SNo x1SNo x2SNo x3SNoLe 0 x3SNoLe x0 x1SNoLe x2 x3SNoLe (mul_SNo x0 x2) (mul_SNo x1 x3) (proof)
Known add_SNo_minus_SNo_linvadd_SNo_minus_SNo_linv : ∀ x0 . SNo x0add_SNo (minus_SNo x0) x0 = 0
Theorem bd5ca.. : ∀ x0 x1 . ordinal x0ordinal x1add_SNo (minus_SNo (ordsucc x0)) (ordsucc x1) = add_SNo (minus_SNo x0) x1 (proof)
Known int_SNo_casesint_SNo_cases : ∀ x0 : ι → ο . (∀ x1 . x1omegax0 x1)(∀ x1 . x1omegax0 (minus_SNo x1))∀ x1 . x1intx0 x1
Known minus_SNo_involminus_SNo_invol : ∀ x0 . SNo x0minus_SNo (minus_SNo x0) = x0
Known omega_SNoomega_SNo : ∀ x0 . x0omegaSNo x0
Known divides_int_minus_SNodivides_int_minus_SNo : ∀ x0 x1 . divides_int x0 x1divides_int x0 (minus_SNo 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_minus_minusmul_SNo_minus_minus : ∀ x0 x1 . SNo x0SNo x1mul_SNo (minus_SNo x0) (minus_SNo x1) = mul_SNo x0 x1
Known nat_complete_indnat_complete_ind : ∀ x0 : ι → ο . (∀ x1 . nat_p x1(∀ x2 . x2x1x0 x2)x0 x1)∀ x1 . nat_p x1x0 x1
Known ordinal_SNoLt_Inordinal_SNoLt_In : ∀ x0 x1 . ordinal x0ordinal x1SNoLt x0 x1x0x1
Known aa7e8..nonneg_int_nat_p : ∀ x0 . x0intSNoLe 0 x0nat_p x0
Known int_add_SNoint_add_SNo : ∀ x0 . x0int∀ x1 . x1intadd_SNo x0 x1int
Known int_minus_SNoint_minus_SNo : ∀ x0 . x0intminus_SNo x0int
Known SNoLtLeSNoLtLe : ∀ x0 x1 . SNoLt x0 x1SNoLe 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 add_SNo_Lt2add_SNo_Lt2 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x1 x2SNoLt (add_SNo x0 x1) (add_SNo x0 x2)
Known minus_SNo_Lt_contra1minus_SNo_Lt_contra1 : ∀ x0 x1 . SNo x0SNo x1SNoLt (minus_SNo x0) x1SNoLt (minus_SNo x1) x0
Known divides_int_1divides_int_1 : ∀ x0 . x0intdivides_int 1 x0
Known SNoLtLe_traSNoLtLe_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x0 x1SNoLe x1 x2SNoLt x0 x2
Known 84495.. : ∀ x0 . nat_p x0SNoLe 0 x0
Known SNoLtLe_orSNoLtLe_or : ∀ x0 x1 . SNo x0SNo x1or (SNoLt x0 x1) (SNoLe x1 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 SNoLeLt_traSNoLeLt_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x0 x1SNoLt x1 x2SNoLt x0 x2
Known mul_SNo_nonneg_nonnegmul_SNo_nonneg_nonneg : ∀ x0 x1 . SNo x0SNo x1SNoLe 0 x0SNoLe 0 x1SNoLe 0 (mul_SNo x0 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 mul_SNo_zeroRmul_SNo_zeroR : ∀ x0 . SNo x0mul_SNo x0 0 = 0
Known nat_p_omeganat_p_omega : ∀ x0 . nat_p x0x0omega
Known mul_SNo_com_3_0_1mul_SNo_com_3_0_1 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2mul_SNo x0 (mul_SNo x1 x2) = mul_SNo x1 (mul_SNo x0 x2)
Known int_SNoint_SNo : ∀ x0 . x0intSNo x0
Known divides_int_mul_SNo_Ldivides_int_mul_SNo_L : ∀ x0 x1 x2 . x2intdivides_int x0 x1divides_int x0 (mul_SNo x1 x2)
Known ordinal_In_SNoLtordinal_In_SNoLt : ∀ x0 . ordinal x0∀ x1 . x1x0SNoLt x1 x0
Known nat_transnat_trans : ∀ x0 . nat_p x0∀ x1 . x1x0x1x0
Known divides_int_divides_natdivides_int_divides_nat : ∀ x0 . x0omega∀ x1 . x1omegadivides_int x0 x1divides_nat x0 x1
Theorem 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) (proof)
Known mul_SNo_oneRmul_SNo_oneR : ∀ x0 . SNo x0mul_SNo x0 1 = x0
Known add_SNo_minus_R2add_SNo_minus_R2 : ∀ x0 x1 . SNo x0SNo x1add_SNo (add_SNo x0 x1) (minus_SNo x1) = x0
Known add_SNo_Lt3add_SNo_Lt3 : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3SNoLt x0 x2SNoLt x1 x3SNoLt (add_SNo x0 x1) (add_SNo x2 x3)
Known mul_nat_mul_SNomul_nat_mul_SNo : ∀ x0 . x0omega∀ x1 . x1omegamul_nat x0 x1 = mul_SNo x0 x1
Known add_nat_add_SNoadd_nat_add_SNo : ∀ x0 . x0omega∀ x1 . x1omegaadd_nat x0 x1 = add_SNo x0 x1
Known add_SNo_Le2add_SNo_Le2 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x1 x2SNoLe (add_SNo x0 x1) (add_SNo x0 x2)
Known minus_SNo_Le_contraminus_SNo_Le_contra : ∀ x0 x1 . SNo x0SNo x1SNoLe x0 x1SNoLe (minus_SNo x1) (minus_SNo x0)
Known add_SNo_Le1add_SNo_Le1 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x0 x2SNoLe (add_SNo x0 x1) (add_SNo x2 x1)
Theorem d3d9f.. : ∀ x0 . prime_nat x0∀ x1 . x1x0∀ x2 . x2x0divides_int x0 (add_SNo (mul_SNo x1 x1) (minus_SNo (mul_SNo x2 x2)))or (x1 = x2) (x1 = add_SNo x0 (minus_SNo x2)) (proof)
Definition odd_natodd_nat := λ x0 . and (x0omega) (∀ x1 . x1omegax0 = mul_nat 2 x1∀ x2 : ο . x2)
Known dnegdneg : ∀ x0 : ο . not (not x0)x0
Definition even_nateven_nat := λ x0 . and (x0omega) (∀ x1 : ο . (∀ x2 . and (x2omega) (x0 = mul_nat 2 x2)x1)x1)
Known odd_nat_even_nat_Sodd_nat_even_nat_S : ∀ x0 . odd_nat x0even_nat (ordsucc x0)
Known nat_2nat_2 : nat_p 2
Known d67ed.. : ∀ x0 . SNo x0mul_SNo 2 x0 = add_SNo x0 x0
Definition injinj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3x0x2 x3x1) (∀ x3 . x3x0∀ x4 . x4x0x2 x3 = x2 x4x3 = x4)
Definition atleastpatleastp := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . inj x0 x1 x3x2)x2
Known 4fb58..Pigeonhole_not_atleastp_ordsucc : ∀ x0 . nat_p x0not (atleastp (ordsucc x0) x0)
Param setsumsetsum : ιιι
Known atleastp_traatleastp_tra : ∀ x0 x1 x2 . atleastp x0 x1atleastp x1 x2atleastp x0 x2
Param equipequip : ιιο
Known equip_atleastpequip_atleastp : ∀ x0 x1 . equip x0 x1atleastp x0 x1
Known c88e0.. : ∀ x0 x1 x2 x3 . nat_p x0nat_p x1equip x0 x2equip x1 x3equip (add_nat x0 x1) (setsum x2 x3)
Known equip_refequip_ref : ∀ x0 . equip x0 x0
Param combine_funcscombine_funcs : ιι(ιι) → (ιι) → ιι
Param Inj0Inj0 : ιι
Param Inj1Inj1 : ιι
Known setsum_Inj_invsetsum_Inj_inv : ∀ x0 x1 x2 . x2setsum x0 x1or (∀ x3 : ο . (∀ x4 . and (x4x0) (x2 = Inj0 x4)x3)x3) (∀ x3 : ο . (∀ x4 . and (x4x1) (x2 = Inj1 x4)x3)x3)
Known combine_funcs_eq1combine_funcs_eq1 : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 . combine_funcs x0 x1 x2 x3 (Inj0 x4) = x2 x4
Known combine_funcs_eq2combine_funcs_eq2 : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 . combine_funcs x0 x1 x2 x3 (Inj1 x4) = x3 x4
Known add_SNo_comadd_SNo_com : ∀ x0 x1 . SNo x0SNo x1add_SNo x0 x1 = add_SNo x1 x0
Known SNo_2SNo_2 : SNo 2
Known ordinal_Emptyordinal_Empty : ordinal 0
Known add_SNo_Le3add_SNo_Le3 : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3SNoLe x0 x2SNoLe x1 x3SNoLe (add_SNo x0 x1) (add_SNo x2 x3)
Known add_SNo_minus_Lt1badd_SNo_minus_Lt1b : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x0 (add_SNo x2 x1)SNoLt (add_SNo x0 (minus_SNo x1)) x2
Known SNoLt_0_1SNoLt_0_1 : SNoLt 0 1
Known neq_1_0neq_1_0 : 1 = 0∀ x0 : ο . x0
Known SNo_zero_or_sqr_posSNo_zero_or_sqr_pos : ∀ x0 . SNo x0or (x0 = 0) (SNoLt 0 (mul_SNo x0 x0))
Known SNo_add_SNo_4SNo_add_SNo_4 : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3SNo (add_SNo x0 (add_SNo x1 (add_SNo x2 x3)))
Known SNo_add_SNo_3SNo_add_SNo_3 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNo (add_SNo x0 (add_SNo x1 x2))
Known SNo_sqr_nonnegSNo_sqr_nonneg : ∀ x0 . SNo x0SNoLe 0 (mul_SNo x0 x0)
Known SNoLe_antisymSNoLe_antisym : ∀ x0 x1 . SNo x0SNo x1SNoLe x0 x1SNoLe x1 x0x0 = x1
Known 48da5.. : SNo 4
Known 23c65.. : ∀ x0 . SNo x0mul_SNo 4 x0 = add_SNo x0 (add_SNo x0 (add_SNo x0 x0))
Known 7b468.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . SNo x0SNo x1SNo x2SNo x3SNo x4SNo x5SNo x6SNo x7SNoLe x0 x4SNoLe x1 x5SNoLe x2 x6SNoLe x3 x7SNoLe (add_SNo x0 (add_SNo x1 (add_SNo x2 x3))) (add_SNo x4 (add_SNo x5 (add_SNo x6 x7)))
Known b5021.. : ∀ x0 x1 . SNo x0SNo x1mul_SNo (add_SNo x0 (minus_SNo x1)) (add_SNo x0 (minus_SNo x1)) = add_SNo (mul_SNo x0 x0) (add_SNo (minus_SNo (mul_SNo 2 (mul_SNo x0 x1))) (mul_SNo x1 x1))
Known mul_SNo_com_4_inner_midmul_SNo_com_4_inner_mid : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3mul_SNo (mul_SNo x0 x1) (mul_SNo x2 x3) = mul_SNo (mul_SNo x0 x2) (mul_SNo x1 x3)
Known ecc46.. : mul_SNo 2 2 = 4
Known 8b4bf.. : ∀ x0 x1 . SNo x0SNo x1mul_SNo (add_SNo x0 x1) (add_SNo x0 x1) = add_SNo (mul_SNo x0 x0) (add_SNo (mul_SNo 2 (mul_SNo x0 x1)) (mul_SNo x1 x1))
Known add_SNo_assoc_4add_SNo_assoc_4 : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3add_SNo x0 (add_SNo x1 (add_SNo x2 x3)) = add_SNo (add_SNo x0 (add_SNo x1 x2)) x3
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 nat_3nat_3 : nat_p 3
Known SNoLt_traSNoLt_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x0 x1SNoLt x1 x2SNoLt x0 x2
Known SNoLt_1_2SNoLt_1_2 : SNoLt 1 2
Known divides_int_mul_SNo_Rdivides_int_mul_SNo_R : ∀ x0 x1 x2 . x2intdivides_int x0 x1divides_int x0 (mul_SNo x2 x1)
Known int_mul_SNoint_mul_SNo : ∀ x0 . x0int∀ x1 . x1intmul_SNo x0 x1int
Known add_SNo_minus_Lt1add_SNo_minus_Lt1 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt (add_SNo x0 (minus_SNo x1)) x2SNoLt x0 (add_SNo x2 x1)
Known In_irrefIn_irref : ∀ x0 . nIn x0 x0
Known add_SNo_minus_Le2badd_SNo_minus_Le2b : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe (add_SNo x2 x1) x0SNoLe x2 (add_SNo x0 (minus_SNo x1))
Known ordinal_Subq_SNoLeordinal_Subq_SNoLe : ∀ x0 x1 . ordinal x0ordinal x1x0x1SNoLe x0 x1
Known ordinal_ordsucc_In_Subqordinal_ordsucc_In_Subq : ∀ x0 . ordinal x0∀ x1 . x1x0ordsucc x1x0
Known add_SNo_1_1_2add_SNo_1_1_2 : add_SNo 1 1 = 2
Theorem 12389.. : ∀ x0 . prime_nat x0odd_nat x0∀ x1 : ο . (∀ x2 . and (x2setminus x0 (Sing 0)) (∀ x3 : ο . (∀ x4 . and (x4omega) (∀ x5 : ο . (∀ x6 . and (x6omega) (∀ x7 : ο . (∀ x8 . and (x8omega) (∀ x9 : ο . (∀ x10 . and (x10omega) (mul_SNo x2 x0 = add_SNo (mul_SNo x4 x4) (add_SNo (mul_SNo x6 x6) (add_SNo (mul_SNo x8 x8) (mul_SNo x10 x10))))x9)x9)x7)x7)x5)x5)x3)x3)x1)x1 (proof)
Known 69709.. : (∀ x0 . prime_nat x0odd_nat x0∀ x1 : ο . (∀ x2 . and (x2setminus x0 (Sing 0)) (∀ x3 : ο . (∀ x4 . and (x4omega) (∀ x5 : ο . (∀ x6 . and (x6omega) (∀ x7 : ο . (∀ x8 . and (x8omega) (∀ x9 : ο . (∀ x10 . and (x10omega) (mul_SNo x2 x0 = add_SNo (mul_SNo x4 x4) (add_SNo (mul_SNo x6 x6) (add_SNo (mul_SNo x8 x8) (mul_SNo x10 x10))))x9)x9)x7)x7)x5)x5)x3)x3)x1)x1)(∀ x0 . nat_p x0∀ x1 . x1omega∀ x2 . x2omega∀ x3 . x3omega∀ x4 . x4omegamul_SNo 2 x0 = add_SNo (mul_SNo x1 x1) (add_SNo (mul_SNo x2 x2) (add_SNo (mul_SNo x3 x3) (mul_SNo x4 x4)))∀ x5 : ο . (∀ x6 . x6omega∀ x7 . x7omega∀ x8 . x8omega∀ x9 . x9omegax0 = add_SNo (mul_SNo x6 x6) (add_SNo (mul_SNo x7 x7) (add_SNo (mul_SNo x8 x8) (mul_SNo x9 x9)))x5)x5)∀ 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
Known 36e2b.. : ∀ x0 . nat_p x0∀ x1 . x1omega∀ x2 . x2omega∀ x3 . x3omega∀ x4 . x4omegamul_SNo 2 x0 = add_SNo (mul_SNo x1 x1) (add_SNo (mul_SNo x2 x2) (add_SNo (mul_SNo x3 x3) (mul_SNo x4 x4)))∀ x5 : ο . (∀ x6 . x6omega∀ x7 . x7omega∀ x8 . x8omega∀ x9 . x9omegax0 = add_SNo (mul_SNo x6 x6) (add_SNo (mul_SNo x7 x7) (add_SNo (mul_SNo x8 x8) (mul_SNo x9 x9)))x5)x5
Theorem f673c.. : ∀ 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 (proof)
Known 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
Theorem 09f1b.. : ∀ 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)
Known mul_SNo_In_omegamul_SNo_In_omega : ∀ x0 . x0omega∀ x1 . x1omegamul_SNo x0 x1omega
Known add_SNo_In_omegaadd_SNo_In_omega : ∀ x0 . x0omega∀ x1 . x1omegaadd_SNo x0 x1omega
Theorem 47d21.. : ∀ x0 . x0omega∀ x1 : ο . (∀ x2 . and (x2omega) (∀ x3 : ο . (∀ x4 . and (x4omega) (∀ x5 : ο . (∀ x6 . and (x6omega) (∀ x7 : ο . (∀ x8 . and (x8omega) (x0 = add_nat (mul_nat x2 x2) (add_nat (mul_nat x4 x4) (add_nat (mul_nat x6 x6) (mul_nat x8 x8))))x7)x7)x5)x5)x3)x3)x1)x1 (proof)