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 b1 being FinSequence of the Instructions of SCM+FSA ex k1 being Element of NAT st
( k1 + k = 1 & b1 = <*(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 b1 being FinSequence of the Instructions of SCM+FSA ex k1 being Element of 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: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