PrintForm
Definitions
mb
automata
1
Sections
GenAutomata
Doc
At:
ts
eq
wf
a,b:ts(). (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 (Unfold `ts_eq` 0) THEN (Unfold `ts_case` 0) THEN (Repeat (DT 1)) THEN (Repeat (DT 2))
Generated subgoals:
None
About:
PrintForm
Definitions
mb
automata
1
Sections
GenAutomata
Doc
a,b:ts(). (a=b) 
If (
p.is_term `union` (clause_type i p)) ((Analyze i) THEN (Reduce 0)) Id in
(Unfold `ts` 0) THEN (Unfold `ts_eq` 0) THEN (Unfold `ts_case` 0) THEN (Repeat (DT 1))
THEN
(Repeat (DT 2))