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 consider k1 being Element of NAT such that
A1: k1 + 1 = k and
A2: a := k = Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) by Def2;
thus a := k = Load ((aSeq a,k) ^ <*(halt SCM+FSA )*>) by A1, A2, Def3; :: thesis: verum

end;

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

then consider k1 being Element of NAT such that
A4: k1 + k = 1 and
A5: a := k = Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) by Def2;
thus a := k = Load ((aSeq a,k) ^ <*(halt SCM+FSA )*>) by A3, A4, A5, Def3; :: thesis: verum

end;

end;