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

By: RWW "member_st_app" -1 THEN ExRepD THEN AllHyps (InstHyp [y1;a1t]) THEN Try (BackThruSomeHyp THEN (RWW "member_append" 0) THEN SimpConcl)

Generated subgoals:

1 19. a1: SimpleType
20. a1 term_types(ds;st;de;y2)
21. a1t term_types(ds;st;de;y1)
trace_consistent(rho;da;tr.proj;y1)

2 19. a1: SimpleType
20. a1 term_types(ds;st;de;y2)
21. a1t term_types(ds;st;de;y1)
22. [[y1]] e1 s1 a tr = [[y1]] e1 s2 a tr [[a1t]] rho
[[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

1	19. `a1:` `SimpleType` 20. `a1 term_types(ds;st;de;y2)` 21. `a1t term_types(ds;st;de;y1)` `trace_consistent(rho;da;tr.proj;y1)`
2	19. `a1:` `SimpleType` 20. `a1 term_types(ds;st;de;y2)` 21. `a1t term_types(ds;st;de;y1)` 22. `[[y1]] e1 s1 a tr = [[y1]] e1 s2 a tr [[a1t]] rho` `[[y1]] e1 s1 a tr([[y2]] e1 s1 a tr) = [[y1]] e1 s2 a tr([[y2]] e1 s2 a tr) [[t]] rho`