module A201605.Everything where


--------------------------------------------------------------------------------

-- original version, plus unfinished attempt at adding products and coproducts

open import A201605.AbelChapman
open import A201605.AbelChapmanPlus
open import A201605.Experiments


--------------------------------------------------------------------------------

-- common

open import A201605.AbelChapmanExtended.Delay
open import A201605.AbelChapmanExtended.StrongBisimilarity
open import A201605.AbelChapmanExtended.Convergence


--------------------------------------------------------------------------------

-- added products and empty type only

open import A201605.AbelChapmanExtended.Syntax
open import A201605.AbelChapmanExtended.OPE
open import A201605.AbelChapmanExtended.Renaming.Syntax
open import A201605.AbelChapmanExtended.Renaming.OPE
open import A201605.AbelChapmanExtended.Normalization
open import A201605.AbelChapmanExtended.Renaming.Normalization1
open import A201605.AbelChapmanExtended.Renaming.Normalization2
open import A201605.AbelChapmanExtended.Renaming.Convergence
open import A201605.AbelChapmanExtended.Semantics
open import A201605.AbelChapmanExtended.Renaming.Semantics
open import A201605.AbelChapmanExtended.Reflection
open import A201605.AbelChapmanExtended.Termination
open import A201605.AbelChapmanExtended.Examples


--------------------------------------------------------------------------------

-- added products and coproducts

open import A201605.AbelChapmanExtended2.Syntax
open import A201605.AbelChapmanExtended2.OPE
open import A201605.AbelChapmanExtended2.Renaming
open import A201605.AbelChapmanExtended2.Normalization
open import A201605.AbelChapmanExtended2.Semantics
open import A201605.AbelChapmanExtended2.RenamingLemmas.OPE
open import A201605.AbelChapmanExtended2.RenamingLemmas.Normalization1
open import A201605.AbelChapmanExtended2.RenamingLemmas.Normalization2
open import A201605.AbelChapmanExtended2.RenamingLemmas.Convergence
open import A201605.AbelChapmanExtended2.RenamingLemmas.Semantics
open import A201605.AbelChapmanExtended2.Reflection
open import A201605.AbelChapmanExtended2.Termination
open import A201605.AbelChapmanExtended2.Examples


--------------------------------------------------------------------------------

-- experiments

open import A201605.TowardsAltArtemov.SyntaxCatholic
open import A201605.TowardsAltArtemov.SyntaxSimple
open import A201605.TowardsAltArtemov.SyntaxSimpleCatholic
open import A201605.TowardsAltArtemov.SyntaxSimpleCatholicRadical
open import A201605.TowardsAltArtemov.NormalizationCatholic
open import A201605.TowardsAltArtemov.NormalizationSimple
open import A201605.TowardsAltArtemov.NormalizationSimpleCatholic


--------------------------------------------------------------------------------

-- TODO: separate

open import A201605.AltArtemov.Everything


--------------------------------------------------------------------------------