Nuprl - Pf closed pred mng 1

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

1. p: Fmla
2. rho: Decl
3. ds: Collection(dec())
4. daa: Collection(dec())
5. da1: Collection(SimpleType)
6. da2: Collection(SimpleType)
7. de: sig()
8. s: {[[ds]] rho}
9. e: {[[de]] rho}
10. a1: Top
11. a2: Top
12. tr: trace_env([[daa]] rho)
13. trace_consistent_pred(rho;daa;tr.proj;p)
14. tc_pred(p;ds;da1;de)
15. closed_pred(p)

[[p]] rho ds da1 de e s a1 tr [[p]] rho ds da2 de e s a2 tr

By: Unfold `pred_mng` 0 THEN Analyze 0 THEN Analyze 0 THEN RepeatFor 2 (ParallelOp -1) THEN NthHypSq -1 THEN BackThru Thm* r:rel(), rho,ds,da1,da2,de,s,e,a1,a2,tr:Top. closed_rel(r) ([[r]] rho ds da1 de e s a1 tr ~ [[r]] rho ds da2 de e s a2 tr) THEN EasyHypThen Auto

Generated subgoals:

1 (r:rel(). r p [[r]] rho ds da1 de e s a1 tr) Prop

2 (r:rel(). r p [[r]] rho ds da2 de e s a2 tr) Prop

About:

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

1	`(r:rel(). r p [[r]] rho ds da1 de e s a1 tr) Prop`
2	`(r:rel(). r p [[r]] rho ds da2 de e s a2 tr) Prop`