Nuprl - Pf term_mng

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

1. ds: Collection(dec())
2. da: Collection(dec())
3. st: Collection(SimpleType)
4. de: sig()
5. rho: Decl
6. e1: {1of([[de]] rho)}
7. s1: {[[ds]] rho}
8. s2: {[[ds]] rho}
9. a: [[st]] rho
10. tr: trace_env([[da]] rho)
11. u: Term

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

By: TermInd -1 THEN Reduce 0 THEN Try (Auto THEN (Try (Fold `decl` 0)) THEN (InstHyp [x1] -2 ORELSE InstHyp [x] -2) THEN (Try (RWW "member_singleton" 0)) THEN (RWW "member_dec_lookup" -2) THEN (HypSubst -1 0) THEN (Try (Fold `member` 0)) THEN (Try (BackThru Thm* ds:Collection(dec()), rho:Decl, x:Label, y:[[ds]] rho(x) , a:SimpleType. mk_dec(x, a) ds y [[a]] rho))) THEN Try (Auto THEN (Try (Fold `decl` 0)) THEN (RW ColMemberC -1) THEN (HypSubstSq -1 0) THEN (Try (Unfold `r_select` 0)) THEN (AllHyps (i. (Unfold `sig_mng` i) THEN (Unfold `record` i) THEN (Unfold `decl_type` i) THEN (Reduce i)))) THEN Try (Auto THEN (Try (BackThru Thm* sts:Collection(SimpleType), rho:Decl, v:[[sts]] rho , s:SimpleType. s sts v [[s]] rho)) THEN (Try (Fold `decl` 0)))

Generated subgoals:

1 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

2 1. ds: Collection{i}(dec())
2. da: Collection{i}(dec())
3. st: Collection{i}(SimpleType)
4. de: sig()
5. rho: Decl{i}
6. e1: {1of(sig_mng{i:l} (de; 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: {v:Term| u1(v) }
15. y2: {v:Term| u1(v) }
16. t: SimpleType
17. trace_consistent(rho;da;tr.proj;y1 y2)
18. x:Label. (x term_vars(y1) @ term_vars(y2)) s1.x = s2.x
19. t st_app(term_types(ds;st;de;y1);term_types(ds;st;de;y2))
[[y1]] e1 s1 a tr([[y2]] e1 s1 a tr) = [[y1]] e1 s2 a tr([[y2]] e1 s2 a tr) [[t]] rho

About:

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