Theory "marker"

Parents bool

Signature

Constant	Type
:-	:ind -> bool -> bool
AC	:bool -> bool -> bool
Abbrev	:bool -> bool
Cong	:bool -> bool
Exclude	:α -> bool
IfCases	:bool
Req0	:bool
ReqD	:bool
stmarker	:α -> α
unint	:α -> α

Definitions

unint_def

⊢ ∀x. unint x = x

stmarker_def

⊢ ∀x. stmarker x = x

ReqD_def

⊢ ReqD ⇔ T

Req0_def

⊢ Req0 ⇔ T

label_def

⊢ ∀lab argument. (lab :- argument) ⇔ argument

IfCases_def

⊢ IfCases ⇔ T

Exclude_def

⊢ ∀x. Exclude x ⇔ T

Cong_def

⊢ ∀x. Cong x ⇔ x

AC_DEF

⊢ ∀b1 b2. AC b1 b2 ⇔ b1 ∧ b2

Abbrev_def

⊢ ∀x. Abbrev x ⇔ x

Theorems

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)

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_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)