| Loop_with_defs_cex2 = λ 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) (∀ x23 : ο . (∀ x24 . and (In x24 x1) (not (x7 x24 (x2 (x4 x5 x16) (x10 x18 x20 x16)) x22 = x5)) ⟶ x23) ⟶ x23) ⟶ x21) ⟶ x21) ⟶ x19) ⟶ x19) ⟶ x17) ⟶ x17) ⟶ x15) ⟶ x15) |
|