| 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 . and (In x15 x1) (∃ x17 . and (In x17 x1) (∃ x19 . and (In x19 x1) (∃ x21 . and (In x21 x1) (not (x6 (x2 (x3 (x9 x17 x19 x15) x5) x15) x21 = x5)))))) |
|