blocks : theory begin sit, location : type action : type s, s_{1}, s_{2}, s_{3} : var sit a, a_{1}, a_{2}, a_{3} : var action S_{0} : sit f, g : var [nat → nat] J, J_{1} : var [nat → bool] result(a, s) : sit b, b_{1}, b_{2}, b_{3}, b_{4}, b_{5}, n, n_{1} : var nat l, l_{1}, l_{2}, l_{3} : var location top(b) : location On(b, l, s) : bool P, P_{1}, P_{2}, P_{3} : var [[nat, nat] → bool] trans(P) : [[nat, nat] → bool] above(b, b_{1}, s) : bool = trans(λ b_{1}, b_{2} : On(b_{1}, top(b_{2}), s))(b, b_{1}) table2 : location I(b) : bool = On(b, table2, S_{0}) Less(b, b_{1}, b_{2}) : bool = above(b_{2}, b, S_{0}) ∧ I(b) ∧ (above(b_{1}, b, S_{0}) ∨ b = b_{1}) Bset(b, b_{1}) : bool = (above(b_{1}, b, S_{0}) ∨ b = b_{1}) ∧ I(b) move(b, l) : action Finite(J) : bool = ∃ f, g, b_{1}, b_{2} : (∀ J_{1} :

(J_{1}(b_{1}) ∧ (∀ b : J_{1}(b) ⊃ J_{1}(f(b)))) ⊃

∀b : J(b) ⊃ J_{1}(b))∧

(∀ J_{1} :

(J_{1}(b_{2}) ∧ (∀ b : J_{1}(b) ⊃ J_{1}(g(b)))) ⊃
∀b : J(b) ⊃ J_{1}(b))∧

(∀ b : f(g(b)) = b ∧ g(f(b)) = b)

Clear(l, s) : bool = ((l = table2)∨

(∃ b : ∀ b_{1} : l = top(b_{1}) ∧ ¬On(b_{1}, top(b), s))) closurelocation : axiom ∀ l : ∃ b : l = top(b) ∨ l = table2 uniquelocation : axiom ∀ b, b_{1} : top(b_{1}) = top(b) ⊃ b = b_{1} uniquelocation2 : axiom ∀ b : top(b) ≠ table2 closureaction : axiom ∀ a : ∃ b, l : a = move(b, l) uniqueaction : axiom

∀ b, l, b_{1}, l_{1} : move(b, l) = move(b_{1}, l_{1}) ⊃ b = b_{1} ∧ l = l_{1} uniquesit : axiom ∀ s, a : result(a, s) ≠ S_{0} uniquesit2 : axiom

∀ s, s_{1}, a, a_{1} :

result(a, s) = result(a_{1}, s_{1}) ⊃ a = a_{1} ∧ s = s_{1} transdef : axiom

∀ P :

(∀ b, b_{1} : P (b, b_{1}) ⊃ trans(P)(b, b_{1}))∧

(∀ b, b_{1}, b_{2} : P (b, b_{1}) ∧ trans(P)(b_{1}, b_{2}) ⊃ trans(P)(b, b_{2}))∧

(∀ P_{1} :
((∀ b, b_{1} : P (b, b_{1}) ⊃ P_{1}(b, b_{1}))∧
(∀ b, b_{1}, b_{2} :
P (b, b_{1})∧
P_{1}(b_{1}, b_{2}) ⊃
P_{1}(b, b_{2}))∧
(∀ b, b_{1} :
P_{1}(b, b_{1}) ⊃
trans(P)(b, b_{1}))) ⊃
(∀ b, b_{1} : trans(P)(b, b_{1}) ⊃ P_{1}(b, b_{1})))

constraint0 : axiom ∀ b, s : ∃ l : On(b, l, s) constraint1 : axiom

∀ b, s : ∃ b_{1} : On(b_{1}, table2, s) ∧ (above(b, b_{1}, s) ∨ b = b_{1}) constraint2 : axiom

∀ b, s :

(¬On(b, table2, s)) ⊃

(∃ b_{1} :

On(b, top(b_{1}), s) ∧ ∀ b_{2} : On(b, top(b_{1}), s) ⊃ b_{1} = b_{2})

constraint3 : axiom ∀ b, b_{1}, s : On(b, top(b_{1}), s) ⊃ (¬On(b, table2, s)) constraint4 : axiom

∀ b, b_{1}, b_{2}, s : On(b_{1}, top(b), s) ∧ On(b_{2}, top(b), s) ⊃ b_{1} = b_{2} constraint5 : axiom ∀ b, s : ∃ b_{1} : ∀ b_{2} : ¬On(b_{2}, top(b_{1}), s) ∧ (above(b_{1}, b, s) ∨ b = b_{1})

expclosure : axiom ∀ b, b_{1}, l, l_{1}, s : On(b_{1}, l_{1}, result(move(b, l), s)) ⇔ (b ≠ b_{1} ∧ On(b_{1}, l_{1}, s))∨

(b = b_{1}∧

l = l_{1}∧

top(b) ≠ l∧

Clear(top(b), s)∧ Clear(l, s))∨

(((¬Clear(top(b), s) ∨ (¬Clear(l, s)))∨

(l ≠ l_{1} ∧ b ≠ b_{1})∨ top(b) = l)∧

On(b_{1}, l_{1}, s))

expclear : theorem ∀ l, b, l_{1}, s : Clear(l, result(move(b, l), s)) ⇔ (l = table2)∨

(l ≠ l_{1} ∧ Clear(l, s))∨

(On(b, l, s)∧ Clear(top(b), s)∧ Clear(l_{1}, s)∧ top(b) ≠ l_{1})∨

(l = l_{1}∧

(¬Clear(top(b), s)∨ l_{1} = top(b)))

disjoint : theorem ∀ b, b_{1} : b ≠ b_{1} ⊃ (∀ b_{2} : (¬Bset(b, b_{2})) ∨ (¬Bset(b_{1}, b_{2})))

finite : theorem ∀ b : I(b) ⊃ Finite(λ b_{1} : Bset(b, b_{1}))

union : theorem ∀ b : ∃ b_{1} : Bset(b_{1}, b)

lessisrel : theorem ∀ b, b_{1}, b_{2} : Less(b, b_{1}, b_{2}) ⊃ Bset(b, b_{1}) ∧ Bset(b, b_{2})

transitivity : theorem ∀ b, b_{1}, b_{2}, b_{3} : Less(b, b_{1}, b_{2}) ∧ Less(b, b_{2}, b_{3}) ⊃ Less(b, b_{1}, b_{3})

antisymmetry : theorem ∀ b, b_{1} : ¬(Less(b, b_{1}, b_{2}) ∧ Less(b, b_{2}, b_{1}))

totality : theorem ∀ b, b_{1}, b_{2} : Bset(b, b_{1}) ∧ Bset(b, b_{2}) ⊃ (Less(b, b_{1}, b_{2}) ∨ Less(b, b_{2}, b_{1}))

Testone : theorem On(1, top(2), S_{0}) ∧ Clear(top(1), S_{0}) ⊃ On(1, table2, result(move(1, table2), S_{0}))∧

Clear(top(2), result(move(1, table2), S_{0}))

end blocks