Nuprl - Proof: member-es-before

(4steps total) PrintForm Definitions Lemmas mb event system 3 Sections EventSystems Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: member-es-before

the_es:ES, e',e:E. (e

before(e'))

(e <loc e')

By:	LocLessInd THEN Analyze 0 THEN RecUnfold `es-before` 0 THEN SplitOnConclITE

Generated subgoals:

1 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  nil)  (e <loc j)
1 step

2 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)
2 steps

About:

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

(4steps total) PrintForm Definitions Lemmas mb event system 3 Sections EventSystems Doc

1	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 nil) (e <loc j)	1 step
2	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)	2 steps