Nuprl - Pf term_types

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

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

By: Analyze 0 THEN TermInd -1 THEN Unfold `term_types` 0 THEN Reduce 0 THEN Try (Fold `term_types` 0) THEN Try RelRST

Generated subgoals:

1 1. t: Term
2. u: TermType{i'}
3. w: t:{v:Term| u(v) }ds:Collection{i}(dec()), da1,da2:Collection{i}(SimpleType), de:sig(). closed_term(t) term_types(ds;da1;de;t) = term_types(ds;da2;de;t)
4. x: Label
5. ds: Collection{i}(dec())
6. da1: Collection{i}(SimpleType)
7. da2: Collection{i}(SimpleType)
8. de: sig()
9. closed_term(x)
da1 = da2

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

About:

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