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 EXTPRO_1:def 4 :: 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 NAT holds (Exec (b1,s)) . b2 = s . b2
let j be Instruction of (SCM R); :: thesis: for b1 being Element of NAT 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 Data-Locations SCM : 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 Data-Locations SCM : verum } or c in { [5,{},<*a,r*>] where a is Element of Data-Locations SCM, r is Element of R : verum } ) by AMI_3:72, XBOOLE_0:def 3;
then ( c in ({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of Data-Locations SCM : 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 Data-Locations SCM : verum } or c in { [5,{},<*a,r*>] where a is Element of Data-Locations SCM, 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 Data-Locations SCM : 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 Data-Locations SCM : verum } or c in { [5,{},<*a,r*>] where a is Element of Data-Locations SCM, 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 Data-Locations SCM : verum } or c in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of Data-Locations SCM : I in {1,2,3,4} } or c in { [5,{},<*a,r*>] where a is Element of Data-Locations SCM, 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 Data-Locations SCM holds not c = [3,{},<*mk,ml*>] ) & ( for mk, ml being Element of Data-Locations SCM holds not c = [4,{},<*mk,ml*>] ) ) by RECDEF_2:def 3;
A5: for mk being Element of Data-Locations SCM
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 Data-Locations SCM holds not c = [7,<*mk*>,<*ml*>] ) ) by RECDEF_2:def 2;
( ( for mk, ml being Element of Data-Locations SCM holds not c = [1,{},<*mk,ml*>] ) & ( for mk, ml being Element of Data-Locations SCM 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, AMI_3:72, 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 Data-Locations SCM : verum } ; :: thesis: (SCM-Exec-Res (c,S)) . l9 = S . l9
then ex i being Element of NAT ex a being Element of Data-Locations SCM 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 AMI_3:72, 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 Data-Locations SCM : 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 Data-Locations SCM 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, AMI_3:72, 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, AMI_3:72, 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, AMI_3:72, 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, AMI_3:72, 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 Data-Locations SCM, r is Element of R : verum } ; :: thesis: (SCM-Exec-Res (c,S)) . l9 = S . l9
then ex a being Element of Data-Locations SCM 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 AMI_3:72, 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