Theory SemanticPrimitivesAuxiliary

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

theory "SemanticPrimitivesAuxiliary" 

imports
  Main
  "HOL-Library.Datatype_Records"
  "LEM.Lem_pervasives"
  "LEM.Lem_list_extra"
  "LEM.Lem_string"
  "Lib"
  "Namespace"
  "Ast"
  "Ffi"
  "FpSem"
  "LEM.Lem_string_extra"
  "SemanticPrimitives"

begin 


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

termination pmatch by lexicographic_order

termination do_eq by lexicographic_order

termination v_to_list by lexicographic_order

termination v_to_char_list by lexicographic_order

termination vs_to_string by lexicographic_order



end