Nuprl - Pf term_typing2 1 1

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

1. ds: Collection{i}(dec())
2. daa: Collection{i}(dec())
3. da: Collection{i}(SimpleType)
4. de: sig()
5. rho: Decl{i}
6. t: Term
7. u: TermType{i'}
8. w: t:{v:Term| u(v) }s,s':{[[ds]] rho}, e:{1of(sig_mng{i:l}(de; rho))}, a:SimpleType, v:[[da]] rho , tr:trace_env([[daa]] rho). trace_consistent(rho;daa;tr.proj;t) a term_types(ds;da;de;t) [[t]] e s s' v tr [[a]] rho
9. y1: Label

s,s':{[[ds]] rho}, e:{1of(sig_mng{i:l}(de; rho))}, a:SimpleType, v:[[da]] rho , tr:trace_env([[daa]] rho). trace_consistent(rho;daa;tr.proj;trace(y1)) a < lbl_pr( < Trace, y1 > ) > tr.y1 [[a]] rho

By: Auto THEN RW ColMemberC -1 THEN HypSubstSq -1 0

Generated subgoal:

1 10. s: {[[ds]] rho}
11. s': {[[ds]] rho}
12. e: {1of(sig_mng{i:l} (de; rho))}
13. a: SimpleType
14. v: [[da]] rho
15. tr: trace_env([[daa]] rho)
16. trace_consistent(rho;daa;tr.proj;trace(y1))
17. a = lbl_pr( < Trace, y1 > )
tr.y1 [[lbl_pr( < Trace, y1 > )]] rho

About:

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