Nuprl - Proof: s-pre-init-rule1 2 2 1 1 1 1 2 2 1 1 2

(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 2 1 1 2

1. i : Id
2. a : Id
3. x : Id
4. A : Type
5. T : Type
6. c : A
7. P : A

Prop
8. (

s,v. P(s(x),v))

State(x : A)

Prop
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. a

s,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. a

s,v. P(s(x),v))

D
12.

12. (

D':Dsys.
12. (D

D'
12. (

12. ((

w:World, p:FairFifo.
12. ((PossibleWorld(D';w)
12. ((

12. (((

v:T. (

s,v. P(s(x),v))((

x@0.x : c(x@0)?

),v))

(

e:E. loc(e) = i)))
13. D : Dsys
14. @i: (with ds: x : A
14. @init: x : c
14. action a:T
14. aprecondition a(v) is
14. a

s,v. P(s(x),v))

D
15.

D':Dsys.
15. D

D'
15.

15. (

w:World, p:FairFifo.
15. (PossibleWorld(D';w)
15. (

15. ((vartype(i;x)

r A) & (

e:E. loc(e) = i

first(e)

(x when e) = c))
16.

D':Dsys.
16. D

D'
16.

16. (

w:World, p:FairFifo.
16. (PossibleWorld(D';w)
16. (

16. ((vartype(i;x)

r A)
16. (& (

e:E. loc(e) = i

kind(e) = locl(a)

(valtype(e)

r T))
16. (& (

e:E.
16. (& (loc(e) = i
16. (& (

16. (& ((kind(e) = locl(a)

P((x when e),val(e)))
16. (& (& (

e':E.
16. (& (& ((e <loc e')

e = e'
16. (& (& (& kind(e') = locl(a)

(

v:T.

P((x after e'),v)))))
17.

D':Dsys.
17. D

D'
17.

17. (

w:World, p:FairFifo.
17. (PossibleWorld(D';w)
17. (

17. ((

v:T. (

s,v. P(s(x),v))((

x@0.x : c(x@0)?

),v))

(

e:E. loc(e) = i))
18. D' : Dsys
19. D

D'
20. w : World
21. p : FairFifo
22. PossibleWorld(D';w)
23. (vartype(i;x)

r A) & (

e:E. loc(e) = i

first(e)

(x when e) = c)
23. & (

e:E. loc(e) = i

kind(e) = locl(a)

(valtype(e)

r T))
24. (vartype(i;x)

r A) & (

e:E. loc(e) = i

first(e)

(x when e) = c)
24. & (

e:E. loc(e) = i

kind(e) = locl(a)

(valtype(e)

r T))
25. (vartype(i;x)

r A)
25. & (

e:E. loc(e) = i

kind(e) = locl(a)

(valtype(e)

r T))
25. & (

e:E.
25. & (loc(e) = i
25. & (

25. & ((kind(e) = locl(a)

P((x when e),val(e)))
25. & (& (

e':E.
25. & (& ((e <loc e')

e = e'
25. & (& (& kind(e') = locl(a)

(

v:T.

P((x after e'),v))))
26. (vartype(i;x)

r A) & (

e:E. loc(e) = i

first(e)

(x when e) = c)

(

e:E. loc(e) = i

kind(e) = locl(a)

P((x when e),val(e)))

& ((

v:T. P(c,v))

& (

& ((

e:E. loc(e) = i

Id & kind(e) = locl(a)

(

v:T.

P((x after e),v))))

By:	All Reduce THEN SplitAndHyps THEN BetterSplitAndConcl THEN Try Trivial

Generated subgoals:

1 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':Dsys.
12. (D  D'
12. (
12. ((w:World, p:FairFifo.
12. ((PossibleWorld(D';w)  (v:T. P(c,v))  (e:E. loc(e) = i  Id)))
13. D : Dsys
14. @i: (with ds: x : A
14. @init: x : c
14. action a:T
14. aprecondition a(v) is
14. as,v. P(s(x),v))  D
15. D':Dsys.
15. D  D'
15.
15. (w:World, p:FairFifo.
15. (PossibleWorld(D';w)
15. (
15. ((vartype(i;x) r A)
15. (& (e:E. loc(e) = i  Id  first(e)  (x when e) = c  A))
16. D':Dsys.
16. D  D'
16.
16. (w:World, p:FairFifo.
16. (PossibleWorld(D';w)
16. (
16. ((vartype(i;x) r A)
16. (& (e:E. loc(e) = i  Id  kind(e) = locl(a)  (valtype(e) r T))
16. (& (e:E.
16. (& (loc(e) = i  Id
16. (& (
16. (& ((kind(e) = locl(a)  P((x when e),val(e)))
16. (& (& (e':E.
16. (& (& ((e <loc e')  e = e'
16. (& (& (& kind(e') = locl(a)  (v:T. P((x after e'),v)))))
17. D':Dsys.
17. D  D'
17.
17. (w:World, p:FairFifo.
17. (PossibleWorld(D';w)  (v:T. P(c,v))  (e:E. loc(e) = i  Id))
18. D' : Dsys
19. D  D'
20. w : World
21. p : FairFifo
22. PossibleWorld(D';w)
23. vartype(i;x) r A
24. e:E. loc(e) = i  Id  first(e)  (x when e) = c  A
25. e:E. loc(e) = i  Id  kind(e) = locl(a)  (valtype(e) r T)
26. vartype(i;x) r A
27. e:E. loc(e) = i  Id  first(e)  (x when e) = c  A
28. e:E. loc(e) = i  Id  kind(e) = locl(a)  (valtype(e) r T)
29. vartype(i;x) r A
30. e:E. loc(e) = i  Id  kind(e) = locl(a)  (valtype(e) r T)
31. e:E.
31. loc(e) = i  Id
31.
31. (kind(e) = locl(a)  P((x when e),val(e)))
31. & (e':E.
31. & ((e <loc e')  e = e' & kind(e') = locl(a)  (v:T. P((x after e'),v)))
32. vartype(i;x) r A
33. e:E. loc(e) = i  Id  first(e)  (x when e) = c  A
  e:E. loc(e) = i  Id  kind(e) = locl(a)  P((x when e),val(e))
1 step

2 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':Dsys.
12. (D  D'
12. (
12. ((w:World, p:FairFifo.
12. ((PossibleWorld(D';w)  (v:T. P(c,v))  (e:E. loc(e) = i  Id)))
13. D : Dsys
14. @i: (with ds: x : A
14. @init: x : c
14. action a:T
14. aprecondition a(v) is
14. as,v. P(s(x),v))  D
15. D':Dsys.
15. D  D'
15.
15. (w:World, p:FairFifo.
15. (PossibleWorld(D';w)
15. (
15. ((vartype(i;x) r A)
15. (& (e:E. loc(e) = i  Id  first(e)  (x when e) = c  A))
16. D':Dsys.
16. D  D'
16.
16. (w:World, p:FairFifo.
16. (PossibleWorld(D';w)
16. (
16. ((vartype(i;x) r A)
16. (& (e:E. loc(e) = i  Id  kind(e) = locl(a)  (valtype(e) r T))
16. (& (e:E.
16. (& (loc(e) = i  Id
16. (& (
16. (& ((kind(e) = locl(a)  P((x when e),val(e)))
16. (& (& (e':E.
16. (& (& ((e <loc e')  e = e'
16. (& (& (& kind(e') = locl(a)  (v:T. P((x after e'),v)))))
17. D':Dsys.
17. D  D'
17.
17. (w:World, p:FairFifo.
17. (PossibleWorld(D';w)  (v:T. P(c,v))  (e:E. loc(e) = i  Id))
18. D' : Dsys
19. D  D'
20. w : World
21. p : FairFifo
22. PossibleWorld(D';w)
23. vartype(i;x) r A
24. e:E. loc(e) = i  Id  first(e)  (x when e) = c  A
25. e:E. loc(e) = i  Id  kind(e) = locl(a)  (valtype(e) r T)
26. vartype(i;x) r A
27. e:E. loc(e) = i  Id  first(e)  (x when e) = c  A
28. e:E. loc(e) = i  Id  kind(e) = locl(a)  (valtype(e) r T)
29. vartype(i;x) r A
30. e:E. loc(e) = i  Id  kind(e) = locl(a)  (valtype(e) r T)
31. e:E.
31. loc(e) = i  Id
31.
31. (kind(e) = locl(a)  P((x when e),val(e)))
31. & (e':E.
31. & ((e <loc e')  e = e' & kind(e') = locl(a)  (v:T. P((x after e'),v)))
32. vartype(i;x) r A
33. e:E. loc(e) = i  Id  first(e)  (x when e) = c  A
34. e:E. loc(e) = i  Id  kind(e) = locl(a)  P((x when e),val(e))
  (v:T. P(c,v))

  (e:E. loc(e) = i  Id & kind(e) = locl(a)  (v:T. P((x after e),v)))
5 steps

About:

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

1	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':Dsys. 12. (D D' 12. ( 12. ((w:World, p:FairFifo. 12. ((PossibleWorld(D';w) (v:T. P(c,v)) (e:E. loc(e) = i Id))) 13. D : Dsys 14. @i: (with ds: x : A 14. @init: x : c 14. action a:T 14. aprecondition a(v) is 14. as,v. P(s(x),v)) D 15. D':Dsys. 15. D D' 15. 15. (w:World, p:FairFifo. 15. (PossibleWorld(D';w) 15. ( 15. ((vartype(i;x) r A) 15. (& (e:E. loc(e) = i Id first(e) (x when e) = c A)) 16. D':Dsys. 16. D D' 16. 16. (w:World, p:FairFifo. 16. (PossibleWorld(D';w) 16. ( 16. ((vartype(i;x) r A) 16. (& (e:E. loc(e) = i Id kind(e) = locl(a) (valtype(e) r T)) 16. (& (e:E. 16. (& (loc(e) = i Id 16. (& ( 16. (& ((kind(e) = locl(a) P((x when e),val(e))) 16. (& (& (e':E. 16. (& (& ((e <loc e') e = e' 16. (& (& (& kind(e') = locl(a) (v:T. P((x after e'),v))))) 17. D':Dsys. 17. D D' 17. 17. (w:World, p:FairFifo. 17. (PossibleWorld(D';w) (v:T. P(c,v)) (e:E. loc(e) = i Id)) 18. D' : Dsys 19. D D' 20. w : World 21. p : FairFifo 22. PossibleWorld(D';w) 23. vartype(i;x) r A 24. e:E. loc(e) = i Id first(e) (x when e) = c A 25. e:E. loc(e) = i Id kind(e) = locl(a) (valtype(e) r T) 26. vartype(i;x) r A 27. e:E. loc(e) = i Id first(e) (x when e) = c A 28. e:E. loc(e) = i Id kind(e) = locl(a) (valtype(e) r T) 29. vartype(i;x) r A 30. e:E. loc(e) = i Id kind(e) = locl(a) (valtype(e) r T) 31. e:E. 31. loc(e) = i Id 31. 31. (kind(e) = locl(a) P((x when e),val(e))) 31. & (e':E. 31. & ((e <loc e') e = e' & kind(e') = locl(a) (v:T. P((x after e'),v))) 32. vartype(i;x) r A 33. e:E. loc(e) = i Id first(e) (x when e) = c A e:E. loc(e) = i Id kind(e) = locl(a) P((x when e),val(e))	1 step
2	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':Dsys. 12. (D D' 12. ( 12. ((w:World, p:FairFifo. 12. ((PossibleWorld(D';w) (v:T. P(c,v)) (e:E. loc(e) = i Id))) 13. D : Dsys 14. @i: (with ds: x : A 14. @init: x : c 14. action a:T 14. aprecondition a(v) is 14. as,v. P(s(x),v)) D 15. D':Dsys. 15. D D' 15. 15. (w:World, p:FairFifo. 15. (PossibleWorld(D';w) 15. ( 15. ((vartype(i;x) r A) 15. (& (e:E. loc(e) = i Id first(e) (x when e) = c A)) 16. D':Dsys. 16. D D' 16. 16. (w:World, p:FairFifo. 16. (PossibleWorld(D';w) 16. ( 16. ((vartype(i;x) r A) 16. (& (e:E. loc(e) = i Id kind(e) = locl(a) (valtype(e) r T)) 16. (& (e:E. 16. (& (loc(e) = i Id 16. (& ( 16. (& ((kind(e) = locl(a) P((x when e),val(e))) 16. (& (& (e':E. 16. (& (& ((e <loc e') e = e' 16. (& (& (& kind(e') = locl(a) (v:T. P((x after e'),v))))) 17. D':Dsys. 17. D D' 17. 17. (w:World, p:FairFifo. 17. (PossibleWorld(D';w) (v:T. P(c,v)) (e:E. loc(e) = i Id)) 18. D' : Dsys 19. D D' 20. w : World 21. p : FairFifo 22. PossibleWorld(D';w) 23. vartype(i;x) r A 24. e:E. loc(e) = i Id first(e) (x when e) = c A 25. e:E. loc(e) = i Id kind(e) = locl(a) (valtype(e) r T) 26. vartype(i;x) r A 27. e:E. loc(e) = i Id first(e) (x when e) = c A 28. e:E. loc(e) = i Id kind(e) = locl(a) (valtype(e) r T) 29. vartype(i;x) r A 30. e:E. loc(e) = i Id kind(e) = locl(a) (valtype(e) r T) 31. e:E. 31. loc(e) = i Id 31. 31. (kind(e) = locl(a) P((x when e),val(e))) 31. & (e':E. 31. & ((e <loc e') e = e' & kind(e') = locl(a) (v:T. P((x after e'),v))) 32. vartype(i;x) r A 33. e:E. loc(e) = i Id first(e) (x when e) = c A 34. e:E. loc(e) = i Id kind(e) = locl(a) P((x when e),val(e)) (v:T. P(c,v)) (e:E. loc(e) = i Id & kind(e) = locl(a) (v:T. P((x after e),v)))	5 steps