Nuprl - Proof: frame-rule 2 1 2 1 1 2 2

(17steps total) PrintForm Definitions Lemmas mb event system 6 Sections EventSystems Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: frame-rule 2 1 2 1 1 2 2

1. i : Id
2. L : Knd List
3. x : Id
4. T : Type
5. w : World
6. FairFifo
7. FairFifo
8. vartype(i;x)

r T
9. e1 : Id
10. e2 :

11.

isnull(a(e1;e2))
12. e1 = i
13.

isnull(a(i;e2))
14. islocal(kind(a(i;e2)))
14.

14. deq-member(IdDeq;act(kind(a(i;e2)));1of())
14.

14. 2of()(act(kind(a(i;e2))),

x.s(i;e2).x,val(a(i;e2)))
15.

(True

(kind(a(i;e2))

L))

s(i;e2).x = s(i;e2+1).x
16.

(kind(a(e1;e2))

L)
17.

(kind(a(e1;e2))

s(e1;e2+1).x = s(e1;e2).x

By:	Analyze -3

Generated subgoals:

1 15. (kind(a(e1;e2))  L)
16. (kind(a(e1;e2))  L)
  (True  (kind(a(i;e2))  L))
1 step

2 15. (kind(a(e1;e2))  L)
16. (kind(a(e1;e2))  L)
17. s(i;e2).x = s(i;e2+1).x  T
  s(e1;e2+1).x = s(e1;e2).x  T
1 step

About:

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

(17steps total) PrintForm Definitions Lemmas mb event system 6 Sections EventSystems Doc

1	15. (kind(a(e1;e2)) L) 16. (kind(a(e1;e2)) L) (True (kind(a(i;e2)) L))	1 step
2	15. (kind(a(e1;e2)) L) 16. (kind(a(e1;e2)) L) 17. s(i;e2).x = s(i;e2+1).x T s(e1;e2+1).x = s(e1;e2).x T	1 step