(10steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc

At: rel mng static 2
1. name: relname()
2. r1: Term List
3. rho,ds,da,de,e,s,a,tr,tr',x:Top. rel_mentions_trace( < name,r1 > ) (list_accum(x,t.x([[t]] 1of(e) s a tr');x;r1) ~ list_accum(x,t.x([[t]] 1of(e) s a tr);x;r1))

rho,ds,da,de,e,s,a,tr,tr':Top. rel_mentions_trace( < name,r1 > ) (list_accum(x,t.x ([[t]] 1of(e) s a tr');[[name]] rho 2of(e) ;r1) ~ list_accum(x,t....;...;r1))
By:
Repeat ((ParallelOp -1) THEN (Thin -3))
THEN
SimpleInstHyp [[name]] rho 2of(e) -1
THEN
NthHyp -1
Generated subgoals:

None

About:
pairlistassertapplysqequaltopimpliesall

(10steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc