PrintForm Definitions mb automata 2 Sections GenAutomata Doc

At: term mng2 unprime


t:Term, e,s,s',a,tr:Top. [[unprime(t)]] e s s' a tr ~ [[t]] e s a tr

By:
Analyze 0
THEN
All (Unfolds [`term_mng`;`term_mng2`;`unprime`])
THEN
TermInd 1
THEN
Reduce 0
THEN
Try (Complete Auto)
THEN
All (Folds [`term_mng`;`term_mng2`;`unprime`])
THEN
Try (UnivCD THEN Analyze THEN BackThruSomeHyp)


Generated subgoals:

None

About:
sqequaltopall

PrintForm Definitions mb automata 2 Sections GenAutomata Doc