PrintForm Definitions mb automata 1 Sections GenAutomata Doc

At: assert ts eq

a,b:ts(). (a=b) a = b
By: let DT i If (p.is_term `union` (clause_type i p)) ((Analyze i) THEN (Reduce 0)) Id in (Unfold `ts` 0) THEN UnivCD THEN (Unfold `ts_eq` 0) THEN (Unfold `ts_case` 0) THEN (Repeat (DT 1)) THEN (Repeat (DT 2)) THEN (Try EqLblFwd) THEN (Try ((Repeat Analyze) THEN (Complete Auto))) THEN (Try (SimpHyp -1)) THEN (Try ((HypSubstSq -1 0) THEN (EqLblReflexive 0)))
Generated subgoals:

None

About:
assertequalall

PrintForm Definitions mb automata 1 Sections GenAutomata Doc