1. the_es : ES
2. WellFnd{i}(E;x,y.(x <loc y))
3. j : E
4. k:E. (k <loc j)  (e:E. (e  before(k))  (e <loc k))
5. e : E
6. first(j)
  (e  before(pred(j)) @ [pred(j)])  (e <loc j)

By:

InstHyp [pred(j);e] 4 THEN Try (BackThru Thm* the_es:ES, j:E. first(j)  (pred(j) <loc j)) THEN RWO Thm* the_es:ES, e,e':E. Thm* (e <loc e')  first(e') & e = pred(e')  E  (e <loc pred(e')) 0 THEN RWO Thm* x:T, l1,l2:T List. (x  l1 @ l2)  (x  l1)  (x  l2) 0 THEN RWO Thm* l:T List, a,x:T. (x  [a / l])  x = a  (x  l) 0 THEN RWO Thm* x:T. (x  nil)  False 0

1

7. (e  before(pred(j)))  (e <loc pred(j))   (e  before(pred(j)))  e = pred(j)  E  False      first(j) & e = pred(j)  E  (e <loc pred(j))

1 step

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