At: rel mng 2 addprime111 1. name: relname() 2. r1: Term List 3. rho: Top 4. ds: Top 5. da: Top 6. de: Top 7. e: Top 8. s: Top 9. s': Top 10. a: Top 11. tr: Top 12. u: Term 13. v: Term List 14. z:Top.
list_accum(x,t.x([[t]] 1of(e) s s' a tr);z;map(t.
(t)';v)) ~ list_accum(x,t.x([[t]] 1of(e) s' a tr);z;v) 15. z: Top
[[(u)']] 1of(e) s s' a tr ~ [[u]] 1of(e) s' a tr By: BackThru
Thm*t:Term, e,s,s',a,tr:Top. [[(t)']] e s s' a tr ~ [[t]] e s' a tr Generated subgoals:
z:Top.
list_accum(x,t.x([[t]] 1of(e) s s' a tr);z;map(
t.
(t)';v)) ~ list_accum(x,t.x([[t]] 1of(e) s' a tr);z;v)
[[(u)']] 1of(e) s s' a tr ~ [[u]] 1of(e) s' a tr