let a be Int-Location ; :: thesis: for k being Integer holds rng (aSeq a,k) c= {(a := (intloc 0 )),(AddTo a,(intloc 0 )),(SubFrom a,(intloc 0 ))}
let k be Integer; :: thesis: rng (aSeq a,k) c= {(a := (intloc 0 )),(AddTo a,(intloc 0 )),(SubFrom a,(intloc 0 ))}
now let x be
set ;
:: thesis: ( x in rng (aSeq a,k) implies b1 in {(a := (intloc 0 )),(AddTo a,(intloc 0 )),(SubFrom a,(intloc 0 ))} )assume A1:
x in rng (aSeq a,k)
;
:: thesis: b1 in {(a := (intloc 0 )),(AddTo a,(intloc 0 )),(SubFrom a,(intloc 0 ))}per cases
( ( k > 0 & k = 0 + 1 ) or ( k > 0 & k <> 1 ) or not k > 0 )
;
suppose A2:
(
k > 0 &
k = 0 + 1 )
;
:: thesis: b1 in {(a := (intloc 0 )),(AddTo a,(intloc 0 )),(SubFrom a,(intloc 0 ))}then consider k1 being
Element of
NAT such that A3:
k1 + 1
= k
and A4:
aSeq a,
k = <*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))
by SCMFSA_7:def 3;
aSeq a,
k =
<*(a := (intloc 0 ))*> ^ {}
by A2, A3, A4
.=
<*(a := (intloc 0 ))*>
by FINSEQ_1:47
;
then
rng (aSeq a,k) = {(a := (intloc 0 ))}
by FINSEQ_1:55;
then
x = a := (intloc 0 )
by A1, TARSKI:def 1;
hence
x in {(a := (intloc 0 )),(AddTo a,(intloc 0 )),(SubFrom a,(intloc 0 ))}
by ENUMSET1:def 1;
:: thesis: verum end; suppose A5:
(
k > 0 &
k <> 1 )
;
:: thesis: b1 in {(a := (intloc 0 )),(AddTo a,(intloc 0 )),(SubFrom a,(intloc 0 ))}then consider k1 being
Element of
NAT such that A6:
k1 + 1
= k
and A7:
aSeq a,
k = <*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))
by SCMFSA_7:def 3;
k1 <> 0
by A5, A6;
then A8:
k1 in Seg k1
by FINSEQ_1:5;
rng (aSeq a,k) =
(rng <*(a := (intloc 0 ))*>) \/ (rng (k1 |-> (AddTo a,(intloc 0 ))))
by A7, FINSEQ_1:44
.=
{(a := (intloc 0 ))} \/ (rng ((Seg k1) --> (AddTo a,(intloc 0 ))))
by FINSEQ_1:55
.=
{(a := (intloc 0 ))} \/ {(AddTo a,(intloc 0 ))}
by A8, FUNCOP_1:14
;
then
(
x in {(a := (intloc 0 ))} or
x in {(AddTo a,(intloc 0 ))} )
by A1, XBOOLE_0:def 3;
then
(
x = a := (intloc 0 ) or
x = AddTo a,
(intloc 0 ) )
by TARSKI:def 1;
hence
x in {(a := (intloc 0 )),(AddTo a,(intloc 0 )),(SubFrom a,(intloc 0 ))}
by ENUMSET1:def 1;
:: thesis: verum end; suppose A9:
not
k > 0
;
:: thesis: b1 in {(a := (intloc 0 )),(AddTo a,(intloc 0 )),(SubFrom a,(intloc 0 ))}then consider k1 being
Element of
NAT such that A10:
k1 + k = 1
and A11:
aSeq a,
k = <*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))
by SCMFSA_7:def 3;
k1 <> 0
by A9, A10;
then A12:
k1 in Seg k1
by FINSEQ_1:5;
rng (aSeq a,k) =
(rng <*(a := (intloc 0 ))*>) \/ (rng (k1 |-> (SubFrom a,(intloc 0 ))))
by A11, FINSEQ_1:44
.=
{(a := (intloc 0 ))} \/ (rng ((Seg k1) --> (SubFrom a,(intloc 0 ))))
by FINSEQ_1:55
.=
{(a := (intloc 0 ))} \/ {(SubFrom a,(intloc 0 ))}
by A12, FUNCOP_1:14
;
then
(
x in {(a := (intloc 0 ))} or
x in {(SubFrom a,(intloc 0 ))} )
by A1, XBOOLE_0:def 3;
then
(
x = a := (intloc 0 ) or
x = SubFrom a,
(intloc 0 ) )
by TARSKI:def 1;
hence
x in {(a := (intloc 0 )),(AddTo a,(intloc 0 )),(SubFrom a,(intloc 0 ))}
by ENUMSET1:def 1;
:: thesis: verum end; end;
hence
rng (aSeq a,k) c= {(a := (intloc 0 )),(AddTo a,(intloc 0 )),(SubFrom a,(intloc 0 ))}
by TARSKI:def 3; :: thesis: verum