Search for blocks/addresses/...

Proofgold Address

address
PUa4WXcxspLSe9swy7dbMAJaZMUQ1PPebvL
total
0
mg
-
conjpub
-
current assets
50d4b../ab11c.. bday: 5731 doc published by Pr6Pc..
Param explicit_Natsexplicit_Nats : ιι(ιι) → ο
Param explicit_Nats_primrecexplicit_Nats_primrec : ιι(ιι) → ι(ιιι) → ιι
Known explicit_Nats_Eexplicit_Nats_E : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ο . (explicit_Nats x0 x1 x2x1x0(∀ x4 . x4x0x2 x4x0)(∀ x4 . x4x0x2 x4 = x1∀ x5 : ο . x5)(∀ x4 . x4x0∀ x5 . x5x0x2 x4 = x2 x5x4 = x5)(∀ x4 : ι → ο . x4 x1(∀ x5 . x4 x5x4 (x2 x5))∀ x5 . x5x0x4 x5)x3)explicit_Nats x0 x1 x2x3
Known explicit_Nats_indexplicit_Nats_ind : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2∀ x3 : ι → ο . x3 x1(∀ x4 . x4x0x3 x4x3 (x2 x4))∀ x4 . x4x0x3 x4
Known explicit_Nats_primrec_baseexplicit_Nats_primrec_base : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 . ∀ x4 : ι → ι → ι . explicit_Nats x0 x1 x2explicit_Nats_primrec x0 x1 x2 x3 x4 x1 = x3
Known explicit_Nats_primrec_Sexplicit_Nats_primrec_S : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 . ∀ x4 : ι → ι → ι . explicit_Nats x0 x1 x2∀ x5 . x5x0explicit_Nats_primrec x0 x1 x2 x3 x4 (x2 x5) = x4 x5 (explicit_Nats_primrec x0 x1 x2 x3 x4 x5)
Theorem explicit_Nats_primrec_Pexplicit_Nats_primrec_P : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2∀ x3 : ι → ο . ∀ x4 . x3 x4∀ x5 : ι → ι → ι . (∀ x6 . x6x0∀ x7 . x3 x7x3 (x5 x6 x7))∀ x6 . x6x0x3 (explicit_Nats_primrec x0 x1 x2 x4 x5 x6) (proof)
Definition explicit_Nats_zero_plusexplicit_Nats_zero_plus := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 . explicit_Nats_primrec x0 x1 x2 x4 (λ x5 . x2) x3
Definition explicit_Nats_zero_multexplicit_Nats_zero_mult := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 . explicit_Nats_primrec x0 x1 x2 x1 (λ x5 . explicit_Nats_zero_plus x0 x1 x2 x4) x3
Theorem explicit_Nats_zero_plus_Nexplicit_Nats_zero_plus_N : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2∀ x3 . x3x0∀ x4 . x4x0explicit_Nats_zero_plus x0 x1 x2 x3 x4x0 (proof)
Theorem explicit_Nats_zero_mult_Nexplicit_Nats_zero_mult_N : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2∀ x3 . x3x0∀ x4 . x4x0explicit_Nats_zero_mult x0 x1 x2 x3 x4x0 (proof)
Known explicit_Nats_zero_plus_0Lexplicit_Nats_zero_plus_0L : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2∀ x3 . x3x0explicit_Nats_zero_plus x0 x1 x2 x1 x3 = x3
Known explicit_Nats_zero_plus_SLexplicit_Nats_zero_plus_SL : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2∀ x3 . x3x0∀ x4 . x4x0explicit_Nats_zero_plus x0 x1 x2 (x2 x3) x4 = x2 (explicit_Nats_zero_plus x0 x1 x2 x3 x4)
Known explicit_Nats_zero_mult_0Lexplicit_Nats_zero_mult_0L : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2∀ x3 . x3x0explicit_Nats_zero_mult x0 x1 x2 x1 x3 = x1
Known explicit_Nats_zero_mult_SLexplicit_Nats_zero_mult_SL : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2∀ x3 . x3x0∀ x4 . x4x0explicit_Nats_zero_mult x0 x1 x2 (x2 x3) x4 = explicit_Nats_zero_plus x0 x1 x2 x4 (explicit_Nats_zero_mult x0 x1 x2 x3 x4)
Definition explicit_Nats_one_plusexplicit_Nats_one_plus := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 . explicit_Nats_primrec x0 x1 x2 (x2 x4) (λ x5 . x2) x3
Theorem explicit_Nats_one_plus_Nexplicit_Nats_one_plus_N : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2∀ x3 . x3x0∀ x4 . x4x0explicit_Nats_one_plus x0 x1 x2 x3 x4x0 (proof)
Definition explicit_Nats_one_multexplicit_Nats_one_mult := λ x0 x1 . λ x2 : ι → ι . λ x3 x4 . explicit_Nats_primrec x0 x1 x2 x4 (λ x5 . explicit_Nats_one_plus x0 x1 x2 x4) x3
Theorem explicit_Nats_one_mult_Nexplicit_Nats_one_mult_N : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2∀ x3 . x3x0∀ x4 . x4x0explicit_Nats_one_mult x0 x1 x2 x3 x4x0 (proof)
Definition explicit_Nats_one_expexplicit_Nats_one_exp := λ x0 x1 . λ x2 : ι → ι . λ x3 . explicit_Nats_primrec x0 x1 x2 x3 (λ x4 . explicit_Nats_one_mult x0 x1 x2 x3)
Theorem explicit_Nats_one_exp_Nexplicit_Nats_one_exp_N : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2∀ x3 . x3x0∀ x4 . x4x0explicit_Nats_one_exp x0 x1 x2 x3 x4x0 (proof)
Known explicit_Nats_one_plus_1Lexplicit_Nats_one_plus_1L : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2∀ x3 . x3x0explicit_Nats_one_plus x0 x1 x2 x1 x3 = x2 x3
Known explicit_Nats_one_plus_SLexplicit_Nats_one_plus_SL : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2∀ x3 . x3x0∀ x4 . x4x0explicit_Nats_one_plus x0 x1 x2 (x2 x3) x4 = x2 (explicit_Nats_one_plus x0 x1 x2 x3 x4)
Known explicit_Nats_one_mult_1Lexplicit_Nats_one_mult_1L : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2∀ x3 . x3x0explicit_Nats_one_mult x0 x1 x2 x1 x3 = x3
Known explicit_Nats_one_mult_SLexplicit_Nats_one_mult_SL : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2∀ x3 . x3x0∀ x4 . x4x0explicit_Nats_one_mult x0 x1 x2 (x2 x3) x4 = explicit_Nats_one_plus x0 x1 x2 x4 (explicit_Nats_one_mult x0 x1 x2 x3 x4)
Known explicit_Nats_one_exp_1Lexplicit_Nats_one_exp_1L : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2∀ x3 . x3x0explicit_Nats_one_exp x0 x1 x2 x3 x1 = x3
Known explicit_Nats_one_exp_SLexplicit_Nats_one_exp_SL : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2∀ x3 . x3x0∀ x4 . x4x0explicit_Nats_one_exp x0 x1 x2 x3 (x2 x4) = explicit_Nats_one_mult x0 x1 x2 x3 (explicit_Nats_one_exp x0 x1 x2 x3 x4)
Theorem AssocComm_identitiesAssocComm_identities : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x0)(∀ x2 . x2x0∀ x3 . x3x0∀ x4 . x4x0x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3 = x1 x3 x2)∀ x2 : ο . ((∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0x1 x3 (x1 x4 x5) = x1 x4 (x1 x3 x5))(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0x1 x3 (x1 x4 x5) = x1 x5 (x1 x3 x4))(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0x1 (x1 x3 x4) (x1 x5 x6) = x1 (x1 x3 x5) (x1 x4 x6))(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0x1 x3 (x1 x4 (x1 x5 x6)) = x1 x6 (x1 x3 (x1 x4 x5)))(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0x1 x3 (x1 x4 (x1 x5 x6)) = x1 x5 (x1 x6 (x1 x3 x4)))x2)x2 (proof)
Param explicit_Fieldexplicit_Field : ιιι(ιιι) → (ιιι) → ο
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Known explicit_Field_Eexplicit_Field_E : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ο . (explicit_Field x0 x1 x2 x3 x4(∀ x6 . x6x0∀ x7 . x7x0x3 x6 x7x0)(∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0x3 x6 (x3 x7 x8) = x3 (x3 x6 x7) x8)(∀ x6 . x6x0∀ x7 . x7x0x3 x6 x7 = x3 x7 x6)x1x0(∀ x6 . x6x0x3 x1 x6 = x6)(∀ x6 . x6x0∀ x7 : ο . (∀ x8 . and (x8x0) (x3 x6 x8 = x1)x7)x7)(∀ x6 . x6x0∀ x7 . x7x0x4 x6 x7x0)(∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0x4 x6 (x4 x7 x8) = x4 (x4 x6 x7) x8)(∀ x6 . x6x0∀ x7 . x7x0x4 x6 x7 = x4 x7 x6)x2x0(x2 = x1∀ x6 : ο . x6)(∀ x6 . x6x0x4 x2 x6 = x6)(∀ x6 . x6x0(x6 = x1∀ x7 : ο . x7)∀ x7 : ο . (∀ x8 . and (x8x0) (x4 x6 x8 = x2)x7)x7)(∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0x4 x6 (x3 x7 x8) = x3 (x4 x6 x7) (x4 x6 x8))x5)explicit_Field x0 x1 x2 x3 x4x5
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Known xmxm : ∀ x0 : ο . or x0 (not x0)
Known orIRorIR : ∀ x0 x1 : ο . x1or x0 x1
Known orILorIL : ∀ x0 x1 : ο . x0or x0 x1
Known explicit_Field_zero_multLexplicit_Field_zero_multL : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . x5x0x4 x1 x5 = x1
Theorem explicit_Field_mult_zero_invexplicit_Field_mult_zero_inv : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . x5x0∀ x6 . x6x0x4 x5 x6 = x1or (x5 = x1) (x6 = x1) (proof)
Param explicit_OrderedFieldexplicit_OrderedField : ιιι(ιιι) → (ιιι) → (ιιο) → ο
Definition iffiff := λ x0 x1 : ο . and (x0x1) (x1x0)
Known explicit_OrderedField_Eexplicit_OrderedField_E : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . ∀ x6 : ο . (explicit_OrderedField x0 x1 x2 x3 x4 x5explicit_Field x0 x1 x2 x3 x4(∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0x5 x7 x8x5 x8 x9x5 x7 x9)(∀ x7 . x7x0∀ x8 . x8x0iff (and (x5 x7 x8) (x5 x8 x7)) (x7 = x8))(∀ x7 . x7x0∀ x8 . x8x0or (x5 x7 x8) (x5 x8 x7))(∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0x5 x7 x8x5 (x3 x7 x9) (x3 x8 x9))(∀ x7 . x7x0∀ x8 . x8x0x5 x1 x7x5 x1 x8x5 x1 (x4 x7 x8))x6)explicit_OrderedField x0 x1 x2 x3 x4 x5x6
Theorem explicit_OrderedField_leq_reflexplicit_OrderedField_leq_refl : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_OrderedField x0 x1 x2 x3 x4 x5∀ x6 . x6x0x5 x6 x6 (proof)
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Theorem explicit_OrderedField_leq_antisymexplicit_OrderedField_leq_antisym : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_OrderedField x0 x1 x2 x3 x4 x5∀ x6 . x6x0∀ x7 . x7x0x5 x6 x7x5 x7 x6x6 = x7 (proof)
Theorem explicit_OrderedField_leq_traexplicit_OrderedField_leq_tra : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_OrderedField x0 x1 x2 x3 x4 x5∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0x5 x6 x7x5 x7 x8x5 x6 x8 (proof)
Known explicit_OrderedField_square_nonnegexplicit_OrderedField_square_nonneg : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_OrderedField x0 x1 x2 x3 x4 x5∀ x6 . x6x0x5 x1 (x4 x6 x6)
Theorem explicit_OrderedField_leq_zero_oneexplicit_OrderedField_leq_zero_one : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_OrderedField x0 x1 x2 x3 x4 x5x5 x1 x2 (proof)
Param SepSep : ι(ιο) → ι
Definition natOfOrderedField_pnatOfOrderedField_p := λ x0 x1 x2 . λ x3 x4 : ι → ι → ι . λ x5 : ι → ι → ο . λ x6 . ∀ x7 : ι → ο . x7 x1(∀ x8 . x7 x8x7 (x3 x8 x2))x7 x6
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Known explicit_Nats_Iexplicit_Nats_I : ∀ x0 x1 . ∀ x2 : ι → ι . x1x0(∀ x3 . x3x0x2 x3x0)(∀ x3 . x3x0x2 x3 = x1∀ x4 : ο . x4)(∀ x3 . x3x0∀ x4 . x4x0x2 x3 = x2 x4x3 = x4)(∀ x3 : ι → ο . x3 x1(∀ x4 . x3 x4x3 (x2 x4))∀ x4 . x4x0x3 x4)explicit_Nats x0 x1 x2
Known SepISepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2x0x1 x2x2Sep x0 x1
Known SepESepE : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2Sep x0 x1and (x2x0) (x1 x2)
Known explicit_Field_plus_cancelRexplicit_Field_plus_cancelR : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0x3 x5 x7 = x3 x6 x7x5 = x6
Known FalseEFalseE : False∀ x0 : ο . x0
Known explicit_Nats_natOfOrderedFieldexplicit_Nats_natOfOrderedField : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_OrderedField x0 x1 x2 x3 x4 x5explicit_Nats (Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)) x1 (λ x6 . x3 x6 x2)
Known Sep_SubqSep_Subq : ∀ x0 . ∀ x1 : ι → ο . Sep x0 x1x0
Theorem explicit_PosNats_natOfOrderedFieldexplicit_PosNats_natOfOrderedField : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_OrderedField x0 x1 x2 x3 x4 x5explicit_Nats {x6 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x6 = x1∀ x7 : ο . x7} x2 (λ x6 . x3 x6 x2) (proof)
Param explicit_Field_minusexplicit_Field_minus : ιιι(ιιι) → (ιιι) → ιι
Definition explicit_OrderedField_rationalpexplicit_OrderedField_rationalp := λ x0 x1 x2 . λ x3 x4 : ι → ι → ι . λ x5 : ι → ι → ο . λ x6 . ∀ x7 : ο . (∀ x8 . and (x8{x9 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x9{x10 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x10 = x1∀ x11 : ο . x11}) (x9 = x1)) (x9{x10 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x10 = x1∀ x11 : ο . x11})}) (∀ x9 : ο . (∀ x10 . and (x10{x11 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x11 = x1∀ x12 : ο . x12}) (x4 x10 x6 = x8)x9)x9)x7)x7
Known explicit_Field_dist_Rexplicit_Field_dist_R : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0x4 (x3 x5 x6) x7 = x3 (x4 x5 x7) (x4 x6 x7)
Theorem explicit_OrderedField_Npos_propsexplicit_OrderedField_Npos_props : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_OrderedField x0 x1 x2 x3 x4 x5∀ x6 : ο . ({x7 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x7 = x1∀ x8 : ο . x8}x0explicit_Nats {x7 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x7 = x1∀ x8 : ο . x8} x2 (λ x7 . x3 x7 x2)x2{x7 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x7 = x1∀ x8 : ο . x8}(∀ x7 . x7{x8 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x8 = x1∀ x9 : ο . x9}x3 x7 x2 = x2∀ x8 : ο . x8)(∀ x7 . x7{x8 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x8 = x1∀ x9 : ο . x9}∀ x8 : ι → ο . x8 x2(∀ x9 . x9{x10 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x10 = x1∀ x11 : ο . x11}x8 (x3 x9 x2))x8 x7)(∀ x7 . x7{x8 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x8 = x1∀ x9 : ο . x9}∀ x8 . x8{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10}explicit_Nats_one_plus {x10 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x10 = x1∀ x11 : ο . x11} x2 (λ x10 . x3 x10 x2) x7 x8 = x3 x7 x8)(∀ x7 . x7{x8 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x8 = x1∀ x9 : ο . x9}∀ x8 . x8{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10}explicit_Nats_one_mult {x10 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x10 = x1∀ x11 : ο . x11} x2 (λ x10 . x3 x10 x2) x7 x8 = x4 x7 x8)(∀ x7 . x7{x8 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x8 = x1∀ x9 : ο . x9}∀ x8 . x8{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10}x3 x7 x8{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10})(∀ x7 . x7{x8 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x8 = x1∀ x9 : ο . x9}∀ x8 . x8{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10}x4 x7 x8{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10})x6)x6 (proof)
Known explicit_Field_minus_involexplicit_Field_minus_invol : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . x5x0explicit_Field_minus x0 x1 x2 x3 x4 (explicit_Field_minus x0 x1 x2 x3 x4 x5) = x5
Known explicit_Field_minus_mult_Rexplicit_Field_minus_mult_R : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . x5x0∀ x6 . x6x0x4 x5 (explicit_Field_minus x0 x1 x2 x3 x4 x6) = explicit_Field_minus x0 x1 x2 x3 x4 (x4 x5 x6)
Known explicit_Field_zero_multRexplicit_Field_zero_multR : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . x5x0x4 x5 x1 = x1
Known explicit_Field_minus_plus_distexplicit_Field_minus_plus_dist : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . x5x0∀ x6 . x6x0explicit_Field_minus x0 x1 x2 x3 x4 (x3 x5 x6) = x3 (explicit_Field_minus x0 x1 x2 x3 x4 x5) (explicit_Field_minus x0 x1 x2 x3 x4 x6)
Known explicit_Field_minus_closexplicit_Field_minus_clos : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . x5x0explicit_Field_minus x0 x1 x2 x3 x4 x5x0
Known explicit_Field_minus_Lexplicit_Field_minus_L : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . x5x0x3 (explicit_Field_minus x0 x1 x2 x3 x4 x5) x5 = x1
Known explicit_Field_minus_zeroexplicit_Field_minus_zero : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4explicit_Field_minus x0 x1 x2 x3 x4 x1 = x1
Known SepE2SepE2 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2Sep x0 x1x1 x2
Theorem explicit_OrderedField_Z_propsexplicit_OrderedField_Z_props : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_OrderedField x0 x1 x2 x3 x4 x5∀ x6 : ο . ((∀ x7 . x7{x8 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x8 = x1∀ x9 : ο . x9}explicit_Field_minus x0 x1 x2 x3 x4 x7{x8 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x8{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10}) (x8 = x1)) (x8{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10})})x1{x7 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x7{x8 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x8 = x1∀ x9 : ο . x9}) (x7 = x1)) (x7{x8 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x8 = x1∀ x9 : ο . x9})}{x7 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x7 = x1∀ x8 : ο . x8}{x7 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x7{x8 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x8 = x1∀ x9 : ο . x9}) (x7 = x1)) (x7{x8 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x8 = x1∀ x9 : ο . x9})}{x7 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x7{x8 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x8 = x1∀ x9 : ο . x9}) (x7 = x1)) (x7{x8 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x8 = x1∀ x9 : ο . x9})}x0(∀ x7 . x7{x8 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x8{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10}) (x8 = x1)) (x8{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10})}∀ x8 : ο . (explicit_Field_minus x0 x1 x2 x3 x4 x7{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10}x8)(x7 = x1x8)(x7{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10}x8)x8)x2{x7 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x7{x8 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x8 = x1∀ x9 : ο . x9}) (x7 = x1)) (x7{x8 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x8 = x1∀ x9 : ο . x9})}explicit_Field_minus x0 x1 x2 x3 x4 x2{x7 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x7{x8 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x8 = x1∀ x9 : ο . x9}) (x7 = x1)) (x7{x8 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x8 = x1∀ x9 : ο . x9})}(∀ x7 . x7{x8 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x8{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10}) (x8 = x1)) (x8{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10})}explicit_Field_minus x0 x1 x2 x3 x4 x7{x8 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x8{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10}) (x8 = x1)) (x8{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10})})(∀ x7 . x7{x8 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x8{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10}) (x8 = x1)) (x8{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10})}∀ x8 . x8{x9 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x9{x10 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x10 = x1∀ x11 : ο . x11}) (x9 = x1)) (x9{x10 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x10 = x1∀ x11 : ο . x11})}x3 x7 x8{x9 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x9{x10 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x10 = x1∀ x11 : ο . x11}) (x9 = x1)) (x9{x10 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x10 = x1∀ x11 : ο . x11})})(∀ x7 . x7{x8 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x8{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10}) (x8 = x1)) (x8{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10})}∀ x8 . x8{x9 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x9{x10 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x10 = x1∀ x11 : ο . x11}) (x9 = x1)) (x9{x10 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x10 = x1∀ x11 : ο . x11})}x4 x7 x8{x9 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x9{x10 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x10 = x1∀ x11 : ο . x11}) (x9 = x1)) (x9{x10 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x10 = x1∀ x11 : ο . x11})})x6)x6 (proof)
Theorem explicit_OrderedField_Q_propsexplicit_OrderedField_Q_props : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_OrderedField x0 x1 x2 x3 x4 x5∀ x6 : ο . (Sep x0 (explicit_OrderedField_rationalp x0 x1 x2 x3 x4 x5)x0(∀ x7 . x7Sep x0 (explicit_OrderedField_rationalp x0 x1 x2 x3 x4 x5)∀ x8 : ο . (x7x0∀ x9 . x9{x10 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x10{x11 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x11 = x1∀ x12 : ο . x12}) (x10 = x1)) (x10{x11 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x11 = x1∀ x12 : ο . x12})}∀ x10 . x10{x11 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x11 = x1∀ x12 : ο . x12}x4 x10 x7 = x9x8)x8)(∀ x7 . x7x0∀ x8 . x8{x9 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x9{x10 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x10 = x1∀ x11 : ο . x11}) (x9 = x1)) (x9{x10 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x10 = x1∀ x11 : ο . x11})}∀ x9 . x9{x10 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x10 = x1∀ x11 : ο . x11}x4 x9 x7 = x8x7Sep x0 (explicit_OrderedField_rationalp x0 x1 x2 x3 x4 x5))x6)x6 (proof)
Known explicit_Field_Iexplicit_Field_I : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . (∀ x5 . x5x0∀ x6 . x6x0x3 x5 x6x0)(∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0x3 x5 (x3 x6 x7) = x3 (x3 x5 x6) x7)(∀ x5 . x5x0∀ x6 . x6x0x3 x5 x6 = x3 x6 x5)x1x0(∀ x5 . x5x0x3 x1 x5 = x5)(∀ x5 . x5x0∀ x6 : ο . (∀ x7 . and (x7x0) (x3 x5 x7 = x1)x6)x6)(∀ x5 . x5x0∀ x6 . x6x0x4 x5 x6x0)(∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0x4 x5 (x4 x6 x7) = x4 (x4 x5 x6) x7)(∀ x5 . x5x0∀ x6 . x6x0x4 x5 x6 = x4 x6 x5)x2x0(x2 = x1∀ x5 : ο . x5)(∀ x5 . x5x0x4 x2 x5 = x5)(∀ x5 . x5x0(x5 = x1∀ x6 : ο . x6)∀ x6 : ο . (∀ x7 . and (x7x0) (x4 x5 x7 = x2)x6)x6)(∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0x4 x5 (x3 x6 x7) = x3 (x4 x5 x6) (x4 x5 x7))explicit_Field x0 x1 x2 x3 x4
Known explicit_Field_minus_Rexplicit_Field_minus_R : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . x5x0x3 x5 (explicit_Field_minus x0 x1 x2 x3 x4 x5) = x1
Known explicit_Field_minus_mult_Lexplicit_Field_minus_mult_L : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . x5x0∀ x6 . x6x0x4 (explicit_Field_minus x0 x1 x2 x3 x4 x5) x6 = explicit_Field_minus x0 x1 x2 x3 x4 (x4 x5 x6)
Theorem explicit_OrderedField_explicit_Field_Qexplicit_OrderedField_explicit_Field_Q : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_OrderedField x0 x1 x2 x3 x4 x5explicit_Field (Sep x0 (explicit_OrderedField_rationalp x0 x1 x2 x3 x4 x5)) x1 x2 x3 x4 (proof)
Param explicit_Realsexplicit_Reals : ιιι(ιιι) → (ιιι) → (ιιο) → ο
Param omegaomega : ι
Param nat_primrecnat_primrec : ι(ιιι) → ιι
Definition ltlt := λ x0 x1 x2 . λ x3 x4 : ι → ι → ι . λ x5 : ι → ι → ο . λ x6 x7 . and (x5 x6 x7) (x6 = x7∀ x8 : ο . x8)
Param PiPi : ι(ιι) → ι
Definition setexpsetexp := λ x0 x1 . Pi x1 (λ x2 . x0)
Param apap : ιιι
Known explicit_Reals_Eexplicit_Reals_E : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . ∀ x6 : ο . (explicit_Reals x0 x1 x2 x3 x4 x5explicit_OrderedField x0 x1 x2 x3 x4 x5(∀ x7 . x7x0∀ x8 . x8x0lt x0 x1 x2 x3 x4 x5 x1 x7x5 x1 x8∀ x9 : ο . (∀ x10 . and (x10Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)) (x5 x8 (x4 x10 x7))x9)x9)(∀ x7 . x7setexp x0 (Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5))∀ x8 . x8setexp x0 (Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5))(∀ x9 . x9Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)and (and (x5 (ap x7 x9) (ap x8 x9)) (x5 (ap x7 x9) (ap x7 (x3 x9 x2)))) (x5 (ap x8 (x3 x9 x2)) (ap x8 x9)))∀ x9 : ο . (∀ x10 . and (x10x0) (∀ x11 . x11Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)and (x5 (ap x7 x11) x10) (x5 x10 (ap x8 x11)))x9)x9)x6)explicit_Reals x0 x1 x2 x3 x4 x5x6
Param nat_pnat_p : ιο
Known omega_nat_pomega_nat_p : ∀ x0 . x0omeganat_p x0
Param ordsuccordsucc : ιι
Known nat_indnat_ind : ∀ x0 : ι → ο . x0 0(∀ x1 . nat_p x1x0 x1x0 (ordsucc x1))∀ x1 . nat_p x1x0 x1
Known nat_primrec_0nat_primrec_0 : ∀ x0 . ∀ x1 : ι → ι → ι . nat_primrec x0 x1 0 = x0
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 explicit_Reals_characteristic_0explicit_Reals_characteristic_0 : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_Reals x0 x1 x2 x3 x4 x5∀ x6 . x6omeganat_primrec x2 (λ x8 . x3 x2) x6 = x1∀ x7 : ο . x7 (proof)
Known explicit_OrderedField_Iexplicit_OrderedField_I : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_Field x0 x1 x2 x3 x4(∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0x5 x6 x7x5 x7 x8x5 x6 x8)(∀ x6 . x6x0∀ x7 . x7x0iff (and (x5 x6 x7) (x5 x7 x6)) (x6 = x7))(∀ x6 . x6x0∀ x7 . x7x0or (x5 x6 x7) (x5 x7 x6))(∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0x5 x6 x7x5 (x3 x6 x8) (x3 x7 x8))(∀ x6 . x6x0∀ x7 . x7x0x5 x1 x6x5 x1 x7x5 x1 (x4 x6 x7))explicit_OrderedField x0 x1 x2 x3 x4 x5
Theorem explicit_Reals_subexplicit_Reals_sub : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_OrderedField x0 x1 x2 x3 x4 x5∀ x6 . x6x0x1x6x2x6(∀ x7 . x7x6∀ x8 . x8x6x3 x7 x8x6)(∀ x7 . x7x6explicit_Field_minus x0 x1 x2 x3 x4 x7x6)(∀ x7 . x7x6∀ x8 . x8x6x4 x7 x8x6)(∀ x7 . x7x6(x7 = x1∀ x8 : ο . x8)∀ x8 : ο . (∀ x9 . and (x9x6) (x4 x7 x9 = x2)x8)x8)explicit_OrderedField x6 x1 x2 x3 x4 x5 (proof)
Known set_extset_ext : ∀ x0 x1 . x0x1x1x0x0 = x1
Known SepE1SepE1 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2Sep x0 x1x2x0
Known explicit_Field_plus_cancelLexplicit_Field_plus_cancelL : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0x3 x5 x6 = x3 x5 x7x6 = x7
Theorem explicit_Reals_Q_min_propsexplicit_Reals_Q_min_props : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . ∀ x6 . explicit_OrderedField x0 x1 x2 x3 x4 x5x6x0explicit_Field x6 x1 x2 x3 x4∀ x7 : ο . ((∀ x8 . x8x6explicit_Field_minus x6 x1 x2 x3 x4 x8 = explicit_Field_minus x0 x1 x2 x3 x4 x8)(∀ x8 . x8x6explicit_Field_minus x0 x1 x2 x3 x4 x8x6)Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5) = Sep x6 (natOfOrderedField_p x6 x1 x2 x3 x4 x5){x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10} = {x9 ∈ Sep x6 (natOfOrderedField_p x6 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10}{x9 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x9{x10 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x10 = x1∀ x11 : ο . x11}) (x9 = x1)) (x9{x10 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x10 = x1∀ x11 : ο . x11})} = {x9 ∈ x6|or (or (explicit_Field_minus x6 x1 x2 x3 x4 x9{x10 ∈ Sep x6 (natOfOrderedField_p x6 x1 x2 x3 x4 x5)|x10 = x1∀ x11 : ο . x11}) (x9 = x1)) (x9{x10 ∈ Sep x6 (natOfOrderedField_p x6 x1 x2 x3 x4 x5)|x10 = x1∀ x11 : ο . x11})}Sep x0 (explicit_OrderedField_rationalp x0 x1 x2 x3 x4 x5) = Sep x6 (explicit_OrderedField_rationalp x6 x1 x2 x3 x4 x5)x7)x7 (proof)
Theorem explicit_Reals_Q_minexplicit_Reals_Q_min : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_OrderedField x0 x1 x2 x3 x4 x5∀ x6 . x6x0explicit_Field x6 x1 x2 x3 x4Sep x0 (explicit_OrderedField_rationalp x0 x1 x2 x3 x4 x5)x6 (proof)
Param lamSigma : ι(ιι) → ι
Param If_iIf_i : οιιι
Param encode_bencode_b : ιCT2 ι
Param encode_rencode_r : ι(ιιο) → ι
Definition pack_b_b_r_e_epack_b_b_r_e_e := λ x0 . λ x1 x2 : ι → ι → ι . λ x3 : ι → ι → ο . λ x4 x5 . lam 6 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) (encode_b x0 x1) (If_i (x6 = 2) (encode_b x0 x2) (If_i (x6 = 3) (encode_r x0 x3) (If_i (x6 = 4) x4 x5)))))
Known tuple_6_0_eqtuple_6_0_eq : ∀ x0 x1 x2 x3 x4 x5 . ap (lam 6 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 (If_i (x7 = 3) x3 (If_i (x7 = 4) x4 x5)))))) 0 = x0
Theorem pack_b_b_r_e_e_0_eqpack_b_b_r_e_e_0_eq : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 x6 . x0 = pack_b_b_r_e_e x1 x2 x3 x4 x5 x6x1 = ap x0 0 (proof)
Theorem pack_b_b_r_e_e_0_eq2pack_b_b_r_e_e_0_eq2 : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 . x0 = ap (pack_b_b_r_e_e x0 x1 x2 x3 x4 x5) 0 (proof)
Param decode_bdecode_b : ιιιι
Known tuple_6_1_eqtuple_6_1_eq : ∀ x0 x1 x2 x3 x4 x5 . ap (lam 6 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 (If_i (x7 = 3) x3 (If_i (x7 = 4) x4 x5)))))) 1 = x1
Known decode_encode_bdecode_encode_b : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . x2x0∀ x3 . x3x0decode_b (encode_b x0 x1) x2 x3 = x1 x2 x3
Theorem pack_b_b_r_e_e_1_eqpack_b_b_r_e_e_1_eq : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 x6 . x0 = pack_b_b_r_e_e x1 x2 x3 x4 x5 x6∀ x7 . x7x1∀ x8 . x8x1x2 x7 x8 = decode_b (ap x0 1) x7 x8 (proof)
Theorem pack_b_b_r_e_e_1_eq2pack_b_b_r_e_e_1_eq2 : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 x6 . x6x0∀ x7 . x7x0x1 x6 x7 = decode_b (ap (pack_b_b_r_e_e x0 x1 x2 x3 x4 x5) 1) x6 x7 (proof)
Known tuple_6_2_eqtuple_6_2_eq : ∀ x0 x1 x2 x3 x4 x5 . ap (lam 6 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 (If_i (x7 = 3) x3 (If_i (x7 = 4) x4 x5)))))) 2 = x2
Theorem pack_b_b_r_e_e_2_eqpack_b_b_r_e_e_2_eq : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 x6 . x0 = pack_b_b_r_e_e x1 x2 x3 x4 x5 x6∀ x7 . x7x1∀ x8 . x8x1x3 x7 x8 = decode_b (ap x0 2) x7 x8 (proof)
Theorem pack_b_b_r_e_e_2_eq2pack_b_b_r_e_e_2_eq2 : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 x6 . x6x0∀ x7 . x7x0x2 x6 x7 = decode_b (ap (pack_b_b_r_e_e x0 x1 x2 x3 x4 x5) 2) x6 x7 (proof)
Param decode_rdecode_r : ιιιο
Known tuple_6_3_eqtuple_6_3_eq : ∀ x0 x1 x2 x3 x4 x5 . ap (lam 6 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 (If_i (x7 = 3) x3 (If_i (x7 = 4) x4 x5)))))) 3 = x3
Known decode_encode_rdecode_encode_r : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 . x2x0∀ x3 . x3x0decode_r (encode_r x0 x1) x2 x3 = x1 x2 x3
Theorem pack_b_b_r_e_e_3_eqpack_b_b_r_e_e_3_eq : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 x6 . x0 = pack_b_b_r_e_e x1 x2 x3 x4 x5 x6∀ x7 . x7x1∀ x8 . x8x1x4 x7 x8 = decode_r (ap x0 3) x7 x8 (proof)
Theorem pack_b_b_r_e_e_3_eq2pack_b_b_r_e_e_3_eq2 : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 x6 . x6x0∀ x7 . x7x0x3 x6 x7 = decode_r (ap (pack_b_b_r_e_e x0 x1 x2 x3 x4 x5) 3) x6 x7 (proof)
Known tuple_6_4_eqtuple_6_4_eq : ∀ x0 x1 x2 x3 x4 x5 . ap (lam 6 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 (If_i (x7 = 3) x3 (If_i (x7 = 4) x4 x5)))))) 4 = x4
Theorem pack_b_b_r_e_e_4_eqpack_b_b_r_e_e_4_eq : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 x6 . x0 = pack_b_b_r_e_e x1 x2 x3 x4 x5 x6x5 = ap x0 4 (proof)
Theorem pack_b_b_r_e_e_4_eq2pack_b_b_r_e_e_4_eq2 : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 . x4 = ap (pack_b_b_r_e_e x0 x1 x2 x3 x4 x5) 4 (proof)
Known tuple_6_5_eqtuple_6_5_eq : ∀ x0 x1 x2 x3 x4 x5 . ap (lam 6 (λ x7 . If_i (x7 = 0) x0 (If_i (x7 = 1) x1 (If_i (x7 = 2) x2 (If_i (x7 = 3) x3 (If_i (x7 = 4) x4 x5)))))) 5 = x5
Theorem pack_b_b_r_e_e_5_eqpack_b_b_r_e_e_5_eq : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 x6 . x0 = pack_b_b_r_e_e x1 x2 x3 x4 x5 x6x6 = ap x0 5 (proof)
Theorem pack_b_b_r_e_e_5_eq2pack_b_b_r_e_e_5_eq2 : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 . x5 = ap (pack_b_b_r_e_e x0 x1 x2 x3 x4 x5) 5 (proof)
Known and6Iand6I : ∀ x0 x1 x2 x3 x4 x5 : ο . x0x1x2x3x4x5and (and (and (and (and x0 x1) x2) x3) x4) x5
Theorem pack_b_b_r_e_e_injpack_b_b_r_e_e_inj : ∀ x0 x1 . ∀ x2 x3 x4 x5 : ι → ι → ι . ∀ x6 x7 : ι → ι → ο . ∀ x8 x9 x10 x11 . pack_b_b_r_e_e x0 x2 x4 x6 x8 x10 = pack_b_b_r_e_e x1 x3 x5 x7 x9 x11and (and (and (and (and (x0 = x1) (∀ x12 . x12x0∀ x13 . x13x0x2 x12 x13 = x3 x12 x13)) (∀ x12 . x12x0∀ x13 . x13x0x4 x12 x13 = x5 x12 x13)) (∀ x12 . x12x0∀ x13 . x13x0x6 x12 x13 = x7 x12 x13)) (x8 = x9)) (x10 = x11) (proof)
Known encode_r_extencode_r_ext : ∀ x0 . ∀ x1 x2 : ι → ι → ο . (∀ x3 . x3x0∀ x4 . x4x0iff (x1 x3 x4) (x2 x3 x4))encode_r x0 x1 = encode_r x0 x2
Known encode_b_extencode_b_ext : ∀ x0 . ∀ x1 x2 : ι → ι → ι . (∀ x3 . x3x0∀ x4 . x4x0x1 x3 x4 = x2 x3 x4)encode_b x0 x1 = encode_b x0 x2
Theorem pack_b_b_r_e_e_extpack_b_b_r_e_e_ext : ∀ x0 . ∀ x1 x2 x3 x4 : ι → ι → ι . ∀ x5 x6 : ι → ι → ο . ∀ x7 x8 . (∀ x9 . x9x0∀ x10 . x10x0x1 x9 x10 = x2 x9 x10)(∀ x9 . x9x0∀ x10 . x10x0x3 x9 x10 = x4 x9 x10)(∀ x9 . x9x0∀ x10 . x10x0iff (x5 x9 x10) (x6 x9 x10))pack_b_b_r_e_e x0 x1 x3 x5 x7 x8 = pack_b_b_r_e_e x0 x2 x4 x6 x7 x8 (proof)
Definition struct_b_b_r_e_estruct_b_b_r_e_e := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . x4x2∀ x5 . x5x2x3 x4 x5x2)∀ x4 : ι → ι → ι . (∀ x5 . x5x2∀ x6 . x6x2x4 x5 x6x2)∀ x5 : ι → ι → ο . ∀ x6 . x6x2∀ x7 . x7x2x1 (pack_b_b_r_e_e x2 x3 x4 x5 x6 x7))x1 x0
Theorem pack_struct_b_b_r_e_e_Ipack_struct_b_b_r_e_e_I : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x0)∀ x2 : ι → ι → ι . (∀ x3 . x3x0∀ x4 . x4x0x2 x3 x4x0)∀ x3 : ι → ι → ο . ∀ x4 . x4x0∀ x5 . x5x0struct_b_b_r_e_e (pack_b_b_r_e_e x0 x1 x2 x3 x4 x5) (proof)
Theorem pack_struct_b_b_r_e_e_E1pack_struct_b_b_r_e_e_E1 : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 . struct_b_b_r_e_e (pack_b_b_r_e_e x0 x1 x2 x3 x4 x5)∀ x6 . x6x0∀ x7 . x7x0x1 x6 x7x0 (proof)
Theorem pack_struct_b_b_r_e_e_E2pack_struct_b_b_r_e_e_E2 : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 . struct_b_b_r_e_e (pack_b_b_r_e_e x0 x1 x2 x3 x4 x5)∀ x6 . x6x0∀ x7 . x7x0x2 x6 x7x0 (proof)
Theorem pack_struct_b_b_r_e_e_E4pack_struct_b_b_r_e_e_E4 : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 . struct_b_b_r_e_e (pack_b_b_r_e_e x0 x1 x2 x3 x4 x5)x4x0 (proof)
Theorem pack_struct_b_b_r_e_e_E5pack_struct_b_b_r_e_e_E5 : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 . struct_b_b_r_e_e (pack_b_b_r_e_e x0 x1 x2 x3 x4 x5)x5x0 (proof)
Known iff_refliff_refl : ∀ x0 : ο . iff x0 x0
Theorem struct_b_b_r_e_e_etastruct_b_b_r_e_e_eta : ∀ x0 . struct_b_b_r_e_e x0x0 = pack_b_b_r_e_e (ap x0 0) (decode_b (ap x0 1)) (decode_b (ap x0 2)) (decode_r (ap x0 3)) (ap x0 4) (ap x0 5) (proof)
Definition unpack_b_b_r_e_e_iunpack_b_b_r_e_e_i := λ x0 . λ x1 : ι → (ι → ι → ι)(ι → ι → ι)(ι → ι → ο)ι → ι → ι . x1 (ap x0 0) (decode_b (ap x0 1)) (decode_b (ap x0 2)) (decode_r (ap x0 3)) (ap x0 4) (ap x0 5)
Theorem unpack_b_b_r_e_e_i_equnpack_b_b_r_e_e_i_eq : ∀ x0 : ι → (ι → ι → ι)(ι → ι → ι)(ι → ι → ο)ι → ι → ι . ∀ x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 x6 . (∀ x7 : ι → ι → ι . (∀ x8 . x8x1∀ x9 . x9x1x2 x8 x9 = x7 x8 x9)∀ x8 : ι → ι → ι . (∀ x9 . x9x1∀ x10 . x10x1x3 x9 x10 = x8 x9 x10)∀ x9 : ι → ι → ο . (∀ x10 . x10x1∀ x11 . x11x1iff (x4 x10 x11) (x9 x10 x11))x0 x1 x7 x8 x9 x5 x6 = x0 x1 x2 x3 x4 x5 x6)unpack_b_b_r_e_e_i (pack_b_b_r_e_e x1 x2 x3 x4 x5 x6) x0 = x0 x1 x2 x3 x4 x5 x6 (proof)
Definition unpack_b_b_r_e_e_ounpack_b_b_r_e_e_o := λ x0 . λ x1 : ι → (ι → ι → ι)(ι → ι → ι)(ι → ι → ο)ι → ι → ο . x1 (ap x0 0) (decode_b (ap x0 1)) (decode_b (ap x0 2)) (decode_r (ap x0 3)) (ap x0 4) (ap x0 5)
Theorem unpack_b_b_r_e_e_o_equnpack_b_b_r_e_e_o_eq : ∀ x0 : ι → (ι → ι → ι)(ι → ι → ι)(ι → ι → ο)ι → ι → ο . ∀ x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 x6 . (∀ x7 : ι → ι → ι . (∀ x8 . x8x1∀ x9 . x9x1x2 x8 x9 = x7 x8 x9)∀ x8 : ι → ι → ι . (∀ x9 . x9x1∀ x10 . x10x1x3 x9 x10 = x8 x9 x10)∀ x9 : ι → ι → ο . (∀ x10 . x10x1∀ x11 . x11x1iff (x4 x10 x11) (x9 x10 x11))x0 x1 x7 x8 x9 x5 x6 = x0 x1 x2 x3 x4 x5 x6)unpack_b_b_r_e_e_o (pack_b_b_r_e_e x1 x2 x3 x4 x5 x6) x0 = x0 x1 x2 x3 x4 x5 x6 (proof)
Definition OrderedFieldStructstruct_b_b_r_e_e_ordered_field := λ x0 . and (struct_b_b_r_e_e x0) (unpack_b_b_r_e_e_o x0 (λ x1 . λ x2 x3 : ι → ι → ι . λ x4 : ι → ι → ο . λ x5 x6 . explicit_OrderedField x1 x5 x6 x2 x3 x4))
Known f16ac.. : ∀ x0 x1 x2 . ∀ x3 x4 x5 x6 : ι → ι → ι . (∀ x7 . x7x0∀ x8 . x8x0x3 x7 x8 = x5 x7 x8)(∀ x7 . x7x0∀ x8 . x8x0x4 x7 x8 = x6 x7 x8)explicit_Field x0 x1 x2 x3 x4explicit_Field x0 x1 x2 x5 x6
Known iffIiffI : ∀ x0 x1 : ο . (x0x1)(x1x0)iff x0 x1
Theorem a7a4d.. : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . ∀ x6 x7 : ι → ι → ι . ∀ x8 : ι → ι → ο . (∀ x9 . x9x0∀ x10 . x10x0x3 x9 x10 = x6 x9 x10)(∀ x9 . x9x0∀ x10 . x10x0x4 x9 x10 = x7 x9 x10)(∀ x9 . x9x0∀ x10 . x10x0iff (x5 x9 x10) (x8 x9 x10))explicit_OrderedField x0 x1 x2 x3 x4 x5explicit_OrderedField x0 x1 x2 x6 x7 x8 (proof)
Known iff_symiff_sym : ∀ x0 x1 : ο . iff x0 x1iff x1 x0
Theorem explicit_OrderedField_repindepexplicit_OrderedField_repindep : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . ∀ x6 x7 : ι → ι → ι . ∀ x8 : ι → ι → ο . (∀ x9 . x9x0∀ x10 . x10x0x3 x9 x10 = x6 x9 x10)(∀ x9 . x9x0∀ x10 . x10x0x4 x9 x10 = x7 x9 x10)(∀ x9 . x9x0∀ x10 . x10x0iff (x5 x9 x10) (x8 x9 x10))iff (explicit_OrderedField x0 x1 x2 x3 x4 x5) (explicit_OrderedField x0 x1 x2 x6 x7 x8) (proof)
Known prop_extprop_ext : ∀ x0 x1 : ο . iff x0 x1x0 = x1
Theorem OrderedFieldStruct_unpack_eqOrderedFieldStruct_unpack_eq : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 . unpack_b_b_r_e_e_o (pack_b_b_r_e_e x0 x1 x2 x3 x4 x5) (λ x7 . λ x8 x9 : ι → ι → ι . λ x10 : ι → ι → ο . λ x11 x12 . explicit_OrderedField x7 x11 x12 x8 x9 x10) = explicit_OrderedField x0 x4 x5 x1 x2 x3 (proof)
Definition RealsStructRealsStruct := λ x0 . and (struct_b_b_r_e_e x0) (unpack_b_b_r_e_e_o x0 (λ x1 . λ x2 x3 : ι → ι → ι . λ x4 : ι → ι → ο . λ x5 x6 . explicit_Reals x1 x5 x6 x2 x3 x4))
Known explicit_Reals_Iexplicit_Reals_I : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_OrderedField x0 x1 x2 x3 x4 x5(∀ x6 . x6x0∀ x7 . x7x0lt x0 x1 x2 x3 x4 x5 x1 x6x5 x1 x7∀ x8 : ο . (∀ x9 . and (x9Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)) (x5 x7 (x4 x9 x6))x8)x8)(∀ x6 . x6setexp x0 (Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5))∀ x7 . x7setexp x0 (Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5))(∀ x8 . x8Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)and (and (x5 (ap x6 x8) (ap x7 x8)) (x5 (ap x6 x8) (ap x6 (x3 x8 x2)))) (x5 (ap x7 (x3 x8 x2)) (ap x7 x8)))∀ x8 : ο . (∀ x9 . and (x9x0) (∀ x10 . x10Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)and (x5 (ap x6 x10) x9) (x5 x9 (ap x7 x10)))x8)x8)explicit_Reals x0 x1 x2 x3 x4 x5
Known and3Iand3I : ∀ x0 x1 x2 : ο . x0x1x2and (and x0 x1) x2
Known ap_Piap_Pi : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2Pi x0 x1x3x0ap x2 x3x1 x3
Theorem 32ac0.. : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . ∀ x6 x7 : ι → ι → ι . ∀ x8 : ι → ι → ο . (∀ x9 . x9x0∀ x10 . x10x0x3 x9 x10 = x6 x9 x10)(∀ x9 . x9x0∀ x10 . x10x0x4 x9 x10 = x7 x9 x10)(∀ x9 . x9x0∀ x10 . x10x0iff (x5 x9 x10) (x8 x9 x10))explicit_Reals x0 x1 x2 x3 x4 x5explicit_Reals x0 x1 x2 x6 x7 x8 (proof)
Theorem explicit_Reals_repindepexplicit_Reals_repindep : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . ∀ x6 x7 : ι → ι → ι . ∀ x8 : ι → ι → ο . (∀ x9 . x9x0∀ x10 . x10x0x3 x9 x10 = x6 x9 x10)(∀ x9 . x9x0∀ x10 . x10x0x4 x9 x10 = x7 x9 x10)(∀ x9 . x9x0∀ x10 . x10x0iff (x5 x9 x10) (x8 x9 x10))iff (explicit_Reals x0 x1 x2 x3 x4 x5) (explicit_Reals x0 x1 x2 x6 x7 x8) (proof)
Theorem RealsStruct_unpack_eqRealsStruct_unpack_eq : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 . unpack_b_b_r_e_e_o (pack_b_b_r_e_e x0 x1 x2 x3 x4 x5) (λ x7 . λ x8 x9 : ι → ι → ι . λ x10 : ι → ι → ο . λ x11 x12 . explicit_Reals x7 x11 x12 x8 x9 x10) = explicit_Reals x0 x4 x5 x1 x2 x3 (proof)

previous assets