Search for blocks/addresses/...

Proofgold Asset

asset id
ab8cf4b54a8e68df49f6111eb7a4a87d45f99139f36d6122417dfad4d2983585
asset hash
620f464136d1c23ce668494bf358b93b27ddc782dc7579293fe936043aaaeaea
bday / block
2059
tx
cbccf..
preasset
doc published by PrGxv..
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Known andI : ∀ x0 x1 : ο . x0x1and x0 x1
Theorem and3I : ∀ x0 x1 x2 : ο . x0x1x2and (and x0 x1) x2 (proof)
Definition c4def.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x1))))) (prim1 (λ x0 . x0)))))))))))))))))))))
Definition 6b90c.. := λ x0 x1 . prim0 (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x3 x3) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x2) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x3) (prim0 x2 x3))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x3 x2) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x3 x2)) (prim0 (prim0 x2 x2) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x3) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x3) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x2) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x3) (prim0 x3 x3))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x2) (prim0 x3 x3))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x3) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x3 x3) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x3) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x2) (prim0 x3 x3))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x2 x3) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x3 x2)) (prim0 (prim0 x2 x2) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x3 x3) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x2) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x2) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x3) (prim0 x3 x3))))) (prim1 (λ x2 . x2)))))))))))))))))))))) (prim0 x0 x1)
Definition 5e331.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim1 (λ x0 . x0))))))))))))))))))))
Definition a3eb9.. := λ x0 x1 . prim0 (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x3 x3) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x2) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x3) (prim0 x2 x3))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x3 x2) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x3 x2)) (prim0 (prim0 x2 x2) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x3) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x3) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x2) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x3) (prim0 x3 x3))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x2) (prim0 x3 x3))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x3) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x3 x3) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x3) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x2) (prim0 x3 x3))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x2 x3) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x3 x2)) (prim0 (prim0 x2 x2) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x3) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x2) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x2) (prim0 x3 x2))))) (prim1 (λ x2 . x2))))))))))))))))))))) (prim0 x0 x1)
Definition bf68c.. := λ x0 x1 . prim0 (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x3 x3) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x2) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x3) (prim0 x2 x3))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x3 x2) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x3 x2)) (prim0 (prim0 x2 x2) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x3) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x3) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x2) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x3) (prim0 x3 x3))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x2) (prim0 x3 x3))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x3) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x3 x3) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x3) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x2) (prim0 x3 x3))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x2 x3) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x3 x2)) (prim0 (prim0 x2 x2) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x3) (prim0 x3 x3))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x3) (prim0 x2 x3))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x2) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x3 x2) (prim0 x3 x3))))) (prim1 (λ x2 . x2)))))))))))))))))))))) (prim0 x0 x1)
Definition c9248.. := prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim1 (λ x0 . x0)))))))))))))))))))))
Definition a6e19.. := prim0 (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim1 (λ x0 . x0))))))))))))))))))))))
Definition 2fe34.. := prim0 (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim1 (λ x0 . x0))))))))))))))))))))))
Definition 3e00e.. := λ x0 x1 . prim0 (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x3 x3) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x2) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x3) (prim0 x2 x3))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x3 x2) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x3 x2)) (prim0 (prim0 x2 x2) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x3) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x3) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x2) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x3) (prim0 x3 x3))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x2) (prim0 x3 x3))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x3) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x3 x3) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x3) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x2) (prim0 x3 x3))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x2 x3) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x3 x2)) (prim0 (prim0 x2 x2) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x3 x3) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x3 x3) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x3) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x3 x2) (prim0 x3 x2))))) (prim1 (λ x2 . x2)))))))))))))))))))))) (prim0 x0 x1)
Definition f9341.. := λ x0 x1 . prim0 (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x3 x3) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x2) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x3) (prim0 x2 x3))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x3 x2) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x3 x2)) (prim0 (prim0 x2 x2) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x3) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x3) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x2) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x3) (prim0 x3 x3))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x2) (prim0 x3 x3))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x3) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x3 x3) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x3) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x2) (prim0 x3 x3))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x2 x3) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x3 x2)) (prim0 (prim0 x2 x2) (prim0 x2 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x3) (prim0 x3 x3))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x3 x3) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x3)) (prim0 (prim0 x2 x3) (prim0 x3 x2))))) (prim0 (prim1 (λ x2 . prim1 (λ x3 . prim0 (prim0 (prim0 x3 x2) (prim0 x2 x2)) (prim0 (prim0 x3 x3) (prim0 x2 x3))))) (prim1 (λ x2 . x2)))))))))))))))))))))) (prim0 x0 x1)
Definition 1fa6d.. := prim0 (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim1 (λ x0 . x0))))))))))))))))))))))
Definition 3a365.. := prim0 (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x0 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x1 x0)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x0) (prim0 x1 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x0 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x1 x1))))) (prim1 (λ x0 . x0))))))))))))))))))))))
Definition False := ∀ x0 : ο . x0
Known 92e6a.. : ∀ x0 : ι → ι . ∀ x1 x2 . prim1 x0 = prim0 x1 x2False
Known 50787.. : ∀ x0 x1 x2 x3 . prim0 x0 x1 = prim0 x2 x3x0 = x2
Theorem 8b073.. : ∀ x0 x1 x2 . prim0 (prim1 (λ x4 . prim1 (λ x5 . prim0 (prim0 (prim0 x5 x4) (prim0 x4 x5)) (prim0 (prim0 x5 x5) (prim0 x4 x4))))) x0 = prim0 (prim0 (prim1 (λ x4 . prim1 (λ x5 . prim0 (prim0 (prim0 x5 x4) (prim0 x4 x5)) (prim0 (prim0 x5 x5) (prim0 x4 x4))))) x1) x2∀ x3 : ο . x3 (proof)
Theorem 6641d.. : ∀ x0 x1 x2 . prim0 (prim0 (prim1 (λ x4 . prim1 (λ x5 . prim0 (prim0 (prim0 x5 x4) (prim0 x4 x5)) (prim0 (prim0 x5 x5) (prim0 x4 x4))))) x1) x2 = prim0 (prim1 (λ x4 . prim1 (λ x5 . prim0 (prim0 (prim0 x5 x4) (prim0 x4 x5)) (prim0 (prim0 x5 x5) (prim0 x4 x4))))) x0∀ x3 : ο . x3 (proof)
Theorem 9ec26.. : ∀ x0 x1 . 5e331.. = a3eb9.. x0 x1∀ x2 : ο . x2 (proof)
Theorem 59f91.. : ∀ x0 x1 . 5e331.. = bf68c.. x0 x1∀ x2 : ο . x2 (proof)
Param 236c6.. : ι
Known f558c.. : ∀ x0 x1 . 236c6.. = prim0 x0 x1∀ x2 : ο . x2
Known 93754.. : ∀ x0 x1 x2 x3 . prim0 x0 x1 = prim0 x2 x3x1 = x3
Known db6fe.. : ∀ x0 x1 : ι → ι . ∀ x2 . prim1 x0 = prim1 x1x0 x2 = x1 x2
Theorem a8e2e.. : ∀ x0 x1 x2 x3 . a3eb9.. x0 x1 = bf68c.. x2 x3∀ x4 : ο . x4 (proof)
Known 128d8.. : ∀ x0 x1 x2 x3 . prim0 x0 x1 = prim0 x2 x3∀ x4 : ο . (x0 = x2x1 = x3x4)x4
Theorem 5e750.. : ∀ x0 x1 x2 x3 . a3eb9.. x0 x1 = a3eb9.. x2 x3and (x0 = x2) (x1 = x3) (proof)
Theorem 2f86f.. : ∀ x0 x1 x2 x3 . bf68c.. x0 x1 = bf68c.. x2 x3and (x0 = x2) (x1 = x3) (proof)
Theorem a3634.. : ∀ x0 x1 . c4def.. = 6b90c.. x0 x1∀ x2 : ο . x2 (proof)
Known 0286c.. : ∀ x0 x1 . prim0 x0 x1 = 236c6..False
Theorem 5e60e.. : c4def.. = c9248..∀ x0 : ο . x0 (proof)
Theorem dc5ae.. : ∀ x0 x1 . 6b90c.. x0 x1 = c9248..∀ x2 : ο . x2 (proof)
Theorem 924dd.. : ∀ x0 . c4def.. = a6e19.. x0∀ x1 : ο . x1 (proof)
Theorem a9278.. : ∀ x0 x1 x2 . 6b90c.. x0 x1 = a6e19.. x2∀ x3 : ο . x3 (proof)
Theorem 84bad.. : ∀ x0 . c9248.. = a6e19.. x0∀ x1 : ο . x1 (proof)
Theorem 0cc7e.. : ∀ x0 . c4def.. = 2fe34.. x0∀ x1 : ο . x1 (proof)
Theorem dabcf.. : ∀ x0 x1 x2 . 6b90c.. x0 x1 = 2fe34.. x2∀ x3 : ο . x3 (proof)
Theorem 1832c.. : ∀ x0 . c9248.. = 2fe34.. x0∀ x1 : ο . x1 (proof)
Theorem 7241c.. : ∀ x0 x1 . a6e19.. x0 = 2fe34.. x1∀ x2 : ο . x2 (proof)
Theorem 91964.. : ∀ x0 x1 . c4def.. = 3e00e.. x0 x1∀ x2 : ο . x2 (proof)
Theorem 07fb9.. : ∀ x0 x1 x2 x3 . 6b90c.. x0 x1 = 3e00e.. x2 x3∀ x4 : ο . x4 (proof)
Theorem 77b59.. : ∀ x0 x1 . c9248.. = 3e00e.. x0 x1∀ x2 : ο . x2 (proof)
Theorem 62a09.. : ∀ x0 x1 x2 . a6e19.. x0 = 3e00e.. x1 x2∀ x3 : ο . x3 (proof)
Theorem a0ec1.. : ∀ x0 x1 x2 . 2fe34.. x0 = 3e00e.. x1 x2∀ x3 : ο . x3 (proof)
Theorem a14cf.. : ∀ x0 x1 . c4def.. = f9341.. x0 x1∀ x2 : ο . x2 (proof)
Theorem 72b8e.. : ∀ x0 x1 x2 x3 . 6b90c.. x0 x1 = f9341.. x2 x3∀ x4 : ο . x4 (proof)
Theorem b728e.. : ∀ x0 x1 . c9248.. = f9341.. x0 x1∀ x2 : ο . x2 (proof)
Theorem cec81.. : ∀ x0 x1 x2 . a6e19.. x0 = f9341.. x1 x2∀ x3 : ο . x3 (proof)
Theorem becdb.. : ∀ x0 x1 x2 . 2fe34.. x0 = f9341.. x1 x2∀ x3 : ο . x3 (proof)
Theorem a1a1b.. : ∀ x0 x1 x2 x3 . 3e00e.. x0 x1 = f9341.. x2 x3∀ x4 : ο . x4 (proof)
Theorem b8b08.. : ∀ x0 . c4def.. = 1fa6d.. x0∀ x1 : ο . x1 (proof)
Theorem 0a32f.. : ∀ x0 x1 x2 . 6b90c.. x0 x1 = 1fa6d.. x2∀ x3 : ο . x3 (proof)
Theorem 0482c.. : ∀ x0 . c9248.. = 1fa6d.. x0∀ x1 : ο . x1 (proof)
Theorem 4bdb9.. : ∀ x0 x1 . a6e19.. x0 = 1fa6d.. x1∀ x2 : ο . x2 (proof)
Theorem a5def.. : ∀ x0 x1 . 2fe34.. x0 = 1fa6d.. x1∀ x2 : ο . x2 (proof)
Theorem 54459.. : ∀ x0 x1 x2 . 3e00e.. x0 x1 = 1fa6d.. x2∀ x3 : ο . x3 (proof)
Theorem 38968.. : ∀ x0 x1 x2 . f9341.. x0 x1 = 1fa6d.. x2∀ x3 : ο . x3 (proof)
Theorem f9749.. : ∀ x0 . c4def.. = 3a365.. x0∀ x1 : ο . x1 (proof)
Theorem ff84b.. : ∀ x0 x1 x2 . 6b90c.. x0 x1 = 3a365.. x2∀ x3 : ο . x3 (proof)
Theorem 36b24.. : ∀ x0 . c9248.. = 3a365.. x0∀ x1 : ο . x1 (proof)
Theorem 62476.. : ∀ x0 x1 . a6e19.. x0 = 3a365.. x1∀ x2 : ο . x2 (proof)
Theorem cdd8a.. : ∀ x0 x1 . 2fe34.. x0 = 3a365.. x1∀ x2 : ο . x2 (proof)
Theorem fb77a.. : ∀ x0 x1 x2 . 3e00e.. x0 x1 = 3a365.. x2∀ x3 : ο . x3 (proof)
Theorem 6774e.. : ∀ x0 x1 x2 . f9341.. x0 x1 = 3a365.. x2∀ x3 : ο . x3 (proof)
Theorem 9f429.. : ∀ x0 x1 . 1fa6d.. x0 = 3a365.. x1∀ x2 : ο . x2 (proof)
Theorem ffc37.. : ∀ x0 x1 x2 x3 . 6b90c.. x0 x1 = 6b90c.. x2 x3and (x0 = x2) (x1 = x3) (proof)
Theorem ffefa.. : ∀ x0 x1 x2 x3 . 6b90c.. x0 x1 = 6b90c.. x2 x3x0 = x2 (proof)
Theorem af84e.. : ∀ x0 x1 x2 x3 . 6b90c.. x0 x1 = 6b90c.. x2 x3x1 = x3 (proof)
Theorem 84af1.. : ∀ x0 x1 . a6e19.. x0 = a6e19.. x1x0 = x1 (proof)
Theorem 2eb6f.. : ∀ x0 x1 . 2fe34.. x0 = 2fe34.. x1x0 = x1 (proof)
Theorem 42e43.. : ∀ x0 x1 x2 x3 . 3e00e.. x0 x1 = 3e00e.. x2 x3and (x0 = x2) (x1 = x3) (proof)
Theorem ee7eb.. : ∀ x0 x1 x2 x3 . 3e00e.. x0 x1 = 3e00e.. x2 x3x0 = x2 (proof)
Theorem 67376.. : ∀ x0 x1 x2 x3 . 3e00e.. x0 x1 = 3e00e.. x2 x3x1 = x3 (proof)
Theorem 063ac.. : ∀ x0 x1 x2 x3 . f9341.. x0 x1 = f9341.. x2 x3and (x0 = x2) (x1 = x3) (proof)
Theorem 9efcd.. : ∀ x0 x1 x2 x3 . f9341.. x0 x1 = f9341.. x2 x3x0 = x2 (proof)
Theorem 2b512.. : ∀ x0 x1 x2 x3 . f9341.. x0 x1 = f9341.. x2 x3x1 = x3 (proof)
Theorem a1c68.. : ∀ x0 x1 . 1fa6d.. x0 = 1fa6d.. x1x0 = x1 (proof)
Theorem f684d.. : ∀ x0 x1 . 3a365.. x0 = 3a365.. x1x0 = x1 (proof)
Definition 74e69.. := λ x0 . ∀ x1 : ι → ο . x1 5e331..(∀ x2 x3 . x1 x2x1 x3x1 (a3eb9.. x2 x3))(∀ x2 x3 . x1 x2x1 x3x1 (bf68c.. x2 x3))x1 x0
Theorem e5778.. : 74e69.. 5e331.. (proof)
Theorem c4252.. : ∀ x0 x1 . 74e69.. x074e69.. x174e69.. (a3eb9.. x0 x1) (proof)
Theorem fbf8c.. : ∀ x0 x1 . 74e69.. x074e69.. x174e69.. (bf68c.. x0 x1) (proof)
Theorem facf7.. : ∀ x0 : ι → ο . x0 5e331..(∀ x1 x2 . 74e69.. x1x0 x174e69.. x2x0 x2x0 (a3eb9.. x1 x2))(∀ x1 x2 . 74e69.. x1x0 x174e69.. x2x0 x2x0 (bf68c.. x1 x2))∀ x1 . 74e69.. x1x0 x1 (proof)
Known FalseE : False∀ x0 : ο . x0
Theorem 75262.. : ∀ x0 x1 . 74e69.. (a3eb9.. x0 x1)and (74e69.. x0) (74e69.. x1) (proof)
Theorem 826e0.. : ∀ x0 x1 . 74e69.. (bf68c.. x0 x1)and (74e69.. x0) (74e69.. x1) (proof)
Definition e05e6.. := λ x0 . ∀ x1 : ι → ο . x1 c4def..(∀ x2 x3 . x1 x2x1 x3x1 (6b90c.. x2 x3))x1 c9248..(∀ x2 . x1 x2x1 (a6e19.. x2))(∀ x2 . x1 x2x1 (2fe34.. x2))(∀ x2 x3 . x1 x2x1 x3x1 (3e00e.. x2 x3))(∀ x2 x3 . x1 x2x1 x3x1 (f9341.. x2 x3))(∀ x2 . x1 x2x1 (1fa6d.. x2))(∀ x2 . x1 x2x1 (3a365.. x2))x1 x0
Theorem b24e2.. : e05e6.. c4def.. (proof)
Theorem 05df6.. : ∀ x0 x1 . e05e6.. x0e05e6.. x1e05e6.. (6b90c.. x0 x1) (proof)
Theorem 9dc64.. : e05e6.. c9248.. (proof)
Theorem 82f14.. : ∀ x0 . e05e6.. x0e05e6.. (a6e19.. x0) (proof)
Theorem 6d5ea.. : ∀ x0 . e05e6.. x0e05e6.. (2fe34.. x0) (proof)
Theorem 1a774.. : ∀ x0 x1 . e05e6.. x0e05e6.. x1e05e6.. (3e00e.. x0 x1) (proof)
Theorem 6891d.. : ∀ x0 x1 . e05e6.. x0e05e6.. x1e05e6.. (f9341.. x0 x1) (proof)
Theorem 96df8.. : ∀ x0 . e05e6.. x0e05e6.. (1fa6d.. x0) (proof)
Theorem b6c01.. : ∀ x0 . e05e6.. x0e05e6.. (3a365.. x0) (proof)