hereby :: thesis: ( ( x `1_3 = 9 implies ex b1 being SCM+FSA-State ex i being Integer ex k being Nat st
( k = |.(s . ()).| & i = (s . ()) /. k & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),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 . ()).| & f = (s . ()) +* (k,(s . ())) & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) ) ) & ( x `1_3 = 11 implies ex b1 being SCM+FSA-State st b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),(len (s . ())))),((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 . ()).| & f = k |-> 0 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),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,(),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 ) )
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;
hereby :: thesis: ( ( x `1_3 = 10 implies ex b1 being SCM+FSA-State ex f being FinSequence of INT ex k being Nat st
( k = |.(s . ()).| & f = (s . ()) +* (k,(s . ())) & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) ) ) & ( x `1_3 = 11 implies ex b1 being SCM+FSA-State st b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),(len (s . ())))),((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 . ()).| & f = k |-> 0 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),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,(),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 . ()).| 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 . ()).| & i = (s . ()) /. k & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),i)),((IC s) + 1)) )

reconsider i = (s . ()) /. k as Integer ;
take s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),i)),((IC s) + 1)); :: thesis: ex i being Integer ex k being Nat st
( k = |.(s . ()).| & i = (s . ()) /. k & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),i)),((IC s) + 1)) )

take i = i; :: thesis: ex k being Nat st
( k = |.(s . ()).| & i = (s . ()) /. k & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),i)),((IC s) + 1)) )

take k = k; :: thesis: ( k = |.(s . ()).| & i = (s . ()) /. k & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),i)),((IC s) + 1)) )
thus ( k = |.(s . ()).| & i = (s . ()) /. k & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),i)),((IC s) + 1)) ) ; :: thesis: verum
end;
hereby :: thesis: ( ( x `1_3 = 11 implies ex b1 being SCM+FSA-State st b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),(len (s . ())))),((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 . ()).| & f = k |-> 0 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),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,(),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 . ()).| 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 . ()).| & f = (s . ()) +* (k,(s . ())) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) )

per cases ( k in dom (s . ()) or not k in dom (s . ()) ) ;
suppose A1: k in dom (s . ()) ; :: thesis: ex s1 being SCM+FSA-State ex f being FinSequence of INT ex k being Nat st
( k = |.(s . ()).| & f = (s . ()) +* (k,(s . ())) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) )

set f = (s . ()) +* (k .--> (s . ()));
A2: {k} c= dom (s . ()) by ;
dom ((s . ()) +* (k .--> (s . ()))) = (dom (s . ())) \/ (dom (k .--> (s . ()))) by FUNCT_4:def 1
.= (dom (s . ())) \/ {k}
.= dom (s . ()) by
.= Seg (len (s . ())) by FINSEQ_1:def 3 ;
then reconsider f = (s . ()) +* (k .--> (s . ())) as FinSequence by FINSEQ_1:def 2;
( s . () in INT & rng (k .--> (s . ())) = {(s . ())} ) by ;
then ( rng (s . ()) c= INT & rng (k .--> (s . ())) c= INT ) by ;
then ( rng f c= (rng (s . ())) \/ (rng (k .--> (s . ()))) & (rng (s . ())) \/ (rng (k .--> (s . ()))) c= INT ) by ;
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,(),f)),((IC s) + 1)); :: thesis: ex f being FinSequence of INT ex k being Nat st
( k = |.(s . ()).| & f = (s . ()) +* (k,(s . ())) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) )

take f = f; :: thesis: ex k being Nat st
( k = |.(s . ()).| & f = (s . ()) +* (k,(s . ())) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) )

take k = k; :: thesis: ( k = |.(s . ()).| & f = (s . ()) +* (k,(s . ())) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) )
thus k = |.(s . ()).| ; :: thesis: ( f = (s . ()) +* (k,(s . ())) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) )
thus f = (s . ()) +* (k,(s . ())) by ; :: thesis: s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1))
thus s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) ; :: thesis: verum
end;
suppose A3: not k in dom (s . ()) ; :: thesis: ex s1 being SCM+FSA-State ex f being FinSequence of INT ex k being Nat st
( k = |.(s . ()).| & f = (s . ()) +* (k,(s . ())) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) )

reconsider f = s . () as FinSequence of INT ;
take s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)); :: thesis: ex f being FinSequence of INT ex k being Nat st
( k = |.(s . ()).| & f = (s . ()) +* (k,(s . ())) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) )

take f = f; :: thesis: ex k being Nat st
( k = |.(s . ()).| & f = (s . ()) +* (k,(s . ())) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) )

take k = k; :: thesis: ( k = |.(s . ()).| & f = (s . ()) +* (k,(s . ())) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) )
thus k = |.(s . ()).| ; :: thesis: ( f = (s . ()) +* (k,(s . ())) & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) )
thus f = (s . ()) +* (k,(s . ())) by ; :: thesis: s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1))
thus s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) ; :: thesis: 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,(),(len (s . ())))),((IC s) + 1)) ) ; :: thesis: ( ( x `1_3 = 12 implies ex b1 being SCM+FSA-State ex f being FinSequence of INT ex k being Nat st
( k = |.(s . ()).| & f = k |-> 0 & b1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),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,(),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 :: thesis: ( ( 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,(),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 . ()).| 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 . ()).| & f = k |-> 0 & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),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= 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,(),f)),((IC s) + 1)); :: thesis: ex f being FinSequence of INT ex k being Nat st
( k = |.(s . ()).| & f = k |-> 0 & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) )

take f = f; :: thesis: ex k being Nat st
( k = |.(s . ()).| & f = k |-> 0 & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) )

take k = k; :: thesis: ( k = |.(s . ()).| & f = k |-> 0 & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) )
thus ( k = |.(s . ()).| & f = k |-> 0 & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),f)),((IC s) + 1)) ) ; :: thesis: verum
end;
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 b1 being SCM+FSA-State st b1 = s )
assume 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,(),i)),((IC s) + 1)) )

reconsider i = 1 as Integer ;
take s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),i)),((IC s) + 1)); :: thesis: ex i being Integer st
( i = 1 & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),i)),((IC s) + 1)) )

take i = i; :: thesis: ( i = 1 & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),i)),((IC s) + 1)) )
thus ( i = 1 & s1 = SCM+FSA-Chg ((SCM+FSA-Chg (s,(),i)),((IC s) + 1)) ) ; :: thesis: 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 ) ; :: thesis: verum