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 (SCM R) 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 (SCM R); :: 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 (SCM R); :: 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 c = j as Element of SCM-Instr R by Def1;
( 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 R : 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 R : 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 R : verum } ) by XBOOLE_0:def 3;
reconsider S = s as SCM-State of R by Def1;
reconsider l' = l as Element of NAT by AMI_1:def 4;
A2: Exec j,s = ((SCM-Exec R) . c) . S by Def1
.= SCM-Exec-Res c,S by SCMRING1:def 15 ;

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 R : 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 c `2 = {} by MCART_1:7;
then ( ( 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*>] ) & ( 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*>] ) & ( 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*>] ) & ( for mk being Element of SCM-Data-Loc
for r being Element of R holds not c = [5,<*mk,r*>] ) ) by MCART_1:7;
hence (SCM-Exec-Res c,S) . l' = S . l' by 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 consider i being Element of NAT such that
A3: c = [6,<*i*>] and
verum ;
thus (SCM-Exec-Res c,S) . l' = (SCM-Chg S,(c jump_address )) . l' by A3, 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 consider i being Element of NAT , a being Element of SCM-Data-Loc such that
A4: c = [7,<*i,a*>] and
verum ;
thus (SCM-Exec-Res c,S) . l' = (SCM-Chg S,(IFEQ (S . (c cond_address )),(0. R),(c cjump_address ),(succ (IC S)))) . l' by A4, 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
A5: ( c = [I,<*a,b*>] & I in {1,2,3,4} ) ;

now

per cases ( I = 1 or I = 2 or I = 3 or I = 4 ) by A5, 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 A5, 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 A5, 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 A5, 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 A5, 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 R : verum } ; :: thesis: (SCM-Exec-Res c,S) . l' = S . l'

then consider a being Element of SCM-Data-Loc , r being Element of R such that
A6: c = [5,<*a,r*>] and
verum ;
thus (SCM-Exec-Res c,S) . l' = (SCM-Chg (SCM-Chg S,(c const_address ),(c const_value )),(succ (IC S))) . l' by A6, 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;

hence s . l = (Exec j,s) . l by A2; :: thesis: verum

end;

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