2.1 Basic ITL Theorems

   AndChopA
   AndChopB
   NextChop
   BiChopImpChop
   BoxChopImpChop
   LeftChopImpChop
   RightChopImpChop
   RightChopEqvChop
   ChopOrEqv
   OrChopImpRule
   OrChopEqvRule
   NextImpNext
   NextImpDist
   ChopImpDiamond
   NowImpDiamond
   NextDiamondImpDiamond
   BoxImpNowAndWeakNext
   BoxImpBoxRule
   BoxImpDist
   DiamondEmpty
   BiImpDiImpDi
   DiImpDi
   BiImpBiRule
   LeftChopEqvChop
   DiEqvDi
   BiEqvBi
   LeftChopChopImpChopRule
   AndChopCommute
   StateAndChopImpChopRule
   StateImpChopEqvChop
   ChopEqvStateAndChop
   DiIntro
   BiElim
   BiContraPosImpDist
   BiImpDist
   OrChopEqv
   IfChopEqvRule
   ChopOrImpRule
   ChopOrEqvRule
   EmptyOrChopEqv
   EmptyOrNextChopEqv
   EmptyOrChopImpRule
   EmptyOrChopEqvRule
   EmptyOrNextChopImpRule
   EmptyOrNextChopEqvRule
   ChopEmptyOrImpRule
   BoxStateChopBoxEqvBox
   NotBoxStateImpBoxYieldsNotBox
   BoxStateAndChopEqvChop
   StateEqvBi
   DiNotEqvNotBi
   DiEqvNotBiNot
   BoxAndChopImport
   ChopAndBoxImport
   AndChopAndCommute
   ChopImpChop
   ChopEqvChop
   MultChopImpChop
   BoxChopImpChopBox
   NotChopEqvYieldsNot
   DiamondImpTrueChop
   BiAndChopImport

2023-09-12
Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2023