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

At: assert term eq 4
1. a: Tree(ts())
2. u: Tree(ts())Type{i'}
3. w: a:{v:Tree(ts())| u(v) }b:Tree(ts()). term_eq(a;b) a = b
4. y1: {v:Tree(ts())| u(v) }
5. y2: {v:Tree(ts())| u(v) }
6. b: Tree(ts())
7. u1: Tree(ts())Type{i'}
8. w1: b:{v:Tree(ts())| u1(v) }term_eq(tree_node( < y1, y2 > );b) tree_node( < y1, y2 > ) = b
9. y3: {v:Tree(ts())| u1(v) }
10. y4: {v:Tree(ts())| u1(v) }

(term_eq(y1;y3)term_eq(y2;y4)) tree_node( < y1, y2 > ) = tree_node( < y3, y4 > )
By: All (Fold `term`)
Generated subgoals:

11. a: Term
2. u: TermType{i'}
3. w: a:{v:Term| u(v) }b:Term. term_eq(a;b) a = b
4. y1: {v:Term| u(v) }
5. y2: {v:Term| u(v) }
6. b: Term
7. u1: TermType{i'}
8. w1: b:{v:Term| u1(v) }term_eq(tree_node( < y1, y2 > );b) tree_node( < y1, y2 > ) = b Term
9. y3: {v:Term| u1(v) }
10. y4: {v:Term| u1(v) }
11. term_eq(y1;y3)term_eq(y2;y4)
tree_node( < y1, y2 > ) = tree_node( < y3, y4 > ) Term
21. a: Term
2. u: TermType{i'}
3. w: a:{v:Term| u(v) }b:Term. term_eq(a;b) a = b
4. y1: {v:Term| u(v) }
5. y2: {v:Term| u(v) }
6. b: Term
7. u1: TermType{i'}
8. w1: b:{v:Term| u1(v) }term_eq(tree_node( < y1, y2 > );b) tree_node( < y1, y2 > ) = b Term
9. y3: {v:Term| u1(v) }
10. y4: {v:Term| u1(v) }
11. tree_node( < y1, y2 > ) = tree_node( < y3, y4 > ) Term
term_eq(y1;y3)term_eq(y2;y4)
31. a: Term
2. u: TermType{i'}
3. w: a:{v:Term| u(v) }b:Term. term_eq(a;b) a = b
4. y1: {v:Term| u(v) }
5. y2: {v:Term| u(v) }
6. b: Term
7. u1: TermType{i'}
8. w1: b:{v:Term| u1(v) }term_eq(tree_node( < y1, y2 > );b) tree_node( < y1, y2 > ) = b Term
9. y3: {v:Term| u1(v) }
10. y4: {v:Term| u1(v) }
tree_node( < y1, y2 > ) Term
41. a: Term
2. u: TermType{i'}
3. w: a:{v:Term| u(v) }b:Term. term_eq(a;b) a = b
4. y1: {v:Term| u(v) }
5. y2: {v:Term| u(v) }
6. b: Term
7. u1: TermType{i'}
8. w1: b:{v:Term| u1(v) }term_eq(tree_node( < y1, y2 > );b) tree_node( < y1, y2 > ) = b Term
9. y3: {v:Term| u1(v) }
10. y4: {v:Term| u1(v) }
tree_node( < y3, y4 > ) Term

About:
assertsetapplyfunctionuniverseequalmemberall

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