hereby :: thesis: ( ( x `1_3 = 9 implies ex b_{1} being SCM+FSA-State ex i being Integer ex k being Nat st

( k = |.(s . (x int_addr2)).| & i = (s . (x coll_addr1)) /. k & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr1),i)),((IC s) + 1)) ) ) & ( x `1_3 = 10 implies ex b_{1} 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))) & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),((IC s) + 1)) ) ) & ( x `1_3 = 11 implies ex b_{1} being SCM+FSA-State st b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr3),(len (s . (x coll_addr2))))),((IC s) + 1)) ) & ( x `1_3 = 12 implies ex b_{1} being SCM+FSA-State ex f being FinSequence of INT ex k being Nat st

( k = |.(s . (x int_addr3)).| & f = k |-> 0 & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr2),f)),((IC s) + 1)) ) ) & ( x `1_3 = 13 implies ex b_{1} being SCM+FSA-State ex i being Integer st

( i = 1 & b_{1} = 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 b_{1} being SCM+FSA-State st b_{1} = s ) )

( k = |.(s . (x int_addr2)).| & i = (s . (x coll_addr1)) /. k & b

( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & b

( k = |.(s . (x int_addr3)).| & f = k |-> 0 & b

( i = 1 & b

assume
x `1_3 <= 8
; :: thesis: ex s1 being SCM+FSA-State ex x9 being Element of SCM-Instr ex s9 being SCM-State st

( x = x9 & s9 = s | SCM-Memory & s1 = s +* (SCM-Exec-Res (x9,s9)) )

then reconsider x9 = x as Element of SCM-Instr by SCMFSA_I:2;

reconsider s9 = s | SCM-Memory as SCM-State by Th7;

reconsider s1 = s +* (SCM-Exec-Res (x9,s9)) as SCM+FSA-State by Th8;

take s1 = s1; :: thesis: ex x9 being Element of SCM-Instr ex s9 being SCM-State st

( x = x9 & s9 = s | SCM-Memory & s1 = s +* (SCM-Exec-Res (x9,s9)) )

take x9 = x9; :: thesis: ex s9 being SCM-State st

( x = x9 & s9 = s | SCM-Memory & s1 = s +* (SCM-Exec-Res (x9,s9)) )

take s9 = s9; :: thesis: ( x = x9 & s9 = s | SCM-Memory & s1 = s +* (SCM-Exec-Res (x9,s9)) )

thus x = x9 ; :: thesis: ( s9 = s | SCM-Memory & s1 = s +* (SCM-Exec-Res (x9,s9)) )

thus s9 = s | SCM-Memory ; :: thesis: s1 = s +* (SCM-Exec-Res (x9,s9))

thus s1 = s +* (SCM-Exec-Res (x9,s9)) ; :: thesis: verum

end;( x = x9 & s9 = s | SCM-Memory & s1 = s +* (SCM-Exec-Res (x9,s9)) )

then reconsider x9 = x as Element of SCM-Instr by SCMFSA_I:2;

reconsider s9 = s | SCM-Memory as SCM-State by Th7;

reconsider s1 = s +* (SCM-Exec-Res (x9,s9)) as SCM+FSA-State by Th8;

take s1 = s1; :: thesis: ex x9 being Element of SCM-Instr ex s9 being SCM-State st

( x = x9 & s9 = s | SCM-Memory & s1 = s +* (SCM-Exec-Res (x9,s9)) )

take x9 = x9; :: thesis: ex s9 being SCM-State st

( x = x9 & s9 = s | SCM-Memory & s1 = s +* (SCM-Exec-Res (x9,s9)) )

take s9 = s9; :: thesis: ( x = x9 & s9 = s | SCM-Memory & s1 = s +* (SCM-Exec-Res (x9,s9)) )

thus x = x9 ; :: thesis: ( s9 = s | SCM-Memory & s1 = s +* (SCM-Exec-Res (x9,s9)) )

thus s9 = s | SCM-Memory ; :: thesis: s1 = s +* (SCM-Exec-Res (x9,s9))

thus s1 = s +* (SCM-Exec-Res (x9,s9)) ; :: thesis: verum

hereby :: thesis: ( ( x `1_3 = 10 implies ex b_{1} 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))) & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),((IC s) + 1)) ) ) & ( x `1_3 = 11 implies ex b_{1} being SCM+FSA-State st b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr3),(len (s . (x coll_addr2))))),((IC s) + 1)) ) & ( x `1_3 = 12 implies ex b_{1} being SCM+FSA-State ex f being FinSequence of INT ex k being Nat st

( k = |.(s . (x int_addr3)).| & f = k |-> 0 & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr2),f)),((IC s) + 1)) ) ) & ( x `1_3 = 13 implies ex b_{1} being SCM+FSA-State ex i being Integer st

( i = 1 & b_{1} = 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 b_{1} being SCM+FSA-State st b_{1} = s ) )

( k = |.(s . (x int_addr2)).| & f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) & b

( k = |.(s . (x int_addr3)).| & f = k |-> 0 & b

( i = 1 & b

reconsider k = |.(s . (x int_addr2)).| as Nat ;

assume x `1_3 = 9 ; :: thesis: 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)); :: thesis: 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; :: thesis: 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; :: thesis: ( 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)) ) ; :: thesis: verum

end;assume x `1_3 = 9 ; :: thesis: 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)); :: thesis: 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; :: thesis: 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; :: thesis: ( 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)) ) ; :: thesis: verum

hereby :: thesis: ( ( x `1_3 = 11 implies ex b_{1} being SCM+FSA-State st b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr3),(len (s . (x coll_addr2))))),((IC s) + 1)) ) & ( x `1_3 = 12 implies ex b_{1} being SCM+FSA-State ex f being FinSequence of INT ex k being Nat st

( k = |.(s . (x int_addr3)).| & f = k |-> 0 & b_{1} = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr2),f)),((IC s) + 1)) ) ) & ( x `1_3 = 13 implies ex b_{1} being SCM+FSA-State ex i being Integer st

( i = 1 & b_{1} = 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 b_{1} being SCM+FSA-State st b_{1} = s ) )

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)) )
; :: thesis: ( ( x `1_3 = 12 implies ex b( k = |.(s . (x int_addr3)).| & f = k |-> 0 & b

( i = 1 & b

reconsider k = |.(s . (x int_addr2)).| as Nat ;

assume x `1_3 = 10 ; :: thesis: 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)) )

end;assume x `1_3 = 10 ; :: thesis: 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)) )
;

end;

suppose A1:
k in dom (s . (x coll_addr1))
; :: thesis: 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)) )

( 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)); :: thesis: 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; :: thesis: 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; :: thesis: ( 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)).| ; :: thesis: ( 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; :: thesis: 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)) ; :: thesis: verum

end;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)); :: thesis: 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; :: thesis: 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; :: thesis: ( 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)).| ; :: thesis: ( 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; :: thesis: 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)) ; :: thesis: verum

suppose A3:
not k in dom (s . (x coll_addr1))
; :: thesis: 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)) )

( 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)); :: thesis: 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; :: thesis: 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; :: thesis: ( 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)).| ; :: thesis: ( 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; :: thesis: 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)) ; :: thesis: verum

end;take s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),((IC s) + 1)); :: thesis: 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; :: thesis: 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; :: thesis: ( 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)).| ; :: thesis: ( 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; :: thesis: 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)) ; :: thesis: verum

( k = |.(s . (x int_addr3)).| & f = k |-> 0 & b

( i = 1 & b

hereby :: thesis: ( ( x `1_3 = 13 implies ex b_{1} being SCM+FSA-State ex i being Integer st

( i = 1 & b_{1} = 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 b_{1} being SCM+FSA-State st b_{1} = s ) )

( i = 1 & b

reconsider k = |.(s . (x int_addr3)).| as Nat ;

assume x `1_3 = 12 ; :: thesis: 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)); :: thesis: 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; :: thesis: 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; :: thesis: ( 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)) ) ; :: thesis: verum

end;assume x `1_3 = 12 ; :: thesis: 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)); :: thesis: 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; :: thesis: 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; :: thesis: ( 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)) ) ; :: thesis: verum

hereby :: thesis: ( 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 b_{1} being SCM+FSA-State st b_{1} = s )

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 bassume
x `1_3 = 13
; :: thesis: 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)); :: thesis: 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; :: thesis: ( 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)) ) ; :: thesis: verum

end;( 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)); :: thesis: 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; :: thesis: ( 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)) ) ; :: thesis: verum