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 K99() holds (Exec b₁,s) . b₂ = s . b₂
let i be Instruction of SCM+FSA ; :: thesis: for b₁ being Element of K99() 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;