(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 1 2 1 1
1. i : Id
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)
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
21. e1 : Id
22. e2 : 
23. isnull(a(1of(<e1,e2>);2of(<e1,e2>)))
24. e1 = i
25. t:, j:Id. first(<j,t>)  s(j;t).x = s(j;0).x
26. first(<e1,e2>)
27. s(e1;e2).x = s(e1;0).x
  s(e1;e2).x = v  T
By: ThinTrivial

Generated subgoal:

1 16. x@0:Id. 
16. deq-member(IdDeq;x@0;1of(1of(2of(2of(if eqof(IdDeq)(x,i)
16. deq-member(IdDeq;x@0;1of(1of(2of(2of(if <<[x],x.T>,,<[x],x.v>,,,,,,>
16. deq-member(IdDeq;x@0;1of(1of(2of(2of(else  fi)))))
16. 
16. s(x;0).x@0
16. =
16. 2of(1of(2of(2of(if eqof(IdDeq)(x,i) <<[x],x.T>,,<[x],x.v>,,,,,,>
16. 2of(1of(2of(2of(else  fi))))
16. (x@0)
16.  if deq-member(IdDeq;x@0;1of(1of(if eqof(IdDeq)(x,i)
16.  if deq-member(IdDeq;x@0;1of(1of(if <<[x],x.T>,,<[x],x.v>,,,,,,>
16.  if deq-member(IdDeq;x@0;1of(1of(else  fi)))
16.  if 2of(1of(if eqof(IdDeq)(x,i) <<[x],x.T>,,<[x],x.v>,,,,,,> else  fi))
16.  if (x@0)
16.  else Void fi
17. a:Action(x). 
17. isnull(a)
17. 
17. (valtype(x;a) r if eqof(IdDeq)(x,i) <<[x],x.T>,,<[x],x.v>,,,,,,>
17. (valtype(x;a) r else  fi.da(kind(a)))
18. x@0:Id. 
18. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if eqof(IdDeq)(x,i)
18. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if <<[x],x.T>
18. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
18. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,<[x],x.v>
18. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
18. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
18. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
18. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
18. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,
18. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,>
18. vartype(x;x@0) r if deq-member(IdDeq;x@0;1of(1of(else  fi)))
18. vartype(x;x@0) r if 2of(1of(if eqof(IdDeq)(x,i)
18. vartype(x;x@0) r if 2of(1of(if <<[x],x.T>,,<[x],x.v>,,,,,,>
18. vartype(x;x@0) r if 2of(1of(else  fi))
18. vartype(x;x@0) r if (x@0)
18. vartype(x;x@0) r else Top fi
19. vartype(i;x) r T
20. e1 : Id
21. e2 : 
22. isnull(a(1of(<e1,e2>);2of(<e1,e2>)))
23. e1 = i
24. t:, j:Id. first(<j,t>)  s(j;t).x = s(j;0).x  vartype(j;x)
25. first(<e1,e2>)
26. s(e1;e2).x = s(e1;0).x  vartype(e1;x)
27. s(i;0).x = v  T
  s(e1;e2).x = v  T
7 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