Nuprl - Pf term_types

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

ds1,ds2:Collection(dec()), da1,da2:Collection(SimpleType), de:sig(), t:Term. ds1 = ds2 da1 = da2 term_types(ds1;da1;de;t) = term_types(ds2;da2;de;t)

By: UnivCD THEN TermInd -3 THEN Unfold `term_types` 0 THEN Reduce 0 THEN Try (RW (SweepDnC (HypC 7 ORELSEC HypC 8)) 0) THEN Try (Fold `term_types` 0) THEN Try RelRST

Generated subgoal:

1 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);...)

About:

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