Nuprl - Proof: qsubx repst 1 1 1

(7steps total) PrintForm Definitions Lemmas ElisTarskiPf B Sections NuprlLIB Doc

1. t: Term
2. r: Term
3. t': Term
4. r': Term
5. t IN Term & ref(t) = t'
6. r IN Term & ref(r) = r'

SUBX(t; r) IN Term & ref(SUBX(t; r)) = t'/r'

By: OnHyps [6;5;0] Analyze

Generated subgoals:

1 5. t IN Term
6. ref(t) = t'
7. r IN Term
8. ref(r) = r'
SUBX(t; r) IN Term 1 step

2 5. t IN Term
6. ref(t) = t'
7. r IN Term
8. ref(r) = r'
9. SUBX(t; r) IN Term
ref(SUBX(t; r)) = t'/r' 2 steps

About:

(7steps total) PrintForm Definitions Lemmas ElisTarskiPf B Sections NuprlLIB Doc

1	5. `t IN Term` 6. `ref(t) = t'` 7. `r IN Term` 8. `ref(r) = r'` `SUBX(t; r) IN Term`	1 step

2	5. `t IN Term` 6. `ref(t) = t'` 7. `r IN Term` 8. `ref(r) = r'` 9. `SUBX(t; r) IN Term` `ref(SUBX(t; r)) = t'/r'`	2 steps