Theory Congruence_Classify

theory Congruence_Classify
  imports
    Congruence_Exec
begin

section ‹Deciding a check from a map of residue classes›

text ‹
  The check classifier is derived from Congruence's bundle: the Boolean recursion
  over \<^typ>‹exp› (‹Not›, ‹And›, ‹Or›), the three-way classification, and the
  node-indexed bridge to \<^const>‹checks_proven› come from the comparison tables
  \<^const>‹congruence_lt›/\<^const>‹congruence_eqb› and the evaluator, through the
  ‹congruence_tf› interpretation in
  \<^theory>‹Voblint_Analysis_Congruence.Congruence_Transfer›. Their facts stay under
  ‹congruence_tf.check.›; ‹Congruence_Regression› exercises them.
›

end