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 S1[ 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: S1[ 0 ] ;
A3: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A4: S1[n] ; :: thesis: S1[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;
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 S1[n + 1] ; :: thesis: verum
end;
for n being Nat holds S1[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 S1[ 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: S1[ 0 ] ;
A11: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A12: S1[n] ; :: thesis: S1[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 ) ;
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 S1[n + 1] ; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A10, A11);
hence a := k is really-closed by A9; :: thesis: verum
end;
end;