At: rel mng static111211 1. name: relname() 2. r1: Term List 3. u: Term 4. v: Term List 5. rho: Top 6. ds: Top 7. da: Top 8. de: Top 9. e: Top 10. s: Top 11. a: Top 12. tr: Top 13. tr': Top 14. x:Top.
rel_mentions_trace(mk_rel(name, v))
(list_accum(x,t.x([[t]] 1of(e) s a tr');x;v) ~ list_accum(x,t.x([[t]] 1of(e) s a tr);x;v)) 15. x: Top 16. rel_mentions_trace(mk_rel(name, v))
rel_mentions_trace(mk_rel(name, [u / v])) By: All (i.(Unfold `rel_mentions_trace` i) THEN (Reduce i))
THEN
RW assert_pushdownC 0
THEN
SimpConcl Generated subgoals:
x:Top.
rel_mentions_trace(mk_rel(name, v)) 
(list_accum(x,t.x([[t]] 1of(e) s a tr');x;v) ~ list_accum(x,t.x([[t]] 1of(e) s a tr);x;v))
rel_mentions_trace(mk_rel(name, [u / v]))
i.(Unfold `rel_mentions_trace` i) THEN (Reduce i))