Nuprl - Proof: ma-single-effect0-feasible

(6steps 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: ma-single-effect0-feasible

x:Id, k:Knd, A,T:Type, f:(A

A).

Feasible(ma-single-effect0(x;A;k;T;f))

By:

Auto THEN AssertBY (x : A

x:Id fp-> Type) Auto
THEN
AssertBY (k : T

x:Knd fp-> Type) Auto
THEN
Unfold `ma-single-effect0` 0
THEN
BackThru
Thm*

x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Type,
Thm*

f:(State(ds)

ma-valtype(da; k)

ds(x)?Void).
Thm*

dom(ds). A=ds(x)

A
Thm*

Thm*

dom(da). A=da(k)

Feasible(ma-single-effect(ds; da; k; x; f))
THEN
Try (Complete Auto)

Generated subgoals:

1 1. x : Id
2. k : Knd
3. A : Type
4. T : Type
5. f : ATA
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
3 steps

2 1. x : Id
2. k : Knd
3. A : Type
4. T : Type
5. ATA
6. A
7. T
8. x : A  x:Id fp-> Type
9. k : T  x:Knd fp-> Type
  xdom(x : A). A=x : A(x)   A
1 step

3 1. x : Id
2. k : Knd
3. A : Type
4. T : Type
5. ATA
6. A
7. T
8. x : A  x:Id fp-> Type
9. k : T  x:Knd fp-> Type
  kdom(k : T). A=k : T(k)   A
1 step

About:

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

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

1	1. x : Id 2. k : Knd 3. A : Type 4. T : Type 5. f : ATA 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	3 steps
2	1. x : Id 2. k : Knd 3. A : Type 4. T : Type 5. ATA 6. A 7. T 8. x : A x:Id fp-> Type 9. k : T x:Knd fp-> Type xdom(x : A). A=x : A(x) A	1 step
3	1. x : Id 2. k : Knd 3. A : Type 4. T : Type 5. ATA 6. A 7. T 8. x : A x:Id fp-> Type 9. k : T x:Knd fp-> Type kdom(k : T). A=k : T(k) A	1 step