thus SCM R is halting :: thesis: ( SCM R is definite & SCM R is steady-programmed & SCM R is realistic )

proof

reconsider I = [0 ,{} ] as Instruction of by Th3;
take I ; :: according to AMI_1:def 9 :: thesis: I is halting
thus I is halting by Th21; :: thesis: verum

end;

thus SCM R is definite :: thesis: ( SCM R is steady-programmed & SCM R is realistic )

proof

let l be Instruction-Location of SCM R; :: according to AMI_1:def 14 :: thesis: ObjectKind l = the Instructions of (SCM R)
reconsider L = l as Element of NAT by AMI_1:def 4;
thus ObjectKind l = (SCM-OK R) . L by Def1
.= SCM-Instr R by SCMRING1:6
.= the Instructions of (SCM R) by Def1 ; :: thesis: verum

end;

thus SCM R is steady-programmed :: thesis: SCM R is realistic

proof

let s be State of ; :: according to AMI_1:def 13 :: thesis: for b₁ being Element of the Instructions of (SCM R)
for b₂ being Instruction-Location of SCM R holds (Exec b₁,s) . b₂ = s . b₂
let j be Instruction of ; :: thesis: for b₁ being Instruction-Location of SCM R holds (Exec j,s) . b₁ = s . b₁
let l be Instruction-Location of SCM R; :: thesis: (Exec j,s) . l = s . l
reconsider S = s as SCM-State of by Def1;
reconsider c = j as Element of SCM-Instr R by Def1;
reconsider l' = l as Element of NAT by AMI_1:def 4;
( c in (({[0 ,{} ]} \/ { [I,<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>] where i is Element of NAT : verum } ) \/ { [7,<*i,a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } or c in { [5,<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of : verum } ) by XBOOLE_0:def 3;
then ( c in ({[0 ,{} ]} \/ { [I,<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>] where i is Element of NAT : verum } or c in { [7,<*i,a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } or c in { [5,<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of : verum } ) by XBOOLE_0:def 3;
then A1: ( c in {[0 ,{} ]} \/ { [I,<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } or c in { [6,<*i*>] where i is Element of NAT : verum } or c in { [7,<*i,a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } or c in { [5,<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of : verum } ) by XBOOLE_0:def 3;

A2: now

per cases ( c in {[0 ,{} ]} or c in { [6,<*i*>] where i is Element of NAT : verum } or c in { [7,<*i,a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } or c in { [I,<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } or c in { [5,<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of : verum } ) by A1, XBOOLE_0:def 3;

case c in {[0 ,{} ]} ; :: thesis: (SCM-Exec-Res c,S) . l' = S . l'

then c = [0 ,{} ] by TARSKI:def 1;
then A3: c `2 = {} by MCART_1:7;
then A4: ( ( for mk, ml being Element of SCM-Data-Loc holds not c = [3,<*mk,ml*>] ) & ( for mk, ml being Element of SCM-Data-Loc holds not c = [4,<*mk,ml*>] ) ) by MCART_1:7;
A5: for mk being Element of SCM-Data-Loc
for r being Element of holds not c = [5,<*mk,r*>] by A3, MCART_1:7;
A6: ( ( for mk being Element of NAT holds not c = [6,<*mk*>] ) & ( for mk being Element of NAT
for ml being Element of SCM-Data-Loc holds not c = [7,<*mk,ml*>] ) ) by A3, MCART_1:7;
( ( for mk, ml being Element of SCM-Data-Loc holds not c = [1,<*mk,ml*>] ) & ( for mk, ml being Element of SCM-Data-Loc holds not c = [2,<*mk,ml*>] ) ) by A3, MCART_1:7;
hence (SCM-Exec-Res c,S) . l' = S . l' by A4, A6, A5, SCMRING1:def 14; :: thesis: verum

end;

case c in { [6,<*i*>] where i is Element of NAT : verum } ; :: thesis: (SCM-Exec-Res c,S) . l' = S . l'

then ex i being Element of NAT st c = [6,<*i*>] ;
hence (SCM-Exec-Res c,S) . l' = (SCM-Chg S,(c jump_address )) . l' by SCMRING1:def 14
.= S . l' by SCMRING1:12 ;
:: thesis: verum

end;

case c in { [7,<*i,a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } ; :: thesis: (SCM-Exec-Res c,S) . l' = S . l'

then ex i being Element of NAT ex a being Element of SCM-Data-Loc st c = [7,<*i,a*>] ;
hence (SCM-Exec-Res c,S) . l' = (SCM-Chg S,(IFEQ (S . (c cond_address )),(0. R),(c cjump_address ),(succ (IC S)))) . l' by SCMRING1:def 14
.= S . l' by SCMRING1:12 ;
:: thesis: verum

end;

case c in { [I,<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ; :: thesis: (SCM-Exec-Res c,S) . l' = S . l'

then consider I being Element of Segm 8, a, b being Element of SCM-Data-Loc such that
A7: c = [I,<*a,b*>] and
A8: I in {1,2,3,4} ;

now

per cases ( I = 1 or I = 2 or I = 3 or I = 4 ) by A8, ENUMSET1:def 2;

case I = 1 ; :: thesis: (SCM-Exec-Res c,S) . l' = S . l'

hence (SCM-Exec-Res c,S) . l' = (SCM-Chg (SCM-Chg S,(c address_1 ),(S . (c address_2 ))),(succ (IC S))) . l' by A7, SCMRING1:def 14
.= (SCM-Chg S,(c address_1 ),(S . (c address_2 ))) . l' by SCMRING1:12
.= S . l' by SCMRING1:16 ;
:: thesis: verum

end;

case I = 2 ; :: thesis: (SCM-Exec-Res c,S) . l' = S . l'

hence (SCM-Exec-Res c,S) . l' = (SCM-Chg (SCM-Chg S,(c address_1 ),((S . (c address_1 )) + (S . (c address_2 )))),(succ (IC S))) . l' by A7, SCMRING1:def 14
.= (SCM-Chg S,(c address_1 ),((S . (c address_1 )) + (S . (c address_2 )))) . l' by SCMRING1:12
.= S . l' by SCMRING1:16 ;
:: thesis: verum

end;

case I = 3 ; :: thesis: (SCM-Exec-Res c,S) . l' = S . l'

hence (SCM-Exec-Res c,S) . l' = (SCM-Chg (SCM-Chg S,(c address_1 ),((S . (c address_1 )) - (S . (c address_2 )))),(succ (IC S))) . l' by A7, SCMRING1:def 14
.= (SCM-Chg S,(c address_1 ),((S . (c address_1 )) - (S . (c address_2 )))) . l' by SCMRING1:12
.= S . l' by SCMRING1:16 ;
:: thesis: verum

end;

case I = 4 ; :: thesis: (SCM-Exec-Res c,S) . l' = S . l'

hence (SCM-Exec-Res c,S) . l' = (SCM-Chg (SCM-Chg S,(c address_1 ),((S . (c address_1 )) * (S . (c address_2 )))),(succ (IC S))) . l' by A7, SCMRING1:def 14
.= (SCM-Chg S,(c address_1 ),((S . (c address_1 )) * (S . (c address_2 )))) . l' by SCMRING1:12
.= S . l' by SCMRING1:16 ;
:: thesis: verum

end;

end;

end;

hence (SCM-Exec-Res c,S) . l' = S . l' ; :: thesis: verum

end;

case c in { [5,<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of : verum } ; :: thesis: (SCM-Exec-Res c,S) . l' = S . l'

then ex a being Element of SCM-Data-Loc ex r being Element of st c = [5,<*a,r*>] ;
hence (SCM-Exec-Res c,S) . l' = (SCM-Chg (SCM-Chg S,(c const_address ),(c const_value )),(succ (IC S))) . l' by SCMRING1:def 14
.= (SCM-Chg S,(c const_address ),(c const_value )) . l' by SCMRING1:12
.= S . l' by SCMRING1:16 ;
:: thesis: verum

end;

end;

end;

Exec j,s = ((SCM-Exec R) . c) . S by Def1
.= SCM-Exec-Res c,S by SCMRING1:def 15 ;
hence (Exec j,s) . l = s . l by A2; :: thesis: verum

end;

assume A9: the Instruction-Counter of (SCM R) in NAT ; :: according to AMI_1:def 21 :: thesis: contradiction
the Instruction-Counter of (SCM R) = NAT by Def1;
hence contradiction by A9; :: thesis: verum