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

At: rel mng 2 iff

r1,r2:rel(), ds,daa:Collection(dec()), da:Collection(SimpleType), de:sig(), rho:Decl, e:{[[de]] rho}, s1,s2:{[[ds]] rho}, a:[[da]] rho, tr:trace_env([[daa]] rho). trace_consistent_rel(rho;daa;tr.proj;r1) trace_consistent_rel(rho;daa;tr.proj;r2) tc(r1;ds;da;de) tc(r2;ds;da;de) r1.name = r2.name ||r1.args|| = ||r2.args|| (i:. i < ||r1.args|| [[r1.args[i]]] 1of(e) s1 a tr = [[r2.args[i]]] 1of(e) s1 s2 a tr [[rel_arg_typ(r1.name;i;de)]] rho) ([[r1]] rho ds da de e s1 a tr rel_mng_2(r2; rho; ds; da; de; e; s1; s2; a; tr))
By:
UnivCD
THEN
Try ((Unfold `decl` 0) THEN (Complete Auto))
THEN
Try ((All (Unfolds [`tc`;`tc1`])) THEN (Analyze 1) THEN (Analyze 1) THEN (All Reduce) THEN ExRepD THEN Trivial)
THEN
Try (Complete ((BackThru Thm* r:rel(), i:, ds,da:Collection(dec()), st1:Collection(SimpleType), de:sig(), rho:Decl, s:{[[ds]] rho}, e:{1of([[de]] rho)}, a:[[st1]] rho, tr:trace_env([[da]] rho). trace_consistent_rel(rho;da;tr.proj;r) tc(r;ds;st1;de) i < ||r.args|| [[r.args[i]]] e s a tr [[rel_arg_typ(r.name;i;de)]] rho) THEN (AllHyps (i.(Analyze i) THEN (All Reduce) THEN Trivial))))
THEN
Try (Complete ((HypSubstSq -4 0) THEN (BackThru Thm* r:rel(), i:, ds,da:Collection(dec()), st1:Collection(SimpleType), de:sig(), rho:Decl, s,s':{[[ds]] rho}, e:{1of([[de]] rho)}, a:[[st1]] rho, tr:trace_env([[da]] rho). trace_consistent_rel(rho;da;tr.proj;r) tc(r;ds;st1;de) i < ||r.args|| [[r.args[i]]] e s s' a tr [[rel_arg_typ(r.name;i;de)]] rho) THEN (AllHyps (i.(Analyze i) THEN (All Reduce) THEN Trivial))))
Generated subgoals:

11. r1: rel()
2. r2: rel()
3. ds: Collection(dec())
4. daa: Collection(dec())
5. da: Collection(SimpleType)
6. de: sig()
7. rho: Decl
8. e: {[[de]] rho}
9. s1: {[[ds]] rho}
10. s2: {[[ds]] rho}
11. a: [[da]] rho
12. tr: trace_env([[daa]] rho)
13. trace_consistent_rel(rho;daa;tr.proj;r1)
14. trace_consistent_rel(rho;daa;tr.proj;r2)
15. tc(r1;ds;da;de)
16. tc(r2;ds;da;de)
17. r1.name = r2.name
18. ||r1.args|| = ||r2.args||
19. i:. i < ||r1.args|| [[r1.args[i]]] 1of(e) s1 a tr = [[r2.args[i]]] 1of(e) s1 s2 a tr [[rel_arg_typ(r1.name;i;de)]] rho
[[r1]] rho ds da de e s1 a tr rel_mng_2(r2; rho; ds; da; de; e; s1; s2; a; tr)
21. r1: rel()
2. r2: rel()
3. ds: Collection(dec())
4. daa: Collection(dec())
5. da: Collection(SimpleType)
6. de: sig()
7. rho: Decl
8. e: {[[de]] rho}
9. s1: {[[ds]] rho}
10. s2: {[[ds]] rho}
11. a: [[da]] rho
12. tr: trace_env([[daa]] rho)
13. trace_consistent_rel(rho;daa;tr.proj;r1)
14. trace_consistent_rel(rho;daa;tr.proj;r2)
15. tc(r1;ds;da;de)
16. tc(r2;ds;da;de)
17. r1.name = r2.name
0||r1.args||
31. r1: rel()
2. r2: rel()
3. ds: Collection(dec())
4. daa: Collection(dec())
5. da: Collection(SimpleType)
6. de: sig()
7. rho: Decl
8. e: {[[de]] rho}
9. s1: {[[ds]] rho}
10. s2: {[[ds]] rho}
11. a: [[da]] rho
12. tr: trace_env([[daa]] rho)
13. trace_consistent_rel(rho;daa;tr.proj;r1)
14. trace_consistent_rel(rho;daa;tr.proj;r2)
15. tc(r1;ds;da;de)
16. tc(r2;ds;da;de)
17. r1.name = r2.name
0||r2.args||

About:
natural_numberless_thanequalimpliesall

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