(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 2 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) (b:SimpleType. (x:Label. (x term_primed_vars(t)) (x rel_primed_vars(r))) b term_types(ds;da;de;t) [[term_subst2(as;t)]] 1of(e) s a tr = [[t]] 1of(e) s s' a tr [[b]] rho)
By:
TermInd -3
THEN
Unfolds [`term_subst`;`term_types`] 0
THEN
Reduce 0
THEN
Try (Folds [`term_subst`;`term_types`] 0)
THEN
Analyze 0
THEN
Analyze 0
THEN
Analyze 0
THEN
Analyze 0
Generated subgoals:

13. ds: Collection{i}(dec())
4. daa: Collection{i}(dec())
5. da: Collection{i}(SimpleType)
6. de: sig()
7. rho: Decl{i}
8. e: {sig_mng{i:l} (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)
27. u: TermType{i'}
28. w: t:{v:Term| u(v) }trace_consistent(rho;daa;tr.proj;t) (b:SimpleType. (x:Label. (x term_primed_vars(t)) (x rel_primed_vars(r))) b term_types(ds;da;de;t) [[term_subst2(as;t)]] 1of(e) s a tr = [[t]] 1of(e) s s' a tr [[b]] rho)
29. x1: Label
30. trace_consistent(rho;daa;tr.proj;x1)
31. b: SimpleType
32. x@0:Label. (x@0 nil) (x@0 rel_primed_vars(r))
33. b dec_lookup(ds;x1)
s.x1 = s.x1 [[b]] rho
23. ds: Collection{i}(dec())
4. daa: Collection{i}(dec())
5. da: Collection{i}(SimpleType)
6. de: sig()
7. rho: Decl{i}
8. e: {sig_mng{i:l} (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)
27. u: TermType{i'}
28. w: t:{v:Term| u(v) }trace_consistent(rho;daa;tr.proj;t) (b:SimpleType. (x:Label. (x term_primed_vars(t)) (x rel_primed_vars(r))) b term_types(ds;da;de;t) [[term_subst2(as;t)]] 1of(e) s a tr = [[t]] 1of(e) s s' a tr [[b]] rho)
29. x: Label
30. trace_consistent(rho;daa;tr.proj;x')
31. b: SimpleType
32. x@0:Label. (x@0 [x]) (x@0 rel_primed_vars(r))
33. b dec_lookup(ds;x)
[[apply_alist(as;x;x')]] 1of(e) s a tr = s'.x [[b]] rho
33. ds: Collection{i}(dec())
4. daa: Collection{i}(dec())
5. da: Collection{i}(SimpleType)
6. de: sig()
7. rho: Decl{i}
8. e: {sig_mng{i:l} (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)
27. u: TermType{i'}
28. w: t:{v:Term| u(v) }trace_consistent(rho;daa;tr.proj;t) (b:SimpleType. (x:Label. (x term_primed_vars(t)) (x rel_primed_vars(r))) b term_types(ds;da;de;t) [[term_subst2(as;t)]] 1of(e) s a tr = [[t]] 1of(e) s s' a tr [[b]] rho)
29. x: Label
30. trace_consistent(rho;daa;tr.proj;x)
31. b: SimpleType
32. x@0:Label. (x@0 nil) (x@0 rel_primed_vars(r))
33. b < de.fun(x) >
1of(e).x = 1of(e).x [[b]] rho
43. ds: Collection{i}(dec())
4. daa: Collection{i}(dec())
5. da: Collection{i}(SimpleType)
6. de: sig()
7. rho: Decl{i}
8. e: {sig_mng{i:l} (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)
27. u: TermType{i'}
28. w: t:{v:Term| u(v) }trace_consistent(rho;daa;tr.proj;t) (b:SimpleType. (x:Label. (x term_primed_vars(t)) (x rel_primed_vars(r))) b term_types(ds;da;de;t) [[term_subst2(as;t)]] 1of(e) s a tr = [[t]] 1of(e) s s' a tr [[b]] rho)
29. x: Label
30. trace_consistent(rho;daa;tr.proj;x)
31. b: SimpleType
32. x@0:Label. (x@0 nil) (x@0 rel_primed_vars(r))
33. b da
a = a [[b]] rho
53. ds: Collection{i}(dec())
4. daa: Collection{i}(dec())
5. da: Collection{i}(SimpleType)
6. de: sig()
7. rho: Decl{i}
8. e: {sig_mng{i:l} (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)
27. u: TermType{i'}
28. w: t:{v:Term| u(v) }trace_consistent(rho;daa;tr.proj;t) (b:SimpleType. (x:Label. (x term_primed_vars(t)) (x rel_primed_vars(r))) b term_types(ds;da;de;t) [[term_subst2(as;t)]] 1of(e) s a tr = [[t]] 1of(e) s s' a tr [[b]] rho)
29. y1: Label
30. trace_consistent(rho;daa;tr.proj;trace(y1))
31. b: SimpleType
32. x@0:Label. (x@0 nil) (x@0 rel_primed_vars(r))
33. b < lbl_pr( < Trace, y1 > ) >
tr.y1 = tr.y1 [[b]] rho
63. ds: Collection{i}(dec())
4. daa: Collection{i}(dec())
5. da: Collection{i}(SimpleType)
6. de: sig()
7. rho: Decl{i}
8. e: {sig_mng{i:l} (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)
27. u: TermType{i'}
28. w: t:{v:Term| u(v) }trace_consistent(rho;daa;tr.proj;t) (b:SimpleType. (x:Label. (x term_primed_vars(t)) (x rel_primed_vars(r))) b term_types(ds;da;de;t) [[term_subst2(as;t)]] 1of(e) s a tr = [[t]] 1of(e) s s' a tr [[b]] rho)
29. y1: {v:Term| u(v) }
30. y2: {v:Term| u(v) }
31. trace_consistent(rho;daa;tr.proj;y1 y2)
32. b: SimpleType
33. x:Label. (x term_primed_vars(y1) @ term_primed_vars(y2)) (x rel_primed_vars(r))
34. b st_app(term_types(ds;da;de;y1);term_types(ds;da;de;y2))
[[term_subst2(as;y1)]] 1of(e) s a tr([[term_subst2(as;y2)]] 1of(e) s a tr) = [[y1]] 1of(e) s s' a tr([[y2]] 1of(e) s s' a tr) [[b]] rho

About:
productlistassertintless_thanapplyequalimpliesall

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