(3steps) PrintForm Definitions mb automata 4 Sections GenAutomata Doc

At: rel mng functionality 1
1. r: rel()
2. ds1: Collection(dec())
3. ds2: Collection(dec())
4. da: Collection(dec())
5. da1: Collection(SimpleType)
6. da2: Collection(SimpleType)
7. de: sig()
8. rho: Decl
9. e: {[[de]] rho}
10. s: {[[ds1]] rho}
11. a: [[da1]] rho
12. tr: trace_env([[da]] rho)
13. trace_consistent_rel(rho;da;tr.proj;r)
14. tc(r;ds1;da1;de)
15. ds1 = ds2
16. da1 = da2

[[r]] rho ds1 da1 de e s a tr [[r]] rho ds2 da2 de e s a tr
By:
Analyze 0
THEN
Analyze 0
THEN
Try ((All (Unfold `rel_mng`)) THEN (Complete Auto))
THEN
Try Easy
Generated subgoals:

None

(3steps) PrintForm Definitions mb automata 4 Sections GenAutomata Doc