hereby ( ( x `1_3 = 9 implies ex b1 being SCM+FSA-State ex i being Integer ex k being Nat st
( k = |.(s . (x int_addr2)).| & i = (s . (x coll_addr1)) /. k & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr1),i)),((IC s) + 1)) ) ) & ( x `1_3 = 10 implies ex b1 being SCM+FSA-State ex f being FinSequence of INT ex k being Nat st
( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),((IC s) + 1)) ) ) & ( x `1_3 = 11 implies ex b1 being SCM+FSA-State st b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr3),(len (s . (x coll_addr2))))),((IC s) + 1)) ) & ( x `1_3 = 12 implies ex b1 being SCM+FSA-State ex f being FinSequence of INT ex k being Nat st
( k = |.(s . (x int_addr3)).| & f = k |-> 0 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr2),f)),((IC s) + 1)) ) ) & ( x `1_3 = 13 implies ex b1 being SCM+FSA-State ex i being Integer st
( i = 1 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),((IC s) + 1)) ) ) & ( not x `1_3 <= 8 & not x `1_3 = 9 & not x `1_3 = 10 & not x `1_3 = 11 & not x `1_3 = 12 & not x `1_3 = 13 implies ex b1 being SCM+FSA-State st b1 = s ) )
end;
hereby ( ( x `1_3 = 10 implies ex b1 being SCM+FSA-State ex f being FinSequence of INT ex k being Nat st
( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),((IC s) + 1)) ) ) & ( x `1_3 = 11 implies ex b1 being SCM+FSA-State st b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr3),(len (s . (x coll_addr2))))),((IC s) + 1)) ) & ( x `1_3 = 12 implies ex b1 being SCM+FSA-State ex f being FinSequence of INT ex k being Nat st
( k = |.(s . (x int_addr3)).| & f = k |-> 0 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr2),f)),((IC s) + 1)) ) ) & ( x `1_3 = 13 implies ex b1 being SCM+FSA-State ex i being Integer st
( i = 1 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),((IC s) + 1)) ) ) & ( not x `1_3 <= 8 & not x `1_3 = 9 & not x `1_3 = 10 & not x `1_3 = 11 & not x `1_3 = 12 & not x `1_3 = 13 implies ex b1 being SCM+FSA-State st b1 = s ) )
reconsider k =
|.(s . (x int_addr2)).| as
Nat ;
assume
x `1_3 = 9
;
ex s1 being SCM+FSA-State ex i being Integer ex k being Nat st
( k = |.(s . (x int_addr2)).| & i = (s . (x coll_addr1)) /. k & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr1),i)),((IC s) + 1)) )reconsider i =
(s . (x coll_addr1)) /. k as
Integer ;
take s1 =
SCM+FSA-Chg (
(SCM+FSA-Chg (s,(x int_addr1),i)),
((IC s) + 1));
ex i being Integer ex k being Nat st
( k = |.(s . (x int_addr2)).| & i = (s . (x coll_addr1)) /. k & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr1),i)),((IC s) + 1)) )take i =
i;
ex k being Nat st
( k = |.(s . (x int_addr2)).| & i = (s . (x coll_addr1)) /. k & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr1),i)),((IC s) + 1)) )take k =
k;
( k = |.(s . (x int_addr2)).| & i = (s . (x coll_addr1)) /. k & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr1),i)),((IC s) + 1)) )thus
(
k = |.(s . (x int_addr2)).| &
i = (s . (x coll_addr1)) /. k &
s1 = SCM+FSA-Chg (
(SCM+FSA-Chg (s,(x int_addr1),i)),
((IC s) + 1)) )
;
verum
end;
hereby ( ( x `1_3 = 11 implies ex b1 being SCM+FSA-State st b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr3),(len (s . (x coll_addr2))))),((IC s) + 1)) ) & ( x `1_3 = 12 implies ex b1 being SCM+FSA-State ex f being FinSequence of INT ex k being Nat st
( k = |.(s . (x int_addr3)).| & f = k |-> 0 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr2),f)),((IC s) + 1)) ) ) & ( x `1_3 = 13 implies ex b1 being SCM+FSA-State ex i being Integer st
( i = 1 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),((IC s) + 1)) ) ) & ( not x `1_3 <= 8 & not x `1_3 = 9 & not x `1_3 = 10 & not x `1_3 = 11 & not x `1_3 = 12 & not x `1_3 = 13 implies ex b1 being SCM+FSA-State st b1 = s ) )
reconsider k =
|.(s . (x int_addr2)).| as
Nat ;
assume
x `1_3 = 10
;
ex s1 being SCM+FSA-State ex f being FinSequence of INT ex k being Nat st
( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),((IC s) + 1)) )per cases
( k in dom (s . (x coll_addr1)) or not k in dom (s . (x coll_addr1)) )
;
suppose A1:
k in dom (s . (x coll_addr1))
;
ex s1 being SCM+FSA-State ex f being FinSequence of INT ex k being Nat st
( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),((IC s) + 1)) )set f =
(s . (x coll_addr1)) +* (k .--> (s . (x int_addr1)));
A2:
{k} c= dom (s . (x coll_addr1))
by A1, ZFMISC_1:31;
dom ((s . (x coll_addr1)) +* (k .--> (s . (x int_addr1)))) =
(dom (s . (x coll_addr1))) \/ (dom (k .--> (s . (x int_addr1))))
by FUNCT_4:def 1
.=
(dom (s . (x coll_addr1))) \/ {k}
.=
dom (s . (x coll_addr1))
by A2, XBOOLE_1:12
.=
Seg (len (s . (x coll_addr1)))
by FINSEQ_1:def 3
;
then reconsider f =
(s . (x coll_addr1)) +* (k .--> (s . (x int_addr1))) as
FinSequence by FINSEQ_1:def 2;
(
s . (x int_addr1) in INT &
rng (k .--> (s . (x int_addr1))) = {(s . (x int_addr1))} )
by FUNCOP_1:8, INT_1:def 2;
then
(
rng (s . (x coll_addr1)) c= INT &
rng (k .--> (s . (x int_addr1))) c= INT )
by FINSEQ_1:def 4, ZFMISC_1:31;
then
(
rng f c= (rng (s . (x coll_addr1))) \/ (rng (k .--> (s . (x int_addr1)))) &
(rng (s . (x coll_addr1))) \/ (rng (k .--> (s . (x int_addr1)))) c= INT )
by FUNCT_4:17, XBOOLE_1:8;
then
rng f c= INT
;
then reconsider f =
f as
FinSequence of
INT by FINSEQ_1:def 4;
take s1 =
SCM+FSA-Chg (
(SCM+FSA-Chg (s,(x coll_addr1),f)),
((IC s) + 1));
ex f being FinSequence of INT ex k being Nat st
( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),((IC s) + 1)) )take f =
f;
ex k being Nat st
( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),((IC s) + 1)) )take k =
k;
( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),((IC s) + 1)) )thus
k = |.(s . (x int_addr2)).|
;
( f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),((IC s) + 1)) )thus
f = (s . (x coll_addr1)) +* (
k,
(s . (x int_addr1)))
by A1, FUNCT_7:def 3;
s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),((IC s) + 1))thus
s1 = SCM+FSA-Chg (
(SCM+FSA-Chg (s,(x coll_addr1),f)),
((IC s) + 1))
;
verum end; suppose A3:
not
k in dom (s . (x coll_addr1))
;
ex s1 being SCM+FSA-State ex f being FinSequence of INT ex k being Nat st
( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),((IC s) + 1)) )reconsider f =
s . (x coll_addr1) as
FinSequence of
INT ;
take s1 =
SCM+FSA-Chg (
(SCM+FSA-Chg (s,(x coll_addr1),f)),
((IC s) + 1));
ex f being FinSequence of INT ex k being Nat st
( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),((IC s) + 1)) )take f =
f;
ex k being Nat st
( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),((IC s) + 1)) )take k =
k;
( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),((IC s) + 1)) )thus
k = |.(s . (x int_addr2)).|
;
( f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),((IC s) + 1)) )thus
f = (s . (x coll_addr1)) +* (
k,
(s . (x int_addr1)))
by A3, FUNCT_7:def 3;
s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),((IC s) + 1))thus
s1 = SCM+FSA-Chg (
(SCM+FSA-Chg (s,(x coll_addr1),f)),
((IC s) + 1))
;
verum end; end;
end;
thus
( x `1_3 = 11 implies ex s1 being SCM+FSA-State st s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr3),(len (s . (x coll_addr2))))),((IC s) + 1)) )
; ( ( x `1_3 = 12 implies ex b1 being SCM+FSA-State ex f being FinSequence of INT ex k being Nat st
( k = |.(s . (x int_addr3)).| & f = k |-> 0 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr2),f)),((IC s) + 1)) ) ) & ( x `1_3 = 13 implies ex b1 being SCM+FSA-State ex i being Integer st
( i = 1 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),((IC s) + 1)) ) ) & ( not x `1_3 <= 8 & not x `1_3 = 9 & not x `1_3 = 10 & not x `1_3 = 11 & not x `1_3 = 12 & not x `1_3 = 13 implies ex b1 being SCM+FSA-State st b1 = s ) )
hereby ( ( x `1_3 = 13 implies ex b1 being SCM+FSA-State ex i being Integer st
( i = 1 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),((IC s) + 1)) ) ) & ( not x `1_3 <= 8 & not x `1_3 = 9 & not x `1_3 = 10 & not x `1_3 = 11 & not x `1_3 = 12 & not x `1_3 = 13 implies ex b1 being SCM+FSA-State st b1 = s ) )
reconsider k =
|.(s . (x int_addr3)).| as
Nat ;
assume
x `1_3 = 12
;
ex s1 being SCM+FSA-State ex f being FinSequence of INT ex k being Nat st
( k = |.(s . (x int_addr3)).| & f = k |-> 0 & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr2),f)),((IC s) + 1)) )
0 in INT
by INT_1:def 2;
then A4:
{0} c= INT
by ZFMISC_1:31;
k |-> 0 = (Seg k) --> 0
by FINSEQ_2:def 2;
then
rng (k |-> 0) c= {0}
by FUNCOP_1:13;
then
rng (k |-> 0) c= INT
by A4;
then reconsider f =
k |-> 0 as
FinSequence of
INT by FINSEQ_1:def 4;
take s1 =
SCM+FSA-Chg (
(SCM+FSA-Chg (s,(x coll_addr2),f)),
((IC s) + 1));
ex f being FinSequence of INT ex k being Nat st
( k = |.(s . (x int_addr3)).| & f = k |-> 0 & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr2),f)),((IC s) + 1)) )take f =
f;
ex k being Nat st
( k = |.(s . (x int_addr3)).| & f = k |-> 0 & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr2),f)),((IC s) + 1)) )take k =
k;
( k = |.(s . (x int_addr3)).| & f = k |-> 0 & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr2),f)),((IC s) + 1)) )thus
(
k = |.(s . (x int_addr3)).| &
f = k |-> 0 &
s1 = SCM+FSA-Chg (
(SCM+FSA-Chg (s,(x coll_addr2),f)),
((IC s) + 1)) )
;
verum
end;
hereby ( not x `1_3 <= 8 & not x `1_3 = 9 & not x `1_3 = 10 & not x `1_3 = 11 & not x `1_3 = 12 & not x `1_3 = 13 implies ex b1 being SCM+FSA-State st b1 = s )
assume
x `1_3 = 13
;
ex s1 being SCM+FSA-State ex i being Integer st
( i = 1 & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),((IC s) + 1)) )reconsider i = 1 as
Integer ;
take s1 =
SCM+FSA-Chg (
(SCM+FSA-Chg (s,(x int_addr),i)),
((IC s) + 1));
ex i being Integer st
( i = 1 & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),((IC s) + 1)) )take i =
i;
( i = 1 & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),((IC s) + 1)) )thus
(
i = 1 &
s1 = SCM+FSA-Chg (
(SCM+FSA-Chg (s,(x int_addr),i)),
((IC s) + 1)) )
;
verum
end;
thus
( not x `1_3 <= 8 & not x `1_3 = 9 & not x `1_3 = 10 & not x `1_3 = 11 & not x `1_3 = 12 & not x `1_3 = 13 implies ex b1 being SCM+FSA-State st b1 = s )
; verum