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

suppose k > 0 ; :: thesis: a := k is really-closed

then consider k1 being Nat such that
k1 + 1 = k and
A1: a := k = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA) by SCMFSA_7:def 1;
defpred S₁[ Nat] means (<%(a := (intloc 0))%> ^ (a --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA) is really-closed ;
(<%(a := (intloc 0))%> ^ (0 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA) = (<%(a := (intloc 0))%> ^ {}) ^ (Stop SCM+FSA)
.= <%(a := (intloc 0))%> ^ (Stop SCM+FSA)
.= Macro (a := (intloc 0)) ;
then (<%(a := (intloc 0))%> ^ (0 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA) is really-closed ;
then A2: S₁[ 0 ] ;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
set p1 = n --> (AddTo (a,(intloc 0)));

now :: thesis: <%(a := (intloc 0))%> ^ (n --> (AddTo (a,(intloc 0)))) is halt-free

per cases ( n is empty or not n is empty ) ;

suppose n is empty ; :: thesis: <%(a := (intloc 0))%> ^ (n --> (AddTo (a,(intloc 0)))) is halt-free

then n --> (AddTo (a,(intloc 0))) is empty ;
then <%(a := (intloc 0))%> ^ (n --> (AddTo (a,(intloc 0)))) = <%(a := (intloc 0))%> ;
hence <%(a := (intloc 0))%> ^ (n --> (AddTo (a,(intloc 0)))) is halt-free ; :: thesis: verum

end;

suppose A5: not n is empty ; :: thesis: <%(a := (intloc 0))%> ^ (n --> (AddTo (a,(intloc 0)))) is halt-free

then not n --> (AddTo (a,(intloc 0))) is empty ;
then reconsider pp = n --> (AddTo (a,(intloc 0))) as Program of ;
rng pp = {(AddTo (a,(intloc 0)))} by A5, FUNCOP_1:8;
then not halt SCM+FSA in rng pp by TARSKI:def 1;
then pp is halt-free by COMPOS_1:def 11;
hence <%(a := (intloc 0))%> ^ (n --> (AddTo (a,(intloc 0)))) is halt-free ; :: thesis: verum

end;

end;

end;

then reconsider p = <%(a := (intloc 0))%> ^ (n --> (AddTo (a,(intloc 0)))) as halt-free Program of ;
set m = (<%(a := (intloc 0))%> ^ (n --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA);
(<%(a := (intloc 0))%> ^ (n --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA) = stop p ;
then reconsider m = (<%(a := (intloc 0))%> ^ (n --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA) as really-closed MacroInstruction of SCM+FSA by A4;
A7: CutLastLoc m = <%(a := (intloc 0))%> ^ (n --> (AddTo (a,(intloc 0)))) by AFINSQ_2:83;
A8: card (CutLastLoc m) = (card m) -' 1 by VALUED_1:65;
(<%(a := (intloc 0))%> ^ ((Segm (n + 1)) --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA) = (<%(a := (intloc 0))%> ^ (((Segm n) --> (AddTo (a,(intloc 0)))) ^ <%(AddTo (a,(intloc 0)))%>)) ^ (Stop SCM+FSA) by AFINSQ_1:87
.= ((<%(a := (intloc 0))%> ^ (n --> (AddTo (a,(intloc 0))))) ^ <%(AddTo (a,(intloc 0)))%>) ^ (Stop SCM+FSA) by AFINSQ_1:27
.= (<%(a := (intloc 0))%> ^ (n --> (AddTo (a,(intloc 0))))) ^ (<%(AddTo (a,(intloc 0)))%> ^ (Stop SCM+FSA)) by AFINSQ_1:27
.= (<%(a := (intloc 0))%> ^ (n --> (AddTo (a,(intloc 0))))) ^ (Macro (AddTo (a,(intloc 0))))
.= (CutLastLoc m) +* (Shift ((Macro (AddTo (a,(intloc 0)))),((card m) -' 1))) by A7, A8, AFINSQ_1:77
.= (CutLastLoc m) +* (Shift ((Macro (IncAddr ((AddTo (a,(intloc 0))),((card m) -' 1)))),((card m) -' 1))) by COMPOS_0:4
.= (CutLastLoc m) +* (Shift ((IncAddr ((Macro (AddTo (a,(intloc 0)))),((card m) -' 1))),((card m) -' 1))) by COMPOS_1:74
.= (CutLastLoc m) +* (Reloc ((Macro (AddTo (a,(intloc 0)))),((card m) -' 1)))
.= m ';' (Macro (AddTo (a,(intloc 0))))
.= m ';' (AddTo (a,(intloc 0))) ;
then (<%(a := (intloc 0))%> ^ ((n + 1) --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA) is really-closed ;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
hence a := k is really-closed by A1; :: thesis: verum

end;

suppose k <= 0 ; :: thesis: a := k is really-closed

then consider k1 being Nat such that
k1 + k = 1 and
A9: a := k = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA) by SCMFSA_7:def 1;
defpred S₁[ Nat] means (<%(a := (intloc 0))%> ^ (a --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA) is really-closed ;
(<%(a := (intloc 0))%> ^ (0 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA) = (<%(a := (intloc 0))%> ^ {}) ^ (Stop SCM+FSA)
.= <%(a := (intloc 0))%> ^ (Stop SCM+FSA)
.= Macro (a := (intloc 0)) ;
then (<%(a := (intloc 0))%> ^ (0 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA) is really-closed ;
then A10: S₁[ 0 ] ;
A11: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A12: S₁[n] ; :: thesis: S₁[n + 1]
set p1 = n --> (SubFrom (a,(intloc 0)));

now :: thesis: <%(a := (intloc 0))%> ^ (n --> (SubFrom (a,(intloc 0)))) is halt-free

per cases ( n is empty or not n is empty ) ;

suppose n is empty ; :: thesis: <%(a := (intloc 0))%> ^ (n --> (SubFrom (a,(intloc 0)))) is halt-free

then n --> (SubFrom (a,(intloc 0))) is empty ;
then <%(a := (intloc 0))%> ^ (n --> (SubFrom (a,(intloc 0)))) = <%(a := (intloc 0))%> ;
hence <%(a := (intloc 0))%> ^ (n --> (SubFrom (a,(intloc 0)))) is halt-free ; :: thesis: verum

end;

suppose A13: not n is empty ; :: thesis: <%(a := (intloc 0))%> ^ (n --> (SubFrom (a,(intloc 0)))) is halt-free

then not n --> (SubFrom (a,(intloc 0))) is empty ;
then reconsider pp = n --> (SubFrom (a,(intloc 0))) as Program of ;
rng pp = {(SubFrom (a,(intloc 0)))} by A13, FUNCOP_1:8;
then not halt SCM+FSA in rng pp by TARSKI:def 1;
then pp is halt-free by COMPOS_1:def 11;
hence <%(a := (intloc 0))%> ^ (n --> (SubFrom (a,(intloc 0)))) is halt-free ; :: thesis: verum

end;

end;

end;

then reconsider p = <%(a := (intloc 0))%> ^ (n --> (SubFrom (a,(intloc 0)))) as halt-free Program of ;
set m = (<%(a := (intloc 0))%> ^ (n --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA);
(<%(a := (intloc 0))%> ^ (n --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA) = stop p ;
then reconsider m = (<%(a := (intloc 0))%> ^ (n --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA) as really-closed MacroInstruction of SCM+FSA by A12;
A15: CutLastLoc m = <%(a := (intloc 0))%> ^ (n --> (SubFrom (a,(intloc 0)))) by AFINSQ_2:83;
A16: card (CutLastLoc m) = (card m) -' 1 by VALUED_1:65;
(<%(a := (intloc 0))%> ^ ((Segm (n + 1)) --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA) = (<%(a := (intloc 0))%> ^ (((Segm n) --> (SubFrom (a,(intloc 0)))) ^ <%(SubFrom (a,(intloc 0)))%>)) ^ (Stop SCM+FSA) by AFINSQ_1:87
.= ((<%(a := (intloc 0))%> ^ (n --> (SubFrom (a,(intloc 0))))) ^ <%(SubFrom (a,(intloc 0)))%>) ^ (Stop SCM+FSA) by AFINSQ_1:27
.= (<%(a := (intloc 0))%> ^ (n --> (SubFrom (a,(intloc 0))))) ^ (<%(SubFrom (a,(intloc 0)))%> ^ (Stop SCM+FSA)) by AFINSQ_1:27
.= (<%(a := (intloc 0))%> ^ (n --> (SubFrom (a,(intloc 0))))) ^ (Macro (SubFrom (a,(intloc 0))))
.= (CutLastLoc m) +* (Shift ((Macro (SubFrom (a,(intloc 0)))),((card m) -' 1))) by A15, A16, AFINSQ_1:77
.= (CutLastLoc m) +* (Shift ((Macro (IncAddr ((SubFrom (a,(intloc 0))),((card m) -' 1)))),((card m) -' 1))) by COMPOS_0:4
.= (CutLastLoc m) +* (Shift ((IncAddr ((Macro (SubFrom (a,(intloc 0)))),((card m) -' 1))),((card m) -' 1))) by COMPOS_1:74
.= (CutLastLoc m) +* (Reloc ((Macro (SubFrom (a,(intloc 0)))),((card m) -' 1)))
.= m ';' (Macro (SubFrom (a,(intloc 0))))
.= m ';' (SubFrom (a,(intloc 0))) ;
then (<%(a := (intloc 0))%> ^ ((n + 1) --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA) is really-closed ;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A10, A11);
hence a := k is really-closed by A9; :: thesis: verum

end;

end;