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

At: assert term eq

a,b:Term. term_eq(a;b) a = b
By:
Unfold `term` 0
THEN
Analyze 0
THEN
TreeInd -1
THEN
Analyze 0
THEN
TreeInd -1
THEN
RecUnfold `term_eq` 0
THEN
Reduce 0
Generated subgoals:

11. 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. x: ts()
5. b: Tree(ts())
6. u1: Tree(ts())Type{i'}
7. w1: b:{v:Tree(ts())| u1(v) }term_eq(tree_leaf(x);b) tree_leaf(x) = b Tree(ts())
8. x1: ts()
(x=x1) tree_leaf(x) = tree_leaf(x1) Tree(ts())
21. 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. x: ts()
5. b: Tree(ts())
6. u1: Tree(ts())Type{i'}
7. w1: b:{v:Tree(ts())| u1(v) }term_eq(tree_leaf(x);b) tree_leaf(x) = b Tree(ts())
8. y1: {v:Tree(ts())| u1(v) }
9. y2: {v:Tree(ts())| u1(v) }
False tree_leaf(x) = tree_node( < y1, y2 > )
31. 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. x: ts()
False tree_node( < y1, y2 > ) = tree_leaf(x)
41. 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 > )

About:
assertequalfalseall

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