(5steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc

At: trace consistent rel subst2 2
1. r: rel()
2. as: (LabelTerm) List
3. daa: Collection(dec())
4. rho: Decl
5. te: LabelLabel
6. i:||r.args||. trace_consistent(rho;daa;te;r.args[i])
7. subst_mentions_trace(as)
8. i: ||map(t.term_subst2(as;t);r.args)||
9. trace_consistent(rho;daa;te;r.args[i])
10. ||map(t.term_subst2(as;t);r.args)|| = ||r.args||

trace_consistent(rho;daa;te;map(t.term_subst2(as;t);r.args)[i])
By:
RepeatFor 2 (ParallelOp -2)
THEN
ParallelOp -1
THEN
Subst' (map(t.term_subst2(as;t);r.args)[i] = term_subst2(as;r.args[i])) -1
Generated subgoals:

19. g:Label. term_mentions_guard(g;r.args[i]) (([[ < d daa | te(g,d.lbl) > ]] rho) List) (rho(lbl_pr( < Trace, g > )))
10. ||map(t.term_subst2(as;t);r.args)|| = ||r.args||
11. g: Label
12. term_mentions_guard(g;map(t.term_subst2(as;t);r.args)[i])
13. x,y:Term. x = y (x ~ y)
map(t.term_subst2(as;t);r.args)[i] = term_subst2(as;r.args[i])
29. g:Label. term_mentions_guard(g;r.args[i]) (([[ < d daa | te(g,d.lbl) > ]] rho) List) (rho(lbl_pr( < Trace, g > )))
10. ||map(t.term_subst2(as;t);r.args)|| = ||r.args||
11. g: Label
12. term_mentions_guard(g;term_subst2(as;r.args[i]))
term_mentions_guard(g;r.args[i])

About:
productlistboolassertintnatural_numberlambdafunctionequalall

(5steps) PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc