Search for blocks/addresses/...

Proofgold Signed Transaction

vin
Pr314../31480..
PUaoA../2d008..
vout
Pr314../0a545.. 44.17 bars
TMbZk../f3ee3.. ownership of 04384.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMLPm../05633.. ownership of b397c.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMGPm../6bce3.. ownership of c1c8c.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMYzs../8d689.. ownership of 1725f.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMRx2../69b96.. ownership of 6bcc6.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMcpg../86ea0.. ownership of afb66.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMRRy../82f8c.. ownership of d5a6d.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMPET../6458c.. ownership of 1801e.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMPHj../204b2.. ownership of c6b1a.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMTWU../aff5f.. ownership of 0afb2.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMYqS../703de.. ownership of 15814.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMSSZ../580ce.. ownership of c79d0.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMKQs../567d7.. ownership of 6c1cd.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMd1v../50df2.. ownership of 40638.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMcDC../2ae97.. ownership of c5c4d.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMSTi../9cdca.. ownership of 016da.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMMsG../536fb.. ownership of d04ad.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMboi../16d5d.. ownership of 33c12.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMa8q../86163.. ownership of 95a41.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMWQ9../c59c5.. ownership of d59bf.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMY2W../50e44.. ownership of 8db9d.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMTXt../e52ff.. ownership of abda0.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMNmC../f4161.. ownership of a2bb4.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMZQJ../19cc8.. ownership of 955f6.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMHu4../a9a5d.. ownership of b09b9.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMHoo../59bb7.. ownership of db687.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
PUS8F../72a16.. doc published by PrQUS..
Param SNoSNo : ιο
Param SNoLeSNoLe : ιιο
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Param sqrt_SNo_nonnegsqrt_SNo_nonneg : ιι
Param mul_SNomul_SNo : ιιι
Param SNoS_SNoS_ : ιι
Param SNoLevSNoLev : ιι
Known SNoLev_indSNoLev_ind : ∀ x0 : ι → ο . (∀ x1 . SNo x1(∀ x2 . x2SNoS_ (SNoLev x1)x0 x2)x0 x1)∀ x1 . SNo x1x0 x1
Param SNoCutSNoCut : ιιι
Param famunionfamunion : ι(ιι) → ι
Param omegaomega : ι
Param apap : ιιι
Param SNo_sqrtauxSNo_sqrtaux : ι(ιι) → ιι
Param ordsuccordsucc : ιι
Known sqrt_SNo_nonneg_eqsqrt_SNo_nonneg_eq : ∀ x0 . SNo x0sqrt_SNo_nonneg x0 = SNoCut (famunion omega (λ x2 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x2) 0)) (famunion omega (λ x2 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x2) 1))
Param SNoLtSNoLt : ιιο
Param nat_pnat_p : ιο
Definition SNoCutPSNoCutP := λ x0 x1 . and (and (∀ x2 . x2x0SNo x2) (∀ x2 . x2x1SNo x2)) (∀ x2 . x2x0∀ x3 . x3x1SNoLt x2 x3)
Known sqrt_SNo_nonneg_prop1bsqrt_SNo_nonneg_prop1b : ∀ x0 . SNo x0SNoLe 0 x0(∀ x1 . nat_p x1and (∀ x2 . x2ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 0and (and (SNo x2) (SNoLe 0 x2)) (SNoLt (mul_SNo x2 x2) x0)) (∀ x2 . x2ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 1and (and (SNo x2) (SNoLe 0 x2)) (SNoLt x0 (mul_SNo x2 x2))))SNoCutP (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 0)) (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 1))
Known sqrt_SNo_nonneg_prop1asqrt_SNo_nonneg_prop1a : ∀ x0 . SNo x0SNoLe 0 x0(∀ x1 . x1SNoS_ (SNoLev x0)SNoLe 0 x1and (and (SNo (sqrt_SNo_nonneg x1)) (SNoLe 0 (sqrt_SNo_nonneg x1))) (mul_SNo (sqrt_SNo_nonneg x1) (sqrt_SNo_nonneg x1) = x1))∀ x1 . nat_p x1and (∀ x2 . x2ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 0and (and (SNo x2) (SNoLe 0 x2)) (SNoLt (mul_SNo x2 x2) x0)) (∀ x2 . x2ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 1and (and (SNo x2) (SNoLe 0 x2)) (SNoLt x0 (mul_SNo x2 x2)))
Param binunionbinunion : ιιι
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Param SNoEq_SNoEq_ : ιιιο
Known SNoCutP_SNoCut_impredSNoCutP_SNoCut_impred : ∀ x0 x1 . SNoCutP x0 x1∀ x2 : ο . (SNo (SNoCut x0 x1)SNoLev (SNoCut x0 x1)ordsucc (binunion (famunion x0 (λ x3 . ordsucc (SNoLev x3))) (famunion x1 (λ x3 . ordsucc (SNoLev x3))))(∀ x3 . x3x0SNoLt x3 (SNoCut x0 x1))(∀ x3 . x3x1SNoLt (SNoCut x0 x1) x3)(∀ x3 . SNo x3(∀ x4 . x4x0SNoLt x4 x3)(∀ x4 . x4x1SNoLt x3 x4)and (SNoLev (SNoCut x0 x1)SNoLev x3) (SNoEq_ (SNoLev (SNoCut x0 x1)) (SNoCut x0 x1) x3))x2)x2
Known and3Iand3I : ∀ x0 x1 x2 : ο . x0x1x2and (and x0 x1) x2
Known sqrt_SNo_nonneg_prop1csqrt_SNo_nonneg_prop1c : ∀ x0 . SNo x0SNoLe 0 x0SNoCutP (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 0)) (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 1))(∀ x1 . x1famunion omega (λ x2 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x2) 1)∀ x2 : ο . (SNo x1SNoLe 0 x1SNoLt x0 (mul_SNo x1 x1)x2)x2)SNoLe 0 (SNoCut (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 0)) (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 1)))
Known SNoLt_trichotomy_or_impredSNoLt_trichotomy_or_impred : ∀ x0 x1 . SNo x0SNo x1∀ x2 : ο . (SNoLt x0 x1x2)(x0 = x1x2)(SNoLt x1 x0x2)x2
Known SNo_mul_SNoSNo_mul_SNo : ∀ x0 x1 . SNo x0SNo x1SNo (mul_SNo x0 x1)
Definition FalseFalse := ∀ x0 : ο . x0
Known FalseEFalseE : False∀ x0 : ο . x0
Known sqrt_SNo_nonneg_prop1dsqrt_SNo_nonneg_prop1d : ∀ x0 . SNo x0SNoLe 0 x0(∀ x1 . x1SNoS_ (SNoLev x0)SNoLe 0 x1and (and (SNo (sqrt_SNo_nonneg x1)) (SNoLe 0 (sqrt_SNo_nonneg x1))) (mul_SNo (sqrt_SNo_nonneg x1) (sqrt_SNo_nonneg x1) = x1))SNoCutP (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 0)) (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 1))SNoLe 0 (SNoCut (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 0)) (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 1)))SNoLt (mul_SNo (SNoCut (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 0)) (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 1))) (SNoCut (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 0)) (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 1)))) x0False
Known sqrt_SNo_nonneg_prop1esqrt_SNo_nonneg_prop1e : ∀ x0 . SNo x0SNoLe 0 x0(∀ x1 . x1SNoS_ (SNoLev x0)SNoLe 0 x1and (and (SNo (sqrt_SNo_nonneg x1)) (SNoLe 0 (sqrt_SNo_nonneg x1))) (mul_SNo (sqrt_SNo_nonneg x1) (sqrt_SNo_nonneg x1) = x1))SNoCutP (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 0)) (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 1))SNoLe 0 (SNoCut (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 0)) (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 1)))SNoLt x0 (mul_SNo (SNoCut (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 0)) (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 1))) (SNoCut (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 0)) (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 1))))False
Known famunionE_impredfamunionE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2famunion x0 x1∀ x3 : ο . (∀ x4 . x4x0x2x1 x4x3)x3
Known omega_nat_pomega_nat_p : ∀ x0 . x0omeganat_p x0
Theorem sqrt_SNo_nonneg_prop1sqrt_SNo_nonneg_prop1 : ∀ x0 . SNo x0SNoLe 0 x0and (and (SNo (sqrt_SNo_nonneg x0)) (SNoLe 0 (sqrt_SNo_nonneg x0))) (mul_SNo (sqrt_SNo_nonneg x0) (sqrt_SNo_nonneg x0) = x0) (proof)
Param ordinalordinal : ιο
Param SNo_SNo_ : ιιο
Known SNoS_E2SNoS_E2 : ∀ x0 . ordinal x0∀ x1 . x1SNoS_ x0∀ x2 : ο . (SNoLev x1x0ordinal (SNoLev x1)SNo x1SNo_ (SNoLev x1) x1x2)x2
Known SNoLev_ordinalSNoLev_ordinal : ∀ x0 . SNo x0ordinal (SNoLev x0)
Theorem SNo_sqrtaux_0_1_propSNo_sqrtaux_0_1_prop : ∀ x0 . SNo x0SNoLe 0 x0∀ x1 . nat_p x1and (∀ x2 . x2ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 0and (and (SNo x2) (SNoLe 0 x2)) (SNoLt (mul_SNo x2 x2) x0)) (∀ x2 . x2ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 1and (and (SNo x2) (SNoLe 0 x2)) (SNoLt x0 (mul_SNo x2 x2))) (proof)
Theorem SNo_sqrtaux_0_propSNo_sqrtaux_0_prop : ∀ x0 . SNo x0SNoLe 0 x0∀ x1 . nat_p x1∀ x2 . x2ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 0and (and (SNo x2) (SNoLe 0 x2)) (SNoLt (mul_SNo x2 x2) x0) (proof)
Theorem SNo_sqrtaux_1_propSNo_sqrtaux_1_prop : ∀ x0 . SNo x0SNoLe 0 x0∀ x1 . nat_p x1∀ x2 . x2ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 1and (and (SNo x2) (SNoLe 0 x2)) (SNoLt x0 (mul_SNo x2 x2)) (proof)
Theorem SNo_sqrt_SNo_SNoCutPSNo_sqrt_SNo_SNoCutP : ∀ x0 . SNo x0SNoLe 0 x0SNoCutP (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 0)) (famunion omega (λ x1 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x1) 1)) (proof)
Theorem SNo_sqrt_SNo_nonnegSNo_sqrt_SNo_nonneg : ∀ x0 . SNo x0SNoLe 0 x0SNo (sqrt_SNo_nonneg x0) (proof)
Theorem sqrt_SNo_nonneg_nonnegsqrt_SNo_nonneg_nonneg : ∀ x0 . SNo x0SNoLe 0 x0SNoLe 0 (sqrt_SNo_nonneg x0) (proof)
Theorem sqrt_SNo_nonneg_sqrsqrt_SNo_nonneg_sqr : ∀ x0 . SNo x0SNoLe 0 x0mul_SNo (sqrt_SNo_nonneg x0) (sqrt_SNo_nonneg x0) = x0 (proof)
Known SNo_0SNo_0 : SNo 0
Definition notnot := λ x0 : ο . x0False
Definition nInnIn := λ x0 x1 . not (x0x1)
Known Empty_eqEmpty_eq : ∀ x0 . (∀ x1 . nIn x1 x0)x0 = 0
Known EmptyEEmptyE : ∀ x0 . nIn x0 0
Known SNoCut_0_0SNoCut_0_0 : SNoCut 0 0 = 0
Known nat_indnat_ind : ∀ x0 : ι → ο . x0 0(∀ x1 . nat_p x1x0 x1x0 (ordsucc x1))∀ x1 . nat_p x1x0 x1
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Param lamSigma : ι(ιι) → ι
Param If_iIf_i : οιιι
Param SepSep : ι(ιο) → ι
Param SNoLSNoL : ιι
Definition SNoL_nonnegSNoL_nonneg := λ x0 . Sep (SNoL x0) (SNoLe 0)
Param SNoRSNoR : ιι
Known SNo_sqrtaux_0SNo_sqrtaux_0 : ∀ x0 . ∀ x1 : ι → ι . SNo_sqrtaux x0 x1 0 = lam 2 (λ x3 . If_i (x3 = 0) (prim5 (SNoL_nonneg x0) x1) (prim5 (SNoR x0) x1))
Known tuple_2_0_eqtuple_2_0_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 0 = x0
Known SNoL_nonneg_0SNoL_nonneg_0 : SNoL_nonneg 0 = 0
Known Repl_EmptyRepl_Empty : ∀ x0 : ι → ι . prim5 0 x0 = 0
Known tuple_2_1_eqtuple_2_1_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 1 = x1
Known SNoR_0SNoR_0 : SNoR 0 = 0
Param SNo_sqrtauxsetSNo_sqrtauxset : ιιιι
Known SNo_sqrtaux_SSNo_sqrtaux_S : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . nat_p x2SNo_sqrtaux x0 x1 (ordsucc x2) = lam 2 (λ x4 . If_i (x4 = 0) (binunion (ap (SNo_sqrtaux x0 x1 x2) 0) (SNo_sqrtauxset (ap (SNo_sqrtaux x0 x1 x2) 0) (ap (SNo_sqrtaux x0 x1 x2) 1) x0)) (binunion (binunion (ap (SNo_sqrtaux x0 x1 x2) 1) (SNo_sqrtauxset (ap (SNo_sqrtaux x0 x1 x2) 0) (ap (SNo_sqrtaux x0 x1 x2) 0) x0)) (SNo_sqrtauxset (ap (SNo_sqrtaux x0 x1 x2) 1) (ap (SNo_sqrtaux x0 x1 x2) 1) x0)))
Known SNo_sqrtauxset_0SNo_sqrtauxset_0 : ∀ x0 x1 . SNo_sqrtauxset 0 x0 x1 = 0
Known binunion_idlbinunion_idl : ∀ x0 . binunion 0 x0 = x0
Theorem sqrt_SNo_nonneg_0sqrt_SNo_nonneg_0 : sqrt_SNo_nonneg 0 = 0 (proof)
Known SNo_1SNo_1 : SNo 1
Known set_extset_ext : ∀ x0 x1 . x0x1x1x0x0 = x1
Known cases_1cases_1 : ∀ x0 . x01∀ x1 : ι → ο . x1 0x1 x0
Known famunionIfamunionI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2x0x3x1 x2x3famunion x0 x1
Known nat_p_omeganat_p_omega : ∀ x0 . nat_p x0x0omega
Known nat_0nat_0 : nat_p 0
Known In_0_1In_0_1 : 01
Known SNoL_1SNoL_1 : SNoL 1 = 1
Known SNoR_1SNoR_1 : SNoR 1 = 0
Known SNo_etaSNo_eta : ∀ x0 . SNo x0x0 = SNoCut (SNoL x0) (SNoR x0)
Known SNoL_nonneg_1SNoL_nonneg_1 : SNoL_nonneg 1 = 1
Known ReplE_impredReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2prim5 x0 x1∀ x3 : ο . (∀ x4 . x4x0x2 = x1 x4x3)x3
Known ReplIReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2x0x1 x2prim5 x0 x1
Known SNo_sqrtauxset_0'SNo_sqrtauxset_0 : ∀ x0 x1 . SNo_sqrtauxset x0 0 x1 = 0
Known binunion_idrbinunion_idr : ∀ x0 . binunion x0 0 = x0
Param add_SNoadd_SNo : ιιι
Param div_SNodiv_SNo : ιιι
Known SNo_sqrtauxset_ESNo_sqrtauxset_E : ∀ x0 x1 x2 x3 . x3SNo_sqrtauxset x0 x1 x2∀ x4 : ο . (∀ x5 . x5x0∀ x6 . x6x1SNoLt 0 (add_SNo x5 x6)x3 = div_SNo (add_SNo x2 (mul_SNo x5 x6)) (add_SNo x5 x6)x4)x4
Known add_SNo_0Radd_SNo_0R : ∀ x0 . SNo x0add_SNo x0 0 = x0
Known SNoLt_irrefSNoLt_irref : ∀ x0 . not (SNoLt x0 x0)
Theorem sqrt_SNo_nonneg_1sqrt_SNo_nonneg_1 : sqrt_SNo_nonneg 1 = 1 (proof)
Known SepISepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2x0x1 x2x2Sep x0 x1
Known SNoL_ISNoL_I : ∀ x0 . SNo x0∀ x1 . SNo x1SNoLev x1SNoLev x0SNoLt x1 x0x1SNoL x0
Known SNoLev_0SNoLev_0 : SNoLev 0 = 0
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Known SNoLeESNoLeE : ∀ x0 x1 . SNo x0SNo x1SNoLe x0 x1or (SNoLt x0 x1) (x0 = x1)
Known SNoLe_refSNoLe_ref : ∀ x0 . SNoLe x0 x0
Theorem sqrt_SNo_nonneg_0inL0sqrt_SNo_nonneg_0inL0 : ∀ x0 . SNo x0SNoLe 0 x00SNoLev x00ap (SNo_sqrtaux x0 sqrt_SNo_nonneg 0) 0 (proof)
Theorem sqrt_SNo_nonneg_Lnonemptysqrt_SNo_nonneg_Lnonempty : ∀ x0 . SNo x0SNoLe 0 x00SNoLev x0famunion omega (λ x2 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x2) 0) = 0∀ x1 : ο . x1 (proof)
Known SNoR_ISNoR_I : ∀ x0 . SNo x0∀ x1 . SNo x1SNoLev x1SNoLev x0SNoLt x0 x1x1SNoR x0
Known ordinal_SNoLevordinal_SNoLev : ∀ x0 . ordinal x0SNoLev x0 = x0
Known nat_p_ordinalnat_p_ordinal : ∀ x0 . nat_p x0ordinal x0
Known nat_1nat_1 : nat_p 1
Known In_irrefIn_irref : ∀ x0 . nIn x0 x0
Known binunionI1binunionI1 : ∀ x0 x1 x2 . x2x0x2binunion x0 x1
Known binunionI2binunionI2 : ∀ x0 x1 x2 . x2x1x2binunion x0 x1
Known SNo_sqrtauxset_ISNo_sqrtauxset_I : ∀ x0 x1 x2 x3 . x3x0∀ x4 . x4x1SNoLt 0 (add_SNo x3 x4)div_SNo (add_SNo x2 (mul_SNo x3 x4)) (add_SNo x3 x4)SNo_sqrtauxset x0 x1 x2
Known SNoLtLeSNoLtLe : ∀ x0 x1 . SNoLt x0 x1SNoLe x0 x1
Known SNoLt_0_1SNoLt_0_1 : SNoLt 0 1
Definition TransSetTransSet := λ x0 . ∀ x1 . x1x0x1x0
Known ordinal_TransSetordinal_TransSet : ∀ x0 . ordinal x0TransSet x0
Theorem sqrt_SNo_nonneg_Rnonemptysqrt_SNo_nonneg_Rnonempty : ∀ x0 . SNo x0SNoLe 0 x01SNoLev x0famunion omega (λ x2 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x2) 1) = 0∀ x1 : ο . x1 (proof)