Nuprl - Pf term_types_functionality 1

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

1. ds1: Collection{i}(dec())
2. ds2: Collection{i}(dec())
3. da1: Collection{i}(SimpleType)
4. da2: Collection{i}(SimpleType)
5. de: sig()
6. t: Term
7. ds1 = ds2
8. da1 = da2
9. u: TermType{i'}
10. w: t:{v:Term| u(v) }term_types(ds1;da1;de;t) = term_types(ds2;da2;de;t)
11. y1: {v:Term| u(v) }
12. y2: {v:Term| u(v) }

st_app(term_types(ds1;da1;de;y1);term_types(ds1;da1;de;y2)) = st_app(term_types(ds2;da2;de;y1);...)

By: InstHyp [y1] -3 THEN InstHyp [y2] -4

Generated subgoal:

1 13. term_types(ds1;da1;de;y1) = term_types(ds2;da2;de;y1)
14. term_types(ds1;da1;de;y2) = term_types(ds2;da2;de;y2)
st_app(term_types(ds1;da1;de;y1);term_types(ds1;da1;de;y2)) = st_app(term_types(ds2;da2;de;y1);...)

About:

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