Nuprl - Proof: int seg well founded down

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: int seg well founded down

, j:{i...}. WellFnd{u}({i..j

};x,y.x>y)

By:	Auto THEN FwdThru: Thm* r:(AAProp), B:Type, f:(BA). Thm* WellFnd{i}(A;x,y.r(x,y)) WellFnd{i}(B;x,y.r(f(x),f(y))) on [ WellFnd{u}({i...};x,y.x<y) ] Using:[B:= {i..j} \| f(x):= j+i-x]

Generated subgoals:

1 1. i :
2. {i...}
WellFnd{u}({i...};x,y.x<y)
1 step

2 1. i :
2. j : {i...}
3. WellFnd{u}({i..j};x,y.j+i-x<j+i-y)
WellFnd{u}({i..j};x,y.x>y)
1 step

About:

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

1	1. i : 2. {i...} WellFnd{u}({i...};x,y.x<y)	1 step
2	1. i : 2. j : {i...} 3. WellFnd{u}({i..j};x,y.j+i-x<j+i-y) WellFnd{u}({i..j};x,y.x>y)	1 step