(6steps) PrintForm Definitions mb automata 2 Sections GenAutomata Doc

At: member st app1 2
1. s1: Tree(Label+Unit)
2. s2: SimpleType
3. s: SimpleType
4. u: Tree(Label+Unit)Type{i'}
5. w: s1:{v:Tree(Label+Unit)| u(v) }s st_app1(s1;s2) st_eq(s1;s2s)
6. y1: {v:Tree(Label+Unit)| u(v) }
7. y2: {v:Tree(Label+Unit)| u(v) }

s if st_eq(y1;s2) < y2 > else < > fi st_eq(tree_node( < y1, y2 > );tree_node( < s2, s > ))
By:
All (Fold `st`)
THEN
SplitOnConclITE
Generated subgoals:

11. s1: SimpleType
2. s2: SimpleType
3. s: SimpleType
4. u: SimpleTypeType{i'}
5. w: s1:{v:SimpleType| u(v) }s st_app1(s1;s2) st_eq(s1;s2s)
6. y1: {v:SimpleType| u(v) }
7. y2: {v:SimpleType| u(v) }
8. st_eq(y1;s2)
s < y2 > st_eq(tree_node( < y1, y2 > );tree_node( < s2, s > ))
21. s1: SimpleType
2. s2: SimpleType
3. s: SimpleType
4. u: SimpleTypeType{i'}
5. w: s1:{v:SimpleType| u(v) }s st_app1(s1;s2) st_eq(s1;s2s)
6. y1: {v:SimpleType| u(v) }
7. y2: {v:SimpleType| u(v) }
8. st_eq(y1;s2)
s < > st_eq(tree_node( < y1, y2 > );tree_node( < s2, s > ))

About:
ifthenelseassertunitunionsetapplyfunctionuniverse

(6steps) PrintForm Definitions mb automata 2 Sections GenAutomata Doc