(43steps total) PrintForm Definitions Lemmas mb event system 7 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: s-pre-init-rule1 2
1. i : Id
2. a : Id
3. x : Id
4. A : Type
5. T : Type
6. c : A
7. P : ATProp
8. (s,v. P(s(x),v))  State(x : A)TProp
  @i: (with ds: x : A
  @init: x : c
  action a:T
  aprecondition a(v) is
  as,v. P(s(x),v))
   Dsys
  & (D:Dsys. 
  & (@i: (with ds: x : A
  & (@init: x : c
  & (action a:T
  & (aprecondition a(v) is
  & (as,v. P(s(x),v))  D
  & (
  & (D 
  & (realizes es.(vartype(i;x) r A)
  & (realizes es.& (e:E. loc(e) = i  Id  first(e)  (x when e) = c  A)
  & (realizes es.& (e:E. 
  & (realizes es.& (loc(e) = i  Id
  & (realizes es.& (
  & (realizes es.& (kind(e) = locl(a)  Knd  (valtype(e) r T))
  & (realizes es.& (e:E. 
  & (realizes es.& (loc(e) = i  Id
  & (realizes es.& (
  & (realizes es.& (kind(e) = locl(a)  Knd  P((x when e),val(e)))
  & (realizes es.& & ((v:T. P(c,v))
  & (realizes es.& & (
  & (realizes es.& & ((e:E. 
  & (realizes es.& & ((loc(e) = i  Id
  & (realizes es.& & ((& kind(e) = locl(a)  Knd  (v:T. P((x after e),v)))))
By: AssertBY (x@0:Id. x@0  dom(x : A)  x@0  dom(x : c))
(Repeat (Unfolds [`fpf-dom`;`fpf-single`] 0 THEN Reduce 0))
THEN
Assert (x : c  x@0:Id fp-> x : A(x@0)?Void)

Generated subgoals:

1 9. x@0:Id. x@0  dom(x : A)  x@0  dom(x : c)
  x : c  x@0:Id fp-> x : A(x@0)?Void
1 step
2 9. x@0:Id. x@0  dom(x : A)  x@0  dom(x : c)
10. x : c  x@0:Id fp-> x : A(x@0)?Void
  @i: (with ds: x : A
  @init: x : c
  action a:T
  aprecondition a(v) is
  as,v. P(s(x),v))
   Dsys
  & (D:Dsys. 
  & (@i: (with ds: x : A
  & (@init: x : c
  & (action a:T
  & (aprecondition a(v) is
  & (as,v. P(s(x),v))  D
  & (
  & (D 
  & (realizes es.(vartype(i;x) r A)
  & (realizes es.& (e:E. loc(e) = i  Id  first(e)  (x when e) = c  A)
  & (realizes es.& (e:E. 
  & (realizes es.& (loc(e) = i  Id
  & (realizes es.& (
  & (realizes es.& (kind(e) = locl(a)  Knd  (valtype(e) r T))
  & (realizes es.& (e:E. 
  & (realizes es.& (loc(e) = i  Id
  & (realizes es.& (
  & (realizes es.& (kind(e) = locl(a)  Knd  P((x when e),val(e)))
  & (realizes es.& & ((v:T. P(c,v))
  & (realizes es.& & (
  & (realizes es.& & ((e:E. 
  & (realizes es.& & ((loc(e) = i  Id
  & (realizes es.& & ((& kind(e) = locl(a)  Knd  (v:T. P((x after e),v)))))
33 steps

About:
assertvoidlambdaapplyfunctionuniverseequalmember
subtype_relpropimpliesandorall
exists
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(43steps total) PrintForm Definitions Lemmas mb event system 7 Sections EventSystems Doc