hereby :: thesis:

assume InsCode x <= 8 ; :: thesis:
then reconsider x' = x as Element of SCM-Instr by Th3;
reconsider s' = (s | SCM-Memory ) +* (NAT --> x') as SCM-State by Th18;
reconsider s1 = (s +* (SCM-Exec-Res x',s')) +* (s | NAT ) as SCM+FSA-State by Th19;
take s1 = s1; :: thesis:
take x' = x'; :: thesis:
take s' = s'; :: thesis:
thus x = x' ; :: thesis:
thus s' = (s | SCM-Memory ) +* (NAT --> x') ; :: thesis:
thus s1 = (s +* (SCM-Exec-Res x',s')) +* (s | NAT ) ; :: thesis:

end;

hereby :: thesis:

assume InsCode x = 9 ; :: thesis:
reconsider k = abs (s . (x int_addr2 )) as Element of NAT ;
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:

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

per cases ;

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

then A2: {k} c= dom (s . (x coll_addr1 )) by ZFMISC_1:37;
set f = (s . (x coll_addr1 )) +* (k .--> (s . (x int_addr1 )));
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;
A3: rng f c= (rng (s . (x coll_addr1 ))) \/ (rng (k .--> (s . (x int_addr1 )))) by FUNCT_4:18;
A4: rng (s . (x coll_addr1 )) c= INT by FINSEQ_1:def 4;
A5: s . (x int_addr1 ) in INT by INT_1:def 2;
rng (k .--> (s . (x int_addr1 ))) = {(s . (x int_addr1 ))} by FUNCOP_1:14;
then rng (k .--> (s . (x int_addr1 ))) c= INT by A5, ZFMISC_1:37;
then (rng (s . (x coll_addr1 ))) \/ (rng (k .--> (s . (x int_addr1 )))) c= INT by A4, XBOOLE_1:8;
then rng f c= INT by A3, 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 A6: 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 A6, FUNCT_7:def 3; :: thesis:
thus s1 = SCM+FSA-Chg (SCM+FSA-Chg s,(x coll_addr1 ),f),(succ (IC s)) ; :: thesis:

end;

thus ( InsCode x = 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:

assume InsCode x = 12 ; :: thesis:
reconsider k = abs (s . (x int_addr3 )) as Element of NAT ;
k |-> 0 = (Seg k) --> 0 by FINSEQ_2:def 2;
then A7: rng (k |-> 0 ) c= {0 } by FUNCOP_1:19;
0 in INT by INT_1:def 2;
then {0 } c= INT by ZFMISC_1:37;
then rng (k |-> 0 ) c= INT by A7, 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 InsCode x <= 8 & not InsCode x = 9 & not InsCode x = 10 & not InsCode x = 11 & not InsCode x = 12 implies ex b₁ being SCM+FSA-State st b₁ = s ) ; :: thesis: