Proofgold Address

Param and : ο → ο → ο
Param 244aa.. : (ι → ι → ο) → ο
Param 5d0c6.. : (ι → ι → ο) → ο
Param True : ο
Definition 65ce4.. := λ x0 : ι → ι → ο . and (and (244aa.. x0) (5d0c6.. x0)) True
Param 39ffe.. : (ι → ι → ο) → ο
Param 29aed.. : (ι → ι → ο) → ο
Definition c4aab.. := λ x0 : ι → ι → ο . and (and (39ffe.. x0) (29aed.. x0)) True
Definition 0eacd.. := 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 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 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 x1) (prim0 x0 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 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x1 x0))))) (prim1 (λ x0 . x0)))))))))
Param 57d6a.. : ι → ι → ι
Param 67ee8.. : ι
Param 27862.. : ι
Param bcddf.. : ι → (ι → ι) → ι
Param 1f2c4.. : ι
Param 25ca3.. : ι
Param 62f06.. : ι
Param 5b8fe.. : ι
Definition 472f9.. := 57d6a.. 67ee8.. (57d6a.. 27862.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..)))))
Definition 30336.. := λ x0 : ι → ι → ο . and (65ce4.. x0) (x0 0eacd.. 472f9..)
Param d478c.. : (ι → ι → ο) → (ι → ι → ο) → ι → ο
Conjecture 2d490.. : ∀ x0 x1 : ι → ι → ο . 65ce4.. x0 ⟶ c4aab.. x1 ⟶ d478c.. x0 x1 472f9..
Definition c85c4.. := 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 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 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 x1) (prim0 x0 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 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 x1 x0) (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)))))))))))
Param 3cd3c.. : ι
Param cb931.. : ι
Param 7a0ec.. : ι
Definition 164ed.. := 57d6a.. 3cd3c.. (57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x1) x1)))))
Definition e81b6.. := λ x0 : ι → ι → ο . and (30336.. x0) (x0 c85c4.. 164ed..)
Conjecture c05c7.. : ∀ x0 x1 : ι → ι → ο . 30336.. x0 ⟶ c4aab.. x1 ⟶ d478c.. x0 x1 164ed..
Definition 81b7d.. := 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 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 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 x1) (prim0 x0 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 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 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 x1 x0) (prim0 x1 x1))))) (prim1 (λ x0 . x0)))))))))))))
Param f3baa.. : ι
Definition e09bd.. := 57d6a.. 3cd3c.. (57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . 57d6a.. (57d6a.. 7a0ec.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..)) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..))) (λ x2 . 57d6a.. (57d6a.. f3baa.. (57d6a.. x2 x1)) (57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x3 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x1) x3)) (57d6a.. x2 x3)))))))))))
Definition 8e134.. := λ x0 : ι → ι → ο . and (e81b6.. x0) (x0 81b7d.. e09bd..)
Conjecture d577a.. : ∀ x0 x1 : ι → ι → ο . e81b6.. x0 ⟶ c4aab.. x1 ⟶ d478c.. x0 x1 e09bd..
Definition fb467.. := 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 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 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 x1) (prim0 x0 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 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 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 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 x0 x1)) (prim0 (prim0 x1 x1) (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 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 x1))))) (prim1 (λ x0 . x0))))))))))))))))
Definition c7387.. := 57d6a.. 3cd3c.. (57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x2 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x2) x1)) (57d6a.. (57d6a.. 7a0ec.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..)) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..))) (λ x3 . 57d6a.. (57d6a.. f3baa.. (57d6a.. x3 x1)) (57d6a.. x3 x2)))))))))))
Definition 5c69a.. := bcddf.. 1f2c4.. (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x2 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x2) x1)) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 81b7d.. x0) x2) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x3 . 57d6a.. (57d6a.. 7a0ec.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..)) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..))) (λ x4 . 57d6a.. (57d6a.. f3baa.. (57d6a.. x4 x3)) (57d6a.. x4 x2)))))) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..))) (λ x3 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. x3 x2)) (λ x4 . x4)))) x1)))))
Definition 3228a.. := λ x0 : ι → ι → ο . and (8e134.. x0) (x0 fb467.. c7387..)
Conjecture 56b32.. : ∀ x0 x1 : ι → ι → ο . 8e134.. x0 ⟶ c4aab.. x1 ⟶ d478c.. x0 x1 c7387..
Param 6fe8d.. : (ι → ι → ο) → (ι → ι → ο) → (ι → ι → ο) → ι → ι → ο
Param 5c39b.. : ι → ι → ο
Conjecture 9e9cb.. : ∀ x0 x1 : ι → ι → ο . 8e134.. x0 ⟶ c4aab.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 5c69a.. c7387..
Definition 4fb85.. := λ x0 : ι → ι → ο . and (c4aab.. x0) (x0 fb467.. 5c69a..)
Definition ba2b1.. := 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 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 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 x1) (prim0 x0 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 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 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 x1 x0) (prim0 x1 x1))))) (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 x1))))) (prim1 (λ x0 . x0)))))))))))))))
Definition 88efa.. := 57d6a.. 3cd3c.. (57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . 57d6a.. (57d6a.. 7a0ec.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..)) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..))) (λ x2 . 57d6a.. (57d6a.. f3baa.. (57d6a.. x2 x1)) (57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x3 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x3) x1)) (57d6a.. x2 x3)))))))))))
Definition fc59c.. := bcddf.. 1f2c4.. (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..))) (λ x2 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. x2 x1)) (λ x3 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x4 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x4) x1)) (λ x5 . 57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. fb467.. x0) x1) x4) x5) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (57d6a.. x2))) x3))))))
Definition d4967.. := λ x0 : ι → ι → ο . and (3228a.. x0) (x0 ba2b1.. 88efa..)
Conjecture 7e7eb.. : ∀ x0 x1 : ι → ι → ο . 3228a.. x0 ⟶ 4fb85.. x1 ⟶ d478c.. x0 x1 88efa..
Conjecture 8014a.. : ∀ x0 x1 : ι → ι → ο . 3228a.. x0 ⟶ 4fb85.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. fc59c.. 88efa..
Definition 99c12.. := λ x0 : ι → ι → ο . and (4fb85.. x0) (x0 ba2b1.. fc59c..)
Definition 2a8bd.. := 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 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 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 x1) (prim0 x0 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 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 x0)) (prim0 (prim0 x1 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 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 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 x1)) (prim0 (prim0 x0 x0) (prim0 x1 x1))))) (prim1 (λ x0 . x0))))))))))))))))
Definition e09bd.. := 57d6a.. 3cd3c.. (57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . 57d6a.. (57d6a.. 7a0ec.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..)) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..))) (λ x2 . 57d6a.. (57d6a.. f3baa.. (57d6a.. x2 x1)) (57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x3 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x1) x3)) (57d6a.. x2 x3)))))))))))
Definition 5da2d.. := bcddf.. 1f2c4.. (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..))) (λ x2 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. x2 x1)) (λ x3 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x4 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x1) x4)) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 81b7d.. x0) x1) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (57d6a.. x2))) x3) x4)))))))
Definition 24e94.. := λ x0 : ι → ι → ο . and (d4967.. x0) (x0 2a8bd.. e09bd..)
Conjecture 23459.. : ∀ x0 x1 : ι → ι → ο . d4967.. x0 ⟶ 99c12.. x1 ⟶ d478c.. x0 x1 e09bd..
Conjecture ad066.. : ∀ x0 x1 : ι → ι → ο . d4967.. x0 ⟶ 99c12.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 5da2d.. e09bd..
Definition 541bd.. := λ x0 : ι → ι → ο . and (99c12.. x0) (x0 2a8bd.. 5da2d..)
Definition 57faf.. := 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 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 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 x1) (prim0 x0 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 x0)) (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 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 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x1 x0))))) (prim1 (λ x0 . x0)))))))))))))
Definition 2f7dd.. := 57d6a.. 3cd3c.. (57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x2 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x1) x2)) (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x2) x1))))))))
Definition fef4a.. := bcddf.. 1f2c4.. (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x2 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x1) x2)) (λ x3 . 57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 2a8bd.. x0) x1) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x4 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x4) x1))) (57d6a.. (57d6a.. c85c4.. x0) x1)) x2) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 2a8bd.. x0) x1) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x1)))) (57d6a.. (57d6a.. c85c4.. x0) x1)) x2) x3)))))
Definition ece00.. := λ x0 : ι → ι → ο . and (24e94.. x0) (x0 57faf.. 2f7dd..)
Conjecture 1f6c7.. : ∀ x0 x1 : ι → ι → ο . 24e94.. x0 ⟶ 541bd.. x1 ⟶ d478c.. x0 x1 2f7dd..
Conjecture a71f4.. : ∀ x0 x1 : ι → ι → ο . 24e94.. x0 ⟶ 541bd.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. fef4a.. 2f7dd..
Definition c5074.. := λ x0 : ι → ι → ο . and (541bd.. x0) (x0 57faf.. fef4a..)
Definition a809c.. := 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 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 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 x1) (prim0 x0 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 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 x0)) (prim0 (prim0 x1 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 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 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 x1))))) (prim1 (λ x0 . x0))))))))))))))))
Definition 88efa.. := 57d6a.. 3cd3c.. (57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . 57d6a.. (57d6a.. 7a0ec.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..)) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..))) (λ x2 . 57d6a.. (57d6a.. f3baa.. (57d6a.. x2 x1)) (57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x3 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x3) x1)) (57d6a.. x2 x3)))))))))))
Definition b84f8.. := bcddf.. 1f2c4.. (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) 5b8fe..))) (λ x2 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. x2 x1)) (λ x3 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x4 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x4) x1)) (λ x5 . 57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 81b7d.. x0) x1) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (57d6a.. x2))) x3) x4) (57d6a.. (57d6a.. (57d6a.. (57d6a.. 57faf.. x0) x4) x1) x5)))))))
Definition 426f2.. := λ x0 : ι → ι → ο . and (ece00.. x0) (x0 a809c.. 88efa..)
Conjecture 19fff.. : ∀ x0 x1 : ι → ι → ο . ece00.. x0 ⟶ c5074.. x1 ⟶ d478c.. x0 x1 88efa..
Conjecture f04b5.. : ∀ x0 x1 : ι → ι → ο . ece00.. x0 ⟶ c5074.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. b84f8.. 88efa..
Definition 176ea.. := λ x0 : ι → ι → ο . and (c5074.. x0) (x0 a809c.. b84f8..)
Definition b759b.. := 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 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 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 x1) (prim0 x0 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 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 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 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 x1)) (prim0 (prim0 x1 x0) (prim0 x1 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 x1) (prim0 x0 x0))))) (prim1 (λ x0 . x0)))))))))))))))
Definition 69fe6.. := 57d6a.. 3cd3c.. (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . 57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x1 . 57d6a.. (57d6a.. f3baa.. x0) (57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. 5b8fe..) x0) x1)) x1))))))
Definition 3d9f4.. := bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x1 . bcddf.. (57d6a.. 3cd3c.. x0) (λ x2 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. 5b8fe..) x0) x1)) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 81b7d.. 5b8fe..) x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x3 . x3))) x2) x1)))))
Definition 149e9.. := λ x0 : ι → ι → ο . and (426f2.. x0) (x0 b759b.. 69fe6..)
Conjecture df7cd.. : ∀ x0 x1 : ι → ι → ο . 426f2.. x0 ⟶ 176ea.. x1 ⟶ d478c.. x0 x1 69fe6..
Conjecture 081ca.. : ∀ x0 x1 : ι → ι → ο . 426f2.. x0 ⟶ 176ea.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 3d9f4.. 69fe6..
Definition 4c37b.. := λ x0 : ι → ι → ο . and (176ea.. x0) (x0 b759b.. 3d9f4..)
Definition 74eba.. := 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 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 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 x1) (prim0 x0 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 x0)) (prim0 (prim0 x1 x1) (prim0 x0 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 x0) (prim0 x0 x1))))) (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 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 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x1 x0))))) (prim1 (λ x0 . x0)))))))))))))))
Definition 9a13d.. := 57d6a.. 3cd3c.. (57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x2 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x3 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x1) x2)) (57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x2) x3)) (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x1) x3)))))))))))
Definition 14a50.. := bcddf.. 1f2c4.. (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x2 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x3 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x1) x2)) (λ x4 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x2) x3)) (λ x5 . 57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. ba2b1.. x0) x2) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x6 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x6) x3))) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 2a8bd.. x0) x1) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x6 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x6) x3))) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 2a8bd.. x0) x1) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x1)))) (57d6a.. (57d6a.. c85c4.. x0) x1)) x3) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. a809c.. x0) x2) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x6 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x6) x3))) x5) x1) x4))) x2) x4)) x1) x4))))))
Definition 8840c.. := λ x0 : ι → ι → ο . and (149e9.. x0) (x0 74eba.. 9a13d..)
Conjecture cf051.. : ∀ x0 x1 : ι → ι → ο . 149e9.. x0 ⟶ 4c37b.. x1 ⟶ d478c.. x0 x1 9a13d..
Conjecture c6ef0.. : ∀ x0 x1 : ι → ι → ο . 149e9.. x0 ⟶ 4c37b.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 14a50.. 9a13d..
Definition f2960.. := λ x0 : ι → ι → ο . and (4c37b.. x0) (x0 74eba.. 14a50..)
Definition cdbc5.. := 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 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 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 x1) (prim0 x0 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 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 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 x0 x1))))) (prim1 (λ x0 . x0)))))))))))
Definition 5030a.. := 57d6a.. 3cd3c.. (57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x1 . 57d6a.. (57d6a.. 7a0ec.. (57d6a.. (57d6a.. 62f06.. x0) x1)) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) x1))) (λ x2 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x3 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x4 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x3) x4)) (57d6a.. (57d6a.. (57d6a.. 0eacd.. x1) (57d6a.. x2 x3)) (57d6a.. x2 x4)))))))))))))
Definition 0065e.. := bcddf.. 1f2c4.. (λ x0 . bcddf.. 1f2c4.. (λ x1 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) x1))) (λ x2 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x3 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x4 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x3) x4)) (λ x5 . 57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. ba2b1.. x0) x4) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x6 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. x1) (57d6a.. x2 x6)) (57d6a.. x2 x4)))) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 2a8bd.. x0) x3) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x6 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. x1) (57d6a.. x2 x6)) (57d6a.. x2 x4)))) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 2a8bd.. x0) x3) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x6 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. x1) (57d6a.. x2 x3)) (57d6a.. x2 x6)))) (57d6a.. (57d6a.. c85c4.. x1) (57d6a.. x2 x3))) x4) x5)) x4) x5)) x3) x5))))))
Definition 436d2.. := λ x0 : ι → ι → ο . and (8840c.. x0) (x0 cdbc5.. 5030a..)
Conjecture 2c56b.. : ∀ x0 x1 : ι → ι → ο . 8840c.. x0 ⟶ f2960.. x1 ⟶ d478c.. x0 x1 5030a..
Conjecture 5c292.. : ∀ x0 x1 : ι → ι → ο . 8840c.. x0 ⟶ f2960.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 0065e.. 5030a..
Definition f07f8.. := λ x0 : ι → ι → ο . and (f2960.. x0) (x0 cdbc5.. 0065e..)
Definition 086a0.. := 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 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 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 x1) (prim0 x0 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 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 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 x0 x1))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x1) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (prim1 (λ x0 . x0))))))))))))
Definition f52d3.. := 57d6a.. 3cd3c.. (57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x1 . 57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x2 . 57d6a.. (57d6a.. 7a0ec.. (57d6a.. (57d6a.. 62f06.. x0) (57d6a.. (57d6a.. 62f06.. x1) x2))) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) (57d6a.. (57d6a.. 62f06.. x1) x2)))) (λ x3 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x4 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x5 . 57d6a.. (57d6a.. 7a0ec.. x1) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x1)) (λ x6 . 57d6a.. (57d6a.. 7a0ec.. x1) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x1)) (λ x7 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x4) x5)) (57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x1) x6) x7)) (57d6a.. (57d6a.. (57d6a.. 0eacd.. x2) (57d6a.. (57d6a.. x3 x4) x6)) (57d6a.. (57d6a.. x3 x5) x7))))))))))))))))))))
Definition a70d1.. := bcddf.. 1f2c4.. (λ x0 . bcddf.. 1f2c4.. (λ x1 . bcddf.. 1f2c4.. (λ x2 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. (57d6a.. (57d6a.. 62f06.. x0) (57d6a.. (57d6a.. 62f06.. x1) x2)))) (λ x3 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x4 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x5 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x1)) (λ x6 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x1)) (λ x7 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x4) x5)) (λ x8 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x1) x6) x7)) (λ x9 . 57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. ba2b1.. x0) x5) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x10 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. x2) (57d6a.. (57d6a.. x3 x10) x6)) (57d6a.. (57d6a.. x3 x5) x7)))) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. ba2b1.. x1) x7) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x1)) (λ x10 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. x2) (57d6a.. (57d6a.. x3 x5) x10)) (57d6a.. (57d6a.. x3 x5) x7)))) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 2a8bd.. x0) x4) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x10 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. x2) (57d6a.. (57d6a.. x3 x10) x7)) (57d6a.. (57d6a.. x3 x5) x7)))) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 2a8bd.. x1) x6) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x1)) (λ x10 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. x2) (57d6a.. (57d6a.. x3 x4) x10)) (57d6a.. (57d6a.. x3 x5) x7)))) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 2a8bd.. x0) x4) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x10 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. x2) (57d6a.. (57d6a.. x3 x4) x6)) (57d6a.. (57d6a.. x3 x10) x7)))) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. 2a8bd.. x1) x6) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x1)) (λ x10 . 57d6a.. (57d6a.. (57d6a.. 0eacd.. x2) (57d6a.. (57d6a.. x3 x4) x6)) (57d6a.. (57d6a.. x3 x4) x10)))) (57d6a.. (57d6a.. c85c4.. x2) (57d6a.. (57d6a.. x3 x4) x6))) x7) x9)) x5) x8)) x7) x9)) x5) x8)) x6) x9)) x4) x8))))))))))
Definition d3d9d.. := λ x0 : ι → ι → ο . and (436d2.. x0) (x0 086a0.. f52d3..)
Conjecture 3b5f0.. : ∀ x0 x1 : ι → ι → ο . 436d2.. x0 ⟶ f07f8.. x1 ⟶ d478c.. x0 x1 f52d3..
Conjecture d0468.. : ∀ x0 x1 : ι → ι → ο . 436d2.. x0 ⟶ f07f8.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. a70d1.. f52d3..
Definition f51da.. := λ x0 : ι → ι → ο . and (f07f8.. x0) (x0 086a0.. a70d1..)
Definition de906.. := 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 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 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 x1) (prim0 x0 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 x0 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 x0) (prim0 x1 x1))))) (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 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))))) (prim1 (λ x0 . x0))))))))))))))
Param ae581.. : ι
Definition 54a4f.. := 57d6a.. 3cd3c.. (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (57d6a.. (57d6a.. f3baa.. ae581..))))
Definition 71c49.. := bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x1 . x1)))) (λ x1 . 57d6a.. x1 x0))
Definition 9603b.. := λ x0 : ι → ι → ο . and (d3d9d.. x0) (x0 de906.. 54a4f..)
Conjecture 0d946.. : ∀ x0 x1 : ι → ι → ο . d3d9d.. x0 ⟶ f51da.. x1 ⟶ d478c.. x0 x1 54a4f..
Conjecture 94b30.. : ∀ x0 x1 : ι → ι → ο . d3d9d.. x0 ⟶ f51da.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 71c49.. 54a4f..
Definition 68791.. := λ x0 : ι → ι → ο . and (f51da.. x0) (x0 de906.. 71c49..)
Definition 22293.. := 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 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 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 x1) (prim0 x0 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 x1 x1)) (prim0 (prim0 x0 x0) (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 x0) (prim0 x1 x1))))) (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 x1 x0) (prim0 x1 x1))))) (prim1 (λ x0 . x0))))))))))))))
Param c8911.. : ι
Definition af10d.. := 57d6a.. 3cd3c.. (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . 57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x1 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. f3baa.. x0) ae581..)) x1)) (57d6a.. (57d6a.. f3baa.. (57d6a.. c8911.. x0)) x1))))))
Definition 5f696.. := bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x1 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. f3baa.. x0) ae581..)) x1)) (λ x2 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. c8911.. x0)) (57d6a.. x2))))
Definition 0ec24.. := λ x0 : ι → ι → ο . and (9603b.. x0) (x0 22293.. af10d..)
Conjecture 56228.. : ∀ x0 x1 : ι → ι → ο . 9603b.. x0 ⟶ 68791.. x1 ⟶ d478c.. x0 x1 af10d..
Conjecture be1a5.. : ∀ x0 x1 : ι → ι → ο . 9603b.. x0 ⟶ 68791.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 5f696.. af10d..
Definition 9aa0b.. := λ x0 : ι → ι → ο . and (68791.. x0) (x0 22293.. 5f696..)
Definition 0ad46.. := 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 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 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 x1) (prim0 x0 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 x1) (prim0 x1 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 x1) (prim0 x0 x1))))) (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 x0)) (prim0 (prim0 x1 x0) (prim0 x1 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 x1))))) (prim1 (λ x0 . x0)))))))))))))
Definition b02dd.. := 57d6a.. 3cd3c.. (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . 57d6a.. (57d6a.. f3baa.. x0) (57d6a.. (57d6a.. f3baa.. (57d6a.. c8911.. x0)) ae581..))))
Definition 7e03f.. := bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . bcddf.. (57d6a.. 3cd3c.. x0) (λ x1 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. c8911.. x0)) (57d6a.. (57d6a.. (57d6a.. (57d6a.. 22293.. x0) ae581..) (bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. f3baa.. x0) ae581..)) (λ x2 . 57d6a.. x2 x1))))))
Definition ab95a.. := λ x0 : ι → ι → ο . and (0ec24.. x0) (x0 0ad46.. b02dd..)
Conjecture 18783.. : ∀ x0 x1 : ι → ι → ο . 0ec24.. x0 ⟶ 9aa0b.. x1 ⟶ d478c.. x0 x1 b02dd..
Conjecture bcfb2.. : ∀ x0 x1 : ι → ι → ο . 0ec24.. x0 ⟶ 9aa0b.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 7e03f.. b02dd..
Definition a3364.. := λ x0 : ι → ι → ο . and (9aa0b.. x0) (x0 0ad46.. 7e03f..)
Definition ee03a.. := 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 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 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 x1) (prim0 x0 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 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 x0) (prim0 x1 x1))))) (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 x0 x0) (prim0 x0 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 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 x0) (prim0 x1 x1))))) (prim1 (λ x0 . x0)))))))))))))))))
Definition 6543a.. := 57d6a.. 3cd3c.. (57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . 57d6a.. (57d6a.. 7a0ec.. 5b8fe..) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x1 . 57d6a.. (57d6a.. f3baa.. (57d6a.. (57d6a.. f3baa.. x0) x1)) (57d6a.. (57d6a.. f3baa.. (57d6a.. c8911.. x1)) (57d6a.. c8911.. x0)))))))
Definition 476c5.. := bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. 5b8fe..)) (λ x1 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. f3baa.. x0) x1)) (λ x2 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. c8911.. x1)) (λ x3 . bcddf.. (57d6a.. 3cd3c.. x0) (λ x4 . 57d6a.. (57d6a.. (57d6a.. 0ad46.. x1) (57d6a.. x2 x4)) x3)))))
Definition 43682.. := λ x0 : ι → ι → ο . and (ab95a.. x0) (x0 ee03a.. 6543a..)
Conjecture c2121.. : ∀ x0 x1 : ι → ι → ο . ab95a.. x0 ⟶ a3364.. x1 ⟶ d478c.. x0 x1 6543a..
Conjecture abebd.. : ∀ x0 x1 : ι → ι → ο . ab95a.. x0 ⟶ a3364.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 476c5.. 6543a..
Definition dee3e.. := λ x0 : ι → ι → ο . and (a3364.. x0) (x0 ee03a.. 476c5..)
Definition 4f606.. := 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 x0) (prim0 x0 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x1)) (prim0 (prim0 x1 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 x1) (prim0 x0 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 x0)) (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 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 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 x0) (prim0 x1 x1))))) (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 x0))))) (prim0 (prim1 (λ x0 . prim1 (λ x1 . prim0 (prim0 (prim0 x1 x0) (prim0 x0 x0)) (prim0 (prim0 x1 x1) (prim0 x1 x0))))) (prim1 (λ x0 . x0)))))))))))))))))
Definition daa3d.. := 57d6a.. 3cd3c.. (57d6a.. cb931.. (bcddf.. 1f2c4.. (λ x0 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . 57d6a.. (57d6a.. 7a0ec.. x0) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x2 . 57d6a.. (57d6a.. f3baa.. (57d6a.. c8911.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x1) x2))) (57d6a.. c8911.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x2) x1)))))))))
Definition 65146.. := bcddf.. 1f2c4.. (λ x0 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x1 . bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (λ x2 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. c8911.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x1) x2))) (λ x3 . bcddf.. (57d6a.. 3cd3c.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x2) x1)) (λ x4 . 57d6a.. (57d6a.. (57d6a.. 0ad46.. (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x1) x2)) (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. (57d6a.. a809c.. x0) x1) (bcddf.. (57d6a.. 67ee8.. (57d6a.. 25ca3.. x0)) (57d6a.. (57d6a.. (57d6a.. 0eacd.. x0) x1)))) (57d6a.. (57d6a.. c85c4.. x0) x1)) x2) x4)) x3)))))
Definition aac29.. := λ x0 : ι → ι → ο . and (43682.. x0) (x0 4f606.. daa3d..)
Conjecture 8816a.. : ∀ x0 x1 : ι → ι → ο . 43682.. x0 ⟶ dee3e.. x1 ⟶ d478c.. x0 x1 daa3d..
Conjecture 82e8c.. : ∀ x0 x1 : ι → ι → ο . 43682.. x0 ⟶ dee3e.. x1 ⟶ 6fe8d.. x0 x1 5c39b.. 65146.. daa3d..
Definition 505b1.. := λ x0 : ι → ι → ο . and (dee3e.. x0) (x0 4f606.. 65146..)