(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
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. (True  (kind(a(i;e2))  L))  s(i;e2).x = s(i;e2+1).x
16. Dec((kind(a(e1;e2))  L))
  (s(e1;e2+1).x = s(e1;e2).x  T  (kind(a(e1;e2))  L))
  & ((kind(a(e1;e2))  L)  s(e1;e2+1).x = s(e1;e2).x  T)
By: Analyze -1 THEN Try (DoSubsume THEN Subst (e1 = i) 0)

Generated subgoals:

1 16. (kind(a(e1;e2))  L)
17. s(e1;e2+1).x = s(e1;e2).x  T
  (kind(a(e1;e2))  L)
4 steps
2 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  T
16. (kind(a(e1;e2))  L)
17. (kind(a(e1;e2))  L)
  s(e1;e2+1).x = s(e1;e2).x  T
3 steps

About:
listassertdecidablenatural_numberaddlambda
applyuniverseequalsubtype_relimpliesandtrue
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