Nuprl - Pf rel mng 2 iff 1

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

1. 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)

By: All (Unfolds [`rel_mng_2`;`rel_mng`])

Generated subgoal:

1 list_accum(x,t.x([[t]] 1of(e) s1 a tr);[[r1.name]] rho 2of(e) ;r1.args) list_accum(x,t.x([[t]] 1of(e) s1 s2 a tr);[[r2.name]] rho 2of(e) ;r2.args)

About:

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