(9steps) PrintForm Definitions Lemmas mb automata 1 Sections GenAutomata Doc

At: assert st eq 2 1
1. s1: SimpleType
2. s2: SimpleType
3. s1 = s2

st_eq(s2;s2)
By:
Unfold `st` 2
THEN
TreeInd 2
THEN
RecUnfold `st_eq` 0
THEN
Reduce 0
THEN
Try ((Analyze -1) THEN (Reduce 0) THEN (BackThru Thm* l:Pattern. l = l))
THEN
All (Fold `st`)
THEN
RW assert_pushdownC 0
THEN
SmAuto
Generated subgoals:

None

About:
assertequal

(9steps) PrintForm Definitions Lemmas mb automata 1 Sections GenAutomata Doc