- move_left_conj
-
|- ∀p q m.
(p ∧ stmarker m ⇔ stmarker m ∧ p) ∧
((stmarker m ∧ p) ∧ q ⇔ stmarker m ∧ p ∧ q) ∧
(p ∧ stmarker m ∧ q ⇔ stmarker m ∧ p ∧ q)
- move_right_conj
-
|- ∀p q m.
(stmarker m ∧ p ⇔ p ∧ stmarker m) ∧
(p ∧ q ∧ stmarker m ⇔ (p ∧ q) ∧ stmarker m) ∧
((p ∧ stmarker m) ∧ q ⇔ (p ∧ q) ∧ stmarker m)
- move_left_disj
-
|- ∀p q m.
(p ∨ stmarker m ⇔ stmarker m ∨ p) ∧
((stmarker m ∨ p) ∨ q ⇔ stmarker m ∨ p ∨ q) ∧
(p ∨ stmarker m ∨ q ⇔ stmarker m ∨ p ∨ q)
- move_right_disj
-
|- ∀p q m.
(stmarker m ∨ p ⇔ p ∨ stmarker m) ∧
(p ∨ q ∨ stmarker m ⇔ (p ∨ q) ∨ stmarker m) ∧
((p ∨ stmarker m) ∨ q ⇔ (p ∨ q) ∨ stmarker m)