(5steps) PrintForm Definitions mb automata 3 Sections GenAutomata Doc

At: rel mng nil 2
1. name: relname()
2. r1: Term List
3. te:(LabelLabel), rho,ds,da,de,e,s,a,x:Top. list_accum(x,t.x ([[t]] 1of(e) s a mk_trace_env(nil, te));x;r1) ~ list_accum(x,t.x([[t]] 1of(e) s a niltrace());x;r1)

te:(LabelLabel), rho,ds,da,de,e,s,a:Top. list_accum(x,t.x ([[t]] 1of(e) s a mk_trace_env(nil, te));[[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:
listnilboolapplyfunctionsqequaltopall

(5steps) PrintForm Definitions mb automata 3 Sections GenAutomata Doc