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
  2.2 Further properties of Diamond-i and Box-i
   ImpDi
   NotDiFalse
   DiState
   StateChop
   StateChopExportA
   StateAndChopImport
   StateAndChop
   StateAndEmptyChop
   StateAndNextChop
   NextStateAndChop
   StateYieldsEqv
   StateAndDi
   DiNext
   DiNextState
   StateImpBiGen
   ChopAndNotChopImp
   ChopAndYieldsImp
   ChopAndYieldsMP
   OrYieldsImp
   LeftYieldsImpYields
   LeftYieldsEqvYields
   StateImpYields
   StateAndYieldsImpYields
   AndYieldsA
   AndYieldsB
   RightYieldsImpYields
   RightYieldsEqvYields
   BoxImpYields
   BoxEqvTrueYields
   YieldsGen
   YieldsAndYieldsEqvYieldsAnd
   YieldsAndYieldsImpAndYieldsAnd
   YieldsYieldsEqvChopYields
   EmptyYields
   NextYields
   SkipChopEqvNext
   SkipYieldsEqvWeakNext
   NextImpSkipYields
   MoreEqvSkipChopTrue
   MoreChopImpMore
   ChopMoreImpMore
   MoreChopEqvNextDiamond
   NotEqvYieldsMore
   LeftChopImpMoreRule
   RightChopImpMoreRule
   NotDiEqvBiNot
   ChopImpDi
   TrueEqvTrueChopTrue
   DiEqvDiDi
   BiEqvBiBi
   DiOrEqv
   DiAndA
   DiAndB
   DiAndImpAnd
   DiSkipEqvMore
   DiMoreEqvMore
   DiIfEqvRule
   DiEmpty
  2.3 Properties of Diamond-a and Box-a
   DaEqvDtDi
   DaEqvDiDt
   DtDiEqvDiDt
   BaEqvBiBt
   BaEqvBtBi
   BtBiEqvBiBt
   DaNotEqvNotBa
   DaEqvNotBaNot
   BaElim
   DaIntro
   BaImpBt
   BaImpBi
   BaGen
   BaImpDist
   DaEqvDaDa
   BaEqvBaBa
   BaLeftChopImpChop
   BaRightChopImpChop
   BaAndChopImport
   ChopAndBaImport
   BaChopImpChopBa
   BoxStateEqvBaBoxState
   DiNotBaImpNotBa
   NotBaChopImpNotBa
  2.4 Properties of Fin
   AndFinEqvChopStateAndEmpty
   FinChopEqvOr
   FinChopEqvDiamond
   FinYields
   AndFinChopEqvStateAndChop
   DiAndFinEqvChopState
   BiImpFinEqvYieldsState
   ChopFinImpFin
   FinImpYieldsFin
   ChopAndFin
   ChopAndNotFin
   FinChopChain
   ChopRule
   ChopRep
   ChopRepAndFin
   MoreChopLoop
   MoreChopContra
   ChopLoop
   ChopContra
  2.5 Properties of chop-plus
   ImpChopPlus
   ChopChopPlusImpChopPlus
   ChopPlusEqvOrChopChopPlus
   ChopPlusIntro
   ChopPlusElim
   ChopPlusElimWithoutMore
   ChopPlusImpChopPlus
   ChopPlusEqvChopPlus
  2.6 Properties of chop-star
   CSEqv
   EmptyImpCS
   ChopPlusImpCS
   ImpCS
   CSChopEqvOrChopPlusChop
   CSEqvOrChopCS
   ChopCSImpCS
   CSAndMoreImpChopPlus
   CSAndMoreEqvAndMoreChop
   CSAndMoreImpChopCS
   CSAndMoreImpCSChop
   CSMoreNotImpChopCSAndMore
   CSChopCSImpCS
   CSChopImpCS
   CSCSImpCS
   CSImpCS
   CSEqvCS
   AndCSA
   AndCSB
   CSIntro
   CSElim
   CSElimWithoutMore
   CSChopEqvChopOrRule
   CSChopIntroRule
   CSImpBox
   BoxCSEqvBox
   BoxStateAndCSEqvCS
   BaCSImpCS
   BaCSEqvCS
   BaAndCSImport
  2.7 Properties of While
   WhileEqvIf
   WhileChopEqvIf
   WhileChopEqvIfRule
   WhileImpFin
   WhileEqvEmptyOrChopWhile
   WhileIntro
   WhileElim
   BaWhileImpWhile
   WhileImpWhile
  2.8 Properties of Halt
   HaltChopEqv
   AndHaltChopImp
   NotAndHaltChopImpNext
   NotAndHaltChopImpSkipYields
   HaltChopImpNotHaltChopNot
   HaltChopImpHaltYields
   HaltChopAnd
   HaltAndChopAndHaltChopImpHaltAndChopAnd
   HaltImpBoxYields
  2.9 Properties of groups of chops
   ChopGroupMerge
   ChopGroupGroupMerge
   ChopGroupImpCS
   MultChopImpCS
   NestedChopImpChop
   MultNestedChopImpChop