Nuprl - Pf rel mng wf closed 1

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

1. rho: Decl
2. ds: Collection(dec())
3. daa: Collection(dec())
4. da1: Collection(SimpleType)
5. de: sig()
6. s: {[[ds]] rho}
7. e: {[[de]] rho}
8. tr: trace_env([[daa]] rho)
9. r: rel()
10. closed_rel(r)
11. tc(r;ds;da1;de)
12. trace_consistent_rel(rho;daa;tr.proj;r)

[[r]] rho ds da1 de e s tr Prop

By: Assert ([[r]] rho ds < > de e s tr Prop)

Generated subgoals:

1 [[r]] rho ds < > de e s tr Prop

2 13. [[r]] rho ds < > de e s tr Prop
[[r]] rho ds da1 de e s tr Prop

About:

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

1	`[[r]] rho ds < > de e s tr Prop`
2	13. `[[r]] rho ds < > de e s tr Prop` `[[r]] rho ds da1 de e s tr Prop`