JumpPart (halt SCM+FSA) is empty by LmX, RECDEF_2:def 2;
then halt SCM+FSA is ins-loc-free by COMPOS_1:def 37;
hence SCM+FSA is proper-halt by COMPOS_1:def 39; :: thesis: ( SCM+FSA is realistic & SCM+FSA is IC-Ins-separated & SCM+FSA is definite & SCM+FSA is steady-programmed )
thus SCM+FSA is realistic :: thesis: ( SCM+FSA is IC-Ins-separated & SCM+FSA is definite & SCM+FSA is steady-programmed )

proof

assume the Instruction-Counter of SCM+FSA in NAT ; :: according to COMPOS_1:def 12 :: thesis: contradiction
hence contradiction by FUNCT_7:def 1, SCMFSA_1:5; :: thesis: verum

end;

ObjectKind (IC SCM+FSA) = NAT by FUNCT_7:def 1, SCMFSA_1:5, SCMFSA_1:9;
hence SCM+FSA is IC-Ins-separated by COMPOS_1:def 6; :: thesis: ( SCM+FSA is definite & SCM+FSA is steady-programmed )
thus SCM+FSA is definite :: thesis: SCM+FSA is steady-programmed

proof

let l be Element of NAT ; :: according to COMPOS_1:def 8 :: thesis: the Object-Kind of SCM+FSA . l = the Instructions of SCM+FSA
thus the Object-Kind of SCM+FSA . l = the Instructions of SCM+FSA by SCMFSA_1:11; :: thesis: verum

end;

let s be State of SCM+FSA; :: according to AMI_1:def 13 :: thesis: for b₁ being Element of the Instructions of SCM+FSA
for b₂ being Element of NAT holds (Exec (b₁,s)) . b₂ = s . b₂
let i be Instruction of SCM+FSA; :: thesis: for b₁ being Element of NAT holds (Exec (i,s)) . b₁ = s . b₁
let l be Element of NAT ; :: thesis: (Exec (i,s)) . l = s . l
A1: ( i in SCM-Instr \/ { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13, dB, dA is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : L in {9,10} } or i in { [K,{},<*dC,fB*>] where K is Element of Segm 13, dC is Element of SCM+FSA-Data-Loc , fB is Element of SCM+FSA-Data*-Loc : K in {11,12} } ) by XBOOLE_0:def 3;
reconsider l9 = l as Element of NAT ;
reconsider S = s as Element of product SCM+FSA-OK by PBOOLE:155;
reconsider I = i as Element of SCM+FSA-Instr ;

per cases ( i in SCM-Instr or i in { [J,{},<*dB,fA,dA*>] where J is Element of Segm 13, dB, dA is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : J in {9,10} } or i in { [K,{},<*dC,fB*>] where K is Element of Segm 13, dC is Element of SCM+FSA-Data-Loc , fB is Element of SCM+FSA-Data*-Loc : K in {11,12} } ) by A1, XBOOLE_0:def 3;

suppose i in SCM-Instr ; :: thesis: (Exec (i,s)) . l = s . l

then reconsider I = i as Instruction of SCM ;
reconsider S = (s | SCM-Memory) +* (NAT --> I) as State of SCM by Th73;
dom s = the carrier of SCM+FSA by PARTFUN1:def 4
.= (({NAT} \/ SCM+FSA-Data-Loc) \/ SCM+FSA-Data*-Loc) \/ NAT by SCMFSA_1:8 ;
then ( dom (s | NAT) = (dom s) /\ NAT & l in dom s ) by RELAT_1:90, XBOOLE_0:def 3;
then A3: l in dom (s | NAT) by XBOOLE_0:def 4;
thus (Exec (i,s)) . l = ((s +* (Exec (I,S))) +* (s | NAT)) . l by Th75
.= (s | NAT) . l by A3, FUNCT_4:14
.= s . l by A3, FUNCT_1:70 ; :: thesis: verum

end;

suppose i in { [J,{},<*dB,fA,dA*>] where J is Element of Segm 13, dB, dA is Element of SCM+FSA-Data-Loc , fA is Element of SCM+FSA-Data*-Loc : J in {9,10} } ; :: thesis: (Exec (i,s)) . l = s . l

then consider J being Element of Segm 13, dB, dA being Element of SCM+FSA-Data-Loc , fA being Element of SCM+FSA-Data*-Loc such that
A4: i = [J,{},<*dB,fA,dA*>] and
A5: J in {9,10} ;

now

per cases ( J = 9 or J = 10 ) by A5, TARSKI:def 2;

suppose J = 9 ; :: thesis: (SCM+FSA-Exec-Res (I,S)) . l9 = S . l9

then InsCode I = 9 by A4, RECDEF_2:def 1;
then consider i being Integer, k being Element of NAT such that
k = abs (S . (I int_addr2)) and
i = (S . (I coll_addr1)) /. k and
A6: SCM+FSA-Exec-Res (I,S) = SCM+FSA-Chg ((SCM+FSA-Chg (S,(I int_addr1),i)),(succ (IC S))) by SCMFSA_1:def 17;
thus (SCM+FSA-Exec-Res (I,S)) . l9 = (SCM+FSA-Chg (S,(I int_addr1),i)) . l9 by A6, SCMFSA_1:23
.= S . l9 by SCMFSA_1:28 ; :: thesis: verum

end;

suppose J = 10 ; :: thesis: (SCM+FSA-Exec-Res (I,S)) . l9 = S . l9

then InsCode I = 10 by A4, RECDEF_2:def 1;
then consider f being FinSequence of INT , k being Element of NAT such that
k = abs (S . (I int_addr2)) and
f = (S . (I coll_addr1)) +* (k,(S . (I int_addr1))) and
A7: SCM+FSA-Exec-Res (I,S) = SCM+FSA-Chg ((SCM+FSA-Chg (S,(I coll_addr1),f)),(succ (IC S))) by SCMFSA_1:def 17;
thus (SCM+FSA-Exec-Res (I,S)) . l9 = (SCM+FSA-Chg (S,(I coll_addr1),f)) . l9 by A7, SCMFSA_1:23
.= S . l9 by SCMFSA_1:32 ; :: thesis: verum

end;

end;

end;

hence (Exec (i,s)) . l = s . l by SCMFSA_1:def 18; :: thesis: verum

end;

suppose i in { [K,{},<*dC,fB*>] where K is Element of Segm 13, dC is Element of SCM+FSA-Data-Loc , fB is Element of SCM+FSA-Data*-Loc : K in {11,12} } ; :: thesis: (Exec (i,s)) . l = s . l

then consider J being Element of Segm 13, dC being Element of SCM+FSA-Data-Loc , fB being Element of SCM+FSA-Data*-Loc such that
A8: i = [J,{},<*dC,fB*>] and
A9: J in {11,12} ;

now

per cases ( J = 11 or J = 12 ) by A9, TARSKI:def 2;

suppose J = 11 ; :: thesis: (SCM+FSA-Exec-Res (I,S)) . l9 = S . l9

then InsCode I = 11 by A8, RECDEF_2:def 1;
hence (SCM+FSA-Exec-Res (I,S)) . l9 = (SCM+FSA-Chg ((SCM+FSA-Chg (S,(I int_addr3),(len (S . (I coll_addr2))))),(succ (IC S)))) . l9 by SCMFSA_1:def 17
.= (SCM+FSA-Chg (S,(I int_addr3),(len (S . (I coll_addr2))))) . l9 by SCMFSA_1:23
.= S . l9 by SCMFSA_1:28 ;
:: thesis: verum

end;

suppose J = 12 ; :: thesis: (SCM+FSA-Exec-Res (I,S)) . l9 = S . l9

then InsCode I = 12 by A8, RECDEF_2:def 1;
then consider f being FinSequence of INT , k being Element of NAT such that
k = abs (S . (I int_addr3)) and
f = k |-> 0 and
A10: SCM+FSA-Exec-Res (I,S) = SCM+FSA-Chg ((SCM+FSA-Chg (S,(I coll_addr2),f)),(succ (IC S))) by SCMFSA_1:def 17;
thus (SCM+FSA-Exec-Res (I,S)) . l9 = (SCM+FSA-Chg (S,(I coll_addr2),f)) . l9 by A10, SCMFSA_1:23
.= S . l9 by SCMFSA_1:32 ; :: thesis: verum

end;

end;

end;

hence (Exec (i,s)) . l = s . l by SCMFSA_1:def 18; :: thesis: verum

end;

end;