let a be Int-Location ; :: thesis: for k being Integer holds a := k = Load ((aSeq a,k) ^ <*(halt SCM+FSA )*>)
let k be Integer; :: thesis: a := k = Load ((aSeq a,k) ^ <*(halt SCM+FSA )*>)

per cases ( k > 0 or k <= 0 ) ;

suppose k > 0 ; :: thesis: a := k = Load ((aSeq a,k) ^ <*(halt SCM+FSA )*>)

then ex k1 being Element of NAT st
( k1 + 1 = k & a := k = Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) ) by Def2;
hence a := k = Load ((aSeq a,k) ^ <*(halt SCM+FSA )*>) by Def3; :: thesis: verum

end;

suppose A1: k <= 0 ; :: thesis: a := k = Load ((aSeq a,k) ^ <*(halt SCM+FSA )*>)

then ex k1 being Element of NAT st
( k1 + k = 1 & a := k = Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) ) by Def2;
hence a := k = Load ((aSeq a,k) ^ <*(halt SCM+FSA )*>) by A1, Def3; :: thesis: verum

end;

end;