Theory "marker"

Parents     bool

Signature

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

Definitions

AC_DEF 
⊢ ∀b1 b2. AC b1 b2 ⇔ b1 ∧ b2
Abbrev_def 
⊢ ∀x. Abbrev x ⇔ x
Case_def 
⊢ ∀X. Case X ⇔ T
Cong_def 
⊢ ∀x. Cong x ⇔ x
Exclude_def 
⊢ ∀x. Exclude x ⇔ T
IfCases_def 
⊢ IfCases ⇔ T
Req0_def 
⊢ Req0 ⇔ T
ReqD_def 
⊢ ReqD ⇔ T
label_def 
⊢ ∀lab argument. (lab :- argument) ⇔ argument
stmarker_def 
⊢ ∀x. stmarker x = x
unint_def 
⊢ ∀x. unint x = x
usingThm_def 
⊢ ∀b. marker$usingThm b ⇔ b
using_def 
⊢ ∀x. marker$using x ⇔ T

Theorems

Abbrev_CONG 
⊢ (r1 = r2) ⇒ (Abbrev (v = r1) ⇔ Abbrev (v = r2))
add_Case 
⊢ ∀X. P ⇔ Case X ⇒ P
elim_Case 
⊢ (Case X ∧ Y ⇔ Y) ∧ (Y ∧ Case X ⇔ Y) ∧ (Case X ⇒ Y ⇔ Y)
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_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_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_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)