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

At: closed rel mng2 1
1. r: rel()
2. rho: Top
3. ds: Top
4. da1: Top
5. da2: Top
6. de: Top
7. s: Top
8. s': Top
9. e: Top
10. a1: Top
11. a2: Top
12. tr: Top
13. closed_rel(r)

rel_mng_2(r; rho; ds; da1; de; e; s; s'; a1; tr) ~ rel_mng_2(r; rho; ds; da2; de; e; s; s'; a2; tr)
By:
MoveToConcl -1
THEN
Unfolds [`closed_rel`;`rel_mng_2`] 0
THEN
Unfold `rel_free_vars` 0
THEN
GenConcl (r.args = l)
THEN
GenConcl ([[r.name]] rho 2of(e) = X)
Generated subgoal:

113. l: Term List
14. r.args = l
15. X: Top
16. [[r.name]] rho 2of(e) = X
reduce(t,vs. term_free_vars(t) @ vs;nil;l) = nil (list_accum(x,t.x([[t]] 1of(e) s s' a1 tr);X;l) ~ list_accum(x,t.x([[t]] 1of(e) s s' a2 tr);X;l))

About:
listnillambdaapplyequalsqequaltopimplies

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