T,T':Type, x:Id, c:T, a:Id, P:(T
T'Prop).
ma-single-pre-init1(x;T;c;a;T';x,v.P(x,v)) 
MsgA T,T':Type, x:Id, c:T, a:Id, P:(TT'Prop).
ma-single-pre-init1(x;T;c;a;T';x,v.P(x,v)) MsgA| By: |
THEN Analyze THEN Try (Complete Auto) |
| 1 |
2. T' : Type 3. x : Id 4. T 5. Id 6. P : T T'Prop
7. s : State(x : T) ( v.P(s(x),v)) T'Prop | 2 steps |
| 2 |
2. T' : Type 3. x : Id 4. T 5. Id 6. T T'Prop
(x@0.x : T(x@0)?Void) IdType | 1 step |
About:
 |  |  |  |  |  |  |  |