Nuprl - Pf term primed vars term vars

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

x:Label, u:Term. (x term_primed_vars(u)) (x term_vars(u))

By: Analyze 0 THEN Analyze 0 THEN TermInd -1 THEN Reduce 0

Generated subgoals:

1 1. x: Label
2. u: Term
3. u1: TermType{i'}
4. w: u:{v:Term| u1(v) }(x term_primed_vars(u)) (x term_vars(u))
5. x2: Label
6. (x nil)
(x [x2])

2 1. x: Label
2. u: Term
3. u1: TermType{i'}
4. w: u:{v:Term| u1(v) }(x term_primed_vars(u)) (x term_vars(u))
5. y1: {v:Term| u1(v) }
6. y2: {v:Term| u1(v) }
7. (x term_primed_vars(y1) @ term_primed_vars(y2))
(x term_vars(y1) @ term_vars(y2))

About:

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

1	1. `x:` `Label` 2. `u:` `Term` 3. `u1:` `TermType{i'}` 4. `w:` `u:{v:Term\| u1(v) }(x term_primed_vars(u)) (x term_vars(u))` 5. `x2:` `Label` 6. `(x nil)` `(x [x2])`
2	1. `x:` `Label` 2. `u:` `Term` 3. `u1:` `TermType{i'}` 4. `w:` `u:{v:Term\| u1(v) }(x term_primed_vars(u)) (x term_vars(u))` 5. `y1:` `{v:Term\| u1(v) }` 6. `y2:` `{v:Term\| u1(v) }` 7. `(x term_primed_vars(y1) @ term_primed_vars(y2))` `(x term_vars(y1) @ term_vars(y2))`