(65steps) (too big for print form) Definitions Lemmas mb automata 4 Sections GenAutomata Doc

At: rel subst mng 2 iff 1 2 1 1 2 2 2 1 2 1 1 2 1 1
1. r: rel()
2. as: (LabelTerm) List
3. ds: Collection(dec())
4. daa: Collection(dec())
5. da: Collection(SimpleType)
6. de: sig()
7. rho: Decl
8. e: {[[de]] rho}
9. s: {[[ds]] rho}
10. s': {[[ds]] rho}
11. k: Label
12. a: [[da]] rho
13. tr: trace_env([[daa]] rho)
14. trace_consistent_rel(rho;daa;tr.proj;r)
15. tc(r;ds;da;de)
16. subst_mentions_trace(as)
17. x:Label. (x rel_primed_vars(r)) (t:SimpleType. mk_dec(x, t) ds t term_types(ds;da;de;apply_alist(as;x;x)) & s'.x = [[apply_alist(as;x;x)]] 1of(e) s a tr [[t]] rho)
18. tc(rel_subst2(as;r);ds;da;de)
19. trace_consistent_rel(rho;daa;tr.proj;rel_subst2(as;r))
20. ||rel_subst2(as;r).args|| = ||r.args||
21. i:
22. i < ||rel_subst2(as;r).args||
23. i < ||r.args||
24. t: Term
25. r.args[i] = t
26. tc1(r;de)

trace_consistent(rho;daa;tr.proj;t)
By: AllHyps (h.(Unfold `trace_consistent_rel` h) THEN (InstHyp [i] h))
Generated subgoal:

114. i:||r.args||. trace_consistent(rho;daa;tr.proj;r.args[i])
15. tc(r;ds;da;de)
16. subst_mentions_trace(as)
17. x:Label. (x rel_primed_vars(r)) (t:SimpleType. mk_dec(x, t) ds t term_types(ds;da;de;apply_alist(as;x;x)) & s'.x = [[apply_alist(as;x;x)]] 1of(e) s a tr [[t]] rho)
18. tc(rel_subst2(as;r);ds;da;de)
19. i:||rel_subst2(as;r).args||. trace_consistent(rho;daa;tr.proj;rel_subst2(as;r).args[i])
20. ||rel_subst2(as;r).args|| = ||r.args||
21. i:
22. i < ||rel_subst2(as;r).args||
23. i < ||r.args||
24. t: Term
25. r.args[i] = t
26. tc1(r;de)
27. trace_consistent(rho;daa;tr.proj;rel_subst2(as;r).args[i])
28. trace_consistent(rho;daa;tr.proj;r.args[i])
trace_consistent(rho;daa;tr.proj;t)

About:
productlistassertintless_thanequalimpliesall

(65steps) (too big for print form) Definitions Lemmas mb automata 4 Sections GenAutomata Doc