hereby :: thesis:

assume x `1_3 <= 8 ; :: thesis:
then reconsider x9 = x as Element of SCM-Instr by Th3;
reconsider s9 = (s | SCM-Memory ) +* (NAT --> x9) as SCM-State by Th18;
reconsider s1 = (s +* (SCM-Exec-Res x9,s9)) +* (s | NAT ) 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 ) +* (NAT --> x9) ; :: thesis:
thus s1 = (s +* (SCM-Exec-Res x9,s9)) +* (s | NAT ) ; :: 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:37;
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:19
.= 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:14, 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:37;
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:18, 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:37;
k |-> 0 = (Seg k) --> 0 by FINSEQ_2:def 2;
then rng (k |-> 0 ) c= {0 } by FUNCOP_1:19;
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;

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