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