Nuprl - Pf pred mng functionality 1 2

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

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

(r:rel(). r p1 [[r]] rho ds1 da1 de e s a tr) (r:rel(). r p2 [[r]] rho ds2 da2 de e s a tr)

By: Analyze 0 THEN Analyze 0 THEN Try (Analyze 0)

Generated subgoals:

1 20. r:rel(). r p1 [[r]] rho ds1 da1 de e s a tr
21. r: rel()
r p2 [[r]] rho ds2 da2 de e s a tr

2 (r:rel(). r p1 [[r]] rho ds1 da1 de e s a tr) Prop

3 20. r:rel(). r p2 [[r]] rho ds2 da2 de e s a tr
21. r: rel()
r p1 [[r]] rho ds1 da1 de e s a tr

4 (r:rel(). r p2 [[r]] rho ds2 da2 de e s a tr) Prop

About:

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

1	20. `r:rel(). r p1 [[r]] rho ds1 da1 de e s a tr` 21. `r:` `rel()` `r p2 [[r]] rho ds2 da2 de e s a tr`
2	`(r:rel(). r p1 [[r]] rho ds1 da1 de e s a tr) Prop`
3	20. `r:rel(). r p2 [[r]] rho ds2 da2 de e s a tr` 21. `r:` `rel()` `r p1 [[r]] rho ds1 da1 de e s a tr`
4	`(r:rel(). r p2 [[r]] rho ds2 da2 de e s a tr) Prop`