Library AutoIndTac

Library Base

• Base Library for ICL
• De Morgan laws
• Size recursion
• Iteration
• Decidability
• Lists
• Decidability laws for lists
• Membership
• Disjointness
• Inclusion
• Setoid rewriting with list inclusion and list equivalence
• Equivalence
• Filter
• Element removal
• Cardinality
• Duplicate-free lists
• Power lists
• Finite closure iteration
• Deprecated names, defined for backward compatibilitly

Library CFP

• Syntax of Context-Free Programs
• Null Program and Iteration
  • Functional extensionality for substitutions
  • Decidability of syntactic equivalence
  • Notions for substitutions

Library Congruence

• Congruence for recursion
• Congruence for sequential composition and choice
  • Registration of program equivalence as congruence relation for rewriting

Library DirectLinearizer

• Traces of tail-recursive programs under substitution
  • Construction of traces of tail-recursive programs under substitution
  • Deconstruction of traces of tail-recursive programs under substition
• Linearizer
• Correctness of the linearizer
  • Preservation of tail recursion
  • Establishment of linearity
  • Trace construction of linearized programs
  • Trace deconstruction of linearized programs
  • Correctness

Library DistributeFix

• Unfolding properties of decomposed recursions
• Distributivity of decomposed recursions
• Transformation from decomposed recursions to iterations

Library Equivalences

• Equivalences from Kleene algebras
  • Unfolding
• No right annulation of the null program

Library FreeVariables

• Predicate for free variables
• Properties of bound
• Correspondence of bound and boundT

Library IMP

• Axiomatization
• Abstract IMP
• Big-step semantics
• Context-free abstractions
  • Inversion lemmas for cfa
• Tail recursion of context-free abstractions
• Execution of traces on states
• Correspondance of IMP and CFP

Library Linearity

• Linear tail recursion for context-free programs
• Properties of lin

Library RegLinearizer

• Linearizer for regular programs
• Correctness of the linearizer

Library Regularity

• Regularity for context-free programs
• Properties of reg
• Alternative characterization of regularity
• Correspondence of reg and regi

Library Regularizer

• Decomposer
• Correctness of the decomposer
• Regularizer
• Correctness of the regularizer

Library Substitutivity

• Inversion lemmas for substitution
• Altenative trace predicate for programs under substitution
• Correctness of TCsubst
• Trace substitution
• Correctness of trace substitution
• Substitutivity of the trace semantics

Library TailRecursion

• Tail recursion for context-free programs
• Properties of tailrec
• Characterization of the traces of tail-recursive programs
• Alternative characterization of tail recursion not using bound
• Properties of trec
• Correspondence of trec and tailrec

Library TraceSemantics

• Trace semantics for context-free programs
• Equivalence based on trace semantics
• Properties of trace semantics
  • Prefix closedness
  • Correspondence of program renaming and trace renaming
• Properties of the null program

Library Traces

• Definition of Traces
• Total and partial traces
• Trace concatenation
• Inversion Lemmas for trace concatenation
• Properties of concat
• Removing the last element of a trace
• Properties of butLast
• Renaming traces
• Properties of ren_trace
• Free variables of traces
• Properties of boundT
• Characterization of trace endings
• Properties of terminal
• Characterization of tail recursion for traces
• Properties of tailrec_trace

Library Unfolding

• Unfolding operator
• Properties of unfold
• Characterization of the traces of recursions using unfold

Library Util