| Loop_with_defs_cex1 = λ x1 . λ x2 x3 x4 : ι → ι → ι . λ x5 . λ x6 : ι → ι → ι . λ x7 : ι → ι → ι → ι . λ x8 : ι → ι → ι . λ x9 x10 : ι → ι → ι → ι . λ x11 x12 x13 x14 : ι → ι → ι . and (Loop_with_defs x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) (∀ x15 : ο . (∀ x16 . and (In x16 x1) (∀ x17 : ο . (∀ x18 . and (In x18 x1) (∀ x19 : ο . (∀ x20 . and (In x20 x1) (∀ x21 : ο . (∀ x22 . and (In x22 x1) (not (x6 (x2 (x3 (x9 x18 x20 x16) x5) x16) x22 = x5)) ⟶ x21) ⟶ x21) ⟶ x19) ⟶ x19) ⟶ x17) ⟶ x17) ⟶ x15) ⟶ x15) |
|