Nuprl - Pf pred mng2 addprime 1

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

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

By: AllHyps (InstHyp [(r)'])

Generated subgoals:

1 (r)' (p)'

2 17. rel_mng_2((r)'; rho; ds; da; de; e; s; s'; a; tr)
[[r]] rho ds da de e s' a tr

About:

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

1	`(r)' (p)'`
2	17. `rel_mng_2((r)'; rho; ds; da; de; e; s; s'; a; tr)` `[[r]] rho ds da de e s' a tr`