1 | 1. the_graph: Graph 2. the_obj: GraphObject(the_graph) 3. P: Vertices(the_graph) traversal(the_graph) traversal(the_graph) Prop 4. s: traversal(the_graph) 5. i: Vertices(the_graph) 6. s:traversal(the_graph), i:Vertices(the_graph). (inl(i) s) (inr(i) s)  P(i,s,nil) 7. s1,s2,s3:traversal(the_graph), i,j:Vertices(the_graph).
i-the_graph- > j

paren(Vertices(the_graph);s2)

paren(Vertices(the_graph);s3)  P(j,s1,s2)  P(i,s2 @ s1,s3)  P(i,s1,s3 @ s2) 8. s1,s2:traversal(the_graph), i:Vertices(the_graph).
(inl(i) s1)  (inr(i) s1)  P(i,[inr(i) / s1],s2)  P(i,s1,[inl(i) / (s2 @ [inr(i)])]) 9. x,y:Vertices(the_graph). the_obj.eq(x,y)  x = y 10. T:Type, s:T, x:Vertices(the_graph), f:(T Vertices(the_graph) T).
L:Vertices(the_graph) List.
( y:Vertices(the_graph). x-the_graph- > y  (y L))
& the_obj.eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L) 11. T:Type, s:T, f:(T Vertices(the_graph) T).
L:Vertices(the_graph) List.
no_repeats(Vertices(the_graph);L)
& ( y:Vertices(the_graph). (y L))
& the_obj.vacc(f,s) = list_accum(s',x'.f(s',x');s;L) 12. s1: traversal(the_graph) 13. i1: Vertices(the_graph) 14. (inl(i1) s1) (inr(i1) s1) l_disjoint(Vertices(the_graph)+Vertices(the_graph);nil;s1) | 1 step |
  |
2 | 1. the_graph: Graph 2. the_obj: GraphObject(the_graph) 3. P: Vertices(the_graph) traversal(the_graph) traversal(the_graph) Prop 4. s: traversal(the_graph) 5. i: Vertices(the_graph) 6. s:traversal(the_graph), i:Vertices(the_graph). (inl(i) s) (inr(i) s)  P(i,s,nil) 7. s1,s2,s3:traversal(the_graph), i,j:Vertices(the_graph).
i-the_graph- > j

paren(Vertices(the_graph);s2)

paren(Vertices(the_graph);s3)  P(j,s1,s2)  P(i,s2 @ s1,s3)  P(i,s1,s3 @ s2) 8. s1,s2:traversal(the_graph), i:Vertices(the_graph).
(inl(i) s1)  (inr(i) s1)  P(i,[inr(i) / s1],s2)  P(i,s1,[inl(i) / (s2 @ [inr(i)])]) 9. x,y:Vertices(the_graph). the_obj.eq(x,y)  x = y 10. T:Type, s:T, x:Vertices(the_graph), f:(T Vertices(the_graph) T).
L:Vertices(the_graph) List.
( y:Vertices(the_graph). x-the_graph- > y  (y L))
& the_obj.eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L) 11. T:Type, s:T, f:(T Vertices(the_graph) T).
L:Vertices(the_graph) List.
no_repeats(Vertices(the_graph);L)
& ( y:Vertices(the_graph). (y L))
& the_obj.vacc(f,s) = list_accum(s',x'.f(s',x');s;L) 12. s1: traversal(the_graph) 13. i1: Vertices(the_graph) 14. (inl(i1) s1) (inr(i1) s1) no_repeats(Vertices(the_graph)+Vertices(the_graph);nil) | 1 step |
  |
3 | 1. the_graph: Graph 2. the_obj: GraphObject(the_graph) 3. P: Vertices(the_graph) traversal(the_graph) traversal(the_graph) Prop 4. s: traversal(the_graph) 5. i: Vertices(the_graph) 6. s:traversal(the_graph), i:Vertices(the_graph). (inl(i) s) (inr(i) s)  P(i,s,nil) 7. s1,s2,s3:traversal(the_graph), i,j:Vertices(the_graph).
i-the_graph- > j

paren(Vertices(the_graph);s2)

paren(Vertices(the_graph);s3)  P(j,s1,s2)  P(i,s2 @ s1,s3)  P(i,s1,s3 @ s2) 8. s1,s2:traversal(the_graph), i:Vertices(the_graph).
(inl(i) s1)  (inr(i) s1)  P(i,[inr(i) / s1],s2)  P(i,s1,[inl(i) / (s2 @ [inr(i)])]) 9. x,y:Vertices(the_graph). the_obj.eq(x,y)  x = y 10. T:Type, s:T, x:Vertices(the_graph), f:(T Vertices(the_graph) T).
L:Vertices(the_graph) List.
( y:Vertices(the_graph). x-the_graph- > y  (y L))
& the_obj.eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L) 11. T:Type, s:T, f:(T Vertices(the_graph) T).
L:Vertices(the_graph) List.
no_repeats(Vertices(the_graph);L)
& ( y:Vertices(the_graph). (y L))
& the_obj.vacc(f,s) = list_accum(s',x'.f(s',x');s;L) 12. s1: traversal(the_graph) 13. i1: Vertices(the_graph) 14. (inl(i1) s1) (inr(i1) s1) paren(Vertices(the_graph);nil) | 1 step |
  |
4 | 1. the_graph: Graph 2. the_obj: GraphObject(the_graph) 3. P: Vertices(the_graph) traversal(the_graph) traversal(the_graph) Prop 4. s: traversal(the_graph) 5. i: Vertices(the_graph) 6. s:traversal(the_graph), i:Vertices(the_graph). (inl(i) s) (inr(i) s)  P(i,s,nil) 7. s1,s2,s3:traversal(the_graph), i,j:Vertices(the_graph).
i-the_graph- > j

paren(Vertices(the_graph);s2)

paren(Vertices(the_graph);s3)  P(j,s1,s2)  P(i,s2 @ s1,s3)  P(i,s1,s3 @ s2) 8. s1,s2:traversal(the_graph), i:Vertices(the_graph).
(inl(i) s1)  (inr(i) s1)  P(i,[inr(i) / s1],s2)  P(i,s1,[inl(i) / (s2 @ [inr(i)])]) 9. x,y:Vertices(the_graph). the_obj.eq(x,y)  x = y 10. T:Type, s:T, x:Vertices(the_graph), f:(T Vertices(the_graph) T).
L:Vertices(the_graph) List.
( y:Vertices(the_graph). x-the_graph- > y  (y L))
& the_obj.eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L) 11. T:Type, s:T, f:(T Vertices(the_graph) T).
L:Vertices(the_graph) List.
no_repeats(Vertices(the_graph);L)
& ( y:Vertices(the_graph). (y L))
& the_obj.vacc(f,s) = list_accum(s',x'.f(s',x');s;L) 12. s1: traversal(the_graph) 13. s2: traversal(the_graph) 14. s3: traversal(the_graph) 15. i1: Vertices(the_graph) 16. j: Vertices(the_graph) 17. i1-the_graph- > j 18. P(j,s1,s2) 19. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1) 20. no_repeats(Vertices(the_graph)+Vertices(the_graph);s2) 21. paren(Vertices(the_graph);s2) 22. P(i1,s2 @ s1,s3) 23. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s3;s2 @ s1) 24. no_repeats(Vertices(the_graph)+Vertices(the_graph);s3) 25. paren(Vertices(the_graph);s3) l_disjoint(Vertices(the_graph)+Vertices(the_graph);s3 @ s2;s1) | 1 step |
  |
5 | 1. the_graph: Graph 2. the_obj: GraphObject(the_graph) 3. P: Vertices(the_graph) traversal(the_graph) traversal(the_graph) Prop 4. s: traversal(the_graph) 5. i: Vertices(the_graph) 6. s:traversal(the_graph), i:Vertices(the_graph). (inl(i) s) (inr(i) s)  P(i,s,nil) 7. s1,s2,s3:traversal(the_graph), i,j:Vertices(the_graph).
i-the_graph- > j

paren(Vertices(the_graph);s2)

paren(Vertices(the_graph);s3)  P(j,s1,s2)  P(i,s2 @ s1,s3)  P(i,s1,s3 @ s2) 8. s1,s2:traversal(the_graph), i:Vertices(the_graph).
(inl(i) s1)  (inr(i) s1)  P(i,[inr(i) / s1],s2)  P(i,s1,[inl(i) / (s2 @ [inr(i)])]) 9. x,y:Vertices(the_graph). the_obj.eq(x,y)  x = y 10. T:Type, s:T, x:Vertices(the_graph), f:(T Vertices(the_graph) T).
L:Vertices(the_graph) List.
( y:Vertices(the_graph). x-the_graph- > y  (y L))
& the_obj.eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L) 11. T:Type, s:T, f:(T Vertices(the_graph) T).
L:Vertices(the_graph) List.
no_repeats(Vertices(the_graph);L)
& ( y:Vertices(the_graph). (y L))
& the_obj.vacc(f,s) = list_accum(s',x'.f(s',x');s;L) 12. s1: traversal(the_graph) 13. s2: traversal(the_graph) 14. s3: traversal(the_graph) 15. i1: Vertices(the_graph) 16. j: Vertices(the_graph) 17. i1-the_graph- > j 18. P(j,s1,s2) 19. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1) 20. no_repeats(Vertices(the_graph)+Vertices(the_graph);s2) 21. paren(Vertices(the_graph);s2) 22. P(i1,s2 @ s1,s3) 23. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s3;s2 @ s1) 24. no_repeats(Vertices(the_graph)+Vertices(the_graph);s3) 25. paren(Vertices(the_graph);s3) no_repeats(Vertices(the_graph)+Vertices(the_graph);s3 @ s2) | 1 step |
  |
6 | 1. the_graph: Graph 2. the_obj: GraphObject(the_graph) 3. P: Vertices(the_graph) traversal(the_graph) traversal(the_graph) Prop 4. s: traversal(the_graph) 5. i: Vertices(the_graph) 6. s:traversal(the_graph), i:Vertices(the_graph). (inl(i) s) (inr(i) s)  P(i,s,nil) 7. s1,s2,s3:traversal(the_graph), i,j:Vertices(the_graph).
i-the_graph- > j

paren(Vertices(the_graph);s2)

paren(Vertices(the_graph);s3)  P(j,s1,s2)  P(i,s2 @ s1,s3)  P(i,s1,s3 @ s2) 8. s1,s2:traversal(the_graph), i:Vertices(the_graph).
(inl(i) s1)  (inr(i) s1)  P(i,[inr(i) / s1],s2)  P(i,s1,[inl(i) / (s2 @ [inr(i)])]) 9. x,y:Vertices(the_graph). the_obj.eq(x,y)  x = y 10. T:Type, s:T, x:Vertices(the_graph), f:(T Vertices(the_graph) T).
L:Vertices(the_graph) List.
( y:Vertices(the_graph). x-the_graph- > y  (y L))
& the_obj.eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L) 11. T:Type, s:T, f:(T Vertices(the_graph) T).
L:Vertices(the_graph) List.
no_repeats(Vertices(the_graph);L)
& ( y:Vertices(the_graph). (y L))
& the_obj.vacc(f,s) = list_accum(s',x'.f(s',x');s;L) 12. s1: traversal(the_graph) 13. s2: traversal(the_graph) 14. s3: traversal(the_graph) 15. i1: Vertices(the_graph) 16. j: Vertices(the_graph) 17. i1-the_graph- > j 18. P(j,s1,s2) 19. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;s1) 20. no_repeats(Vertices(the_graph)+Vertices(the_graph);s2) 21. paren(Vertices(the_graph);s2) 22. P(i1,s2 @ s1,s3) 23. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s3;s2 @ s1) 24. no_repeats(Vertices(the_graph)+Vertices(the_graph);s3) 25. paren(Vertices(the_graph);s3) paren(Vertices(the_graph);s3 @ s2) | 1 step |
  |
7 | 1. the_graph: Graph 2. the_obj: GraphObject(the_graph) 3. P: Vertices(the_graph) traversal(the_graph) traversal(the_graph) Prop 4. s: traversal(the_graph) 5. i: Vertices(the_graph) 6. s:traversal(the_graph), i:Vertices(the_graph). (inl(i) s) (inr(i) s)  P(i,s,nil) 7. s1,s2,s3:traversal(the_graph), i,j:Vertices(the_graph).
i-the_graph- > j

paren(Vertices(the_graph);s2)

paren(Vertices(the_graph);s3)  P(j,s1,s2)  P(i,s2 @ s1,s3)  P(i,s1,s3 @ s2) 8. s1,s2:traversal(the_graph), i:Vertices(the_graph).
(inl(i) s1)  (inr(i) s1)  P(i,[inr(i) / s1],s2)  P(i,s1,[inl(i) / (s2 @ [inr(i)])]) 9. x,y:Vertices(the_graph). the_obj.eq(x,y)  x = y 10. T:Type, s:T, x:Vertices(the_graph), f:(T Vertices(the_graph) T).
L:Vertices(the_graph) List.
( y:Vertices(the_graph). x-the_graph- > y  (y L))
& the_obj.eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L) 11. T:Type, s:T, f:(T Vertices(the_graph) T).
L:Vertices(the_graph) List.
no_repeats(Vertices(the_graph);L)
& ( y:Vertices(the_graph). (y L))
& the_obj.vacc(f,s) = list_accum(s',x'.f(s',x');s;L) 12. s1: traversal(the_graph) 13. s2: traversal(the_graph) 14. i1: Vertices(the_graph) 15. ((inl(i1) s1) (inr(i1) s1)) 16. P(i1,[inr(i1) / s1],s2) 17. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;[inr(i1) / s1]) 18. no_repeats(Vertices(the_graph)+Vertices(the_graph);s2) 19. paren(Vertices(the_graph);s2) P(i1,s1,[inl(i1) / (s2 @ [inr(i1)])]) | 1 step |
  |
8 | 1. the_graph: Graph 2. the_obj: GraphObject(the_graph) 3. P: Vertices(the_graph) traversal(the_graph) traversal(the_graph) Prop 4. s: traversal(the_graph) 5. i: Vertices(the_graph) 6. s:traversal(the_graph), i:Vertices(the_graph). (inl(i) s) (inr(i) s)  P(i,s,nil) 7. s1,s2,s3:traversal(the_graph), i,j:Vertices(the_graph).
i-the_graph- > j

paren(Vertices(the_graph);s2)

paren(Vertices(the_graph);s3)  P(j,s1,s2)  P(i,s2 @ s1,s3)  P(i,s1,s3 @ s2) 8. s1,s2:traversal(the_graph), i:Vertices(the_graph).
(inl(i) s1)  (inr(i) s1)  P(i,[inr(i) / s1],s2)  P(i,s1,[inl(i) / (s2 @ [inr(i)])]) 9. x,y:Vertices(the_graph). the_obj.eq(x,y)  x = y 10. T:Type, s:T, x:Vertices(the_graph), f:(T Vertices(the_graph) T).
L:Vertices(the_graph) List.
( y:Vertices(the_graph). x-the_graph- > y  (y L))
& the_obj.eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L) 11. T:Type, s:T, f:(T Vertices(the_graph) T).
L:Vertices(the_graph) List.
no_repeats(Vertices(the_graph);L)
& ( y:Vertices(the_graph). (y L))
& the_obj.vacc(f,s) = list_accum(s',x'.f(s',x');s;L) 12. s1: traversal(the_graph) 13. s2: traversal(the_graph) 14. i1: Vertices(the_graph) 15. ((inl(i1) s1) (inr(i1) s1)) 16. P(i1,[inr(i1) / s1],s2) 17. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;[inr(i1) / s1]) 18. no_repeats(Vertices(the_graph)+Vertices(the_graph);s2) 19. paren(Vertices(the_graph);s2) l_disjoint(Vertices(the_graph)+Vertices(the_graph);[inl(i1) / (s2 @ [inr(i1)])];s1) | 1 step |
  |
9 | 1. the_graph: Graph 2. the_obj: GraphObject(the_graph) 3. P: Vertices(the_graph) traversal(the_graph) traversal(the_graph) Prop 4. s: traversal(the_graph) 5. i: Vertices(the_graph) 6. s:traversal(the_graph), i:Vertices(the_graph). (inl(i) s) (inr(i) s)  P(i,s,nil) 7. s1,s2,s3:traversal(the_graph), i,j:Vertices(the_graph).
i-the_graph- > j

paren(Vertices(the_graph);s2)

paren(Vertices(the_graph);s3)  P(j,s1,s2)  P(i,s2 @ s1,s3)  P(i,s1,s3 @ s2) 8. s1,s2:traversal(the_graph), i:Vertices(the_graph).
(inl(i) s1)  (inr(i) s1)  P(i,[inr(i) / s1],s2)  P(i,s1,[inl(i) / (s2 @ [inr(i)])]) 9. x,y:Vertices(the_graph). the_obj.eq(x,y)  x = y 10. T:Type, s:T, x:Vertices(the_graph), f:(T Vertices(the_graph) T).
L:Vertices(the_graph) List.
( y:Vertices(the_graph). x-the_graph- > y  (y L))
& the_obj.eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L) 11. T:Type, s:T, f:(T Vertices(the_graph) T).
L:Vertices(the_graph) List.
no_repeats(Vertices(the_graph);L)
& ( y:Vertices(the_graph). (y L))
& the_obj.vacc(f,s) = list_accum(s',x'.f(s',x');s;L) 12. s1: traversal(the_graph) 13. s2: traversal(the_graph) 14. i1: Vertices(the_graph) 15. ((inl(i1) s1) (inr(i1) s1)) 16. P(i1,[inr(i1) / s1],s2) 17. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;[inr(i1) / s1]) 18. no_repeats(Vertices(the_graph)+Vertices(the_graph);s2) 19. paren(Vertices(the_graph);s2) no_repeats(Vertices(the_graph)+Vertices(the_graph);[inl(i1) / (s2 @ [inr(i1)])]) | 6 steps |
  |
10 | 1. the_graph: Graph 2. the_obj: GraphObject(the_graph) 3. P: Vertices(the_graph) traversal(the_graph) traversal(the_graph) Prop 4. s: traversal(the_graph) 5. i: Vertices(the_graph) 6. s:traversal(the_graph), i:Vertices(the_graph). (inl(i) s) (inr(i) s)  P(i,s,nil) 7. s1,s2,s3:traversal(the_graph), i,j:Vertices(the_graph).
i-the_graph- > j

paren(Vertices(the_graph);s2)

paren(Vertices(the_graph);s3)  P(j,s1,s2)  P(i,s2 @ s1,s3)  P(i,s1,s3 @ s2) 8. s1,s2:traversal(the_graph), i:Vertices(the_graph).
(inl(i) s1)  (inr(i) s1)  P(i,[inr(i) / s1],s2)  P(i,s1,[inl(i) / (s2 @ [inr(i)])]) 9. x,y:Vertices(the_graph). the_obj.eq(x,y)  x = y 10. T:Type, s:T, x:Vertices(the_graph), f:(T Vertices(the_graph) T).
L:Vertices(the_graph) List.
( y:Vertices(the_graph). x-the_graph- > y  (y L))
& the_obj.eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L) 11. T:Type, s:T, f:(T Vertices(the_graph) T).
L:Vertices(the_graph) List.
no_repeats(Vertices(the_graph);L)
& ( y:Vertices(the_graph). (y L))
& the_obj.vacc(f,s) = list_accum(s',x'.f(s',x');s;L) 12. s1: traversal(the_graph) 13. s2: traversal(the_graph) 14. i1: Vertices(the_graph) 15. ((inl(i1) s1) (inr(i1) s1)) 16. P(i1,[inr(i1) / s1],s2) 17. l_disjoint(Vertices(the_graph)+Vertices(the_graph);s2;[inr(i1) / s1]) 18. no_repeats(Vertices(the_graph)+Vertices(the_graph);s2) 19. paren(Vertices(the_graph);s2) paren(Vertices(the_graph);[inl(i1) / (s2 @ [inr(i1)])]) | 1 step |