thus SCM+FSA is realistic :: thesis: ( SCM+FSA is IC-Ins-separated & SCM+FSA is definite & SCM+FSA is steady-programmed )

proof

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

end;

thus SCM+FSA is IC-Ins-separated :: thesis: ( SCM+FSA is definite & SCM+FSA is steady-programmed )

proof

ObjectKind (IC SCM+FSA ) = NAT by FUNCT_7:def 1, SCMFSA_1:5, SCMFSA_1:9;
hence SCM+FSA is IC-Ins-separated by AMI_1:def 11; :: thesis: verum

end;

thus SCM+FSA is definite :: thesis: SCM+FSA is steady-programmed

proof

let l be Instruction-Location of SCM+FSA ; :: according to AMI_1:def 14 :: thesis: ObjectKind l = the Instructions of SCM+FSA
l in NAT by AMI_1:def 4;
hence ObjectKind 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 Instruction-Location of SCM+FSA holds (Exec b₁,s) . b₂ = s . b₂
let i be Instruction of SCM+FSA ; :: thesis: for b₁ being Instruction-Location of SCM+FSA holds (Exec i,s) . b₁ = s . b₁
let l be Instruction-Location of SCM+FSA ; :: thesis: (Exec i,s) . l = s . l
A2: ( 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 I = i as Element of SCM+FSA-Instr ;
reconsider S = s as Element of product SCM+FSA-OK ;
reconsider l' = l as Element of NAT by AMI_1:def 4;

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 A2, 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 SCMFSA_1:18;
A3: dom (s | NAT ) = (dom s) /\ NAT by RELAT_1:90;
A4: l in NAT by AMI_1:def 4;
dom s = dom SCM+FSA-OK by CARD_3:18
.= (({NAT } \/ SCM+FSA-Data-Loc ) \/ SCM+FSA-Data*-Loc ) \/ NAT by FUNCT_2:def 1, SCMFSA_1:8 ;
then l in dom s by A4, XBOOLE_0:def 3;
then A5: l in dom (s | NAT ) by A3, A4, XBOOLE_0:def 4;
thus (Exec i,s) . l = ((s +* (Exec I,S)) +* (s | NAT )) . l by Th75
.= (s | NAT ) . l by A5, FUNCT_4:14
.= s . l by A5, 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
A6: i = [J,<*dB,fA,dA*>] and
A7: J in {9,10} ;

now

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

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

then InsCode I = 9 by A6, MCART_1:7;
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
A8: 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) . l' = (SCM+FSA-Chg S,(I int_addr1 ),i) . l' by A8, SCMFSA_1:23
.= S . l' by SCMFSA_1:28 ; :: thesis: verum

end;

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

then InsCode I = 10 by A6, MCART_1:7;
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
A9: 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) . l' = (SCM+FSA-Chg S,(I coll_addr1 ),f) . l' by A9, SCMFSA_1:23
.= S . l' 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
A10: i = [J,<*dC,fB*>] and
A11: J in {11,12} ;

now

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

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

then InsCode I = 11 by A10, MCART_1:7;
hence (SCM+FSA-Exec-Res I,S) . l' = (SCM+FSA-Chg (SCM+FSA-Chg S,(I int_addr3 ),(len (S . (I coll_addr2 )))),(succ (IC S))) . l' by SCMFSA_1:def 17
.= (SCM+FSA-Chg S,(I int_addr3 ),(len (S . (I coll_addr2 )))) . l' by SCMFSA_1:23
.= S . l' by SCMFSA_1:28 ;
:: thesis: verum

end;

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

then InsCode I = 12 by A10, MCART_1:7;
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
A12: 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) . l' = (SCM+FSA-Chg S,(I coll_addr2 ),f) . l' by A12, SCMFSA_1:23
.= S . l' 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;