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

At: rel mng nil 1
1. name: relname()
2. r1: Term List

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)
By:
ListInd -1
THEN
All (Fold `mk_rel`)
THEN
All (Unfold `rel_mng`)
THEN
All Reduce
THEN
Try (Complete Auto)
Generated subgoal:

13. u: Term
4. v: Term List
5. 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;v) ~ list_accum(x,t.x([[t]] 1of(e) s a niltrace());x;v)
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 ([[u]] 1of(e) s a mk_trace_env(nil, te));v) ~ list_accum(x,t....;x (...);v)

About:
listnilboolapplyfunctionsqequaltopall

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