(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: effect-rule1
  i,x,y:Id, k:Knd, T,A,B:Type, f:(ABTA).
  y = x
  
  @i: ma-single-effect1(x;A;y;B;k;T;f)  Dsys
  & (D:Dsys. 
  & (@i: ma-single-effect1(x;A;y;B;k;T;f)  D
  & (
  & (D 
  & (realizes es.(vartype(i;x) r A) & (vartype(i;y) r B)
  & (realizes es.& (e:E. 
  & (realizes es.& (loc(e) = i  Id  kind(e) = k  Knd  (valtype(e) r T))
  & (realizes es.& (e:E. 
  & (realizes es.& (loc(e) = i  Id
  & (realizes es.& (
  & (realizes es.& (kind(e) = k  Knd
  & (realizes es.& (
  & (realizes es.& ((x after e) = f((x when e),(y when e),val(e))  A))
By: UnivCD THEN Unfold `ma-single-effect1` 0
THEN
AssertBY (x : A  y : B  x:Id fp-> Type) Auto
THEN
AssertBY (k : T  k:Knd fp-> Type) Auto
THEN
Inst Thm: s-effect-rule [i;x;k;x : A  y : B;k : T;s,v. f(s(x),s(y),v)]

Generated subgoals:

1 1. Id
2. x : Id
3. y : Id
4. k : Knd
5. T : Type
6. A : Type
7. B : Type
8. f : ABTA
9. y = x
10. x : A  y : B  x:Id fp-> Type
11. k : T  k:Knd fp-> Type
12. s : State(x : A  y : B)
13. v : ma-valtype(k : T; k)
  f(s(x),s(y),v)  x : A  y : B(x)?Void
15 steps
2 1. i : Id
2. x : Id
3. y : Id
4. k : Knd
5. T : Type
6. A : Type
7. B : Type
8. f : ABTA
9. y = x
10. x : A  y : B  x:Id fp-> Type
11. k : T  k:Knd fp-> Type
12. @i: ma-single-effect(x : A  y : B; k : T; k; x; (s,v. f(s(x),s(y),v)))
12.  Dsys
12. & (D:Dsys. 
12. & (@i: ma-single-effect(x : A  y : B; k : T; k; x; (s,v. f(s(x),s(y),v))
12. & (@i: ma-single-effect()  D
12. & (
12. & (D 
12. & (realizes es.(x@0:Id. vartype(i;x@0) r x : A  y : B(x@0)?Top)
12. & (realizes es.& (e:E. 
12. & (realizes es.& (loc(e) = i  Id
12. & (realizes es.& (
12. & (realizes es.& ((valtype(e) r ma-valtype(k : T; kind(e))))
12. & (realizes es.& (e:E. 
12. & (realizes es.& (loc(e) = i  Id
12. & (realizes es.& (
12. & (realizes es.& (kind(e) = k  Knd
12. & (realizes es.& (
12. & (realizes es.& ((x after e)
12. & (realizes es.& (=
12. & (realizes es.& ((s,v. f(s(x),s(y),v))((z.(z when e)),val(e))
12. & (realizes es.& ( x : A  y : B(x)?Top))
  @i: ma-single-effect(x : A  y : B; k : T; k; x; (s,v. f(s(x),s(y),v)))
   Dsys
  & (D:Dsys. 
  & (@i: ma-single-effect(x : A  y : B; k : T; k; x; (s,v. f(s(x),s(y),v))
  & (@i: ma-single-effect()  D
  & (
  & (D 
  & (realizes es.(vartype(i;x) r A) & (vartype(i;y) r B)
  & (realizes es.& (e:E. 
  & (realizes es.& (loc(e) = i  Id  kind(e) = k  Knd  (valtype(e) r T))
  & (realizes es.& (e:E. 
  & (realizes es.& (loc(e) = i  Id
  & (realizes es.& (
  & (realizes es.& (kind(e) = k  Knd
  & (realizes es.& (
  & (realizes es.& ((x after e) = f((x when e),(y when e),val(e))  A))
1 step

About:
voidlambdaapplyfunctionuniverseequal
membertopsubtype_relimpliesandall
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