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

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

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)) [not for witness]
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.

(kind(a(e1;e2))

L)
16.

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

(True

(kind(a(i;e2))

L))

By:	Analyze 0 THEN ThinTrivial THEN Analyze -3 THEN NthHypEq -1 THEN Repeat Analyze

Generated subgoals:

None

About:

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