(35steps 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: init-rule 2 1
1. i : Id
2. T : Type
3. v : T
4. x : Id
5. w : World
6. p : FairFifo
7. FairFifo
8. i@0,x@0:Id.
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if eqof(IdDeq)(i@0,i)
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if <<[x],x.T>
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,<[x],x.v>
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,>
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(else  fi)))
8. vartype(i@0;x@0) r if 2of(1of(if eqof(IdDeq)(i@0,i)
8. vartype(i@0;x@0) r if 2of(1of(if <<[x],x.T>,,<[x],x.v>,,,,,,>
8. vartype(i@0;x@0) r if 2of(1of(else  fi))
8. vartype(i@0;x@0) r if (x@0)
8. vartype(i@0;x@0) r else Top fi
9. i@0:Id, a:Action(i@0).
9. isnull(a)
9. 
9. (valtype(i@0;a) r if eqof(IdDeq)(i@0,i) <<[x],x.T>,,<[x],x.v>,,,,,,>
9. (valtype(i@0;a) r else  fi.da(kind(a)))
10. l:IdLnk, tg:Id.
10. (w.M(l,tg)) r if eqof(IdDeq)(source(l),i) <<[x],x.T>,,<[x],x.v>,,,,,,>
10. (w.M(l,tg)) r else  fi.da(rcv(l; tg))
11. i@0,x@0:Id.
11. deq-member(IdDeq;x@0;1of(1of(2of(2of(if eqof(IdDeq)(i@0,i)
11. deq-member(IdDeq;x@0;1of(1of(2of(2of(if <<[x],x.T>,,<[x],x.v>,,,,,,>
11. deq-member(IdDeq;x@0;1of(1of(2of(2of(else  fi)))))
11. 
11. s(i@0;0).x@0
11. =
11. 2of(1of(2of(2of(if eqof(IdDeq)(i@0,i) <<[x],x.T>,,<[x],x.v>,,,,,,>
11. 2of(1of(2of(2of(else  fi))))
11. (x@0)
12. x@0:Id. (eqof(IdDeq)(x,x@0)  false)  s(i;0).x@0 = v
13. a:Action(i). 
13. isnull(a)  (valtype(i;a) r <<[x],x.T>,,<[x],x.v>,,,,,,>.da(kind(a)))
14. x@0:Id. vartype(i;x@0) r if eqof(IdDeq)(x,x@0)  false T else Top fi
15. vartype(i;x) r T
16. True  s(i;0).x = v
17. x@0:Id. 
17. deq-member(IdDeq;x@0;1of(1of(2of(2of(if eqof(IdDeq)(x,i)
17. deq-member(IdDeq;x@0;1of(1of(2of(2of(if <<[x],x.T>,,<[x],x.v>,,,,,,>
17. deq-member(IdDeq;x@0;1of(1of(2of(2of(else  fi)))))
17. 
17. s(x;0).x@0
17. =
17. 2of(1of(2of(2of(if eqof(IdDeq)(x,i) <<[x],x.T>,,<[x],x.v>,,,,,,>
17. 2of(1of(2of(2of(else  fi))))
17. (x@0)
18. a:Action(x). 
18. isnull(a)
18. 
18. (valtype(x;a) r if eqof(IdDeq)(x,i) <<[x],x.T>,,<[x],x.v>,,,,,,>
18. (valtype(x;a) r else  fi.da(kind(a)))
19. x@0:Id. 
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if eqof(IdDeq)(x,i)
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if <<[x],x.T>
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,<[x],x.v>
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,>
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(else  fi)))
19. vartype(x;x@0) r if 2of(1of(if eqof(IdDeq)(x,i)
19. vartype(x;x@0) r if 2of(1of(if <<[x],x.T>,,<[x],x.v>,,,,,,>
19. vartype(x;x@0) r if 2of(1of(else  fi))
19. vartype(x;x@0) r if (x@0)
19. vartype(x;x@0) r else Top fi
20. vartype(i;x) r T
  e:E. loc(e) = i  Id  first(e)  (x when e) = v  T
By: Repeat (Unfolds [`es-E`;`es-loc`;`es-first`;`es-when`;`es-Loc`] 0 THEN Reduce 0)

Generated subgoal:

1 2. T : Type
3. v : T
4. x : Id
5. w : World
6. FairFifo
7. FairFifo
8. i@0,x@0:Id.
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if eqof(IdDeq)(i@0,i)
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if <<[x],x.T>
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,<[x],x.v>
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,>
8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(else  fi)))
8. vartype(i@0;x@0) r if 2of(1of(if eqof(IdDeq)(i@0,i)
8. vartype(i@0;x@0) r if 2of(1of(if <<[x],x.T>,,<[x],x.v>,,,,,,>
8. vartype(i@0;x@0) r if 2of(1of(else  fi))
8. vartype(i@0;x@0) r if (x@0)
8. vartype(i@0;x@0) r else Top fi
9. i@0:Id, a:Action(i@0).
9. isnull(a)
9. 
9. (valtype(i@0;a) r if eqof(IdDeq)(i@0,i) <<[x],x.T>,,<[x],x.v>,,,,,,>
9. (valtype(i@0;a) r else  fi.da(kind(a)))
10. l:IdLnk, tg:Id.
10. (w.M(l,tg)) r if eqof(IdDeq)(source(l),i) <<[x],x.T>,,<[x],x.v>,,,,,,>
10. (w.M(l,tg)) r else  fi.da(rcv(l; tg))
11. i@0,x@0:Id.
11. deq-member(IdDeq;x@0;1of(1of(2of(2of(if eqof(IdDeq)(i@0,i)
11. deq-member(IdDeq;x@0;1of(1of(2of(2of(if <<[x],x.T>,,<[x],x.v>,,,,,,>
11. deq-member(IdDeq;x@0;1of(1of(2of(2of(else  fi)))))
11. 
11. s(i@0;0).x@0
11. =
11. 2of(1of(2of(2of(if eqof(IdDeq)(i@0,i) <<[x],x.T>,,<[x],x.v>,,,,,,>
11. 2of(1of(2of(2of(else  fi))))
11. (x@0)
11.  if deq-member(IdDeq;x@0;1of(1of(if eqof(IdDeq)(i@0,i)
11.  if deq-member(IdDeq;x@0;1of(1of(if <<[x],x.T>,,<[x],x.v>,,,,,,>
11.  if deq-member(IdDeq;x@0;1of(1of(else  fi)))
11.  if 2of(1of(if eqof(IdDeq)(i@0,i) <<[x],x.T>,,<[x],x.v>,,,,,,>
11.  if 2of(1of(else  fi))
11.  if (x@0)
11.  else Void fi
12. x@0:Id. 
12. (eqof(IdDeq)(x,x@0)  false)
12. 
12. s(i;0).x@0 = v  if eqof(IdDeq)(x,x@0)  false T else Void fi
13. a:Action(i). 
13. isnull(a)  (valtype(i;a) r <<[x],x.T>,,<[x],x.v>,,,,,,>.da(kind(a)))
14. x@0:Id. vartype(i;x@0) r if eqof(IdDeq)(x,x@0)  false T else Top fi
15. vartype(i;x) r T
16. True  s(i;0).x = v  T
17. x@0:Id. 
17. deq-member(IdDeq;x@0;1of(1of(2of(2of(if eqof(IdDeq)(x,i)
17. deq-member(IdDeq;x@0;1of(1of(2of(2of(if <<[x],x.T>,,<[x],x.v>,,,,,,>
17. deq-member(IdDeq;x@0;1of(1of(2of(2of(else  fi)))))
17. 
17. s(x;0).x@0
17. =
17. 2of(1of(2of(2of(if eqof(IdDeq)(x,i) <<[x],x.T>,,<[x],x.v>,,,,,,>
17. 2of(1of(2of(2of(else  fi))))
17. (x@0)
17.  if deq-member(IdDeq;x@0;1of(1of(if eqof(IdDeq)(x,i)
17.  if deq-member(IdDeq;x@0;1of(1of(if <<[x],x.T>,,<[x],x.v>,,,,,,>
17.  if deq-member(IdDeq;x@0;1of(1of(else  fi)))
17.  if 2of(1of(if eqof(IdDeq)(x,i) <<[x],x.T>,,<[x],x.v>,,,,,,> else  fi))
17.  if (x@0)
17.  else Void fi
18. a:Action(x). 
18. isnull(a)
18. 
18. (valtype(x;a) r if eqof(IdDeq)(x,i) <<[x],x.T>,,<[x],x.v>,,,,,,>
18. (valtype(x;a) r else  fi.da(kind(a)))
19. x@0:Id. 
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if eqof(IdDeq)(x,i)
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if <<[x],x.T>
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,<[x],x.v>
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,>
19. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(else  fi)))
19. vartype(x;x@0) r if 2of(1of(if eqof(IdDeq)(x,i)
19. vartype(x;x@0) r if 2of(1of(if <<[x],x.T>,,<[x],x.v>,,,,,,>
19. vartype(x;x@0) r if 2of(1of(else  fi))
19. vartype(x;x@0) r if (x@0)
19. vartype(x;x@0) r else Top fi
20. vartype(i;x) r T
  e:E. loc(e) = i  Id  first(e)  (x when e) = v  T
28 steps

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

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