Nuprl - Pf term_typing2 1 2

(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: {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

By: UnivCD THEN RWW "member_st_app" -1 THEN ExRepD THEN AllHyps (i.InstHyp [y2;s;s';e;a1;v;tr] i) THEN AllHyps (i.InstHyp [y1;s;s';e;a1a;v;tr] i) THEN Reduce -1 THEN AllHyps (h. (RepeatFor 2 (ParallelOp h)) THEN (ParallelOp -1) THEN (Reduce 0) THEN (RW assert_pushdownC 0) THEN (Complete SimpConcl))

Generated subgoals:

None

About:

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