Search for blocks/addresses/...

Proofgold Address

address
PUZr25iDGJDxwfDsTtuMn5bg8JteLTdt5r9
total
0
mg
-
conjpub
-
current assets
5d982../e80a4.. bday: 4970 doc published by Pr6Pc..
Param explicit_Realsexplicit_Reals : ιιι(ιιι) → (ιιι) → (ιιο) → ο
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Param ReplSep2ReplSep2 : ι(ιι) → (ιιο) → CT2 ι
Param TrueTrue : ο
Param explicit_Field_minusexplicit_Field_minus : ιιι(ιιι) → (ιιι) → ιι
Known 455b2.. : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . ∀ x6 : ι → ι → ι . explicit_Reals x0 x1 x2 x3 x4 x5(∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0x6 x7 x8 = x6 x9 x10and (x7 = x9) (x8 = x10))∀ x7 : ο . ((∀ x8 . x8x0∀ x9 . x9x0x6 x8 x9ReplSep2 x0 (λ x10 . x0) (λ x10 x11 . True) x6)(∀ x8 . x8x0∀ x9 . x9x0prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x6 x8 x9 = x6 x11 x14)x13)x13)x12)x12) = x8)(∀ x8 . x8x0∀ x9 . x9x0prim0 (λ x11 . ∀ x12 : ο . (x11x0x6 x8 x9 = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x6 x8 x9 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12) = x9)(∀ x8 . x8ReplSep2 x0 (λ x9 . x0) (λ x9 x10 . True) x6prim0 (λ x9 . ∀ x10 : ο . (x9x0(∀ x11 : ο . (∀ x12 . and (x12x0) (x8 = x6 x9 x12)x11)x11)x10)x10)x0)(∀ x8 . x8ReplSep2 x0 (λ x9 . x0) (λ x9 x10 . True) x6prim0 (λ x9 . ∀ x10 : ο . (x9x0x8 = x6 (prim0 (λ x12 . ∀ x13 : ο . (x12x0(∀ x14 : ο . (∀ x15 . and (x15x0) (x8 = x6 x12 x15)x14)x14)x13)x13)) x9x10)x10)x0)(∀ x8 . x8ReplSep2 x0 (λ x9 . x0) (λ x9 x10 . True) x6∀ x9 . x9ReplSep2 x0 (λ x10 . x0) (λ x10 x11 . True) x6prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x8 = x6 x11 x14)x13)x13)x12)x12) = prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x9 = x6 x11 x14)x13)x13)x12)x12)prim0 (λ x11 . ∀ x12 : ο . (x11x0x8 = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12) = prim0 (λ x11 . ∀ x12 : ο . (x11x0x9 = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x9 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)x8 = x9)x6 x1 x1ReplSep2 x0 (λ x8 . x0) (λ x8 x9 . True) x6x6 x2 x1ReplSep2 x0 (λ x8 . x0) (λ x8 x9 . True) x6(∀ x8 . x8ReplSep2 x0 (λ x9 . x0) (λ x9 x10 . True) x6∀ x9 . x9ReplSep2 x0 (λ x10 . x0) (λ x10 x11 . True) x6x6 (x3 (prim0 (λ x10 . ∀ x11 : ο . (x10x0(∀ x12 : ο . (∀ x13 . and (x13x0) (x8 = x6 x10 x13)x12)x12)x11)x11)) (prim0 (λ x10 . ∀ x11 : ο . (x10x0(∀ x12 : ο . (∀ x13 . and (x13x0) (x9 = x6 x10 x13)x12)x12)x11)x11))) (x3 (prim0 (λ x10 . ∀ x11 : ο . (x10x0x8 = x6 (prim0 (λ x13 . ∀ x14 : ο . (x13x0(∀ x15 : ο . (∀ x16 . and (x16x0) (x8 = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11)) (prim0 (λ x10 . ∀ x11 : ο . (x10x0x9 = x6 (prim0 (λ x13 . ∀ x14 : ο . (x13x0(∀ x15 : ο . (∀ x16 . and (x16x0) (x9 = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11)))ReplSep2 x0 (λ x10 . x0) (λ x10 x11 . True) x6)(∀ x8 . x8ReplSep2 x0 (λ x9 . x0) (λ x9 x10 . True) x6∀ x9 . x9ReplSep2 x0 (λ x10 . x0) (λ x10 x11 . True) x6prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x6 (x3 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x9 = x6 x16 x19)x18)x18)x17)x17))) (x3 (prim0 (λ x16 . ∀ x17 : ο . (x16x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) = x6 x11 x14)x13)x13)x12)x12) = x3 (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x8 = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x9 = x6 x11 x14)x13)x13)x12)x12)))(∀ x8 . x8ReplSep2 x0 (λ x9 . x0) (λ x9 x10 . True) x6∀ x9 . x9ReplSep2 x0 (λ x10 . x0) (λ x10 x11 . True) x6prim0 (λ x11 . ∀ x12 : ο . (x11x0x6 (x3 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x9 = x6 x14 x17)x16)x16)x15)x15))) (x3 (prim0 (λ x14 . ∀ x15 : ο . (x14x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x6 (x3 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20))) (x3 (prim0 (λ x19 . ∀ x20 : ο . (x19x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12) = x3 (prim0 (λ x11 . ∀ x12 : ο . (x11x0x8 = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0x9 = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x9 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)))(∀ x8 . x8ReplSep2 x0 (λ x9 . x0) (λ x9 x10 . True) x6∀ x9 . x9ReplSep2 x0 (λ x10 . x0) (λ x10 x11 . True) x6x6 (x3 (x4 (prim0 (λ x10 . ∀ x11 : ο . (x10x0(∀ x12 : ο . (∀ x13 . and (x13x0) (x8 = x6 x10 x13)x12)x12)x11)x11)) (prim0 (λ x10 . ∀ x11 : ο . (x10x0(∀ x12 : ο . (∀ x13 . and (x13x0) (x9 = x6 x10 x13)x12)x12)x11)x11))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x10 . ∀ x11 : ο . (x10x0x8 = x6 (prim0 (λ x13 . ∀ x14 : ο . (x13x0(∀ x15 : ο . (∀ x16 . and (x16x0) (x8 = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11)) (prim0 (λ x10 . ∀ x11 : ο . (x10x0x9 = x6 (prim0 (λ x13 . ∀ x14 : ο . (x13x0(∀ x15 : ο . (∀ x16 . and (x16x0) (x9 = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11))))) (x3 (x4 (prim0 (λ x10 . ∀ x11 : ο . (x10x0(∀ x12 : ο . (∀ x13 . and (x13x0) (x8 = x6 x10 x13)x12)x12)x11)x11)) (prim0 (λ x10 . ∀ x11 : ο . (x10x0x9 = x6 (prim0 (λ x13 . ∀ x14 : ο . (x13x0(∀ x15 : ο . (∀ x16 . and (x16x0) (x9 = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11))) (x4 (prim0 (λ x10 . ∀ x11 : ο . (x10x0x8 = x6 (prim0 (λ x13 . ∀ x14 : ο . (x13x0(∀ x15 : ο . (∀ x16 . and (x16x0) (x8 = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11)) (prim0 (λ x10 . ∀ x11 : ο . (x10x0(∀ x12 : ο . (∀ x13 . and (x13x0) (x9 = x6 x10 x13)x12)x12)x11)x11))))ReplSep2 x0 (λ x10 . x0) (λ x10 x11 . True) x6)(∀ x8 . x8ReplSep2 x0 (λ x9 . x0) (λ x9 x10 . True) x6∀ x9 . x9ReplSep2 x0 (λ x10 . x0) (λ x10 x11 . True) x6prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x6 (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x9 = x6 x16 x19)x18)x18)x17)x17))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))))) (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x9 = x6 x16 x19)x18)x18)x17)x17)))) = x6 x11 x14)x13)x13)x12)x12) = x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x8 = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x9 = x6 x11 x14)x13)x13)x12)x12))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0x8 = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0x9 = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x9 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)))))(∀ x8 . x8ReplSep2 x0 (λ x9 . x0) (λ x9 x10 . True) x6∀ x9 . x9ReplSep2 x0 (λ x10 . x0) (λ x10 x11 . True) x6prim0 (λ x11 . ∀ x12 : ο . (x11x0x6 (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x9 = x6 x14 x17)x16)x16)x15)x15))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))))) (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x9 = x6 x14 x17)x16)x16)x15)x15)))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x6 (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))))) (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20)))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12) = x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x8 = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0x9 = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x9 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))) (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0x8 = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x9 = x6 x11 x14)x13)x13)x12)x12))))x7)x7
Param explicit_Fieldexplicit_Field : ιιι(ιιι) → (ιιι) → ο
Param explicit_Complexexplicit_Complex : ι(ιι) → (ιι) → ιιι(ιιι) → (ιιι) → ο
Param SubqSubq : ιιο
Known 6b23b.. : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . ∀ x6 : ι → ι → ι . explicit_Reals x0 x1 x2 x3 x4 x5(∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0x6 x7 x8 = x6 x9 x10and (x7 = x9) (x8 = x10))explicit_Field (ReplSep2 x0 (λ x7 . x0) (λ x7 x8 . True) x6) (x6 x1 x1) (x6 x2 x1) (λ x7 x8 . x6 (x3 (prim0 (λ x9 . and (x9x0) (∀ x10 : ο . (∀ x11 . and (x11x0) (x7 = x6 x9 x11)x10)x10))) (prim0 (λ x9 . and (x9x0) (∀ x10 : ο . (∀ x11 . and (x11x0) (x8 = x6 x9 x11)x10)x10)))) (x3 (prim0 (λ x9 . and (x9x0) (x7 = x6 (prim0 (λ x11 . and (x11x0) (∀ x12 : ο . (∀ x13 . and (x13x0) (x7 = x6 x11 x13)x12)x12))) x9))) (prim0 (λ x9 . and (x9x0) (x8 = x6 (prim0 (λ x11 . and (x11x0) (∀ x12 : ο . (∀ x13 . and (x13x0) (x8 = x6 x11 x13)x12)x12))) x9))))) (λ x7 x8 . x6 (x3 (x4 (prim0 (λ x9 . and (x9x0) (∀ x10 : ο . (∀ x11 . and (x11x0) (x7 = x6 x9 x11)x10)x10))) (prim0 (λ x9 . and (x9x0) (∀ x10 : ο . (∀ x11 . and (x11x0) (x8 = x6 x9 x11)x10)x10)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x9 . and (x9x0) (x7 = x6 (prim0 (λ x11 . and (x11x0) (∀ x12 : ο . (∀ x13 . and (x13x0) (x7 = x6 x11 x13)x12)x12))) x9))) (prim0 (λ x9 . and (x9x0) (x8 = x6 (prim0 (λ x11 . and (x11x0) (∀ x12 : ο . (∀ x13 . and (x13x0) (x8 = x6 x11 x13)x12)x12))) x9)))))) (x3 (x4 (prim0 (λ x9 . and (x9x0) (∀ x10 : ο . (∀ x11 . and (x11x0) (x7 = x6 x9 x11)x10)x10))) (prim0 (λ x9 . and (x9x0) (x8 = x6 (prim0 (λ x11 . and (x11x0) (∀ x12 : ο . (∀ x13 . and (x13x0) (x8 = x6 x11 x13)x12)x12))) x9)))) (x4 (prim0 (λ x9 . and (x9x0) (x7 = x6 (prim0 (λ x11 . and (x11x0) (∀ x12 : ο . (∀ x13 . and (x13x0) (x7 = x6 x11 x13)x12)x12))) x9))) (prim0 (λ x9 . and (x9x0) (∀ x10 : ο . (∀ x11 . and (x11x0) (x8 = x6 x9 x11)x10)x10))))))∀ x7 : ο . (explicit_Complex (ReplSep2 x0 (λ x8 . x0) (λ x8 x9 . True) x6) (λ x8 . x6 (prim0 (λ x9 . and (x9x0) (∀ x10 : ο . (∀ x11 . and (x11x0) (x8 = x6 x9 x11)x10)x10))) x1) (λ x8 . x6 (prim0 (λ x9 . and (x9x0) (x8 = x6 (prim0 (λ x11 . and (x11x0) (∀ x12 : ο . (∀ x13 . and (x13x0) (x8 = x6 x11 x13)x12)x12))) x9))) x1) (x6 x1 x1) (x6 x2 x1) (x6 x1 x2) (λ x8 x9 . x6 (x3 (prim0 (λ x10 . and (x10x0) (∀ x11 : ο . (∀ x12 . and (x12x0) (x8 = x6 x10 x12)x11)x11))) (prim0 (λ x10 . and (x10x0) (∀ x11 : ο . (∀ x12 . and (x12x0) (x9 = x6 x10 x12)x11)x11)))) (x3 (prim0 (λ x10 . and (x10x0) (x8 = x6 (prim0 (λ x12 . and (x12x0) (∀ x13 : ο . (∀ x14 . and (x14x0) (x8 = x6 x12 x14)x13)x13))) x10))) (prim0 (λ x10 . and (x10x0) (x9 = x6 (prim0 (λ x12 . and (x12x0) (∀ x13 : ο . (∀ x14 . and (x14x0) (x9 = x6 x12 x14)x13)x13))) x10))))) (λ x8 x9 . x6 (x3 (x4 (prim0 (λ x10 . and (x10x0) (∀ x11 : ο . (∀ x12 . and (x12x0) (x8 = x6 x10 x12)x11)x11))) (prim0 (λ x10 . and (x10x0) (∀ x11 : ο . (∀ x12 . and (x12x0) (x9 = x6 x10 x12)x11)x11)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x10 . and (x10x0) (x8 = x6 (prim0 (λ x12 . and (x12x0) (∀ x13 : ο . (∀ x14 . and (x14x0) (x8 = x6 x12 x14)x13)x13))) x10))) (prim0 (λ x10 . and (x10x0) (x9 = x6 (prim0 (λ x12 . and (x12x0) (∀ x13 : ο . (∀ x14 . and (x14x0) (x9 = x6 x12 x14)x13)x13))) x10)))))) (x3 (x4 (prim0 (λ x10 . and (x10x0) (∀ x11 : ο . (∀ x12 . and (x12x0) (x8 = x6 x10 x12)x11)x11))) (prim0 (λ x10 . and (x10x0) (x9 = x6 (prim0 (λ x12 . and (x12x0) (∀ x13 : ο . (∀ x14 . and (x14x0) (x9 = x6 x12 x14)x13)x13))) x10)))) (x4 (prim0 (λ x10 . and (x10x0) (x8 = x6 (prim0 (λ x12 . and (x12x0) (∀ x13 : ο . (∀ x14 . and (x14x0) (x8 = x6 x12 x14)x13)x13))) x10))) (prim0 (λ x10 . and (x10x0) (∀ x11 : ο . (∀ x12 . and (x12x0) (x9 = x6 x10 x12)x11)x11))))))((∀ x8 . x8x0x6 x8 x1 = x8)∀ x8 : ο . ((∀ x9 : ο . ((∀ x10 : ο . ((∀ x11 : ο . ((∀ x12 : ο . (x0ReplSep2 x0 (λ x13 . x0) (λ x13 x14 . True) x6(∀ x13 . x13x0prim0 (λ x15 . and (x15x0) (∀ x16 : ο . (∀ x17 . and (x17x0) (x13 = x6 x15 x17)x16)x16)) = x13)x12)x12)x6 x1 x1 = x1x11)x11)x6 x2 x1 = x2x10)x10)(∀ x10 . x10x0∀ x11 . x11x0x6 (x3 (prim0 (λ x13 . and (x13x0) (∀ x14 : ο . (∀ x15 . and (x15x0) (x10 = x6 x13 x15)x14)x14))) (prim0 (λ x13 . and (x13x0) (∀ x14 : ο . (∀ x15 . and (x15x0) (x11 = x6 x13 x15)x14)x14)))) (x3 (prim0 (λ x13 . and (x13x0) (x10 = x6 (prim0 (λ x15 . and (x15x0) (∀ x16 : ο . (∀ x17 . and (x17x0) (x10 = x6 x15 x17)x16)x16))) x13))) (prim0 (λ x13 . and (x13x0) (x11 = x6 (prim0 (λ x15 . and (x15x0) (∀ x16 : ο . (∀ x17 . and (x17x0) (x11 = x6 x15 x17)x16)x16))) x13)))) = x3 x10 x11)x9)x9)(∀ x9 . x9x0∀ x10 . x10x0x6 (x3 (x4 (prim0 (λ x12 . and (x12x0) (∀ x13 : ο . (∀ x14 . and (x14x0) (x9 = x6 x12 x14)x13)x13))) (prim0 (λ x12 . and (x12x0) (∀ x13 : ο . (∀ x14 . and (x14x0) (x10 = x6 x12 x14)x13)x13)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x12 . and (x12x0) (x9 = x6 (prim0 (λ x14 . and (x14x0) (∀ x15 : ο . (∀ x16 . and (x16x0) (x9 = x6 x14 x16)x15)x15))) x12))) (prim0 (λ x12 . and (x12x0) (x10 = x6 (prim0 (λ x14 . and (x14x0) (∀ x15 : ο . (∀ x16 . and (x16x0) (x10 = x6 x14 x16)x15)x15))) x12)))))) (x3 (x4 (prim0 (λ x12 . and (x12x0) (∀ x13 : ο . (∀ x14 . and (x14x0) (x9 = x6 x12 x14)x13)x13))) (prim0 (λ x12 . and (x12x0) (x10 = x6 (prim0 (λ x14 . and (x14x0) (∀ x15 : ο . (∀ x16 . and (x16x0) (x10 = x6 x14 x16)x15)x15))) x12)))) (x4 (prim0 (λ x12 . and (x12x0) (x9 = x6 (prim0 (λ x14 . and (x14x0) (∀ x15 : ο . (∀ x16 . and (x16x0) (x9 = x6 x14 x16)x15)x15))) x12))) (prim0 (λ x12 . and (x12x0) (∀ x13 : ο . (∀ x14 . and (x14x0) (x10 = x6 x12 x14)x13)x13))))) = x4 x9 x10)x8)x8)x7)x7
Known 95cf4.. : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . ∀ x6 : ι → ι → ι . (∀ x7 . x7x0∀ x8 . x8x0x6 x7 x8ReplSep2 x0 (λ x9 . x0) (λ x9 x10 . True) x6)(∀ x7 . x7x0∀ x8 . x8x0prim0 (λ x10 . ∀ x11 : ο . (x10x0(∀ x12 : ο . (∀ x13 . and (x13x0) (x6 x7 x8 = x6 x10 x13)x12)x12)x11)x11) = x7)(∀ x7 . x7x0∀ x8 . x8x0prim0 (λ x10 . ∀ x11 : ο . (x10x0x6 x7 x8 = x6 (prim0 (λ x13 . ∀ x14 : ο . (x13x0(∀ x15 : ο . (∀ x16 . and (x16x0) (x6 x7 x8 = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11) = x8)(∀ x7 . x7ReplSep2 x0 (λ x8 . x0) (λ x8 x9 . True) x6prim0 (λ x8 . ∀ x9 : ο . (x8x0(∀ x10 : ο . (∀ x11 . and (x11x0) (x7 = x6 x8 x11)x10)x10)x9)x9)x0)(∀ x7 . x7ReplSep2 x0 (λ x8 . x0) (λ x8 x9 . True) x6prim0 (λ x8 . ∀ x9 : ο . (x8x0x7 = x6 (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x7 = x6 x11 x14)x13)x13)x12)x12)) x8x9)x9)x0)(∀ x7 . x7ReplSep2 x0 (λ x8 . x0) (λ x8 x9 . True) x6∀ x8 . x8ReplSep2 x0 (λ x9 . x0) (λ x9 x10 . True) x6prim0 (λ x10 . ∀ x11 : ο . (x10x0(∀ x12 : ο . (∀ x13 . and (x13x0) (x7 = x6 x10 x13)x12)x12)x11)x11) = prim0 (λ x10 . ∀ x11 : ο . (x10x0(∀ x12 : ο . (∀ x13 . and (x13x0) (x8 = x6 x10 x13)x12)x12)x11)x11)prim0 (λ x10 . ∀ x11 : ο . (x10x0x7 = x6 (prim0 (λ x13 . ∀ x14 : ο . (x13x0(∀ x15 : ο . (∀ x16 . and (x16x0) (x7 = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11) = prim0 (λ x10 . ∀ x11 : ο . (x10x0x8 = x6 (prim0 (λ x13 . ∀ x14 : ο . (x13x0(∀ x15 : ο . (∀ x16 . and (x16x0) (x8 = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11)x7 = x8)x6 x1 x1ReplSep2 x0 (λ x7 . x0) (λ x7 x8 . True) x6x6 x2 x1ReplSep2 x0 (λ x7 . x0) (λ x7 x8 . True) x6(∀ x7 . x7ReplSep2 x0 (λ x8 . x0) (λ x8 x9 . True) x6∀ x8 . x8ReplSep2 x0 (λ x9 . x0) (λ x9 x10 . True) x6x6 (x3 (prim0 (λ x9 . ∀ x10 : ο . (x9x0(∀ x11 : ο . (∀ x12 . and (x12x0) (x7 = x6 x9 x12)x11)x11)x10)x10)) (prim0 (λ x9 . ∀ x10 : ο . (x9x0(∀ x11 : ο . (∀ x12 . and (x12x0) (x8 = x6 x9 x12)x11)x11)x10)x10))) (x3 (prim0 (λ x9 . ∀ x10 : ο . (x9x0x7 = x6 (prim0 (λ x12 . ∀ x13 : ο . (x12x0(∀ x14 : ο . (∀ x15 . and (x15x0) (x7 = x6 x12 x15)x14)x14)x13)x13)) x9x10)x10)) (prim0 (λ x9 . ∀ x10 : ο . (x9x0x8 = x6 (prim0 (λ x12 . ∀ x13 : ο . (x12x0(∀ x14 : ο . (∀ x15 . and (x15x0) (x8 = x6 x12 x15)x14)x14)x13)x13)) x9x10)x10)))ReplSep2 x0 (λ x9 . x0) (λ x9 x10 . True) x6)(∀ x7 . x7ReplSep2 x0 (λ x8 . x0) (λ x8 x9 . True) x6∀ x8 . x8ReplSep2 x0 (λ x9 . x0) (λ x9 x10 . True) x6prim0 (λ x10 . ∀ x11 : ο . (x10x0(∀ x12 : ο . (∀ x13 . and (x13x0) (x6 (x3 (prim0 (λ x15 . ∀ x16 : ο . (x15x0(∀ x17 : ο . (∀ x18 . and (x18x0) (x7 = x6 x15 x18)x17)x17)x16)x16)) (prim0 (λ x15 . ∀ x16 : ο . (x15x0(∀ x17 : ο . (∀ x18 . and (x18x0) (x8 = x6 x15 x18)x17)x17)x16)x16))) (x3 (prim0 (λ x15 . ∀ x16 : ο . (x15x0x7 = x6 (prim0 (λ x18 . ∀ x19 : ο . (x18x0(∀ x20 : ο . (∀ x21 . and (x21x0) (x7 = x6 x18 x21)x20)x20)x19)x19)) x15x16)x16)) (prim0 (λ x15 . ∀ x16 : ο . (x15x0x8 = x6 (prim0 (λ x18 . ∀ x19 : ο . (x18x0(∀ x20 : ο . (∀ x21 . and (x21x0) (x8 = x6 x18 x21)x20)x20)x19)x19)) x15x16)x16))) = x6 x10 x13)x12)x12)x11)x11) = x3 (prim0 (λ x10 . ∀ x11 : ο . (x10x0(∀ x12 : ο . (∀ x13 . and (x13x0) (x7 = x6 x10 x13)x12)x12)x11)x11)) (prim0 (λ x10 . ∀ x11 : ο . (x10x0(∀ x12 : ο . (∀ x13 . and (x13x0) (x8 = x6 x10 x13)x12)x12)x11)x11)))(∀ x7 . x7ReplSep2 x0 (λ x8 . x0) (λ x8 x9 . True) x6∀ x8 . x8ReplSep2 x0 (λ x9 . x0) (λ x9 x10 . True) x6prim0 (λ x10 . ∀ x11 : ο . (x10x0x6 (x3 (prim0 (λ x13 . ∀ x14 : ο . (x13x0(∀ x15 : ο . (∀ x16 . and (x16x0) (x7 = x6 x13 x16)x15)x15)x14)x14)) (prim0 (λ x13 . ∀ x14 : ο . (x13x0(∀ x15 : ο . (∀ x16 . and (x16x0) (x8 = x6 x13 x16)x15)x15)x14)x14))) (x3 (prim0 (λ x13 . ∀ x14 : ο . (x13x0x7 = x6 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) x13x14)x14)) (prim0 (λ x13 . ∀ x14 : ο . (x13x0x8 = x6 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) x13x14)x14))) = x6 (prim0 (λ x13 . ∀ x14 : ο . (x13x0(∀ x15 : ο . (∀ x16 . and (x16x0) (x6 (x3 (prim0 (λ x18 . ∀ x19 : ο . (x18x0(∀ x20 : ο . (∀ x21 . and (x21x0) (x7 = x6 x18 x21)x20)x20)x19)x19)) (prim0 (λ x18 . ∀ x19 : ο . (x18x0(∀ x20 : ο . (∀ x21 . and (x21x0) (x8 = x6 x18 x21)x20)x20)x19)x19))) (x3 (prim0 (λ x18 . ∀ x19 : ο . (x18x0x7 = x6 (prim0 (λ x21 . ∀ x22 : ο . (x21x0(∀ x23 : ο . (∀ x24 . and (x24x0) (x7 = x6 x21 x24)x23)x23)x22)x22)) x18x19)x19)) (prim0 (λ x18 . ∀ x19 : ο . (x18x0x8 = x6 (prim0 (λ x21 . ∀ x22 : ο . (x21x0(∀ x23 : ο . (∀ x24 . and (x24x0) (x8 = x6 x21 x24)x23)x23)x22)x22)) x18x19)x19))) = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11) = x3 (prim0 (λ x10 . ∀ x11 : ο . (x10x0x7 = x6 (prim0 (λ x13 . ∀ x14 : ο . (x13x0(∀ x15 : ο . (∀ x16 . and (x16x0) (x7 = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11)) (prim0 (λ x10 . ∀ x11 : ο . (x10x0x8 = x6 (prim0 (λ x13 . ∀ x14 : ο . (x13x0(∀ x15 : ο . (∀ x16 . and (x16x0) (x8 = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11)))(∀ x7 . x7ReplSep2 x0 (λ x8 . x0) (λ x8 x9 . True) x6∀ x8 . x8ReplSep2 x0 (λ x9 . x0) (λ x9 x10 . True) x6x6 (x3 (x4 (prim0 (λ x9 . ∀ x10 : ο . (x9x0(∀ x11 : ο . (∀ x12 . and (x12x0) (x7 = x6 x9 x12)x11)x11)x10)x10)) (prim0 (λ x9 . ∀ x10 : ο . (x9x0(∀ x11 : ο . (∀ x12 . and (x12x0) (x8 = x6 x9 x12)x11)x11)x10)x10))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x9 . ∀ x10 : ο . (x9x0x7 = x6 (prim0 (λ x12 . ∀ x13 : ο . (x12x0(∀ x14 : ο . (∀ x15 . and (x15x0) (x7 = x6 x12 x15)x14)x14)x13)x13)) x9x10)x10)) (prim0 (λ x9 . ∀ x10 : ο . (x9x0x8 = x6 (prim0 (λ x12 . ∀ x13 : ο . (x12x0(∀ x14 : ο . (∀ x15 . and (x15x0) (x8 = x6 x12 x15)x14)x14)x13)x13)) x9x10)x10))))) (x3 (x4 (prim0 (λ x9 . ∀ x10 : ο . (x9x0(∀ x11 : ο . (∀ x12 . and (x12x0) (x7 = x6 x9 x12)x11)x11)x10)x10)) (prim0 (λ x9 . ∀ x10 : ο . (x9x0x8 = x6 (prim0 (λ x12 . ∀ x13 : ο . (x12x0(∀ x14 : ο . (∀ x15 . and (x15x0) (x8 = x6 x12 x15)x14)x14)x13)x13)) x9x10)x10))) (x4 (prim0 (λ x9 . ∀ x10 : ο . (x9x0x7 = x6 (prim0 (λ x12 . ∀ x13 : ο . (x12x0(∀ x14 : ο . (∀ x15 . and (x15x0) (x7 = x6 x12 x15)x14)x14)x13)x13)) x9x10)x10)) (prim0 (λ x9 . ∀ x10 : ο . (x9x0(∀ x11 : ο . (∀ x12 . and (x12x0) (x8 = x6 x9 x12)x11)x11)x10)x10))))ReplSep2 x0 (λ x9 . x0) (λ x9 x10 . True) x6)(∀ x7 . x7ReplSep2 x0 (λ x8 . x0) (λ x8 x9 . True) x6∀ x8 . x8ReplSep2 x0 (λ x9 . x0) (λ x9 x10 . True) x6prim0 (λ x10 . ∀ x11 : ο . (x10x0(∀ x12 : ο . (∀ x13 . and (x13x0) (x6 (x3 (x4 (prim0 (λ x15 . ∀ x16 : ο . (x15x0(∀ x17 : ο . (∀ x18 . and (x18x0) (x7 = x6 x15 x18)x17)x17)x16)x16)) (prim0 (λ x15 . ∀ x16 : ο . (x15x0(∀ x17 : ο . (∀ x18 . and (x18x0) (x8 = x6 x15 x18)x17)x17)x16)x16))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x15 . ∀ x16 : ο . (x15x0x7 = x6 (prim0 (λ x18 . ∀ x19 : ο . (x18x0(∀ x20 : ο . (∀ x21 . and (x21x0) (x7 = x6 x18 x21)x20)x20)x19)x19)) x15x16)x16)) (prim0 (λ x15 . ∀ x16 : ο . (x15x0x8 = x6 (prim0 (λ x18 . ∀ x19 : ο . (x18x0(∀ x20 : ο . (∀ x21 . and (x21x0) (x8 = x6 x18 x21)x20)x20)x19)x19)) x15x16)x16))))) (x3 (x4 (prim0 (λ x15 . ∀ x16 : ο . (x15x0(∀ x17 : ο . (∀ x18 . and (x18x0) (x7 = x6 x15 x18)x17)x17)x16)x16)) (prim0 (λ x15 . ∀ x16 : ο . (x15x0x8 = x6 (prim0 (λ x18 . ∀ x19 : ο . (x18x0(∀ x20 : ο . (∀ x21 . and (x21x0) (x8 = x6 x18 x21)x20)x20)x19)x19)) x15x16)x16))) (x4 (prim0 (λ x15 . ∀ x16 : ο . (x15x0x7 = x6 (prim0 (λ x18 . ∀ x19 : ο . (x18x0(∀ x20 : ο . (∀ x21 . and (x21x0) (x7 = x6 x18 x21)x20)x20)x19)x19)) x15x16)x16)) (prim0 (λ x15 . ∀ x16 : ο . (x15x0(∀ x17 : ο . (∀ x18 . and (x18x0) (x8 = x6 x15 x18)x17)x17)x16)x16)))) = x6 x10 x13)x12)x12)x11)x11) = x3 (x4 (prim0 (λ x10 . ∀ x11 : ο . (x10x0(∀ x12 : ο . (∀ x13 . and (x13x0) (x7 = x6 x10 x13)x12)x12)x11)x11)) (prim0 (λ x10 . ∀ x11 : ο . (x10x0(∀ x12 : ο . (∀ x13 . and (x13x0) (x8 = x6 x10 x13)x12)x12)x11)x11))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x10 . ∀ x11 : ο . (x10x0x7 = x6 (prim0 (λ x13 . ∀ x14 : ο . (x13x0(∀ x15 : ο . (∀ x16 . and (x16x0) (x7 = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11)) (prim0 (λ x10 . ∀ x11 : ο . (x10x0x8 = x6 (prim0 (λ x13 . ∀ x14 : ο . (x13x0(∀ x15 : ο . (∀ x16 . and (x16x0) (x8 = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11)))))(∀ x7 . x7ReplSep2 x0 (λ x8 . x0) (λ x8 x9 . True) x6∀ x8 . x8ReplSep2 x0 (λ x9 . x0) (λ x9 x10 . True) x6prim0 (λ x10 . ∀ x11 : ο . (x10x0x6 (x3 (x4 (prim0 (λ x13 . ∀ x14 : ο . (x13x0(∀ x15 : ο . (∀ x16 . and (x16x0) (x7 = x6 x13 x16)x15)x15)x14)x14)) (prim0 (λ x13 . ∀ x14 : ο . (x13x0(∀ x15 : ο . (∀ x16 . and (x16x0) (x8 = x6 x13 x16)x15)x15)x14)x14))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x13 . ∀ x14 : ο . (x13x0x7 = x6 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) x13x14)x14)) (prim0 (λ x13 . ∀ x14 : ο . (x13x0x8 = x6 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) x13x14)x14))))) (x3 (x4 (prim0 (λ x13 . ∀ x14 : ο . (x13x0(∀ x15 : ο . (∀ x16 . and (x16x0) (x7 = x6 x13 x16)x15)x15)x14)x14)) (prim0 (λ x13 . ∀ x14 : ο . (x13x0x8 = x6 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) x13x14)x14))) (x4 (prim0 (λ x13 . ∀ x14 : ο . (x13x0x7 = x6 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) x13x14)x14)) (prim0 (λ x13 . ∀ x14 : ο . (x13x0(∀ x15 : ο . (∀ x16 . and (x16x0) (x8 = x6 x13 x16)x15)x15)x14)x14)))) = x6 (prim0 (λ x13 . ∀ x14 : ο . (x13x0(∀ x15 : ο . (∀ x16 . and (x16x0) (x6 (x3 (x4 (prim0 (λ x18 . ∀ x19 : ο . (x18x0(∀ x20 : ο . (∀ x21 . and (x21x0) (x7 = x6 x18 x21)x20)x20)x19)x19)) (prim0 (λ x18 . ∀ x19 : ο . (x18x0(∀ x20 : ο . (∀ x21 . and (x21x0) (x8 = x6 x18 x21)x20)x20)x19)x19))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x18 . ∀ x19 : ο . (x18x0x7 = x6 (prim0 (λ x21 . ∀ x22 : ο . (x21x0(∀ x23 : ο . (∀ x24 . and (x24x0) (x7 = x6 x21 x24)x23)x23)x22)x22)) x18x19)x19)) (prim0 (λ x18 . ∀ x19 : ο . (x18x0x8 = x6 (prim0 (λ x21 . ∀ x22 : ο . (x21x0(∀ x23 : ο . (∀ x24 . and (x24x0) (x8 = x6 x21 x24)x23)x23)x22)x22)) x18x19)x19))))) (x3 (x4 (prim0 (λ x18 . ∀ x19 : ο . (x18x0(∀ x20 : ο . (∀ x21 . and (x21x0) (x7 = x6 x18 x21)x20)x20)x19)x19)) (prim0 (λ x18 . ∀ x19 : ο . (x18x0x8 = x6 (prim0 (λ x21 . ∀ x22 : ο . (x21x0(∀ x23 : ο . (∀ x24 . and (x24x0) (x8 = x6 x21 x24)x23)x23)x22)x22)) x18x19)x19))) (x4 (prim0 (λ x18 . ∀ x19 : ο . (x18x0x7 = x6 (prim0 (λ x21 . ∀ x22 : ο . (x21x0(∀ x23 : ο . (∀ x24 . and (x24x0) (x7 = x6 x21 x24)x23)x23)x22)x22)) x18x19)x19)) (prim0 (λ x18 . ∀ x19 : ο . (x18x0(∀ x20 : ο . (∀ x21 . and (x21x0) (x8 = x6 x18 x21)x20)x20)x19)x19)))) = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11) = x3 (x4 (prim0 (λ x10 . ∀ x11 : ο . (x10x0(∀ x12 : ο . (∀ x13 . and (x13x0) (x7 = x6 x10 x13)x12)x12)x11)x11)) (prim0 (λ x10 . ∀ x11 : ο . (x10x0x8 = x6 (prim0 (λ x13 . ∀ x14 : ο . (x13x0(∀ x15 : ο . (∀ x16 . and (x16x0) (x8 = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11))) (x4 (prim0 (λ x10 . ∀ x11 : ο . (x10x0x7 = x6 (prim0 (λ x13 . ∀ x14 : ο . (x13x0(∀ x15 : ο . (∀ x16 . and (x16x0) (x7 = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11)) (prim0 (λ x10 . ∀ x11 : ο . (x10x0(∀ x12 : ο . (∀ x13 . and (x13x0) (x8 = x6 x10 x13)x12)x12)x11)x11))))explicit_Field x0 x1 x2 x3 x4(∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0x6 x7 x8 = x6 x9 x10∀ x11 : ο . (x7 = x9x8 = x10x11)x11)(∀ x7 . x7ReplSep2 x0 (λ x8 . x0) (λ x8 x9 . True) x6∀ x8 . x8ReplSep2 x0 (λ x9 . x0) (λ x9 x10 . True) x6∀ x9 . x9ReplSep2 x0 (λ x10 . x0) (λ x10 x11 . True) x6x6 (x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x7 = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x6 (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x9 = x6 x16 x19)x18)x18)x17)x17))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))))) (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x9 = x6 x16 x19)x18)x18)x17)x17)))) = x6 x11 x14)x13)x13)x12)x12))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0x7 = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0x6 (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x9 = x6 x14 x17)x16)x16)x15)x15))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))))) (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x9 = x6 x14 x17)x16)x16)x15)x15)))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x6 (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))))) (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20)))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))))) (x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x7 = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0x6 (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x9 = x6 x14 x17)x16)x16)x15)x15))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))))) (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x9 = x6 x14 x17)x16)x16)x15)x15)))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x6 (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))))) (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20)))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))) (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0x7 = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x6 (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x9 = x6 x16 x19)x18)x18)x17)x17))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))))) (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x9 = x6 x16 x19)x18)x18)x17)x17)))) = x6 x11 x14)x13)x13)x12)x12)))) = x6 (x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x6 (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x8 = x6 x16 x19)x18)x18)x17)x17))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0x7 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))))) (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0x7 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x8 = x6 x16 x19)x18)x18)x17)x17)))) = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x9 = x6 x11 x14)x13)x13)x12)x12))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0x6 (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x8 = x6 x14 x17)x16)x16)x15)x15))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0x7 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x7 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))))) (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0x7 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x7 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x8 = x6 x14 x17)x16)x16)x15)x15)))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x6 (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0x7 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x7 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))))) (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0x7 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x7 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0x9 = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x9 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))))) (x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x6 (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x8 = x6 x16 x19)x18)x18)x17)x17))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0x7 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))))) (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0x7 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x8 = x6 x16 x19)x18)x18)x17)x17)))) = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0x9 = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x9 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))) (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0x6 (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x8 = x6 x14 x17)x16)x16)x15)x15))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0x7 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x7 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))))) (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0x7 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x7 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x8 = x6 x14 x17)x16)x16)x15)x15)))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x6 (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0x7 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x7 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))))) (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0x7 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x7 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x9 = x6 x11 x14)x13)x13)x12)x12)))))(∀ x7 . x7ReplSep2 x0 (λ x8 . x0) (λ x8 x9 . True) x6(x7 = x6 x1 x1∀ x8 : ο . x8)∀ x8 : ο . (∀ x9 . and (x9ReplSep2 x0 (λ x10 . x0) (λ x10 x11 . True) x6) (x6 (x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x7 = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x9 = x6 x11 x14)x13)x13)x12)x12))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0x7 = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0x9 = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x9 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))))) (x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x7 = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0x9 = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x9 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))) (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0x7 = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x9 = x6 x11 x14)x13)x13)x12)x12)))) = x6 x2 x1)x8)x8)(∀ x7 . x7ReplSep2 x0 (λ x8 . x0) (λ x8 x9 . True) x6∀ x8 . x8ReplSep2 x0 (λ x9 . x0) (λ x9 x10 . True) x6∀ x9 . x9ReplSep2 x0 (λ x10 . x0) (λ x10 x11 . True) x6x6 (x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x7 = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x6 (x3 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x9 = x6 x16 x19)x18)x18)x17)x17))) (x3 (prim0 (λ x16 . ∀ x17 : ο . (x16x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) = x6 x11 x14)x13)x13)x12)x12))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0x7 = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0x6 (x3 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x9 = x6 x14 x17)x16)x16)x15)x15))) (x3 (prim0 (λ x14 . ∀ x15 : ο . (x14x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x6 (x3 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20))) (x3 (prim0 (λ x19 . ∀ x20 : ο . (x19x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))))) (x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x7 = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0x6 (x3 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x9 = x6 x14 x17)x16)x16)x15)x15))) (x3 (prim0 (λ x14 . ∀ x15 : ο . (x14x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x6 (x3 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20))) (x3 (prim0 (λ x19 . ∀ x20 : ο . (x19x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))) (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0x7 = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x6 (x3 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x9 = x6 x16 x19)x18)x18)x17)x17))) (x3 (prim0 (λ x16 . ∀ x17 : ο . (x16x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) = x6 x11 x14)x13)x13)x12)x12)))) = x6 (x3 (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x6 (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x8 = x6 x16 x19)x18)x18)x17)x17))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0x7 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))))) (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0x7 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x8 = x6 x16 x19)x18)x18)x17)x17)))) = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x6 (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x9 = x6 x16 x19)x18)x18)x17)x17))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0x7 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))))) (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0x7 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x9 = x6 x16 x19)x18)x18)x17)x17)))) = x6 x11 x14)x13)x13)x12)x12))) (x3 (prim0 (λ x11 . ∀ x12 : ο . (x11x0x6 (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x8 = x6 x14 x17)x16)x16)x15)x15))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0x7 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x7 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))))) (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0x7 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x7 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x8 = x6 x14 x17)x16)x16)x15)x15)))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x6 (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0x7 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x7 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))))) (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0x7 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x7 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0x6 (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x9 = x6 x14 x17)x16)x16)x15)x15))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0x7 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x7 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))))) (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0x7 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x7 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x9 = x6 x14 x17)x16)x16)x15)x15)))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x6 (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0x7 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x7 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))))) (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0x7 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x7 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20)))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))))explicit_Field (ReplSep2 x0 (λ x7 . x0) (λ x7 x8 . True) x6) (x6 x1 x1) (x6 x2 x1) (λ x7 x8 . x6 (x3 (prim0 (λ x9 . ∀ x10 : ο . (x9x0(∀ x11 : ο . (∀ x12 . and (x12x0) (x7 = x6 x9 x12)x11)x11)x10)x10)) (prim0 (λ x9 . ∀ x10 : ο . (x9x0(∀ x11 : ο . (∀ x12 . and (x12x0) (x8 = x6 x9 x12)x11)x11)x10)x10))) (x3 (prim0 (λ x9 . ∀ x10 : ο . (x9x0x7 = x6 (prim0 (λ x12 . ∀ x13 : ο . (x12x0(∀ x14 : ο . (∀ x15 . and (x15x0) (x7 = x6 x12 x15)x14)x14)x13)x13)) x9x10)x10)) (prim0 (λ x9 . ∀ x10 : ο . (x9x0x8 = x6 (prim0 (λ x12 . ∀ x13 : ο . (x12x0(∀ x14 : ο . (∀ x15 . and (x15x0) (x8 = x6 x12 x15)x14)x14)x13)x13)) x9x10)x10)))) (λ x7 x8 . x6 (x3 (x4 (prim0 (λ x9 . ∀ x10 : ο . (x9x0(∀ x11 : ο . (∀ x12 . and (x12x0) (x7 = x6 x9 x12)x11)x11)x10)x10)) (prim0 (λ x9 . ∀ x10 : ο . (x9x0(∀ x11 : ο . (∀ x12 . and (x12x0) (x8 = x6 x9 x12)x11)x11)x10)x10))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x9 . ∀ x10 : ο . (x9x0x7 = x6 (prim0 (λ x12 . ∀ x13 : ο . (x12x0(∀ x14 : ο . (∀ x15 . and (x15x0) (x7 = x6 x12 x15)x14)x14)x13)x13)) x9x10)x10)) (prim0 (λ x9 . ∀ x10 : ο . (x9x0x8 = x6 (prim0 (λ x12 . ∀ x13 : ο . (x12x0(∀ x14 : ο . (∀ x15 . and (x15x0) (x8 = x6 x12 x15)x14)x14)x13)x13)) x9x10)x10))))) (x3 (x4 (prim0 (λ x9 . ∀ x10 : ο . (x9x0(∀ x11 : ο . (∀ x12 . and (x12x0) (x7 = x6 x9 x12)x11)x11)x10)x10)) (prim0 (λ x9 . ∀ x10 : ο . (x9x0x8 = x6 (prim0 (λ x12 . ∀ x13 : ο . (x12x0(∀ x14 : ο . (∀ x15 . and (x15x0) (x8 = x6 x12 x15)x14)x14)x13)x13)) x9x10)x10))) (x4 (prim0 (λ x9 . ∀ x10 : ο . (x9x0x7 = x6 (prim0 (λ x12 . ∀ x13 : ο . (x12x0(∀ x14 : ο . (∀ x15 . and (x15x0) (x7 = x6 x12 x15)x14)x14)x13)x13)) x9x10)x10)) (prim0 (λ x9 . ∀ x10 : ο . (x9x0(∀ x11 : ο . (∀ x12 . and (x12x0) (x8 = x6 x9 x12)x11)x11)x10)x10)))))
Param explicit_OrderedFieldexplicit_OrderedField : ιιι(ιιι) → (ιιι) → (ιιο) → ο
Param ltlt : ιιι(ιιι) → (ιιι) → (ιιο) → ιιο
Param SepSep : ι(ιο) → ι
Param natOfOrderedField_pnatOfOrderedField_p : ιιι(ιιι) → (ιιι) → (ιιο) → ιο
Param setexpsetexp : ιιι
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 iffiff : οοο
Param oror : οοο
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 a464a.. : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . ∀ x6 : ι → ι → ι . explicit_Reals x0 x1 x2 x3 x4 x5(∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0x6 x7 x8 = x6 x9 x10∀ x11 : ο . (x7 = x9x8 = x10x11)x11)(∀ x7 . x7ReplSep2 x0 (λ x8 . x0) (λ x8 x9 . True) x6∀ x8 . x8ReplSep2 x0 (λ x9 . x0) (λ x9 x10 . True) x6∀ x9 . x9ReplSep2 x0 (λ x10 . x0) (λ x10 x11 . True) x6x6 (x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x7 = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x6 (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x9 = x6 x16 x19)x18)x18)x17)x17))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))))) (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x9 = x6 x16 x19)x18)x18)x17)x17)))) = x6 x11 x14)x13)x13)x12)x12))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0x7 = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0x6 (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x9 = x6 x14 x17)x16)x16)x15)x15))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))))) (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x9 = x6 x14 x17)x16)x16)x15)x15)))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x6 (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))))) (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20)))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))))) (x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x7 = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0x6 (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x9 = x6 x14 x17)x16)x16)x15)x15))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))))) (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x9 = x6 x14 x17)x16)x16)x15)x15)))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x6 (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))))) (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20)))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))) (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0x7 = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x6 (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x9 = x6 x16 x19)x18)x18)x17)x17))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))))) (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x9 = x6 x16 x19)x18)x18)x17)x17)))) = x6 x11 x14)x13)x13)x12)x12)))) = x6 (x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x6 (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x8 = x6 x16 x19)x18)x18)x17)x17))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0x7 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))))) (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0x7 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x8 = x6 x16 x19)x18)x18)x17)x17)))) = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x9 = x6 x11 x14)x13)x13)x12)x12))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0x6 (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x8 = x6 x14 x17)x16)x16)x15)x15))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0x7 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x7 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))))) (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0x7 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x7 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x8 = x6 x14 x17)x16)x16)x15)x15)))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x6 (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0x7 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x7 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))))) (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0x7 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x7 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0x9 = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x9 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))))) (x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x6 (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x8 = x6 x16 x19)x18)x18)x17)x17))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0x7 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))))) (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0x7 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x8 = x6 x16 x19)x18)x18)x17)x17)))) = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0x9 = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x9 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))) (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0x6 (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x8 = x6 x14 x17)x16)x16)x15)x15))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0x7 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x7 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))))) (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0x7 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x7 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x8 = x6 x14 x17)x16)x16)x15)x15)))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x6 (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0x7 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x7 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))))) (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0x7 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x7 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x9 = x6 x11 x14)x13)x13)x12)x12)))))(∀ x7 . x7ReplSep2 x0 (λ x8 . x0) (λ x8 x9 . True) x6(x7 = x6 x1 x1∀ x8 : ο . x8)∀ x8 : ο . (∀ x9 . and (x9ReplSep2 x0 (λ x10 . x0) (λ x10 x11 . True) x6) (x6 (x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x7 = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x9 = x6 x11 x14)x13)x13)x12)x12))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0x7 = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0x9 = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x9 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))))) (x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x7 = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0x9 = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x9 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))) (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0x7 = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x9 = x6 x11 x14)x13)x13)x12)x12)))) = x6 x2 x1)x8)x8)(∀ x7 . x7ReplSep2 x0 (λ x8 . x0) (λ x8 x9 . True) x6∀ x8 . x8ReplSep2 x0 (λ x9 . x0) (λ x9 x10 . True) x6∀ x9 . x9ReplSep2 x0 (λ x10 . x0) (λ x10 x11 . True) x6x6 (x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x7 = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x6 (x3 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x9 = x6 x16 x19)x18)x18)x17)x17))) (x3 (prim0 (λ x16 . ∀ x17 : ο . (x16x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) = x6 x11 x14)x13)x13)x12)x12))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0x7 = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0x6 (x3 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x9 = x6 x14 x17)x16)x16)x15)x15))) (x3 (prim0 (λ x14 . ∀ x15 : ο . (x14x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x6 (x3 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20))) (x3 (prim0 (λ x19 . ∀ x20 : ο . (x19x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))))) (x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x7 = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0x6 (x3 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x9 = x6 x14 x17)x16)x16)x15)x15))) (x3 (prim0 (λ x14 . ∀ x15 : ο . (x14x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x6 (x3 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20))) (x3 (prim0 (λ x19 . ∀ x20 : ο . (x19x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))) (x4 (prim0 (λ x11 . ∀ x12 : ο . (x11x0x7 = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x6 (x3 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x9 = x6 x16 x19)x18)x18)x17)x17))) (x3 (prim0 (λ x16 . ∀ x17 : ο . (x16x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) = x6 x11 x14)x13)x13)x12)x12)))) = x6 (x3 (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x6 (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x8 = x6 x16 x19)x18)x18)x17)x17))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0x7 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))))) (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0x7 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x8 = x6 x16 x19)x18)x18)x17)x17)))) = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0(∀ x13 : ο . (∀ x14 . and (x14x0) (x6 (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x9 = x6 x16 x19)x18)x18)x17)x17))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0x7 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))))) (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) (x4 (prim0 (λ x16 . ∀ x17 : ο . (x16x0x7 = x6 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (x16x0(∀ x18 : ο . (∀ x19 . and (x19x0) (x9 = x6 x16 x19)x18)x18)x17)x17)))) = x6 x11 x14)x13)x13)x12)x12))) (x3 (prim0 (λ x11 . ∀ x12 : ο . (x11x0x6 (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x8 = x6 x14 x17)x16)x16)x15)x15))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0x7 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x7 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))))) (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0x7 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x7 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x8 = x6 x14 x17)x16)x16)x15)x15)))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x6 (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0x7 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x7 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))))) (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0x7 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x7 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x8 = x6 x19 x22)x21)x21)x20)x20)))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (x11x0x6 (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x9 = x6 x14 x17)x16)x16)x15)x15))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0x7 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x7 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))))) (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) (x4 (prim0 (λ x14 . ∀ x15 : ο . (x14x0x7 = x6 (prim0 (λ x17 . ∀ x18 : ο . (x17x0(∀ x19 : ο . (∀ x20 . and (x20x0) (x7 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x9 = x6 x14 x17)x16)x16)x15)x15)))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (x14x0(∀ x16 : ο . (∀ x17 . and (x17x0) (x6 (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0x7 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x7 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))))) (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) (x4 (prim0 (λ x19 . ∀ x20 : ο . (x19x0x7 = x6 (prim0 (λ x22 . ∀ x23 : ο . (x22x0(∀ x24 : ο . (∀ x25 . and (x25x0) (x7 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (x19x0(∀ x21 : ο . (∀ x22 . and (x22x0) (x9 = x6 x19 x22)x21)x21)x20)x20)))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))))and (explicit_Complex (ReplSep2 x0 (λ x7 . x0) (λ x7 x8 . True) x6) (λ x7 . x6 (prim0 (λ x8 . and (x8x0) (∀ x9 : ο . (∀ x10 . and (x10x0) (x7 = x6 x8 x10)x9)x9))) x1) (λ x7 . x6 (prim0 (λ x8 . and (x8x0) (x7 = x6 (prim0 (λ x10 . and (x10x0) (∀ x11 : ο . (∀ x12 . and (x12x0) (x7 = x6 x10 x12)x11)x11))) x8))) x1) (x6 x1 x1) (x6 x2 x1) (x6 x1 x2) (λ x7 x8 . x6 (x3 (prim0 (λ x9 . and (x9x0) (∀ x10 : ο . (∀ x11 . and (x11x0) (x7 = x6 x9 x11)x10)x10))) (prim0 (λ x9 . and (x9x0) (∀ x10 : ο . (∀ x11 . and (x11x0) (x8 = x6 x9 x11)x10)x10)))) (x3 (prim0 (λ x9 . and (x9x0) (x7 = x6 (prim0 (λ x11 . and (x11x0) (∀ x12 : ο . (∀ x13 . and (x13x0) (x7 = x6 x11 x13)x12)x12))) x9))) (prim0 (λ x9 . and (x9x0) (x8 = x6 (prim0 (λ x11 . and (x11x0) (∀ x12 : ο . (∀ x13 . and (x13x0) (x8 = x6 x11 x13)x12)x12))) x9))))) (λ x7 x8 . x6 (x3 (x4 (prim0 (λ x9 . and (x9x0) (∀ x10 : ο . (∀ x11 . and (x11x0) (x7 = x6 x9 x11)x10)x10))) (prim0 (λ x9 . and (x9x0) (∀ x10 : ο . (∀ x11 . and (x11x0) (x8 = x6 x9 x11)x10)x10)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x9 . and (x9x0) (x7 = x6 (prim0 (λ x11 . and (x11x0) (∀ x12 : ο . (∀ x13 . and (x13x0) (x7 = x6 x11 x13)x12)x12))) x9))) (prim0 (λ x9 . and (x9x0) (x8 = x6 (prim0 (λ x11 . and (x11x0) (∀ x12 : ο . (∀ x13 . and (x13x0) (x8 = x6 x11 x13)x12)x12))) x9)))))) (x3 (x4 (prim0 (λ x9 . and (x9x0) (∀ x10 : ο . (∀ x11 . and (x11x0) (x7 = x6 x9 x11)x10)x10))) (prim0 (λ x9 . and (x9x0) (x8 = x6 (prim0 (λ x11 . and (x11x0) (∀ x12 : ο . (∀ x13 . and (x13x0) (x8 = x6 x11 x13)x12)x12))) x9)))) (x4 (prim0 (λ x9 . and (x9x0) (x7 = x6 (prim0 (λ x11 . and (x11x0) (∀ x12 : ο . (∀ x13 . and (x13x0) (x7 = x6 x11 x13)x12)x12))) x9))) (prim0 (λ x9 . and (x9x0) (∀ x10 : ο . (∀ x11 . and (x11x0) (x8 = x6 x9 x11)x10)x10))))))) ((∀ x7 . x7x0x6 x7 x1 = x7)and (and (and (and (and (x0ReplSep2 x0 (λ x7 . x0) (λ x7 x8 . True) x6) (∀ x7 . x7x0prim0 (λ x9 . and (x9x0) (∀ x10 : ο . (∀ x11 . and (x11x0) (x7 = x6 x9 x11)x10)x10)) = x7)) (x6 x1 x1 = x1)) (x6 x2 x1 = x2)) (∀ x7 . x7x0∀ x8 . x8x0x6 (x3 (prim0 (λ x10 . and (x10x0) (∀ x11 : ο . (∀ x12 . and (x12x0) (x7 = x6 x10 x12)x11)x11))) (prim0 (λ x10 . and (x10x0) (∀ x11 : ο . (∀ x12 . and (x12x0) (x8 = x6 x10 x12)x11)x11)))) (x3 (prim0 (λ x10 . and (x10x0) (x7 = x6 (prim0 (λ x12 . and (x12x0) (∀ x13 : ο . (∀ x14 . and (x14x0) (x7 = x6 x12 x14)x13)x13))) x10))) (prim0 (λ x10 . and (x10x0) (x8 = x6 (prim0 (λ x12 . and (x12x0) (∀ x13 : ο . (∀ x14 . and (x14x0) (x8 = x6 x12 x14)x13)x13))) x10)))) = x3 x7 x8)) (∀ x7 . x7x0∀ x8 . x8x0x6 (x3 (x4 (prim0 (λ x10 . and (x10x0) (∀ x11 : ο . (∀ x12 . and (x12x0) (x7 = x6 x10 x12)x11)x11))) (prim0 (λ x10 . and (x10x0) (∀ x11 : ο . (∀ x12 . and (x12x0) (x8 = x6 x10 x12)x11)x11)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x10 . and (x10x0) (x7 = x6 (prim0 (λ x12 . and (x12x0) (∀ x13 : ο . (∀ x14 . and (x14x0) (x7 = x6 x12 x14)x13)x13))) x10))) (prim0 (λ x10 . and (x10x0) (x8 = x6 (prim0 (λ x12 . and (x12x0) (∀ x13 : ο . (∀ x14 . and (x14x0) (x8 = x6 x12 x14)x13)x13))) x10)))))) (x3 (x4 (prim0 (λ x10 . and (x10x0) (∀ x11 : ο . (∀ x12 . and (x12x0) (x7 = x6 x10 x12)x11)x11))) (prim0 (λ x10 . and (x10x0) (x8 = x6 (prim0 (λ x12 . and (x12x0) (∀ x13 : ο . (∀ x14 . and (x14x0) (x8 = x6 x12 x14)x13)x13))) x10)))) (x4 (prim0 (λ x10 . and (x10x0) (x7 = x6 (prim0 (λ x12 . and (x12x0) (∀ x13 : ο . (∀ x14 . and (x14x0) (x7 = x6 x12 x14)x13)x13))) x10))) (prim0 (λ x10 . and (x10x0) (∀ x11 : ο . (∀ x12 . and (x12x0) (x8 = x6 x10 x12)x11)x11))))) = x4 x7 x8)) (proof)

previous assets