thus SCM R is halting :: thesis: ( SCM R is definite & SCM R is steady-programmed & SCM R is realistic )
proof
the haltF of (SCM R) = [0 ,{} ,{} ] by Def1;
hence the haltF of (SCM R) is halting by Th21; :: according to AMI_1:def 9 :: thesis: verum
end;
thus SCM R is definite :: thesis: ( SCM R is steady-programmed & SCM R is realistic )
proof
let l be Element of NAT ; :: according to COMPOS_1:def 8 :: thesis: the Object-Kind of (SCM R) . l = the Instructions of (SCM R)
reconsider L = l as Element of NAT ;
thus the Object-Kind of (SCM R) . 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 b1 being Element of the Instructions of (SCM R)
for b2 being Element of K52() holds (Exec b1,s) . b2 = s . b2
let j be Instruction of (SCM R); :: thesis: for b1 being Element of K52() holds (Exec j,s) . b1 = s . b1
let l be Element of NAT ; :: thesis: (Exec j,s) . l = s . l
Y: the Object-Kind of (SCM R) = SCM-OK R by Def1;
reconsider S = s as SCM-State of R by Y, PBOOLE:155;
reconsider c = j as Element of SCM-Instr R by Def1;
reconsider l9 = l as Element of NAT ;
( 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;
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 R : verum } ) by A1, XBOOLE_0:def 3;
case c in {[0 ,{} ,{} ]} ; :: thesis: (SCM-Exec-Res c,S) . l9 = S . l9
then X: c = [0 ,{} ,{} ] by TARSKI:def 1;
then A3: c `3_3 = {} by RECDEF_2:def 3;
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 RECDEF_2:def 3;
A5: for mk being Element of SCM-Data-Loc
for r being Element of R holds not c = [5,{} ,<*mk,r*>] by A3, RECDEF_2:def 3;
c `2_3 = {} by X, RECDEF_2:def 2;
then 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 RECDEF_2:def 2;
( ( 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, RECDEF_2:def 3;
hence (SCM-Exec-Res c,S) . l9 = S . l9 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) . l9 = S . l9
then ex i being Element of NAT st c = [6,<*i*>,{} ] ;
hence (SCM-Exec-Res c,S) . l9 = (SCM-Chg S,(c jump_address )) . l9 by SCMRING1:def 14
.= S . l9 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) . l9 = S . l9
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) . l9 = (SCM-Chg S,(IFEQ (S . (c cond_address )),(0. R),(c cjump_address ),(succ (IC S)))) . l9 by SCMRING1:def 14
.= S . l9 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) . l9 = S . l9
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) . l9 = S . l9
hence (SCM-Exec-Res c,S) . l9 = (SCM-Chg (SCM-Chg S,(c address_1 ),(S . (c address_2 ))),(succ (IC S))) . l9 by A7, SCMRING1:def 14
.= (SCM-Chg S,(c address_1 ),(S . (c address_2 ))) . l9 by SCMRING1:12
.= S . l9 by SCMRING1:16 ;
:: thesis: verum
end;
case I = 2 ; :: thesis: (SCM-Exec-Res c,S) . l9 = S . l9
hence (SCM-Exec-Res c,S) . l9 = (SCM-Chg (SCM-Chg S,(c address_1 ),((S . (c address_1 )) + (S . (c address_2 )))),(succ (IC S))) . l9 by A7, SCMRING1:def 14
.= (SCM-Chg S,(c address_1 ),((S . (c address_1 )) + (S . (c address_2 )))) . l9 by SCMRING1:12
.= S . l9 by SCMRING1:16 ;
:: thesis: verum
end;
case I = 3 ; :: thesis: (SCM-Exec-Res c,S) . l9 = S . l9
hence (SCM-Exec-Res c,S) . l9 = (SCM-Chg (SCM-Chg S,(c address_1 ),((S . (c address_1 )) - (S . (c address_2 )))),(succ (IC S))) . l9 by A7, SCMRING1:def 14
.= (SCM-Chg S,(c address_1 ),((S . (c address_1 )) - (S . (c address_2 )))) . l9 by SCMRING1:12
.= S . l9 by SCMRING1:16 ;
:: thesis: verum
end;
case I = 4 ; :: thesis: (SCM-Exec-Res c,S) . l9 = S . l9
hence (SCM-Exec-Res c,S) . l9 = (SCM-Chg (SCM-Chg S,(c address_1 ),((S . (c address_1 )) * (S . (c address_2 )))),(succ (IC S))) . l9 by A7, SCMRING1:def 14
.= (SCM-Chg S,(c address_1 ),((S . (c address_1 )) * (S . (c address_2 )))) . l9 by SCMRING1:12
.= S . l9 by SCMRING1:16 ;
:: thesis: verum
end;
end;
end;
hence (SCM-Exec-Res c,S) . l9 = S . l9 ; :: 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) . l9 = S . l9
then ex a being Element of SCM-Data-Loc ex r being Element of R st c = [5,{} ,<*a,r*>] ;
hence (SCM-Exec-Res c,S) . l9 = (SCM-Chg (SCM-Chg S,(c const_address ),(c const_value )),(succ (IC S))) . l9 by SCMRING1:def 14
.= (SCM-Chg S,(c const_address ),(c const_value )) . l9 by SCMRING1:12
.= S . l9 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 COMPOS_1:def 12 :: thesis: contradiction
the Instruction-Counter of (SCM R) = NAT by Def1;
hence contradiction by A9; :: thesis: verum