hereby :: thesis:

assume x `1_3 <= 8 ; :: thesis:
then reconsider x9 = x as Element of SCM-Instr by Th3;
reconsider s9 = s | SCM-Memory as SCM-State by Th18;
reconsider s1 = s +* (SCM-Exec-Res (x9,s9)) as SCM+FSA-State by Th19;
take s1 = s1; :: thesis:
take x9 = x9; :: thesis:
take s9 = s9; :: thesis:
thus x = x9 ; :: thesis:
thus s9 = s | SCM-Memory ; :: thesis:
thus s1 = s +* (SCM-Exec-Res (x9,s9)) ; :: thesis:

end;

hereby :: thesis:

reconsider k = abs (s . (x int_addr2)) as Element of NAT ;
assume x `1_3 = 9 ; :: thesis:
reconsider i = (s . (x coll_addr1)) /. k as Integer ;
take s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr1),i)),(succ (IC s))); :: thesis:
take i = i; :: thesis:
take k = k; :: thesis:
thus ( k = abs (s . (x int_addr2)) & i = (s . (x coll_addr1)) /. k & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr1),i)),(succ (IC s))) ) ; :: thesis:

end;

hereby :: thesis:

reconsider k = abs (s . (x int_addr2)) as Element of NAT ;
assume x `1_3 = 10 ; :: thesis:

suppose A1: k in dom (s . (x coll_addr1)) ; :: thesis:

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} by FUNCOP_1:13
.= 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 by XBOOLE_1:1;
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)),(succ (IC s))); :: thesis:
take f = f; :: thesis:
take k = k; :: thesis:
thus k = abs (s . (x int_addr2)) ; :: thesis:
thus f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) by A1, FUNCT_7:def 3; :: thesis:
thus s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),(succ (IC s))) ; :: thesis:

end;

suppose A3: not k in dom (s . (x coll_addr1)) ; :: thesis:

reconsider f = s . (x coll_addr1) as FinSequence of INT ;
take s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),(succ (IC s))); :: thesis:
take f = f; :: thesis:
take k = k; :: thesis:
thus k = abs (s . (x int_addr2)) ; :: thesis:
thus f = (s . (x coll_addr1)) +* (k,(s . (x int_addr1))) by A3, FUNCT_7:def 3; :: thesis:
thus s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr1),f)),(succ (IC s))) ; :: thesis:

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))))),(succ (IC s))) ) ; :: thesis:

hereby :: thesis:

reconsider k = abs (s . (x int_addr3)) as Element of NAT ;
assume x `1_3 = 12 ; :: thesis:
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, XBOOLE_1:1;
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)),(succ (IC s))); :: thesis:
take f = f; :: thesis:
take k = k; :: thesis:
thus ( k = abs (s . (x int_addr3)) & f = k |-> 0 & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x coll_addr2),f)),(succ (IC s))) ) ; :: thesis:

end;

hereby :: thesis:

assume x `1_3 = 13 ; :: thesis:
reconsider i = 1 as Integer ;
take s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),(succ (IC s))); :: thesis:
take i = i; :: thesis:
thus ( i = 1 & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(x int_addr),i)),(succ (IC s))) ) ; :: thesis:

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 b₁ being SCM+FSA-State st b₁ = s ) ; :: thesis: