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

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

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

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

end;

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

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

end;

end;