(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 2 1 1 1 1 2 1 1 2 1 1 1
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
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
11. @i: (with ds: x : A
11. @init: x : c
11. action a:T
11. aprecondition a(v) is
11. as,v. P(s(x),v))
11.  Dsys
12. D:Dsys. 
12. @i: (with ds: x : A
12. @init: x : c
12. action a:T
12. aprecondition a(v) is
12. as,v. P(s(x),v))  D
12. 
12. D 
12. realizes es.(v:T. (s,v. P(s(x),v))((x@0.x : c(x@0)?),v))
12. realizes es.
12. realizes es.(e:E. loc(e) = i)
13. @i: (with ds: x : A
13. @init: x : c
13. action a:T
13. aprecondition a(v) is
13. as,v. P(s(x),v))
13.  Dsys
14. @i: ma-single-pre1(x;A;a;T;x,v.P(x,v))  Dsys
15. D:Dsys. 
15. @i: ma-single-pre1(x;A;a;T;x,v.P(x,v))  D
15. 
15. D 
15. realizes es.(vartype(i;x) r A)
15. realizes es.& (e:E. loc(e) = i  kind(e) = locl(a)  (valtype(e) r T))
15. realizes es.& (e:E. 
15. realizes es.& (loc(e) = i
15. realizes es.& (
15. realizes es.& ((kind(e) = locl(a)  P((x when e),val(e)))
15. realizes es.& (& (e':E. 
15. realizes es.& (& ((e <loc e')  e = e'
15. realizes es.& (& (& kind(e') = locl(a)  (v:T. P((x after e'),v))))
16. D : Dsys
17. @i: (with ds: x : A
17. @init: x : c
17. action a:T
17. aprecondition a(v) is
17. as,v. P(s(x),v))  D
18. D 
18. realizes es.(vartype(i;x) r A)
18. realizes es.& (e:E. loc(e) = i  first(e)  (x when e) = c)
  a : s,v. P(s(x),v)  a : s,v. P(s(x),v)
By: Unfold `fpf-cap` 0
THEN
BackThru Thm* B:(AType), x:A, v:B(x), eqa:EqDecider(A). x : v  x : v
THEN
Try (Complete Auto)
THEN
Fold `fpf-cap` 0

Generated subgoals:

1 4. A : Type{i}
5. T : Type{i}
6. c : A
7. P : ATProp{i}
8. (s,v. P(s(x),v))  State(x : A)TProp{i}
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
11. @i: (with ds: x : A
11. @init: x : c
11. action a:T
11. aprecondition a(v) is
11. as,v. P(s(x),v))
11.  Dsys
12. D:Dsys. 
12. @i: (with ds: x : A
12. @init: x : c
12. action a:T
12. aprecondition a(v) is
12. as,v. P(s(x),v))  D
12. 
12. D 
12. realizes es.(v:T. (s,v. P(s(x),v))((x@0.x : c(x@0)?),v))
12. realizes es.
12. realizes es.(e:E. loc(e) = i  Id)
13. @i: (with ds: x : A
13. @init: x : c
13. action a:T
13. aprecondition a(v) is
13. as,v. P(s(x),v))
13.  Dsys
14. @i: ma-single-pre1(x;A;a;T;x,v.P(x,v))  Dsys
15. D:Dsys. 
15. @i: ma-single-pre1(x;A;a;T;x,v.P(x,v))  D
15. 
15. D 
15. realizes es.(vartype(i;x) r A)
15. realizes es.& (e:E. 
15. realizes es.& (loc(e) = i  Id
15. realizes es.& (
15. realizes es.& (kind(e) = locl(a)  Knd  (valtype(e) r T))
15. realizes es.& (e:E. 
15. realizes es.& (loc(e) = i  Id
15. realizes es.& (
15. realizes es.& ((kind(e) = locl(a)  Knd  P((x when e),val(e)))
15. realizes es.& (& (e':E. 
15. realizes es.& (& ((e <loc e')  e = e'  E
15. realizes es.& (& (& kind(e') = locl(a)  Knd  (v:T. P((x after e'),v))))
16. D : Dsys
17. @i: (with ds: x : A
17. @init: x : c
17. action a:T
17. aprecondition a(v) is
17. as,v. P(s(x),v))  D
18. D 
18. realizes es.(vartype(i;x) r A)
18. realizes es.& (e:E. loc(e) = i  Id  first(e)  (x when e) = c  A)
  (a@0.State(x : A)locl(a) : T(locl(a@0))?TopProp{i})  IdType{i'}
2 steps
2   (s,v. P(s(x),v))  State(x : A)locl(a) : T(locl(a))?TopProp
2 steps

About:
assertitvoidlambdaapplyfunctionuniverseequalmembertop
subtype_relpropimpliesandorallexists
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