Nuprl - Proof: recognizer1 realizes 2 2 1 2 1 1 2

(66steps 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: recognizer1 realizes 2 2 1 2 1 1 2

1. T : Type
2. A : Type
3. P : A

4. k : Knd
5. i : Id
6. r : Id
7. x : Id
8. A
9. T
10.

x = r
11. (

loc.

(recognizer1(loc;T;A;P;k;i;r;x)))

Dsys
12. D' : Dsys
13.

loc.

(recognizer1(loc;T;A;P;k;i;r;x))

D'
14. w : World
15. p : FairFifo
16. PossibleWorld(D';w)
17. vartype(i;r)

18.

e@i.first(e)

(r when e) = false

19.

e@i.

(r after e) = (r when e)

kind(e) = k
20. @i: ma-single-effect1(r;

;x;A;k;T;

r,x,v. P(x,v)

Dsys
21. vartype(i;r)

22. vartype(i;x)

r A
23.

e:E. loc(e) = i

kind(e) = k

(valtype(e)

r T)
24.

e:E.
24. loc(e) = i
24.

24. kind(e) = k

(r after e) = (P((x when e),val(e))

(r when e))

e'@i.

first(e')

e'@i.

((r after pred(e'))

(

((

e@0:E.

(((e@0 <loc pred(e'))

e@0 = pred(e')

((& kind(e@0) = k

Knd

((& P((x when e@0),val(e@0))))

((r after e')

(

((

e@0:E.

(((e@0 <loc e')

e@0 = e'

((& kind(e@0) = k

Knd

((& P((x when e@0),val(e@0))))

By:	All (Unfold `alle-at`) THEN Repeat (Analyze 0 THENA Complete Auto) THEN Analyze 0

Generated subgoals:

1 18. e:E. loc(e) = i  Id  first(e)  (r when e) = false
19. e:E. loc(e) = i  Id  (r after e) = (r when e)    kind(e) = k  Knd
20. @i: ma-single-effect1(r;;x;A;k;T;r,x,v. P(x,v)  r)  Dsys
21. vartype(i;r) r
22. vartype(i;x) r A
23. e:E. loc(e) = i  Id  kind(e) = k  Knd  (valtype(e) r T)
24. e:E.
24. loc(e) = i  Id
24.
24. kind(e) = k  Knd  (r after e) = (P((x when e),val(e))  (r when e))
25. e' : E
26. loc(e') = i  Id
27. first(e')
28. (r after pred(e'))
28.
28. (e@0:E.
28. ((e@0 <loc pred(e'))  e@0 = pred(e')  E
28. (& kind(e@0) = k  Knd
28. (& P((x when e@0),val(e@0)))
  (r after e')

  (e@0:E.
  ((e@0 <loc e')  e@0 = e' & kind(e@0) = k  Knd & P((x when e@0),val(e@0)))
33 steps

2 18. e:E. loc(e) = i  Id  first(e)  (r when e) = false
19. e:E. loc(e) = i  Id  (r after e) = (r when e)    kind(e) = k  Knd
20. @i: ma-single-effect1(r;;x;A;k;T;r,x,v. P(x,v)  r)  Dsys
21. vartype(i;r) r
22. vartype(i;x) r A
23. e:E. loc(e) = i  Id  kind(e) = k  Knd  (valtype(e) r T)
24. e:E.
24. loc(e) = i  Id
24.
24. kind(e) = k  Knd  (r after e) = (P((x when e),val(e))  (r when e))
25. e' : E
26. loc(e') = i  Id
27. first(e')
  ((r after pred(e'))
  (
  ((e@0:E.
  (((e@0 <loc pred(e'))  e@0 = pred(e')  E
  ((& kind(e@0) = k  Knd
  ((& P((x when e@0),val(e@0))))
   Prop
1 step

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

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

1	18. e:E. loc(e) = i Id first(e) (r when e) = false 19. e:E. loc(e) = i Id (r after e) = (r when e) kind(e) = k Knd 20. @i: ma-single-effect1(r;;x;A;k;T;r,x,v. P(x,v) r) Dsys 21. vartype(i;r) r 22. vartype(i;x) r A 23. e:E. loc(e) = i Id kind(e) = k Knd (valtype(e) r T) 24. e:E. 24. loc(e) = i Id 24. 24. kind(e) = k Knd (r after e) = (P((x when e),val(e)) (r when e)) 25. e' : E 26. loc(e') = i Id 27. first(e') 28. (r after pred(e')) 28. 28. (e@0:E. 28. ((e@0 <loc pred(e')) e@0 = pred(e') E 28. (& kind(e@0) = k Knd 28. (& P((x when e@0),val(e@0))) (r after e') (e@0:E. ((e@0 <loc e') e@0 = e' & kind(e@0) = k Knd & P((x when e@0),val(e@0)))	33 steps
2	18. e:E. loc(e) = i Id first(e) (r when e) = false 19. e:E. loc(e) = i Id (r after e) = (r when e) kind(e) = k Knd 20. @i: ma-single-effect1(r;;x;A;k;T;r,x,v. P(x,v) r) Dsys 21. vartype(i;r) r 22. vartype(i;x) r A 23. e:E. loc(e) = i Id kind(e) = k Knd (valtype(e) r T) 24. e:E. 24. loc(e) = i Id 24. 24. kind(e) = k Knd (r after e) = (P((x when e),val(e)) (r when e)) 25. e' : E 26. loc(e') = i Id 27. first(e') ((r after pred(e')) ( ((e@0:E. (((e@0 <loc pred(e')) e@0 = pred(e') E ((& kind(e@0) = k Knd ((& P((x when e@0),val(e@0)))) Prop	1 step