thus ( k > 0 implies ex s being FinSequence of the Instructions of SCM+FSA ex k1 being Element of NAT st
( k1 + 1 = k & s = <*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 ))) ) ) :: thesis: ( not k > 0 implies ex b₁ being FinSequence of the Instructions of SCM+FSA ex k1 being Element of NAT st
( k1 + k = 1 & b₁ = <*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 ))) ) )

proof

assume k > 0 ; :: thesis: ex s being FinSequence of the Instructions of SCM+FSA ex k1 being Element of NAT st
( k1 + 1 = k & s = <*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 ))) )
then 0 + 1 <= k by INT_1:20;
then reconsider k1 = k - 1 as Element of NAT by INT_1:18;
take <*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 ))) ; :: thesis: ex k1 being Element of NAT st
( k1 + 1 = k & <*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 ))) = <*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 ))) )
take k1 ; :: thesis: ( k1 + 1 = k & <*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 ))) = <*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 ))) )
thus k1 + 1 = k ; :: thesis: <*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 ))) = <*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))
thus <*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 ))) = <*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 ))) ; :: thesis: verum

end;

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