Theory "marker"

Parents bool

Signature

Constant	Type
unint	:'a -> 'a
stmarker	:'a -> 'a
IfCases	:bool
Cong	:bool -> bool
Abbrev	:bool -> bool
AC	:bool -> bool -> bool

Definitions

stmarker_def

|- !x. stmarker x = x

unint_def

|- !x. unint x = x

Abbrev_def

|- !x. Abbrev x = x

IfCases_def

|- IfCases = T

AC_DEF

|- !b1 b2. AC b1 b2 = b1 /\ b2

Cong_def

|- !x. Cong x = x

Theorems

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)