Nuprl - Pf closed term mng

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

t:Term, e,s,a1,a2,tr:Top. closed_term(t) ([[t]] e s a1 tr ~ [[t]] e s a2 tr)

By: Analyze 0 THEN TermInd -1 THEN Unfold `term_mng` 0 THEN Reduce 0 THEN Try (Complete Auto) THEN Try (Fold `term_mng` 0) THEN RepeatFor 6 (Analyze 0)

Generated subgoals:

1 1. t: Term
2. u: TermType{i'}
3. w: t:{v:Term| u(v) }e,s,a1,a2,tr:Top. closed_term(t) ([[t]] e s a1 tr ~ [[t]] e s a2 tr)
4. x: Label
5. e: Top
6. s: Top
7. a1: Top
8. a2: Top
9. tr: Top
10. closed_term(x)
a1 ~ a2

2 1. t: Term
2. u: TermType{i'}
3. w: t:{v:Term| u(v) }e,s,a1,a2,tr:Top. closed_term(t) ([[t]] e s a1 tr ~ [[t]] e s a2 tr)
4. y1: {v:Term| u(v) }
5. y2: {v:Term| u(v) }
6. e: Top
7. s: Top
8. a1: Top
9. a2: Top
10. tr: Top
11. closed_term(y1 y2)
([[y1]] e s a1 tr([[y2]] e s a1 tr)) ~ ([[y1]] e s a2 tr([[y2]] e s a2 tr))

About:

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

1	1. `t:` `Term` 2. `u:` `TermType{i'}` 3. `w:` `t:{v:Term\| u(v) }e,s,a1,a2,tr:Top. closed_term(t) ([[t]] e s a1 tr ~ [[t]] e s a2 tr)` 4. `x:` `Label` 5. `e:` `Top` 6. `s:` `Top` 7. `a1:` `Top` 8. `a2:` `Top` 9. `tr:` `Top` 10. `closed_term(x)` `a1 ~ a2`
2	1. `t:` `Term` 2. `u:` `TermType{i'}` 3. `w:` `t:{v:Term\| u(v) }e,s,a1,a2,tr:Top. closed_term(t) ([[t]] e s a1 tr ~ [[t]] e s a2 tr)` 4. `y1:` `{v:Term\| u(v) }` 5. `y2:` `{v:Term\| u(v) }` 6. `e:` `Top` 7. `s:` `Top` 8. `a1:` `Top` 9. `a2:` `Top` 10. `tr:` `Top` 11. `closed_term(y1 y2)` `([[y1]] e s a1 tr([[y2]] e s a1 tr)) ~ ([[y1]] e s a2 tr([[y2]] e s a2 tr))`