Nuprl - Proof: ma-single-effect0-feasible 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: ma-single-effect0-feasible 1

1. x : Id
2. k : Knd
3. A : Type
4. T : Type
5. f : A

A
6. A
7. T
8. x : A

x:Id fp-> Type
9. k : T

x:Knd fp-> Type

(

s,v. f(s(x),v))

State(x : A)

ma-valtype(k : T; k)

x : A(x)?Void

By:

Auto

Generated subgoals:

1 10. s : State(x : A)
11. ma-valtype(k : T; k)
s x@0:Idx : A(x@0)?Top
1 step

2 10. State(x : A)
11. v : ma-valtype(k : T; k)
v T
1 step

About:

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

1	10. s : State(x : A) 11. ma-valtype(k : T; k) s x@0:Idx : A(x@0)?Top	1 step
2	10. State(x : A) 11. v : ma-valtype(k : T; k) v T	1 step