PrintForm Definitions mb automata 1 Sections GenAutomata Doc

At: st eq wf

s1,s2:SimpleType. st_eq(s1;s2)
By:
Unfold `st` 0
THEN
RepeatFor 2 ((Analyze 0) THEN (TreeInd -1))
THEN
All (Fold `st`)
THEN
RecUnfold `st_eq` 0
THEN
Reduce 0
THEN
SmAuto
THEN
Analyze 4
THEN
Analyze 8
THEN
Reduce 0
Generated subgoals:

None

About:
boolmemberall

PrintForm Definitions mb automata 1 Sections GenAutomata Doc