SRULE : inference rule

Miscellaneous Rules

• hyp
• lemma
• same

Propositional Rules

• assoc-left
• cases
• cases3
• cases4
• deduct
• disj-imp
• disj-imp-l
• disj-imp-r
• econj
• equiv-implics
• iconj
• idisj-left
• idisj-right
• imp-disj
• imp-disj-l
• imp-disj-r
• implics-equiv
• indirect
• indirect1
• indirect2
• mp
• rulec1
• subst-equiv

Negation Rules

• absurd
• eneg
• ineg
• pullneg
• pushneg

Quantifier Rules

• ab*
• abe
• abu
• egen
• rulec
• ugen
• ui

Substitution Rules

• substitute

Equality Rules

• equiv-eq
• equiv-eq-contr
• equiv-eq-contr*
• equiv-eq-expd
• equiv-eq-expd*
• ext=
• ext=0
• let
• subst=
• subst=l
• subst=r
• sym=

Definition Rules

• edef
• equiv-wffs
• idef

Lambda Conversion Rules

• beta*
• eta*
• lambda*
• lcontr*
• lcontr*-beta
• lcontr*-eta
• lexpd*
• lexpd*-beta
• lexpd*-eta

ETPS documentation homepage

TPS homepage