Search for blocks/addresses/...

Proofgold Asset

asset id
7dff27236a2680c725c0e6228c8447a41c097b692b2f9a502f680df85e740b4c
asset hash
5eb15f8c8c9fd61a1b1312198dde5ab07a4315c3a5b6e359bf0ff04727376c83
bday / block
4950
tx
b9096..
preasset
doc published by Pr6Pc..
Theorem f_eq_if_eq_i : ∀ x0 : ι → ι . ∀ x1 x2 . x1 = x2x0 x1 = x0 x2 (proof)
Theorem f_eq_i_if_eq_i_i : ∀ x0 : ι → ι → ι . ∀ x1 x2 x3 x4 . x1 = x2x3 = x4x0 x1 x3 = x0 x2 x4 (proof)
Param explicit_Fieldexplicit_Field : ιιι(ιιι) → (ιιι) → ο
Param explicit_Field_minusexplicit_Field_minus : ιιι(ιιι) → (ιιι) → ιι
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
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
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_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
Theorem 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 (proof)
Theorem 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) (proof)
Known explicit_Field_minus_multexplicit_Field_minus_mult : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . x5x0explicit_Field_minus x0 x1 x2 x3 x4 x5 = x4 (explicit_Field_minus x0 x1 x2 x3 x4 x2) x5
Known explicit_Field_minus_one_Inexplicit_Field_minus_one_In : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4explicit_Field_minus x0 x1 x2 x3 x4 x2x0
Theorem 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) (proof)
Theorem 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) (proof)
Theorem 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) (proof)
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Known dnegdneg : ∀ x0 : ο . not (not x0)x0
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_square_zero_invexplicit_Field_square_zero_inv : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . x5x0x4 x5 x5 = x1x5 = x1 (proof)
Param explicit_OrderedFieldexplicit_OrderedField : ιιι(ιιι) → (ιιι) → (ιιο) → ο
Definition iffiff := λ x0 x1 : ο . and (x0x1) (x1x0)
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
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_minus_leqexplicit_OrderedField_minus_leq : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_OrderedField x0 x1 x2 x3 x4 x5∀ x6 . x6x0∀ x7 . x7x0x5 x6 x7x5 (explicit_Field_minus x0 x1 x2 x3 x4 x7) (explicit_Field_minus x0 x1 x2 x3 x4 x6) (proof)
Known explicit_Field_minus_squareexplicit_Field_minus_square : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . x5x0x4 (explicit_Field_minus x0 x1 x2 x3 x4 x5) (explicit_Field_minus x0 x1 x2 x3 x4 x5) = x4 x5 x5
Theorem 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) (proof)
Theorem explicit_OrderedField_sum_squares_nonnegexplicit_OrderedField_sum_squares_nonneg : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_OrderedField x0 x1 x2 x3 x4 x5∀ x6 . x6x0∀ x7 . x7x0x5 x1 (x3 (x4 x6 x6) (x4 x7 x7)) (proof)
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Theorem 19c47.. : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_OrderedField x0 x1 x2 x3 x4 x5∀ x6 . x6x0∀ x7 . x7x0x5 x1 x6x5 x1 x7x3 x6 x7 = x1x7 = x1 (proof)
Theorem explicit_OrderedField_sum_nonneg_zero_invexplicit_OrderedField_sum_nonneg_zero_inv : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_OrderedField x0 x1 x2 x3 x4 x5∀ x6 . x6x0∀ x7 . x7x0x5 x1 x6x5 x1 x7x3 x6 x7 = x1and (x6 = x1) (x7 = x1) (proof)
Theorem explicit_OrderedField_sum_squares_zero_invexplicit_OrderedField_sum_squares_zero_inv : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_OrderedField x0 x1 x2 x3 x4 x5∀ x6 . x6x0∀ x7 . x7x0x3 (x4 x6 x6) (x4 x7 x7) = x1and (x6 = x1) (x7 = x1) (proof)