thus ( k > 0 implies ex f being FinPartState of SCM+FSA ex k1 being Element of NAT st
( k1 + 1 = k & f = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) ) :: thesis: ( not k > 0 implies ex b₁ being FinPartState of SCM+FSA ex k1 being Element of NAT st
( k1 + k = 1 & b₁ = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) )

proof

assume k > 0 ; :: thesis: ex f being FinPartState of SCM+FSA ex k1 being Element of NAT st
( k1 + 1 = k & f = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> )
then 0 + 1 <= k by INT_1:20;
then reconsider k1 = k - 1 as Element of NAT by INT_1:18;
set xx = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>;
reconsider xx = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> as FinPartState of SCM+FSA ;
take xx ; :: thesis: ex k1 being Element of NAT st
( k1 + 1 = k & xx = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> )
take k1 ; :: thesis: ( k1 + 1 = k & xx = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> )
thus k1 + 1 = k ; :: thesis: xx = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>
thus xx = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ; :: thesis: verum

end;

assume k <= 0 ; :: thesis: ex b₁ being FinPartState of SCM+FSA ex k1 being Element of NAT st
( k1 + k = 1 & b₁ = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> )
then reconsider k1 = 1 - k as Element of NAT by INT_1:18;
set xx = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>;
reconsider xx = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> as FinPartState of SCM+FSA ;
take xx ; :: thesis: ex k1 being Element of NAT st
( k1 + k = 1 & xx = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> )
take k1 ; :: thesis: ( k1 + k = 1 & xx = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> )
thus k1 + k = 1 ; :: thesis: xx = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>
thus xx = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ; :: thesis: verum