thus ( k > 0 implies ex f being FinPartState of SCM+FSA ex k1 being Element of NAT st
( k1 + 1 = k & f = Load ((<*(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₁ = Load ((<*(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 = Load ((<*(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;
take Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) ; :: thesis: ex k1 being Element of NAT st
( k1 + 1 = k & Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) = Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) )
take k1 ; :: thesis: ( k1 + 1 = k & Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) = Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) )
thus k1 + 1 = k ; :: thesis: Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) = Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)
thus Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) = Load ((<*(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₁ = Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) )
then reconsider k1 = 1 - k as Element of NAT by INT_1:18;
take Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) ; :: thesis: ex k1 being Element of NAT st
( k1 + k = 1 & Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) = Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) )
take k1 ; :: thesis: ( k1 + k = 1 & Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) = Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) )
thus k1 + k = 1 ; :: thesis: Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) = Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)
thus Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) = Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) ; :: thesis: verum