Theory TypeSystemAuxiliary

chapter ‹Generated by Lem from ‹semantics/typeSystem.lem›.›

theory "TypeSystemAuxiliary" 

imports
  Main
  "HOL-Library.Datatype_Records"
  "LEM.Lem_pervasives_extra"
  "Lib"
  "Namespace"
  "Ast"
  "SemanticPrimitives"
  "TypeSystem"

begin 


― ‹‹**************************************************››
― ‹‹                                                  ››
― ‹‹ Termination Proofs                               ››
― ‹‹                                                  ››
― ‹‹**************************************************››

termination check_freevars by lexicographic_order

termination type_subst by lexicographic_order

termination deBruijn_inc by lexicographic_order

termination deBruijn_subst by lexicographic_order

termination check_type_names by lexicographic_order

termination type_name_subst by lexicographic_order

termination is_value by lexicographic_order



end