Search for blocks/addresses/...

Proofgold Address

address
PUhAZyjxSmrZKtj1jXKgWxcaKNMvRCjKHDs
total
0
mg
-
conjpub
-
current assets
4f3b5../43055.. bday: 3859 doc published by PrGxv..
Param explicit_Field : ιιι(ιιι) → (ιιι) → ο
Param explicit_Field_minus : ιιι(ιιι) → (ιιι) → ιι
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Known explicit_Field_E : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ο . (explicit_Field x0 x1 x2 x3 x4(∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0prim1 (x3 x6 x7) x0)(∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0x3 x6 (x3 x7 x8) = x3 (x3 x6 x7) x8)(∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0x3 x6 x7 = x3 x7 x6)prim1 x1 x0(∀ x6 . prim1 x6 x0x3 x1 x6 = x6)(∀ x6 . prim1 x6 x0∀ x7 : ο . (∀ x8 . and (prim1 x8 x0) (x3 x6 x8 = x1)x7)x7)(∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0prim1 (x4 x6 x7) x0)(∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0x4 x6 (x4 x7 x8) = x4 (x4 x6 x7) x8)(∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0x4 x6 x7 = x4 x7 x6)prim1 x2 x0(x2 = x1∀ x6 : ο . x6)(∀ x6 . prim1 x6 x0x4 x2 x6 = x6)(∀ x6 . prim1 x6 x0(x6 = x1∀ x7 : ο . x7)∀ x7 : ο . (∀ x8 . and (prim1 x8 x0) (x4 x6 x8 = x2)x7)x7)(∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0x4 x6 (x3 x7 x8) = x3 (x4 x6 x7) (x4 x6 x8))x5)explicit_Field x0 x1 x2 x3 x4x5
Known explicit_Field_minus_clos : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . prim1 x5 x0prim1 (explicit_Field_minus x0 x1 x2 x3 x4 x5) x0
Known explicit_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 explicit_Field_minus_invol : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . prim1 x5 x0explicit_Field_minus x0 x1 x2 x3 x4 (explicit_Field_minus x0 x1 x2 x3 x4 x5) = x5
Known explicit_Field_minus_L : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . prim1 x5 x0x3 (explicit_Field_minus x0 x1 x2 x3 x4 x5) x5 = x1
Known explicit_Field_minus_R : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . prim1 x5 x0x3 x5 (explicit_Field_minus x0 x1 x2 x3 x4 x5) = x1
Known explicit_Field_dist_R : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . prim1 x5 x0∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0x4 (x3 x5 x6) x7 = x3 (x4 x5 x7) (x4 x6 x7)
Known explicit_Field_minus_plus_dist : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . prim1 x5 x0∀ x6 . prim1 x6 x0explicit_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_mult_L : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . prim1 x5 x0∀ x6 . prim1 x6 x0x4 (explicit_Field_minus x0 x1 x2 x3 x4 x5) x6 = explicit_Field_minus x0 x1 x2 x3 x4 (x4 x5 x6)
Known explicit_Field_minus_mult_R : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . prim1 x5 x0∀ x6 . prim1 x6 x0x4 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_multL : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . prim1 x5 x0x4 x1 x5 = x1
Known explicit_Field_zero_multR : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . prim1 x5 x0x4 x5 x1 = x1
Known explicit_Field_minus_one_In : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4prim1 (explicit_Field_minus x0 x1 x2 x3 x4 x2) x0
Theorem 2f9e6.. : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 : ο . ((∀ x6 . prim1 x6 x0prim1 (explicit_Field_minus x0 x1 x2 x3 x4 x6) x0)explicit_Field_minus x0 x1 x2 x3 x4 x1 = x1(∀ x6 . prim1 x6 x0explicit_Field_minus x0 x1 x2 x3 x4 (explicit_Field_minus x0 x1 x2 x3 x4 x6) = x6)(∀ x6 . prim1 x6 x0x3 (explicit_Field_minus x0 x1 x2 x3 x4 x6) x6 = x1)(∀ x6 . prim1 x6 x0x3 x6 (explicit_Field_minus x0 x1 x2 x3 x4 x6) = x1)(∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0x4 (x3 x6 x7) x8 = x3 (x4 x6 x8) (x4 x7 x8))(∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0explicit_Field_minus x0 x1 x2 x3 x4 (x3 x6 x7) = x3 (explicit_Field_minus x0 x1 x2 x3 x4 x6) (explicit_Field_minus x0 x1 x2 x3 x4 x7))(∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0x4 (explicit_Field_minus x0 x1 x2 x3 x4 x6) x7 = explicit_Field_minus x0 x1 x2 x3 x4 (x4 x6 x7))(∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0x4 x6 (explicit_Field_minus x0 x1 x2 x3 x4 x7) = explicit_Field_minus x0 x1 x2 x3 x4 (x4 x6 x7))(∀ x6 . prim1 x6 x0x4 x1 x6 = x1)(∀ x6 . prim1 x6 x0x4 x6 x1 = x1)prim1 (explicit_Field_minus x0 x1 x2 x3 x4 x2) x0(∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0prim1 (x4 x6 (x4 x7 x8)) x0)(∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0x3 (x3 x6 x7) (x3 x8 x9) = x3 (x3 x6 x9) (x3 x7 x8))(∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0x3 (x3 x6 x7) (x3 x8 x9) = x3 (x3 x6 x8) (x3 x7 x9))x5)x5 (proof)
Param 62ee1.. : ιιι(ιιι) → (ιιι) → (ιιο) → ο
Param 3b429.. : ι(ιι) → (ιιο) → CT2 ι
Definition True := ∀ x0 : ο . x0x0
Param 1216a.. : ι(ιο) → ι
Param explicit_OrderedField : ιιι(ιιι) → (ιιι) → (ιιο) → ο
Param lt : ιιι(ιιι) → (ιιι) → (ιιο) → ιιο
Param natOfOrderedField_p : ιιι(ιιι) → (ιιι) → (ιιο) → ιο
Param b5c9f.. : ιιι
Param f482f.. : ιιι
Known f2fa8.. : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . ∀ x6 : ο . (62ee1.. x0 x1 x2 x3 x4 x5explicit_OrderedField x0 x1 x2 x3 x4 x5(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0lt x0 x1 x2 x3 x4 x5 x1 x7x5 x1 x8∀ x9 : ο . (∀ x10 . and (prim1 x10 (1216a.. x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5))) (x5 x8 (x4 x10 x7))x9)x9)(∀ x7 . prim1 x7 (b5c9f.. x0 (1216a.. x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)))∀ x8 . prim1 x8 (b5c9f.. x0 (1216a.. x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)))(∀ x9 . prim1 x9 (1216a.. x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5))and (and (x5 (f482f.. x7 x9) (f482f.. x8 x9)) (x5 (f482f.. x7 x9) (f482f.. x7 (x3 x9 x2)))) (x5 (f482f.. x8 (x3 x9 x2)) (f482f.. x8 x9)))∀ x9 : ο . (∀ x10 . and (prim1 x10 x0) (∀ x11 . prim1 x11 (1216a.. x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5))and (x5 (f482f.. x7 x11) x10) (x5 x10 (f482f.. x8 x11)))x9)x9)x6)62ee1.. x0 x1 x2 x3 x4 x5x6
Param iff : οοο
Param or : οοο
Known explicit_OrderedField_E : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . ∀ x6 : ο . (explicit_OrderedField x0 x1 x2 x3 x4 x5explicit_Field x0 x1 x2 x3 x4(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0x5 x7 x8x5 x8 x9x5 x7 x9)(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0iff (and (x5 x7 x8) (x5 x8 x7)) (x7 = x8))(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0or (x5 x7 x8) (x5 x8 x7))(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0x5 x7 x8x5 (x3 x7 x9) (x3 x8 x9))(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0x5 x1 x7x5 x1 x8x5 x1 (x4 x7 x8))x6)explicit_OrderedField x0 x1 x2 x3 x4 x5x6
Known b2421.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0x1 x2prim1 x2 (1216a.. x0 x1)
Known Eps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2x1)x1)x0 (prim0 x0)
Known andI : ∀ x0 x1 : ο . x0x1and x0 x1
Known 0cbcb.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ι → ι . ∀ x4 . prim1 x4 (3b429.. x0 x1 x2 x3)∀ x5 : ο . (∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 (x1 x6)x2 x6 x7x4 = x3 x6 x7x5)x5
Known 81c0c.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ι → ι . ∀ x4 . prim1 x4 x0∀ x5 . prim1 x5 (x1 x4)x2 x4 x5prim1 (x3 x4 x5) (3b429.. x0 x1 x2 x3)
Known TrueI : True
Theorem 6e27d.. : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . ∀ x6 : ι → ι → ι . 62ee1.. x0 x1 x2 x3 x4 x5(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0∀ x10 . prim1 x10 x0x6 x7 x8 = x6 x9 x10and (x7 = x9) (x8 = x10))∀ x7 : ο . ((∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0prim1 (x6 x8 x9) (3b429.. x0 (λ x10 . x0) (λ x10 x11 . True) x6))(∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)∀ x9 : ι → ο . (∀ x10 . prim1 x10 x0∀ x11 . prim1 x11 x0x8 = x6 x10 x11x9 (x6 x10 x11))x9 x8)(∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x6 x8 x9 = x6 x11 x13)x12)x12)) = x8)(∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0prim0 (λ x11 . and (prim1 x11 x0) (x6 x8 x9 = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x6 x8 x9 = x6 x13 x15)x14)x14))) x11)) = x9)(∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)prim1 (prim0 (λ x9 . and (prim1 x9 x0) (∀ x10 : ο . (∀ x11 . and (prim1 x11 x0) (x8 = x6 x9 x11)x10)x10))) x0)(∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)prim1 (prim0 (λ x9 . and (prim1 x9 x0) (x8 = x6 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x8 = x6 x11 x13)x12)x12))) x9))) x0)(∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)x8 = x6 (prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x8 = x6 x10 x12)x11)x11))) (prim0 (λ x10 . and (prim1 x10 x0) (x8 = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x8 = x6 x12 x14)x13)x13))) x10))))(∀ x8 . prim1 x8 x0prim1 (x6 x8 x1) (1216a.. (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6) (λ x9 . x6 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x9 = x6 x11 x13)x12)x12))) x1 = x9)))(∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)∀ x9 . prim1 x9 (3b429.. x0 (λ x10 . x0) (λ x10 x11 . True) x6)prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x8 = x6 x11 x13)x12)x12)) = prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x9 = x6 x11 x13)x12)x12))prim0 (λ x11 . and (prim1 x11 x0) (x8 = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x8 = x6 x13 x15)x14)x14))) x11)) = prim0 (λ x11 . and (prim1 x11 x0) (x9 = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x9 = x6 x13 x15)x14)x14))) x11))x8 = x9)prim1 (x6 x1 x1) (3b429.. x0 (λ x8 . x0) (λ x8 x9 . True) x6)prim1 (x6 x2 x1) (3b429.. x0 (λ x8 . x0) (λ x8 x9 . True) x6)(∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0∀ x10 . prim1 x10 x0∀ x11 . prim1 x11 x0x6 (x3 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x6 x8 x9 = x6 x13 x15)x14)x14))) (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x6 x10 x11 = x6 x13 x15)x14)x14)))) (x3 (prim0 (λ x13 . and (prim1 x13 x0) (x6 x8 x9 = x6 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x6 x8 x9 = x6 x15 x17)x16)x16))) x13))) (prim0 (λ x13 . and (prim1 x13 x0) (x6 x10 x11 = x6 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x6 x10 x11 = x6 x15 x17)x16)x16))) x13)))) = x6 (x3 x8 x10) (x3 x9 x11))(∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)∀ x9 . prim1 x9 (3b429.. x0 (λ x10 . x0) (λ x10 x11 . True) x6)x6 (x3 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x8 = x6 x11 x13)x12)x12))) (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x9 = x6 x11 x13)x12)x12)))) (x3 (prim0 (λ x11 . and (prim1 x11 x0) (x8 = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x8 = x6 x13 x15)x14)x14))) x11))) (prim0 (λ x11 . and (prim1 x11 x0) (x9 = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x9 = x6 x13 x15)x14)x14))) x11)))) = x6 (x3 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x8 = x6 x11 x13)x12)x12))) (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x9 = x6 x11 x13)x12)x12)))) (x3 (prim0 (λ x11 . and (prim1 x11 x0) (x8 = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x8 = x6 x13 x15)x14)x14))) x11))) (prim0 (λ x11 . and (prim1 x11 x0) (x9 = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x9 = x6 x13 x15)x14)x14))) x11)))))(∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)∀ x9 . prim1 x9 (3b429.. x0 (λ x10 . x0) (λ x10 x11 . True) x6)prim1 (x6 (x3 (prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x8 = x6 x10 x12)x11)x11))) (prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x9 = x6 x10 x12)x11)x11)))) (x3 (prim0 (λ x10 . and (prim1 x10 x0) (x8 = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x8 = x6 x12 x14)x13)x13))) x10))) (prim0 (λ x10 . and (prim1 x10 x0) (x9 = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x9 = x6 x12 x14)x13)x13))) x10))))) (3b429.. x0 (λ x10 . x0) (λ x10 x11 . True) x6))(∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)∀ x9 . prim1 x9 (3b429.. x0 (λ x10 . x0) (λ x10 x11 . True) x6)prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x6 (x3 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x15 x17)x16)x16))) (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x15 x17)x16)x16)))) (x3 (prim0 (λ x15 . and (prim1 x15 x0) (x8 = x6 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x17 x19)x18)x18))) x15))) (prim0 (λ x15 . and (prim1 x15 x0) (x9 = x6 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x9 = x6 x17 x19)x18)x18))) x15)))) = x6 x11 x13)x12)x12)) = x3 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x8 = x6 x11 x13)x12)x12))) (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x9 = x6 x11 x13)x12)x12))))(∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)∀ x9 . prim1 x9 (3b429.. x0 (λ x10 . x0) (λ x10 x11 . True) x6)prim0 (λ x11 . and (prim1 x11 x0) (x6 (x3 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x8 = x6 x13 x15)x14)x14))) (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x9 = x6 x13 x15)x14)x14)))) (x3 (prim0 (λ x13 . and (prim1 x13 x0) (x8 = x6 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x15 x17)x16)x16))) x13))) (prim0 (λ x13 . and (prim1 x13 x0) (x9 = x6 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x15 x17)x16)x16))) x13)))) = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x6 (x3 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x17 x19)x18)x18))) (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x9 = x6 x17 x19)x18)x18)))) (x3 (prim0 (λ x17 . and (prim1 x17 x0) (x8 = x6 (prim0 (λ x19 . and (prim1 x19 x0) (∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x8 = x6 x19 x21)x20)x20))) x17))) (prim0 (λ x17 . and (prim1 x17 x0) (x9 = x6 (prim0 (λ x19 . and (prim1 x19 x0) (∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x9 = x6 x19 x21)x20)x20))) x17)))) = x6 x13 x15)x14)x14))) x11)) = x3 (prim0 (λ x11 . and (prim1 x11 x0) (x8 = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x8 = x6 x13 x15)x14)x14))) x11))) (prim0 (λ x11 . and (prim1 x11 x0) (x9 = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x9 = x6 x13 x15)x14)x14))) x11))))(∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0∀ x10 . prim1 x10 x0∀ x11 . prim1 x11 x0x6 (x3 (x4 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x6 x8 x9 = x6 x13 x15)x14)x14))) (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x6 x10 x11 = x6 x13 x15)x14)x14)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x13 . and (prim1 x13 x0) (x6 x8 x9 = x6 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x6 x8 x9 = x6 x15 x17)x16)x16))) x13))) (prim0 (λ x13 . and (prim1 x13 x0) (x6 x10 x11 = x6 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x6 x10 x11 = x6 x15 x17)x16)x16))) x13)))))) (x3 (x4 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x6 x8 x9 = x6 x13 x15)x14)x14))) (prim0 (λ x13 . and (prim1 x13 x0) (x6 x10 x11 = x6 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x6 x10 x11 = x6 x15 x17)x16)x16))) x13)))) (x4 (prim0 (λ x13 . and (prim1 x13 x0) (x6 x8 x9 = x6 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x6 x8 x9 = x6 x15 x17)x16)x16))) x13))) (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x6 x10 x11 = x6 x13 x15)x14)x14))))) = x6 (x3 (x4 x8 x10) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 x9 x11))) (x3 (x4 x8 x11) (x4 x9 x10)))(∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)∀ x9 . prim1 x9 (3b429.. x0 (λ x10 . x0) (λ x10 x11 . True) x6)x6 (x3 (x4 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x8 = x6 x11 x13)x12)x12))) (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x9 = x6 x11 x13)x12)x12)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x11 . and (prim1 x11 x0) (x8 = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x8 = x6 x13 x15)x14)x14))) x11))) (prim0 (λ x11 . and (prim1 x11 x0) (x9 = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x9 = x6 x13 x15)x14)x14))) x11)))))) (x3 (x4 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x8 = x6 x11 x13)x12)x12))) (prim0 (λ x11 . and (prim1 x11 x0) (x9 = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x9 = x6 x13 x15)x14)x14))) x11)))) (x4 (prim0 (λ x11 . and (prim1 x11 x0) (x8 = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x8 = x6 x13 x15)x14)x14))) x11))) (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x9 = x6 x11 x13)x12)x12))))) = x6 (x3 (x4 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x8 = x6 x11 x13)x12)x12))) (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x9 = x6 x11 x13)x12)x12)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x11 . and (prim1 x11 x0) (x8 = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x8 = x6 x13 x15)x14)x14))) x11))) (prim0 (λ x11 . and (prim1 x11 x0) (x9 = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x9 = x6 x13 x15)x14)x14))) x11)))))) (x3 (x4 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x8 = x6 x11 x13)x12)x12))) (prim0 (λ x11 . and (prim1 x11 x0) (x9 = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x9 = x6 x13 x15)x14)x14))) x11)))) (x4 (prim0 (λ x11 . and (prim1 x11 x0) (x8 = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x8 = x6 x13 x15)x14)x14))) x11))) (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x9 = x6 x11 x13)x12)x12))))))(∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)∀ x9 . prim1 x9 (3b429.. x0 (λ x10 . x0) (λ x10 x11 . True) x6)prim1 (x3 (x4 (prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x8 = x6 x10 x12)x11)x11))) (prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x9 = x6 x10 x12)x11)x11)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x10 . and (prim1 x10 x0) (x8 = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x8 = x6 x12 x14)x13)x13))) x10))) (prim0 (λ x10 . and (prim1 x10 x0) (x9 = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x9 = x6 x12 x14)x13)x13))) x10)))))) x0)(∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)∀ x9 . prim1 x9 (3b429.. x0 (λ x10 . x0) (λ x10 x11 . True) x6)prim1 (x3 (x4 (prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x8 = x6 x10 x12)x11)x11))) (prim0 (λ x10 . and (prim1 x10 x0) (x9 = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x9 = x6 x12 x14)x13)x13))) x10)))) (x4 (prim0 (λ x10 . and (prim1 x10 x0) (x8 = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x8 = x6 x12 x14)x13)x13))) x10))) (prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x9 = x6 x10 x12)x11)x11))))) x0)(∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)∀ x9 . prim1 x9 (3b429.. x0 (λ x10 . x0) (λ x10 x11 . True) x6)prim1 (x6 (x3 (x4 (prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x8 = x6 x10 x12)x11)x11))) (prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x9 = x6 x10 x12)x11)x11)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x10 . and (prim1 x10 x0) (x8 = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x8 = x6 x12 x14)x13)x13))) x10))) (prim0 (λ x10 . and (prim1 x10 x0) (x9 = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x9 = x6 x12 x14)x13)x13))) x10)))))) (x3 (x4 (prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x8 = x6 x10 x12)x11)x11))) (prim0 (λ x10 . and (prim1 x10 x0) (x9 = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x9 = x6 x12 x14)x13)x13))) x10)))) (x4 (prim0 (λ x10 . and (prim1 x10 x0) (x8 = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x8 = x6 x12 x14)x13)x13))) x10))) (prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x9 = x6 x10 x12)x11)x11)))))) (3b429.. x0 (λ x10 . x0) (λ x10 x11 . True) x6))(∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)∀ x9 . prim1 x9 (3b429.. x0 (λ x10 . x0) (λ x10 x11 . True) x6)prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x6 (x3 (x4 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x15 x17)x16)x16))) (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x15 x17)x16)x16)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x15 . and (prim1 x15 x0) (x8 = x6 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x17 x19)x18)x18))) x15))) (prim0 (λ x15 . and (prim1 x15 x0) (x9 = x6 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x9 = x6 x17 x19)x18)x18))) x15)))))) (x3 (x4 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x15 x17)x16)x16))) (prim0 (λ x15 . and (prim1 x15 x0) (x9 = x6 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x9 = x6 x17 x19)x18)x18))) x15)))) (x4 (prim0 (λ x15 . and (prim1 x15 x0) (x8 = x6 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x17 x19)x18)x18))) x15))) (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x15 x17)x16)x16))))) = x6 x11 x13)x12)x12)) = x3 (x4 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x8 = x6 x11 x13)x12)x12))) (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x9 = x6 x11 x13)x12)x12)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x11 . and (prim1 x11 x0) (x8 = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x8 = x6 x13 x15)x14)x14))) x11))) (prim0 (λ x11 . and (prim1 x11 x0) (x9 = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x9 = x6 x13 x15)x14)x14))) x11))))))(∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)∀ x9 . prim1 x9 (3b429.. x0 (λ x10 . x0) (λ x10 x11 . True) x6)prim0 (λ x11 . and (prim1 x11 x0) (x6 (x3 (x4 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x8 = x6 x13 x15)x14)x14))) (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x9 = x6 x13 x15)x14)x14)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x13 . and (prim1 x13 x0) (x8 = x6 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x15 x17)x16)x16))) x13))) (prim0 (λ x13 . and (prim1 x13 x0) (x9 = x6 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x15 x17)x16)x16))) x13)))))) (x3 (x4 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x8 = x6 x13 x15)x14)x14))) (prim0 (λ x13 . and (prim1 x13 x0) (x9 = x6 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x15 x17)x16)x16))) x13)))) (x4 (prim0 (λ x13 . and (prim1 x13 x0) (x8 = x6 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x15 x17)x16)x16))) x13))) (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x9 = x6 x13 x15)x14)x14))))) = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x6 (x3 (x4 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x17 x19)x18)x18))) (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x9 = x6 x17 x19)x18)x18)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x17 . and (prim1 x17 x0) (x8 = x6 (prim0 (λ x19 . and (prim1 x19 x0) (∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x8 = x6 x19 x21)x20)x20))) x17))) (prim0 (λ x17 . and (prim1 x17 x0) (x9 = x6 (prim0 (λ x19 . and (prim1 x19 x0) (∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x9 = x6 x19 x21)x20)x20))) x17)))))) (x3 (x4 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x17 x19)x18)x18))) (prim0 (λ x17 . and (prim1 x17 x0) (x9 = x6 (prim0 (λ x19 . and (prim1 x19 x0) (∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x9 = x6 x19 x21)x20)x20))) x17)))) (x4 (prim0 (λ x17 . and (prim1 x17 x0) (x8 = x6 (prim0 (λ x19 . and (prim1 x19 x0) (∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x8 = x6 x19 x21)x20)x20))) x17))) (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x9 = x6 x17 x19)x18)x18))))) = x6 x13 x15)x14)x14))) x11)) = x3 (x4 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x8 = x6 x11 x13)x12)x12))) (prim0 (λ x11 . and (prim1 x11 x0) (x9 = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x9 = x6 x13 x15)x14)x14))) x11)))) (x4 (prim0 (λ x11 . and (prim1 x11 x0) (x8 = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x8 = x6 x13 x15)x14)x14))) x11))) (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x9 = x6 x11 x13)x12)x12)))))x7)x7 (proof)

previous assets