| Loop_with_defs = λ x1 . λ x2 x3 x4 : ι → ι → ι . λ x5 . λ x6 : ι → ι → ι . λ x7 : ι → ι → ι → ι . λ x8 : ι → ι → ι . λ x9 x10 : ι → ι → ι → ι . λ x11 x12 x13 x14 : ι → ι → ι . and (and (and (and (Loop x1 x2 x3 x4 x5) (∀ x15 . In x15 x1 ⟶ ∀ x16 . In x16 x1 ⟶ x6 x15 x16 = x3 (x2 x16 x15) (x2 x15 x16))) (∀ x15 . In x15 x1 ⟶ ∀ x16 . In x16 x1 ⟶ ∀ x17 . In x17 x1 ⟶ x7 x15 x16 x17 = x3 (x2 x15 (x2 x16 x17)) (x2 (x2 x15 x16) x17))) (∀ x15 . In x15 x1 ⟶ ∀ x16 . In x16 x1 ⟶ and (and (and (and (x8 x15 x16 = x3 x15 (x2 x16 x15)) (x11 x15 x16 = x2 x15 (x2 x16 (x3 x15 x5)))) (x12 x15 x16 = x2 (x2 (x4 x5 x15) x16) x15)) (x13 x15 x16 = x2 (x3 x15 x16) (x3 (x3 x15 x5) x5))) (x14 x15 x16 = x2 (x4 x5 (x4 x5 x15)) (x4 x16 x15)))) (∀ x15 . In x15 x1 ⟶ ∀ x16 . In x16 x1 ⟶ ∀ x17 . In x17 x1 ⟶ and (x9 x15 x16 x17 = x3 (x2 x16 x15) (x2 x16 (x2 x15 x17))) (x10 x15 x16 x17 = x4 (x2 (x2 x17 x15) x16) (x2 x15 x16))) |
|