Search for blocks/addresses/...

Proofgold Asset

asset id
a920fbeb9a66ad3b566e0067b02b9c68eba38d0a5c30f61d05fc3d589892c55a
asset hash
8958f6d4634330351b2ce7618d6e4c97849d17fb5b278cf8c3c99c0d36beb61e
bday / block
3982
tx
2436f..
preasset
doc published by PrGxv..
Param 62ee1.. : ιιι(ιιι) → (ιιι) → (ιιο) → ο
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Param 3b429.. : ι(ιι) → (ιιο) → CT2 ι
Param True : ο
Param explicit_Field_minus : ιιι(ιιι) → (ιιι) → ιι
Known 1a4bb.. : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . ∀ x6 : ι → ι → ι . 62ee1.. x0 x1 x2 x3 x4 x5(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0∀ x10 . prim1 x10 x0x6 x7 x8 = x6 x9 x10and (x7 = x9) (x8 = x10))∀ x7 : ο . ((∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0prim1 (x6 x8 x9) (3b429.. x0 (λ x10 . x0) (λ x10 x11 . True) x6))(∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x6 x8 x9 = x6 x11 x14)x13)x13)x12)x12) = x8)(∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x6 x8 x9 = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x6 x8 x9 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12) = x9)(∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)prim1 (prim0 (λ x9 . ∀ x10 : ο . (prim1 x9 x0(∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x8 = x6 x9 x12)x11)x11)x10)x10)) x0)(∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)prim1 (prim0 (λ x9 . ∀ x10 : ο . (prim1 x9 x0x8 = x6 (prim0 (λ x12 . ∀ x13 : ο . (prim1 x12 x0(∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x8 = x6 x12 x15)x14)x14)x13)x13)) x9x10)x10)) x0)(∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)∀ x9 . prim1 x9 (3b429.. x0 (λ x10 . x0) (λ x10 x11 . True) x6)prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x8 = x6 x11 x14)x13)x13)x12)x12) = prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x9 = x6 x11 x14)x13)x13)x12)x12)prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x8 = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12) = prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x9 = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)x8 = x9)prim1 (x6 x1 x1) (3b429.. x0 (λ x8 . x0) (λ x8 x9 . True) x6)prim1 (x6 x2 x1) (3b429.. x0 (λ x8 . x0) (λ x8 x9 . True) x6)(∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)∀ x9 . prim1 x9 (3b429.. x0 (λ x10 . x0) (λ x10 x11 . True) x6)prim1 (x6 (x3 (prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0(∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x8 = x6 x10 x13)x12)x12)x11)x11)) (prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0(∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x9 = x6 x10 x13)x12)x12)x11)x11))) (x3 (prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0x8 = x6 (prim0 (λ x13 . ∀ x14 : ο . (prim1 x13 x0(∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x8 = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11)) (prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0x9 = x6 (prim0 (λ x13 . ∀ x14 : ο . (prim1 x13 x0(∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x9 = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11)))) (3b429.. x0 (λ x10 . x0) (λ x10 x11 . True) x6))(∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)∀ x9 . prim1 x9 (3b429.. x0 (λ x10 . x0) (λ x10 x11 . True) x6)prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x6 (x3 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x9 = x6 x16 x19)x18)x18)x17)x17))) (x3 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) = x6 x11 x14)x13)x13)x12)x12) = x3 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x8 = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x9 = x6 x11 x14)x13)x13)x12)x12)))(∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)∀ x9 . prim1 x9 (3b429.. x0 (λ x10 . x0) (λ x10 x11 . True) x6)prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x6 (x3 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x14 x17)x16)x16)x15)x15))) (x3 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x6 (x3 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20))) (x3 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12) = x3 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x8 = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x9 = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)))(∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)∀ x9 . prim1 x9 (3b429.. x0 (λ x10 . x0) (λ x10 x11 . True) x6)prim1 (x6 (x3 (x4 (prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0(∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x8 = x6 x10 x13)x12)x12)x11)x11)) (prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0(∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x9 = x6 x10 x13)x12)x12)x11)x11))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0x8 = x6 (prim0 (λ x13 . ∀ x14 : ο . (prim1 x13 x0(∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x8 = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11)) (prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0x9 = x6 (prim0 (λ x13 . ∀ x14 : ο . (prim1 x13 x0(∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x9 = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11))))) (x3 (x4 (prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0(∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x8 = x6 x10 x13)x12)x12)x11)x11)) (prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0x9 = x6 (prim0 (λ x13 . ∀ x14 : ο . (prim1 x13 x0(∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x9 = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11))) (x4 (prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0x8 = x6 (prim0 (λ x13 . ∀ x14 : ο . (prim1 x13 x0(∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x8 = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11)) (prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0(∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x9 = x6 x10 x13)x12)x12)x11)x11))))) (3b429.. x0 (λ x10 . x0) (λ x10 x11 . True) x6))(∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)∀ x9 . prim1 x9 (3b429.. x0 (λ x10 . x0) (λ x10 x11 . True) x6)prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x6 (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x9 = x6 x16 x19)x18)x18)x17)x17))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))))) (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x9 = x6 x16 x19)x18)x18)x17)x17)))) = x6 x11 x14)x13)x13)x12)x12) = x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x8 = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x9 = x6 x11 x14)x13)x13)x12)x12))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x8 = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x9 = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)))))(∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)∀ x9 . prim1 x9 (3b429.. x0 (λ x10 . x0) (λ x10 x11 . True) x6)prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x6 (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x14 x17)x16)x16)x15)x15))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))))) (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x14 x17)x16)x16)x15)x15)))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x6 (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))))) (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20)))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12) = x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x8 = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x9 = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))) (x4 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x8 = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x9 = x6 x11 x14)x13)x13)x12)x12))))x7)x7
Param explicit_Field : ιιι(ιιι) → (ιιι) → ο
Param 11fac.. : ι(ιι) → (ιι) → ιιι(ιιι) → (ιιι) → ο
Param Subq : ιιο
Known 079d2.. : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . ∀ x6 : ι → ι → ι . 62ee1.. x0 x1 x2 x3 x4 x5(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0∀ x10 . prim1 x10 x0x6 x7 x8 = x6 x9 x10and (x7 = x9) (x8 = x10))explicit_Field (3b429.. x0 (λ x7 . x0) (λ x7 x8 . True) x6) (x6 x1 x1) (x6 x2 x1) (λ x7 x8 . x6 (x3 (prim0 (λ x9 . and (prim1 x9 x0) (∀ x10 : ο . (∀ x11 . and (prim1 x11 x0) (x7 = x6 x9 x11)x10)x10))) (prim0 (λ x9 . and (prim1 x9 x0) (∀ x10 : ο . (∀ x11 . and (prim1 x11 x0) (x8 = x6 x9 x11)x10)x10)))) (x3 (prim0 (λ x9 . and (prim1 x9 x0) (x7 = x6 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x7 = x6 x11 x13)x12)x12))) x9))) (prim0 (λ x9 . and (prim1 x9 x0) (x8 = x6 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x8 = x6 x11 x13)x12)x12))) x9))))) (λ x7 x8 . x6 (x3 (x4 (prim0 (λ x9 . and (prim1 x9 x0) (∀ x10 : ο . (∀ x11 . and (prim1 x11 x0) (x7 = x6 x9 x11)x10)x10))) (prim0 (λ x9 . and (prim1 x9 x0) (∀ x10 : ο . (∀ x11 . and (prim1 x11 x0) (x8 = x6 x9 x11)x10)x10)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x9 . and (prim1 x9 x0) (x7 = x6 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x7 = x6 x11 x13)x12)x12))) x9))) (prim0 (λ x9 . and (prim1 x9 x0) (x8 = x6 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x8 = x6 x11 x13)x12)x12))) x9)))))) (x3 (x4 (prim0 (λ x9 . and (prim1 x9 x0) (∀ x10 : ο . (∀ x11 . and (prim1 x11 x0) (x7 = x6 x9 x11)x10)x10))) (prim0 (λ x9 . and (prim1 x9 x0) (x8 = x6 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x8 = x6 x11 x13)x12)x12))) x9)))) (x4 (prim0 (λ x9 . and (prim1 x9 x0) (x7 = x6 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x7 = x6 x11 x13)x12)x12))) x9))) (prim0 (λ x9 . and (prim1 x9 x0) (∀ x10 : ο . (∀ x11 . and (prim1 x11 x0) (x8 = x6 x9 x11)x10)x10))))))∀ x7 : ο . (11fac.. (3b429.. x0 (λ x8 . x0) (λ x8 x9 . True) x6) (λ x8 . x6 (prim0 (λ x9 . and (prim1 x9 x0) (∀ x10 : ο . (∀ x11 . and (prim1 x11 x0) (x8 = x6 x9 x11)x10)x10))) x1) (λ x8 . x6 (prim0 (λ x9 . and (prim1 x9 x0) (x8 = x6 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x8 = x6 x11 x13)x12)x12))) x9))) x1) (x6 x1 x1) (x6 x2 x1) (x6 x1 x2) (λ x8 x9 . x6 (x3 (prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x8 = x6 x10 x12)x11)x11))) (prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x9 = x6 x10 x12)x11)x11)))) (x3 (prim0 (λ x10 . and (prim1 x10 x0) (x8 = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x8 = x6 x12 x14)x13)x13))) x10))) (prim0 (λ x10 . and (prim1 x10 x0) (x9 = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x9 = x6 x12 x14)x13)x13))) x10))))) (λ x8 x9 . x6 (x3 (x4 (prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x8 = x6 x10 x12)x11)x11))) (prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x9 = x6 x10 x12)x11)x11)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x10 . and (prim1 x10 x0) (x8 = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x8 = x6 x12 x14)x13)x13))) x10))) (prim0 (λ x10 . and (prim1 x10 x0) (x9 = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x9 = x6 x12 x14)x13)x13))) x10)))))) (x3 (x4 (prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x8 = x6 x10 x12)x11)x11))) (prim0 (λ x10 . and (prim1 x10 x0) (x9 = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x9 = x6 x12 x14)x13)x13))) x10)))) (x4 (prim0 (λ x10 . and (prim1 x10 x0) (x8 = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x8 = x6 x12 x14)x13)x13))) x10))) (prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x9 = x6 x10 x12)x11)x11))))))((∀ x8 . prim1 x8 x0x6 x8 x1 = x8)∀ x8 : ο . ((∀ x9 : ο . ((∀ x10 : ο . ((∀ x11 : ο . ((∀ x12 : ο . (Subq x0 (3b429.. x0 (λ x13 . x0) (λ x13 x14 . True) x6)(∀ x13 . prim1 x13 x0prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x13 = x6 x15 x17)x16)x16)) = x13)x12)x12)x6 x1 x1 = x1x11)x11)x6 x2 x1 = x2x10)x10)(∀ x10 . prim1 x10 x0∀ x11 . prim1 x11 x0x6 (x3 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x10 = x6 x13 x15)x14)x14))) (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x11 = x6 x13 x15)x14)x14)))) (x3 (prim0 (λ x13 . and (prim1 x13 x0) (x10 = x6 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x10 = x6 x15 x17)x16)x16))) x13))) (prim0 (λ x13 . and (prim1 x13 x0) (x11 = x6 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x11 = x6 x15 x17)x16)x16))) x13)))) = x3 x10 x11)x9)x9)(∀ x9 . prim1 x9 x0∀ x10 . prim1 x10 x0x6 (x3 (x4 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x9 = x6 x12 x14)x13)x13))) (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x10 = x6 x12 x14)x13)x13)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x12 . and (prim1 x12 x0) (x9 = x6 (prim0 (λ x14 . and (prim1 x14 x0) (∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x9 = x6 x14 x16)x15)x15))) x12))) (prim0 (λ x12 . and (prim1 x12 x0) (x10 = x6 (prim0 (λ x14 . and (prim1 x14 x0) (∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x10 = x6 x14 x16)x15)x15))) x12)))))) (x3 (x4 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x9 = x6 x12 x14)x13)x13))) (prim0 (λ x12 . and (prim1 x12 x0) (x10 = x6 (prim0 (λ x14 . and (prim1 x14 x0) (∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x10 = x6 x14 x16)x15)x15))) x12)))) (x4 (prim0 (λ x12 . and (prim1 x12 x0) (x9 = x6 (prim0 (λ x14 . and (prim1 x14 x0) (∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x9 = x6 x14 x16)x15)x15))) x12))) (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x10 = x6 x12 x14)x13)x13))))) = x4 x9 x10)x8)x8)x7)x7
Known 79042.. : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . ∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0prim1 (x6 x7 x8) (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6))(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0(∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x6 x7 x8 = x6 x10 x13)x12)x12)x11)x11) = x7)(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0x6 x7 x8 = x6 (prim0 (λ x13 . ∀ x14 : ο . (prim1 x13 x0(∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x6 x7 x8 = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11) = x8)(∀ x7 . prim1 x7 (3b429.. x0 (λ x8 . x0) (λ x8 x9 . True) x6)prim1 (prim0 (λ x8 . ∀ x9 : ο . (prim1 x8 x0(∀ x10 : ο . (∀ x11 . and (prim1 x11 x0) (x7 = x6 x8 x11)x10)x10)x9)x9)) x0)(∀ x7 . prim1 x7 (3b429.. x0 (λ x8 . x0) (λ x8 x9 . True) x6)prim1 (prim0 (λ x8 . ∀ x9 : ο . (prim1 x8 x0x7 = x6 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x7 = x6 x11 x14)x13)x13)x12)x12)) x8x9)x9)) x0)(∀ x7 . prim1 x7 (3b429.. x0 (λ x8 . x0) (λ x8 x9 . True) x6)∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0(∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x7 = x6 x10 x13)x12)x12)x11)x11) = prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0(∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x8 = x6 x10 x13)x12)x12)x11)x11)prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0x7 = x6 (prim0 (λ x13 . ∀ x14 : ο . (prim1 x13 x0(∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x7 = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11) = prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0x8 = x6 (prim0 (λ x13 . ∀ x14 : ο . (prim1 x13 x0(∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x8 = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11)x7 = x8)prim1 (x6 x1 x1) (3b429.. x0 (λ x7 . x0) (λ x7 x8 . True) x6)prim1 (x6 x2 x1) (3b429.. x0 (λ x7 . x0) (λ x7 x8 . True) x6)(∀ x7 . prim1 x7 (3b429.. x0 (λ x8 . x0) (λ x8 x9 . True) x6)∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)prim1 (x6 (x3 (prim0 (λ x9 . ∀ x10 : ο . (prim1 x9 x0(∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x7 = x6 x9 x12)x11)x11)x10)x10)) (prim0 (λ x9 . ∀ x10 : ο . (prim1 x9 x0(∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x8 = x6 x9 x12)x11)x11)x10)x10))) (x3 (prim0 (λ x9 . ∀ x10 : ο . (prim1 x9 x0x7 = x6 (prim0 (λ x12 . ∀ x13 : ο . (prim1 x12 x0(∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x7 = x6 x12 x15)x14)x14)x13)x13)) x9x10)x10)) (prim0 (λ x9 . ∀ x10 : ο . (prim1 x9 x0x8 = x6 (prim0 (λ x12 . ∀ x13 : ο . (prim1 x12 x0(∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x8 = x6 x12 x15)x14)x14)x13)x13)) x9x10)x10)))) (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6))(∀ x7 . prim1 x7 (3b429.. x0 (λ x8 . x0) (λ x8 x9 . True) x6)∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0(∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x6 (x3 (prim0 (λ x15 . ∀ x16 : ο . (prim1 x15 x0(∀ x17 : ο . (∀ x18 . and (prim1 x18 x0) (x7 = x6 x15 x18)x17)x17)x16)x16)) (prim0 (λ x15 . ∀ x16 : ο . (prim1 x15 x0(∀ x17 : ο . (∀ x18 . and (prim1 x18 x0) (x8 = x6 x15 x18)x17)x17)x16)x16))) (x3 (prim0 (λ x15 . ∀ x16 : ο . (prim1 x15 x0x7 = x6 (prim0 (λ x18 . ∀ x19 : ο . (prim1 x18 x0(∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x7 = x6 x18 x21)x20)x20)x19)x19)) x15x16)x16)) (prim0 (λ x15 . ∀ x16 : ο . (prim1 x15 x0x8 = x6 (prim0 (λ x18 . ∀ x19 : ο . (prim1 x18 x0(∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x8 = x6 x18 x21)x20)x20)x19)x19)) x15x16)x16))) = x6 x10 x13)x12)x12)x11)x11) = x3 (prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0(∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x7 = x6 x10 x13)x12)x12)x11)x11)) (prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0(∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x8 = x6 x10 x13)x12)x12)x11)x11)))(∀ x7 . prim1 x7 (3b429.. x0 (λ x8 . x0) (λ x8 x9 . True) x6)∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0x6 (x3 (prim0 (λ x13 . ∀ x14 : ο . (prim1 x13 x0(∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x7 = x6 x13 x16)x15)x15)x14)x14)) (prim0 (λ x13 . ∀ x14 : ο . (prim1 x13 x0(∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x8 = x6 x13 x16)x15)x15)x14)x14))) (x3 (prim0 (λ x13 . ∀ x14 : ο . (prim1 x13 x0x7 = x6 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) x13x14)x14)) (prim0 (λ x13 . ∀ x14 : ο . (prim1 x13 x0x8 = x6 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) x13x14)x14))) = x6 (prim0 (λ x13 . ∀ x14 : ο . (prim1 x13 x0(∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x6 (x3 (prim0 (λ x18 . ∀ x19 : ο . (prim1 x18 x0(∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x7 = x6 x18 x21)x20)x20)x19)x19)) (prim0 (λ x18 . ∀ x19 : ο . (prim1 x18 x0(∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x8 = x6 x18 x21)x20)x20)x19)x19))) (x3 (prim0 (λ x18 . ∀ x19 : ο . (prim1 x18 x0x7 = x6 (prim0 (λ x21 . ∀ x22 : ο . (prim1 x21 x0(∀ x23 : ο . (∀ x24 . and (prim1 x24 x0) (x7 = x6 x21 x24)x23)x23)x22)x22)) x18x19)x19)) (prim0 (λ x18 . ∀ x19 : ο . (prim1 x18 x0x8 = x6 (prim0 (λ x21 . ∀ x22 : ο . (prim1 x21 x0(∀ x23 : ο . (∀ x24 . and (prim1 x24 x0) (x8 = x6 x21 x24)x23)x23)x22)x22)) x18x19)x19))) = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11) = x3 (prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0x7 = x6 (prim0 (λ x13 . ∀ x14 : ο . (prim1 x13 x0(∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x7 = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11)) (prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0x8 = x6 (prim0 (λ x13 . ∀ x14 : ο . (prim1 x13 x0(∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x8 = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11)))(∀ x7 . prim1 x7 (3b429.. x0 (λ x8 . x0) (λ x8 x9 . True) x6)∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)prim1 (x6 (x3 (x4 (prim0 (λ x9 . ∀ x10 : ο . (prim1 x9 x0(∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x7 = x6 x9 x12)x11)x11)x10)x10)) (prim0 (λ x9 . ∀ x10 : ο . (prim1 x9 x0(∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x8 = x6 x9 x12)x11)x11)x10)x10))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x9 . ∀ x10 : ο . (prim1 x9 x0x7 = x6 (prim0 (λ x12 . ∀ x13 : ο . (prim1 x12 x0(∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x7 = x6 x12 x15)x14)x14)x13)x13)) x9x10)x10)) (prim0 (λ x9 . ∀ x10 : ο . (prim1 x9 x0x8 = x6 (prim0 (λ x12 . ∀ x13 : ο . (prim1 x12 x0(∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x8 = x6 x12 x15)x14)x14)x13)x13)) x9x10)x10))))) (x3 (x4 (prim0 (λ x9 . ∀ x10 : ο . (prim1 x9 x0(∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x7 = x6 x9 x12)x11)x11)x10)x10)) (prim0 (λ x9 . ∀ x10 : ο . (prim1 x9 x0x8 = x6 (prim0 (λ x12 . ∀ x13 : ο . (prim1 x12 x0(∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x8 = x6 x12 x15)x14)x14)x13)x13)) x9x10)x10))) (x4 (prim0 (λ x9 . ∀ x10 : ο . (prim1 x9 x0x7 = x6 (prim0 (λ x12 . ∀ x13 : ο . (prim1 x12 x0(∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x7 = x6 x12 x15)x14)x14)x13)x13)) x9x10)x10)) (prim0 (λ x9 . ∀ x10 : ο . (prim1 x9 x0(∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x8 = x6 x9 x12)x11)x11)x10)x10))))) (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6))(∀ x7 . prim1 x7 (3b429.. x0 (λ x8 . x0) (λ x8 x9 . True) x6)∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0(∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x6 (x3 (x4 (prim0 (λ x15 . ∀ x16 : ο . (prim1 x15 x0(∀ x17 : ο . (∀ x18 . and (prim1 x18 x0) (x7 = x6 x15 x18)x17)x17)x16)x16)) (prim0 (λ x15 . ∀ x16 : ο . (prim1 x15 x0(∀ x17 : ο . (∀ x18 . and (prim1 x18 x0) (x8 = x6 x15 x18)x17)x17)x16)x16))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x15 . ∀ x16 : ο . (prim1 x15 x0x7 = x6 (prim0 (λ x18 . ∀ x19 : ο . (prim1 x18 x0(∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x7 = x6 x18 x21)x20)x20)x19)x19)) x15x16)x16)) (prim0 (λ x15 . ∀ x16 : ο . (prim1 x15 x0x8 = x6 (prim0 (λ x18 . ∀ x19 : ο . (prim1 x18 x0(∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x8 = x6 x18 x21)x20)x20)x19)x19)) x15x16)x16))))) (x3 (x4 (prim0 (λ x15 . ∀ x16 : ο . (prim1 x15 x0(∀ x17 : ο . (∀ x18 . and (prim1 x18 x0) (x7 = x6 x15 x18)x17)x17)x16)x16)) (prim0 (λ x15 . ∀ x16 : ο . (prim1 x15 x0x8 = x6 (prim0 (λ x18 . ∀ x19 : ο . (prim1 x18 x0(∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x8 = x6 x18 x21)x20)x20)x19)x19)) x15x16)x16))) (x4 (prim0 (λ x15 . ∀ x16 : ο . (prim1 x15 x0x7 = x6 (prim0 (λ x18 . ∀ x19 : ο . (prim1 x18 x0(∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x7 = x6 x18 x21)x20)x20)x19)x19)) x15x16)x16)) (prim0 (λ x15 . ∀ x16 : ο . (prim1 x15 x0(∀ x17 : ο . (∀ x18 . and (prim1 x18 x0) (x8 = x6 x15 x18)x17)x17)x16)x16)))) = x6 x10 x13)x12)x12)x11)x11) = x3 (x4 (prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0(∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x7 = x6 x10 x13)x12)x12)x11)x11)) (prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0(∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x8 = x6 x10 x13)x12)x12)x11)x11))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0x7 = x6 (prim0 (λ x13 . ∀ x14 : ο . (prim1 x13 x0(∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x7 = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11)) (prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0x8 = x6 (prim0 (λ x13 . ∀ x14 : ο . (prim1 x13 x0(∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x8 = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11)))))(∀ x7 . prim1 x7 (3b429.. x0 (λ x8 . x0) (λ x8 x9 . True) x6)∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0x6 (x3 (x4 (prim0 (λ x13 . ∀ x14 : ο . (prim1 x13 x0(∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x7 = x6 x13 x16)x15)x15)x14)x14)) (prim0 (λ x13 . ∀ x14 : ο . (prim1 x13 x0(∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x8 = x6 x13 x16)x15)x15)x14)x14))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x13 . ∀ x14 : ο . (prim1 x13 x0x7 = x6 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) x13x14)x14)) (prim0 (λ x13 . ∀ x14 : ο . (prim1 x13 x0x8 = x6 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) x13x14)x14))))) (x3 (x4 (prim0 (λ x13 . ∀ x14 : ο . (prim1 x13 x0(∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x7 = x6 x13 x16)x15)x15)x14)x14)) (prim0 (λ x13 . ∀ x14 : ο . (prim1 x13 x0x8 = x6 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) x13x14)x14))) (x4 (prim0 (λ x13 . ∀ x14 : ο . (prim1 x13 x0x7 = x6 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) x13x14)x14)) (prim0 (λ x13 . ∀ x14 : ο . (prim1 x13 x0(∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x8 = x6 x13 x16)x15)x15)x14)x14)))) = x6 (prim0 (λ x13 . ∀ x14 : ο . (prim1 x13 x0(∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x6 (x3 (x4 (prim0 (λ x18 . ∀ x19 : ο . (prim1 x18 x0(∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x7 = x6 x18 x21)x20)x20)x19)x19)) (prim0 (λ x18 . ∀ x19 : ο . (prim1 x18 x0(∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x8 = x6 x18 x21)x20)x20)x19)x19))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x18 . ∀ x19 : ο . (prim1 x18 x0x7 = x6 (prim0 (λ x21 . ∀ x22 : ο . (prim1 x21 x0(∀ x23 : ο . (∀ x24 . and (prim1 x24 x0) (x7 = x6 x21 x24)x23)x23)x22)x22)) x18x19)x19)) (prim0 (λ x18 . ∀ x19 : ο . (prim1 x18 x0x8 = x6 (prim0 (λ x21 . ∀ x22 : ο . (prim1 x21 x0(∀ x23 : ο . (∀ x24 . and (prim1 x24 x0) (x8 = x6 x21 x24)x23)x23)x22)x22)) x18x19)x19))))) (x3 (x4 (prim0 (λ x18 . ∀ x19 : ο . (prim1 x18 x0(∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x7 = x6 x18 x21)x20)x20)x19)x19)) (prim0 (λ x18 . ∀ x19 : ο . (prim1 x18 x0x8 = x6 (prim0 (λ x21 . ∀ x22 : ο . (prim1 x21 x0(∀ x23 : ο . (∀ x24 . and (prim1 x24 x0) (x8 = x6 x21 x24)x23)x23)x22)x22)) x18x19)x19))) (x4 (prim0 (λ x18 . ∀ x19 : ο . (prim1 x18 x0x7 = x6 (prim0 (λ x21 . ∀ x22 : ο . (prim1 x21 x0(∀ x23 : ο . (∀ x24 . and (prim1 x24 x0) (x7 = x6 x21 x24)x23)x23)x22)x22)) x18x19)x19)) (prim0 (λ x18 . ∀ x19 : ο . (prim1 x18 x0(∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x8 = x6 x18 x21)x20)x20)x19)x19)))) = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11) = x3 (x4 (prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0(∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x7 = x6 x10 x13)x12)x12)x11)x11)) (prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0x8 = x6 (prim0 (λ x13 . ∀ x14 : ο . (prim1 x13 x0(∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x8 = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11))) (x4 (prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0x7 = x6 (prim0 (λ x13 . ∀ x14 : ο . (prim1 x13 x0(∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x7 = x6 x13 x16)x15)x15)x14)x14)) x10x11)x11)) (prim0 (λ x10 . ∀ x11 : ο . (prim1 x10 x0(∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x8 = x6 x10 x13)x12)x12)x11)x11))))explicit_Field x0 x1 x2 x3 x4(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0∀ x10 . prim1 x10 x0x6 x7 x8 = x6 x9 x10∀ x11 : ο . (x7 = x9x8 = x10x11)x11)(∀ x7 . prim1 x7 (3b429.. x0 (λ x8 . x0) (λ x8 x9 . True) x6)∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)∀ x9 . prim1 x9 (3b429.. x0 (λ x10 . x0) (λ x10 x11 . True) x6)x6 (x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x7 = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x6 (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x9 = x6 x16 x19)x18)x18)x17)x17))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))))) (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (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 : ο . (prim1 x11 x0x7 = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x6 (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x14 x17)x16)x16)x15)x15))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))))) (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x14 x17)x16)x16)x15)x15)))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x6 (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))))) (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20)))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))))) (x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x7 = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x6 (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x14 x17)x16)x16)x15)x15))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))))) (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x14 x17)x16)x16)x15)x15)))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x6 (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))))) (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20)))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))) (x4 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x7 = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x6 (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x9 = x6 x16 x19)x18)x18)x17)x17))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))))) (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x9 = x6 x16 x19)x18)x18)x17)x17)))) = x6 x11 x14)x13)x13)x12)x12)))) = x6 (x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x6 (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x16 x19)x18)x18)x17)x17))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x7 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))))) (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x7 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x16 x19)x18)x18)x17)x17)))) = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x9 = x6 x11 x14)x13)x13)x12)x12))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x6 (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x14 x17)x16)x16)x15)x15))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x7 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x7 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))))) (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x7 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x7 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x14 x17)x16)x16)x15)x15)))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x6 (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x7 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x7 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))))) (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x7 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x7 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x9 = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))))) (x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x6 (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x16 x19)x18)x18)x17)x17))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x7 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))))) (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x7 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x16 x19)x18)x18)x17)x17)))) = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x9 = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))) (x4 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x6 (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x14 x17)x16)x16)x15)x15))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x7 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x7 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))))) (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x7 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x7 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x14 x17)x16)x16)x15)x15)))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x6 (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x7 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x7 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))))) (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x7 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x7 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x9 = x6 x11 x14)x13)x13)x12)x12)))))(∀ x7 . prim1 x7 (3b429.. x0 (λ x8 . x0) (λ x8 x9 . True) x6)(x7 = x6 x1 x1∀ x8 : ο . x8)∀ x8 : ο . (∀ x9 . and (prim1 x9 (3b429.. x0 (λ x10 . x0) (λ x10 x11 . True) x6)) (x6 (x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x7 = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x9 = x6 x11 x14)x13)x13)x12)x12))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x7 = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x9 = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))))) (x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x7 = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x9 = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))) (x4 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x7 = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x9 = x6 x11 x14)x13)x13)x12)x12)))) = x6 x2 x1)x8)x8)(∀ x7 . prim1 x7 (3b429.. x0 (λ x8 . x0) (λ x8 x9 . True) x6)∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)∀ x9 . prim1 x9 (3b429.. x0 (λ x10 . x0) (λ x10 x11 . True) x6)x6 (x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x7 = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x6 (x3 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x9 = x6 x16 x19)x18)x18)x17)x17))) (x3 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (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 : ο . (prim1 x11 x0x7 = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x6 (x3 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x14 x17)x16)x16)x15)x15))) (x3 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x6 (x3 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20))) (x3 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))))) (x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x7 = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x6 (x3 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x14 x17)x16)x16)x15)x15))) (x3 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x6 (x3 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20))) (x3 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))) (x4 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x7 = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x6 (x3 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x9 = x6 x16 x19)x18)x18)x17)x17))) (x3 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) = x6 x11 x14)x13)x13)x12)x12)))) = x6 (x3 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x6 (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x16 x19)x18)x18)x17)x17))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x7 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))))) (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x7 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x16 x19)x18)x18)x17)x17)))) = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x6 (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x9 = x6 x16 x19)x18)x18)x17)x17))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x7 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))))) (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x7 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x9 = x6 x16 x19)x18)x18)x17)x17)))) = x6 x11 x14)x13)x13)x12)x12))) (x3 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x6 (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x14 x17)x16)x16)x15)x15))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x7 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x7 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))))) (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x7 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x7 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x14 x17)x16)x16)x15)x15)))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x6 (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x7 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x7 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))))) (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x7 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x7 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x6 (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x14 x17)x16)x16)x15)x15))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x7 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x7 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))))) (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x7 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x7 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x14 x17)x16)x16)x15)x15)))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x6 (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x7 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x7 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))))) (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x7 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x7 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20)))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))))explicit_Field (3b429.. x0 (λ x7 . x0) (λ x7 x8 . True) x6) (x6 x1 x1) (x6 x2 x1) (λ x7 x8 . x6 (x3 (prim0 (λ x9 . ∀ x10 : ο . (prim1 x9 x0(∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x7 = x6 x9 x12)x11)x11)x10)x10)) (prim0 (λ x9 . ∀ x10 : ο . (prim1 x9 x0(∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x8 = x6 x9 x12)x11)x11)x10)x10))) (x3 (prim0 (λ x9 . ∀ x10 : ο . (prim1 x9 x0x7 = x6 (prim0 (λ x12 . ∀ x13 : ο . (prim1 x12 x0(∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x7 = x6 x12 x15)x14)x14)x13)x13)) x9x10)x10)) (prim0 (λ x9 . ∀ x10 : ο . (prim1 x9 x0x8 = x6 (prim0 (λ x12 . ∀ x13 : ο . (prim1 x12 x0(∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x8 = x6 x12 x15)x14)x14)x13)x13)) x9x10)x10)))) (λ x7 x8 . x6 (x3 (x4 (prim0 (λ x9 . ∀ x10 : ο . (prim1 x9 x0(∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x7 = x6 x9 x12)x11)x11)x10)x10)) (prim0 (λ x9 . ∀ x10 : ο . (prim1 x9 x0(∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x8 = x6 x9 x12)x11)x11)x10)x10))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x9 . ∀ x10 : ο . (prim1 x9 x0x7 = x6 (prim0 (λ x12 . ∀ x13 : ο . (prim1 x12 x0(∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x7 = x6 x12 x15)x14)x14)x13)x13)) x9x10)x10)) (prim0 (λ x9 . ∀ x10 : ο . (prim1 x9 x0x8 = x6 (prim0 (λ x12 . ∀ x13 : ο . (prim1 x12 x0(∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x8 = x6 x12 x15)x14)x14)x13)x13)) x9x10)x10))))) (x3 (x4 (prim0 (λ x9 . ∀ x10 : ο . (prim1 x9 x0(∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x7 = x6 x9 x12)x11)x11)x10)x10)) (prim0 (λ x9 . ∀ x10 : ο . (prim1 x9 x0x8 = x6 (prim0 (λ x12 . ∀ x13 : ο . (prim1 x12 x0(∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x8 = x6 x12 x15)x14)x14)x13)x13)) x9x10)x10))) (x4 (prim0 (λ x9 . ∀ x10 : ο . (prim1 x9 x0x7 = x6 (prim0 (λ x12 . ∀ x13 : ο . (prim1 x12 x0(∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x7 = x6 x12 x15)x14)x14)x13)x13)) x9x10)x10)) (prim0 (λ x9 . ∀ x10 : ο . (prim1 x9 x0(∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x8 = x6 x9 x12)x11)x11)x10)x10)))))
Param explicit_OrderedField : ιιι(ιιι) → (ιιι) → (ιιο) → ο
Param lt : ιιι(ιιι) → (ιιι) → (ιιο) → ιιο
Param 1216a.. : ι(ιο) → ι
Param natOfOrderedField_p : ιιι(ιιι) → (ιιι) → (ιιο) → ιο
Param b5c9f.. : ιιι
Param f482f.. : ιιι
Known f2fa8.. : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . ∀ x6 : ο . (62ee1.. x0 x1 x2 x3 x4 x5explicit_OrderedField x0 x1 x2 x3 x4 x5(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0lt x0 x1 x2 x3 x4 x5 x1 x7x5 x1 x8∀ x9 : ο . (∀ x10 . and (prim1 x10 (1216a.. x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5))) (x5 x8 (x4 x10 x7))x9)x9)(∀ x7 . prim1 x7 (b5c9f.. x0 (1216a.. x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)))∀ x8 . prim1 x8 (b5c9f.. x0 (1216a.. x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)))(∀ x9 . prim1 x9 (1216a.. x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5))and (and (x5 (f482f.. x7 x9) (f482f.. x8 x9)) (x5 (f482f.. x7 x9) (f482f.. x7 (x3 x9 x2)))) (x5 (f482f.. x8 (x3 x9 x2)) (f482f.. x8 x9)))∀ x9 : ο . (∀ x10 . and (prim1 x10 x0) (∀ x11 . prim1 x11 (1216a.. x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5))and (x5 (f482f.. x7 x11) x10) (x5 x10 (f482f.. x8 x11)))x9)x9)x6)62ee1.. x0 x1 x2 x3 x4 x5x6
Param iff : οοο
Param or : οοο
Known explicit_OrderedField_E : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . ∀ x6 : ο . (explicit_OrderedField x0 x1 x2 x3 x4 x5explicit_Field x0 x1 x2 x3 x4(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0x5 x7 x8x5 x8 x9x5 x7 x9)(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0iff (and (x5 x7 x8) (x5 x8 x7)) (x7 = x8))(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0or (x5 x7 x8) (x5 x8 x7))(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0x5 x7 x8x5 (x3 x7 x9) (x3 x8 x9))(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0x5 x1 x7x5 x1 x8x5 x1 (x4 x7 x8))x6)explicit_OrderedField x0 x1 x2 x3 x4 x5x6
Theorem b1312.. : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . ∀ x6 : ι → ι → ι . 62ee1.. x0 x1 x2 x3 x4 x5(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0∀ x10 . prim1 x10 x0x6 x7 x8 = x6 x9 x10∀ x11 : ο . (x7 = x9x8 = x10x11)x11)(∀ x7 . prim1 x7 (3b429.. x0 (λ x8 . x0) (λ x8 x9 . True) x6)∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)∀ x9 . prim1 x9 (3b429.. x0 (λ x10 . x0) (λ x10 x11 . True) x6)x6 (x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x7 = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x6 (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x9 = x6 x16 x19)x18)x18)x17)x17))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))))) (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (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 : ο . (prim1 x11 x0x7 = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x6 (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x14 x17)x16)x16)x15)x15))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))))) (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x14 x17)x16)x16)x15)x15)))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x6 (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))))) (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20)))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))))) (x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x7 = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x6 (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x14 x17)x16)x16)x15)x15))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))))) (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x14 x17)x16)x16)x15)x15)))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x6 (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))))) (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20)))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))) (x4 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x7 = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x6 (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x9 = x6 x16 x19)x18)x18)x17)x17))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))))) (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x9 = x6 x16 x19)x18)x18)x17)x17)))) = x6 x11 x14)x13)x13)x12)x12)))) = x6 (x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x6 (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x16 x19)x18)x18)x17)x17))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x7 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))))) (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x7 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x16 x19)x18)x18)x17)x17)))) = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x9 = x6 x11 x14)x13)x13)x12)x12))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x6 (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x14 x17)x16)x16)x15)x15))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x7 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x7 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))))) (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x7 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x7 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x14 x17)x16)x16)x15)x15)))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x6 (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x7 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x7 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))))) (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x7 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x7 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x9 = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))))) (x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x6 (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x16 x19)x18)x18)x17)x17))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x7 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))))) (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x7 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x16 x19)x18)x18)x17)x17)))) = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x9 = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))) (x4 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x6 (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x14 x17)x16)x16)x15)x15))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x7 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x7 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))))) (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x7 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x7 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x14 x17)x16)x16)x15)x15)))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x6 (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x7 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x7 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))))) (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x7 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x7 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x9 = x6 x11 x14)x13)x13)x12)x12)))))(∀ x7 . prim1 x7 (3b429.. x0 (λ x8 . x0) (λ x8 x9 . True) x6)(x7 = x6 x1 x1∀ x8 : ο . x8)∀ x8 : ο . (∀ x9 . and (prim1 x9 (3b429.. x0 (λ x10 . x0) (λ x10 x11 . True) x6)) (x6 (x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x7 = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x9 = x6 x11 x14)x13)x13)x12)x12))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x7 = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x9 = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))))) (x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x7 = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x9 = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))) (x4 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x7 = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x9 = x6 x11 x14)x13)x13)x12)x12)))) = x6 x2 x1)x8)x8)(∀ x7 . prim1 x7 (3b429.. x0 (λ x8 . x0) (λ x8 x9 . True) x6)∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)∀ x9 . prim1 x9 (3b429.. x0 (λ x10 . x0) (λ x10 x11 . True) x6)x6 (x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x7 = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x6 (x3 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x9 = x6 x16 x19)x18)x18)x17)x17))) (x3 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (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 : ο . (prim1 x11 x0x7 = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x6 (x3 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x14 x17)x16)x16)x15)x15))) (x3 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x6 (x3 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20))) (x3 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))))) (x3 (x4 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x7 = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x6 (x3 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x14 x17)x16)x16)x15)x15))) (x3 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x6 (x3 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20))) (x3 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))) (x4 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x7 = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x6 (x3 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x9 = x6 x16 x19)x18)x18)x17)x17))) (x3 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) = x6 x11 x14)x13)x13)x12)x12)))) = x6 (x3 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x6 (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x16 x19)x18)x18)x17)x17))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x7 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))))) (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x8 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x7 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x16 x19)x18)x18)x17)x17)))) = x6 x11 x14)x13)x13)x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0(∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x6 (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x9 = x6 x16 x19)x18)x18)x17)x17))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x7 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))))) (x3 (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x7 = x6 x16 x19)x18)x18)x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x9 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17))) (x4 (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0x7 = x6 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) x16x17)x17)) (prim0 (λ x16 . ∀ x17 : ο . (prim1 x16 x0(∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x9 = x6 x16 x19)x18)x18)x17)x17)))) = x6 x11 x14)x13)x13)x12)x12))) (x3 (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x6 (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x14 x17)x16)x16)x15)x15))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x7 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x7 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))))) (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x8 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x8 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x7 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x7 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x14 x17)x16)x16)x15)x15)))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x6 (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x7 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x7 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))))) (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x8 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x8 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x7 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x7 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x8 = x6 x19 x22)x21)x21)x20)x20)))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12)) (prim0 (λ x11 . ∀ x12 : ο . (prim1 x11 x0x6 (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x14 x17)x16)x16)x15)x15))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x7 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x7 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))))) (x3 (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x14 x17)x16)x16)x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x9 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x9 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15))) (x4 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0x7 = x6 (prim0 (λ x17 . ∀ x18 : ο . (prim1 x17 x0(∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x7 = x6 x17 x20)x19)x19)x18)x18)) x14x15)x15)) (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x14 x17)x16)x16)x15)x15)))) = x6 (prim0 (λ x14 . ∀ x15 : ο . (prim1 x14 x0(∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x6 (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x7 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x7 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))))) (x3 (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x7 = x6 x19 x22)x21)x21)x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x9 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x9 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20))) (x4 (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0x7 = x6 (prim0 (λ x22 . ∀ x23 : ο . (prim1 x22 x0(∀ x24 : ο . (∀ x25 . and (prim1 x25 x0) (x7 = x6 x22 x25)x24)x24)x23)x23)) x19x20)x20)) (prim0 (λ x19 . ∀ x20 : ο . (prim1 x19 x0(∀ x21 : ο . (∀ x22 . and (prim1 x22 x0) (x9 = x6 x19 x22)x21)x21)x20)x20)))) = x6 x14 x17)x16)x16)x15)x15)) x11x12)x12))))and (11fac.. (3b429.. x0 (λ x7 . x0) (λ x7 x8 . True) x6) (λ x7 . x6 (prim0 (λ x8 . and (prim1 x8 x0) (∀ x9 : ο . (∀ x10 . and (prim1 x10 x0) (x7 = x6 x8 x10)x9)x9))) x1) (λ x7 . x6 (prim0 (λ x8 . and (prim1 x8 x0) (x7 = x6 (prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x7 = x6 x10 x12)x11)x11))) x8))) x1) (x6 x1 x1) (x6 x2 x1) (x6 x1 x2) (λ x7 x8 . x6 (x3 (prim0 (λ x9 . and (prim1 x9 x0) (∀ x10 : ο . (∀ x11 . and (prim1 x11 x0) (x7 = x6 x9 x11)x10)x10))) (prim0 (λ x9 . and (prim1 x9 x0) (∀ x10 : ο . (∀ x11 . and (prim1 x11 x0) (x8 = x6 x9 x11)x10)x10)))) (x3 (prim0 (λ x9 . and (prim1 x9 x0) (x7 = x6 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x7 = x6 x11 x13)x12)x12))) x9))) (prim0 (λ x9 . and (prim1 x9 x0) (x8 = x6 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x8 = x6 x11 x13)x12)x12))) x9))))) (λ x7 x8 . x6 (x3 (x4 (prim0 (λ x9 . and (prim1 x9 x0) (∀ x10 : ο . (∀ x11 . and (prim1 x11 x0) (x7 = x6 x9 x11)x10)x10))) (prim0 (λ x9 . and (prim1 x9 x0) (∀ x10 : ο . (∀ x11 . and (prim1 x11 x0) (x8 = x6 x9 x11)x10)x10)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x9 . and (prim1 x9 x0) (x7 = x6 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x7 = x6 x11 x13)x12)x12))) x9))) (prim0 (λ x9 . and (prim1 x9 x0) (x8 = x6 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x8 = x6 x11 x13)x12)x12))) x9)))))) (x3 (x4 (prim0 (λ x9 . and (prim1 x9 x0) (∀ x10 : ο . (∀ x11 . and (prim1 x11 x0) (x7 = x6 x9 x11)x10)x10))) (prim0 (λ x9 . and (prim1 x9 x0) (x8 = x6 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x8 = x6 x11 x13)x12)x12))) x9)))) (x4 (prim0 (λ x9 . and (prim1 x9 x0) (x7 = x6 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x7 = x6 x11 x13)x12)x12))) x9))) (prim0 (λ x9 . and (prim1 x9 x0) (∀ x10 : ο . (∀ x11 . and (prim1 x11 x0) (x8 = x6 x9 x11)x10)x10))))))) ((∀ x7 . prim1 x7 x0x6 x7 x1 = x7)and (and (and (and (and (Subq x0 (3b429.. x0 (λ x7 . x0) (λ x7 x8 . True) x6)) (∀ x7 . prim1 x7 x0prim0 (λ x9 . and (prim1 x9 x0) (∀ x10 : ο . (∀ x11 . and (prim1 x11 x0) (x7 = x6 x9 x11)x10)x10)) = x7)) (x6 x1 x1 = x1)) (x6 x2 x1 = x2)) (∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0x6 (x3 (prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x7 = x6 x10 x12)x11)x11))) (prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x8 = x6 x10 x12)x11)x11)))) (x3 (prim0 (λ x10 . and (prim1 x10 x0) (x7 = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x7 = x6 x12 x14)x13)x13))) x10))) (prim0 (λ x10 . and (prim1 x10 x0) (x8 = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x8 = x6 x12 x14)x13)x13))) x10)))) = x3 x7 x8)) (∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0x6 (x3 (x4 (prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x7 = x6 x10 x12)x11)x11))) (prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x8 = x6 x10 x12)x11)x11)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x10 . and (prim1 x10 x0) (x7 = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x7 = x6 x12 x14)x13)x13))) x10))) (prim0 (λ x10 . and (prim1 x10 x0) (x8 = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x8 = x6 x12 x14)x13)x13))) x10)))))) (x3 (x4 (prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x7 = x6 x10 x12)x11)x11))) (prim0 (λ x10 . and (prim1 x10 x0) (x8 = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x8 = x6 x12 x14)x13)x13))) x10)))) (x4 (prim0 (λ x10 . and (prim1 x10 x0) (x7 = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x7 = x6 x12 x14)x13)x13))) x10))) (prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x8 = x6 x10 x12)x11)x11))))) = x4 x7 x8)) (proof)