Nuprl - Pf closed term mng2

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

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

By: Analyze 0 THEN TermInd -1 THEN Reduce 0 THEN Try (Complete Auto) THEN RepeatFor 7 (Analyze 0)

Generated subgoals:

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

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

About:

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