| ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 : ι → ι → ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 x9 : ι → ι → ι → ι . ∀ x10 x11 x12 x13 : ι → ι → ι . Loop_with_defs x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ⟶ (∃ x14 . and (In x14 x0) (∃ x16 . and (In x16 x0) (∃ x18 . and (In x18 x0) (∃ x20 . and (In x20 x0) (∃ x22 . and (In x22 x0) (not (x6 x22 (x1 (x3 x4 x14) (x9 x16 x18 x14)) x20 = x4))))))) ⟶ Loop_with_defs_cex2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 |
|
|
|
|
|
|
|
|
|
|