thus ( k > 0 implies ex s being XFinSequence of the InstructionsF of SCM+FSA ex k1 being Nat st
( k1 + 1 = k & s = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) ) ) :: thesis: ( not k > 0 implies ex b1 being XFinSequence of the InstructionsF of SCM+FSA ex k1 being Nat st
( k1 + k = 1 & b1 = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) ) )
proof
assume k > 0 ; :: thesis: ex s being XFinSequence of the InstructionsF of SCM+FSA ex k1 being Nat st
( k1 + 1 = k & s = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) )
then 0 + 1 <= k by INT_1:7;
then reconsider k1 = k - 1 as Element of NAT by INT_1:5;
take <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) ; :: thesis: ex k1 being 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 b1 being XFinSequence of the InstructionsF of SCM+FSA ex k1 being Nat st
( k1 + k = 1 & b1 = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) )
then reconsider k1 = 1 - k as Element of NAT by INT_1:5;
take <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) ; :: thesis: ex k1 being 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