Nuprl - Pf term

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

1. ds: Collection(dec())
2. daa: Collection(dec())
3. da: Collection(SimpleType)
4. de: sig()
5. rho: Decl
6. t: Term

s,s':{[[ds]] rho}, e:{1of([[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

By: TermInd -1 THEN Unfolds [`term_types`;`term_mng2`] 0 THEN Reduce 0 THEN Try (Folds [`term_types`;`term_mng2`] 0) THEN Try (Auto THEN (Try (Fold `r_select` 0)) THEN (BackThru Thm* ds:Collection(dec()), rho:Decl, s:{[[ds]] rho} , x:Label, t:SimpleType. t dec_lookup(ds;x) s.x [[t]] rho)) THEN Try (Complete (Auto THEN (RW ColMemberC -1) THEN (HypSubstSq -1 0) THEN (Unfold `r_select` 0) THEN (AllHyps (i. (Unfold `record` i) THEN (Unfold `sig_mng` i) THEN (Unfold `decl_type` i) THEN (Reduce i))))) THEN Try (Auto THEN (BackThru Thm* sts:Collection(SimpleType), rho:Decl, v:[[sts]] rho , s:SimpleType. s sts v [[s]] rho))

Generated subgoals:

1 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

2 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: {v:Term| u(v) }
10. y2: {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;y1 y2) a st_app(term_types(ds;da;de;y1);term_types(ds;da;de;y2)) [[y1]] e s s' v tr([[y2]] e s s' v tr) [[a]] rho

About:

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