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

At: pred mng2 unprime

p:Fmla, ds,daa:Collection(dec()), da:Collection(SimpleType), de:sig(), rho:Decl, e:{[[de]] rho}, s,s':{[[ds]] rho}, a:[[da]] rho, tr:trace_env([[daa]] rho). trace_consistent_pred(rho;daa;tr.proj;p) tc_pred(p;ds;da;de) (pred_mng_2(pred_unprime(p); rho; ds; da; de; e; s; s'; a; tr) [[p]] rho ds da de e s a tr)
By:
Auto
THEN
All (Unfolds [`pred_mng_2`;`pred_mng`])
THEN
Try (Fold `pred` 0)
THEN
Try (BackThru Thm* P:Fmla, ds:Collection(dec()), da:Collection(SimpleType), de:sig(). tc_pred(P;ds;da;de) tc_pred(pred_unprime(P);ds;da;de))
THEN
Try (BackThru Thm* da:Collection(dec()), P:Fmla, rho:Decl, te:(LabelLabel). trace_consistent_pred(rho;da;te;P) trace_consistent_pred(rho;da;te;pred_unprime(P)))
Generated subgoals:

11. p: Fmla
2. ds: Collection(dec())
3. daa: Collection(dec())
4. da: Collection(SimpleType)
5. de: sig()
6. rho: Decl
7. e: {[[de]] rho}
8. s: {[[ds]] rho}
9. s': {[[ds]] rho}
10. a: [[da]] rho
11. tr: trace_env([[daa]] rho)
12. trace_consistent_pred(rho;daa;tr.proj;p)
13. tc_pred(p;ds;da;de)
14. r:rel(). r pred_unprime(p) rel_mng_2(r; rho; ds; da; de; e; s; s'; a; tr)
15. r: rel()
16. r p
[[r]] rho ds da de e s a tr
21. p: Fmla
2. ds: Collection(dec())
3. daa: Collection(dec())
4. da: Collection(SimpleType)
5. de: sig()
6. rho: Decl
7. e: {[[de]] rho}
8. s: {[[ds]] rho}
9. s': {[[ds]] rho}
10. a: [[da]] rho
11. tr: trace_env([[daa]] rho)
12. trace_consistent_pred(rho;daa;tr.proj;p)
13. tc_pred(p;ds;da;de)
14. r:rel(). r p [[r]] rho ds da de e s a tr
15. r: rel()
16. r pred_unprime(p)
rel_mng_2(r; rho; ds; da; de; e; s; s'; a; tr)
31. p: Fmla{i}
2. ds: Collection{i}(dec())
3. daa: Collection{i}(dec())
4. da: Collection{i}(SimpleType)
5. de: sig()
6. rho: Decl{i}
7. sig_mng{i:l}(de; rho) = sig_mng{i:l}(de; rho)
8. zzz: Decl{i}Decl{i'}
Decl{i} Decl{i'}

About:
subtypeimpliesall

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