Nuprl - Proof: inv image ind tp 1 1 1 1 1 1 2 1 1 1

(32steps total) PrintForm Definitions well fnd Sections StandardLIB Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: inv image ind tp 1 1 1 1 1 1 2 1 1 1

1. T : Type
2. r : T

Prop
3. S : Type
4. f : S

T
5. WellFnd{i}(T;x,y.r(x,y))
6. P : S

Prop
7.

j:S. (

k:S. r(f(k),f(j))

P(k))

P(j)
8. j : T
9.

k:T. r(k,j)

(

n:S. f(n) = k

P(n))
10. n : S
11. f(n) = j
12. nn : S
13. r(f(nn),f(n))

P(nn)

By:	p. let yy var_of_hyp -2 p , let r get_term_arg `f` p , let r_yy mk_apply_term r (mvt yy) in ((DTerm r_yy -5) THEN (Analyze -1) THEN (DTerm (mvt yy) -1) THEN (Analyze -1) (THEN ((NthHyp -1)) p

Generated subgoals:

1 9. n : S
10. f(n) = j
11. nn : S
12. r(f(nn),f(n))
  f(nn)  T
1 step

2 9. n : S
10. f(n) = j
11. nn : S
12. r(f(nn),f(n))
  r(f(nn),j)
3 steps

3 9. n : S
10. f(n) = j
11. nn : S
12. r(f(nn),f(n))
  nn  S
1 step

4 9. n : S
10. f(n) = j
11. nn : S
12. r(f(nn),f(n))
  f(nn) = f(nn)
1 step

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(32steps total) PrintForm Definitions well fnd Sections StandardLIB Doc

1	9. n : S 10. f(n) = j 11. nn : S 12. r(f(nn),f(n)) f(nn) T	1 step
2	9. n : S 10. f(n) = j 11. nn : S 12. r(f(nn),f(n)) r(f(nn),j)	3 steps
3	9. n : S 10. f(n) = j 11. nn : S 12. r(f(nn),f(n)) nn S	1 step
4	9. n : S 10. f(n) = j 11. nn : S 12. r(f(nn),f(n)) f(nn) = f(nn)	1 step