Nuprl - Pf term_mng

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

1. ds: Collection{i}(dec())
2. da: Collection{i}(dec())
3. st: Collection{i}(SimpleType)
4. de: sig()
5. rho: Decl{i}
6. e1: l:Label[[de.fun(l)]] rho
7. s1: {[[ds]] rho}
8. s2: {[[ds]] rho}
9. a: [[st]] rho
10. tr: trace_env([[da]] rho)
11. u: Term
12. u1: TermType{i'}
13. w: u:{v:Term| u1(v) }t:SimpleType. trace_consistent(rho;da;tr.proj;u) (x:Label. (x term_vars(u)) s1.x = s2.x) t term_types(ds;st;de;u) [[u]] e1 s1 a tr = [[u]] e1 s2 a tr [[t]] rho
14. y1: Label
15. t: SimpleType
16. trace_consistent(rho;da;tr.proj;trace(y1))
17. x@0:Label. (x@0 nil) s1.x@0 = s2.x@0
18. t = lbl_pr( < Trace, y1 > )

tr.y1 = tr.y1 [[lbl_pr( < Trace, y1 > )]] rho

By: Fold `member` 0 THEN BackThru Thm* da:Collection(dec()), rho:Decl, tr:trace_env([[da]] rho), y1:Label. trace_consistent(rho;da;tr.proj;trace(y1)) tr.y1 [[lbl_pr( < Trace, y1 > )]] rho

Generated subgoals:

None

About:

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