thus ( k > 0 implies ex f being NAT -defined the InstructionsF of SCM+FSA -valued finite Function ex k1 being Nat st
( k1 + 1 = k & f = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA) ) ) :: thesis: ( not k > 0 implies ex b₁ being NAT -defined the InstructionsF of SCM+FSA -valued finite Function ex k1 being Nat st
( k1 + k = 1 & b₁ = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA) ) )

proof

assume k > 0 ; :: thesis: ex f being NAT -defined the InstructionsF of SCM+FSA -valued finite Function ex k1 being Nat st
( k1 + 1 = k & f = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA) )
then 0 + 1 <= k by INT_1:7;
then reconsider k1 = k - 1 as Element of NAT by INT_1:5;
set xx = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA);
reconsider xx = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA) as NAT -defined the InstructionsF of SCM+FSA -valued finite Function ;
take xx ; :: thesis: ex k1 being Nat st
( k1 + 1 = k & xx = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA) )
take k1 ; :: thesis: ( k1 + 1 = k & xx = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA) )
thus k1 + 1 = k ; :: thesis: xx = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA)
thus xx = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA) ; :: thesis: verum

end;

assume k <= 0 ; :: thesis: ex b₁ being NAT -defined the InstructionsF of SCM+FSA -valued finite Function ex k1 being Nat st
( k1 + k = 1 & b₁ = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA) )
then reconsider k1 = 1 - k as Element of NAT by INT_1:5;
set xx = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA);
reconsider xx = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA) as NAT -defined the InstructionsF of SCM+FSA -valued finite Function ;
take xx ; :: thesis: ex k1 being Nat st
( k1 + k = 1 & xx = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA) )
take k1 ; :: thesis: ( k1 + k = 1 & xx = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA) )
thus k1 + k = 1 ; :: thesis: xx = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA)
thus xx = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA) ; :: thesis: verum