:: SCMPDS_4 semantic presentation
begin
theorem Th1: :: SCMPDS_4:1
for i being Instruction of SCMPDS
for s being State of SCMPDS holds
( InsCode i in {0,1,4,5,6,14} or (Exec (i,s)) . (IC ) = succ (IC s) )
proof
let i be Instruction of SCMPDS; ::_thesis: for s being State of SCMPDS holds
( InsCode i in {0,1,4,5,6,14} or (Exec (i,s)) . (IC ) = succ (IC s) )
let s be State of SCMPDS; ::_thesis: ( InsCode i in {0,1,4,5,6,14} or (Exec (i,s)) . (IC ) = succ (IC s) )
assume A1: not InsCode i in {0,1,4,5,6,14} ; ::_thesis: (Exec (i,s)) . (IC ) = succ (IC s)
then A2: ( InsCode i <> 0 & InsCode i <> 1 ) by ENUMSET1:def_4;
A3: InsCode i <> 6 by A1, ENUMSET1:def_4;
A4: ( InsCode i <> 4 & InsCode i <> 5 ) by A1, ENUMSET1:def_4;
InsCode i <> 14 by A1, ENUMSET1:def_4;
percasesthen ( InsCode i = 2 or InsCode i = 3 or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or InsCode i = 13 ) by A2, A4, A3, NAT_1:60, SCMPDS_2:6;
suppose InsCode i = 2 ; ::_thesis: (Exec (i,s)) . (IC ) = succ (IC s)
then ex a being Int_position ex k1 being Integer st i = a := k1 by SCMPDS_2:28;
hence (Exec (i,s)) . (IC ) = succ (IC s) by SCMPDS_2:45; ::_thesis: verum
end;
suppose InsCode i = 3 ; ::_thesis: (Exec (i,s)) . (IC ) = succ (IC s)
then ex a being Int_position ex k1 being Integer st i = saveIC (a,k1) by SCMPDS_2:29;
hence (Exec (i,s)) . (IC ) = succ (IC s) by SCMPDS_2:59; ::_thesis: verum
end;
suppose InsCode i = 7 ; ::_thesis: (Exec (i,s)) . (IC ) = succ (IC s)
then ex a being Int_position ex k1, k2 being Integer st i = (a,k1) := k2 by SCMPDS_2:33;
hence (Exec (i,s)) . (IC ) = succ (IC s) by SCMPDS_2:46; ::_thesis: verum
end;
suppose InsCode i = 8 ; ::_thesis: (Exec (i,s)) . (IC ) = succ (IC s)
then ex a being Int_position ex k1, k2 being Integer st i = AddTo (a,k1,k2) by SCMPDS_2:34;
hence (Exec (i,s)) . (IC ) = succ (IC s) by SCMPDS_2:48; ::_thesis: verum
end;
suppose InsCode i = 9 ; ::_thesis: (Exec (i,s)) . (IC ) = succ (IC s)
then ex a, b being Int_position ex k1, k2 being Integer st i = AddTo (a,k1,b,k2) by SCMPDS_2:35;
hence (Exec (i,s)) . (IC ) = succ (IC s) by SCMPDS_2:49; ::_thesis: verum
end;
suppose InsCode i = 10 ; ::_thesis: (Exec (i,s)) . (IC ) = succ (IC s)
then ex a, b being Int_position ex k1, k2 being Integer st i = SubFrom (a,k1,b,k2) by SCMPDS_2:36;
hence (Exec (i,s)) . (IC ) = succ (IC s) by SCMPDS_2:50; ::_thesis: verum
end;
suppose InsCode i = 11 ; ::_thesis: (Exec (i,s)) . (IC ) = succ (IC s)
then ex a, b being Int_position ex k1, k2 being Integer st i = MultBy (a,k1,b,k2) by SCMPDS_2:37;
hence (Exec (i,s)) . (IC ) = succ (IC s) by SCMPDS_2:51; ::_thesis: verum
end;
suppose InsCode i = 12 ; ::_thesis: (Exec (i,s)) . (IC ) = succ (IC s)
then ex a, b being Int_position ex k1, k2 being Integer st i = Divide (a,k1,b,k2) by SCMPDS_2:38;
hence (Exec (i,s)) . (IC ) = succ (IC s) by SCMPDS_2:52; ::_thesis: verum
end;
suppose InsCode i = 13 ; ::_thesis: (Exec (i,s)) . (IC ) = succ (IC s)
then ex a, b being Int_position ex k1, k2 being Integer st i = (a,k1) := (b,k2) by SCMPDS_2:39;
hence (Exec (i,s)) . (IC ) = succ (IC s) by SCMPDS_2:47; ::_thesis: verum
end;
end;
end;
theorem :: SCMPDS_4:2
for s1, s2 being State of SCMPDS st IC s1 = IC s2 & ( for a being Int_position holds s1 . a = s2 . a ) holds
s1 = s2
proof
let s1, s2 be State of SCMPDS; ::_thesis: ( IC s1 = IC s2 & ( for a being Int_position holds s1 . a = s2 . a ) implies s1 = s2 )
assume that
A1: IC s1 = IC s2 and
A2: for a being Int_position holds s1 . a = s2 . a ; ::_thesis: s1 = s2
the carrier of SCMPDS = {(IC )} \/ SCM-Data-Loc by SCMPDS_2:84, STRUCT_0:4;
then A3: the carrier of SCMPDS = {(IC )} \/ SCM-Data-Loc
.= {(IC )} \/ SCM-Data-Loc ;
A4: dom (s2 | (dom s2)) = (dom s2) /\ (dom s2) by RELAT_1:61
.= dom s2
.= {(IC )} \/ SCM-Data-Loc by A3, PARTFUN1:def_2 ;
A5: dom (s1 | (dom s1)) = (dom s1) /\ (dom s1) by RELAT_1:61
.= dom s1
.= {(IC )} \/ SCM-Data-Loc by A3, PARTFUN1:def_2 ;
A6: ( s1 | (dom s1) = s1 & s2 | (dom s2) = s2 ) by RELAT_1:69;
now__::_thesis:_for_x_being_set_st_x_in_{(IC_)}_\/_SCM-Data-Loc_holds_
(s1_|_(dom_s1))_._x_=_(s2_|_(dom_s2))_._x
let x be set ; ::_thesis: ( x in {(IC )} \/ SCM-Data-Loc implies (s1 | (dom s1)) . b1 = (s2 | (dom s2)) . b1 )
assume A7: x in {(IC )} \/ SCM-Data-Loc ; ::_thesis: (s1 | (dom s1)) . b1 = (s2 | (dom s2)) . b1
percases ( x in {(IC )} or x in SCM-Data-Loc ) by A7, XBOOLE_0:def_3;
suppose x in {(IC )} ; ::_thesis: (s1 | (dom s1)) . b1 = (s2 | (dom s2)) . b1
then A8: x = IC by TARSKI:def_1;
hence (s1 | (dom s1)) . x = IC s1 by A5, A7, FUNCT_1:47
.= (s2 | (dom s2)) . x by A1, A4, A7, A8, FUNCT_1:47 ;
::_thesis: verum
end;
suppose x in SCM-Data-Loc ; ::_thesis: (s1 | (dom s1)) . b1 = (s2 | (dom s2)) . b1
then A9: x is Int_position by AMI_2:def_16;
thus (s1 | (dom s1)) . x = s1 . x by A5, A7, FUNCT_1:47
.= s2 . x by A2, A9
.= (s2 | (dom s2)) . x by A4, A7, FUNCT_1:47 ; ::_thesis: verum
end;
end;
end;
then s1 | (dom s1) = s2 | (dom s2) by A5, A4, FUNCT_1:2;
hence s1 = s2 by A6; ::_thesis: verum
end;
theorem Th3: :: SCMPDS_4:3
for k1, k2 being Element of NAT st k1 <> k2 holds
DataLoc (k1,0) <> DataLoc (k2,0)
proof
let k1, k2 be Element of NAT ; ::_thesis: ( k1 <> k2 implies DataLoc (k1,0) <> DataLoc (k2,0) )
assume A1: k1 <> k2 ; ::_thesis: DataLoc (k1,0) <> DataLoc (k2,0)
assume DataLoc (k1,0) = DataLoc (k2,0) ; ::_thesis: contradiction
then abs (k1 + 0) = abs (k2 + 0) by XTUPLE_0:1;
then k1 = abs k2 by ABSVALUE:def_1;
hence contradiction by A1, ABSVALUE:def_1; ::_thesis: verum
end;
theorem Th4: :: SCMPDS_4:4
for dl being Int_position ex i being Element of NAT st dl = DataLoc (i,0)
proof
let dl be Int_position; ::_thesis: ex i being Element of NAT st dl = DataLoc (i,0)
dl in SCM-Data-Loc by AMI_2:def_16;
then consider i being Element of NAT such that
A1: dl = [1,i] by AMI_2:23;
take i ; ::_thesis: dl = DataLoc (i,0)
thus dl = DataLoc (i,0) by A1, ABSVALUE:def_1; ::_thesis: verum
end;
scheme :: SCMPDS_4:sch 1
SCMPDSEx{ F1( set ) -> Integer, F2() -> Element of NAT } :
ex S being State of SCMPDS st
( IC S = F2() & ( for i being Element of NAT holds S . (DataLoc (i,0)) = F1(i) ) )
proof
set S1 = {(IC )};
set S2 = SCM-Data-Loc ;
set S3 = NAT ;
defpred S1[ set , set ] means ex m being Element of NAT st
( ( $1 = IC & $2 = F2() ) or ( $1 = DataLoc (m,0) & $2 = F1(m) ) );
A1: for e being set st e in the carrier of SCMPDS holds
ex u being set st S1[e,u]
proof
let e be set ; ::_thesis: ( e in the carrier of SCMPDS implies ex u being set st S1[e,u] )
assume e in the carrier of SCMPDS ; ::_thesis: ex u being set st S1[e,u]
then e in {(IC )} \/ SCM-Data-Loc by SCMPDS_2:84, STRUCT_0:4;
then A2: e in {(IC )} \/ SCM-Data-Loc ;
now__::_thesis:_(_(_e_in_{(IC_)}_&_e_=_IC_)_or_(_e_in_SCM-Data-Loc_&_ex_m_being_Element_of_NAT_st_e_=_DataLoc_(m,0)_)_)
percases ( e in {(IC )} or e in SCM-Data-Loc ) by A2, XBOOLE_0:def_3;
case e in {(IC )} ; ::_thesis: e = IC
hence e = IC by TARSKI:def_1; ::_thesis: verum
end;
case e in SCM-Data-Loc ; ::_thesis: ex m being Element of NAT st e = DataLoc (m,0)
then e is Int_position by AMI_2:def_16;
hence ex m being Element of NAT st e = DataLoc (m,0) by Th4; ::_thesis: verum
end;
end;
end;
then consider m being Element of NAT such that
A3: ( e = IC or e = DataLoc (m,0) ) ;
percases ( e = IC or e = DataLoc (m,0) ) by A3;
supposeA4: e = IC ; ::_thesis: ex u being set st S1[e,u]
take u = F2(); ::_thesis: S1[e,u]
thus S1[e,u] by A4; ::_thesis: verum
end;
supposeA5: e = DataLoc (m,0) ; ::_thesis: ex u being set st S1[e,u]
take u = F1(m); ::_thesis: S1[e,u]
thus S1[e,u] by A5; ::_thesis: verum
end;
end;
end;
consider f being Function such that
A6: dom f = the carrier of SCMPDS and
A7: for e being set st e in the carrier of SCMPDS holds
S1[e,f . e] from CLASSES1:sch_1(A1);
A8: dom the Object-Kind of SCMPDS = the carrier of SCMPDS by FUNCT_2:def_1;
now__::_thesis:_for_x_being_set_st_x_in_dom_the_Object-Kind_of_SCMPDS_holds_
f_._x_in_(the_Values_of_SCMPDS)_._x
let x be set ; ::_thesis: ( x in dom the Object-Kind of SCMPDS implies f . b1 in (the_Values_of SCMPDS) . b1 )
assume A9: x in dom the Object-Kind of SCMPDS ; ::_thesis: f . b1 in (the_Values_of SCMPDS) . b1
then x in {(IC )} \/ SCM-Data-Loc by A8, SCMPDS_2:84, STRUCT_0:4;
then A10: x in {(IC )} \/ SCM-Data-Loc ;
consider m being Element of NAT such that
A11: ( ( x = IC & f . x = F2() ) or ( x = DataLoc (m,0) & f . x = F1(m) ) ) by A7, A8, A9;
percases ( x in SCM-Data-Loc or x in {(IC )} ) by A10, XBOOLE_0:def_3;
suppose x in SCM-Data-Loc ; ::_thesis: f . b1 in (the_Values_of SCMPDS) . b1
then x is Int_position by AMI_2:def_16;
then (the_Values_of SCMPDS) . x = Values (DataLoc (m,0)) by A11, SCMPDS_2:43
.= INT by SCMPDS_2:5 ;
hence f . x in (the_Values_of SCMPDS) . x by A11, INT_1:def_2; ::_thesis: verum
end;
supposeA12: x in {(IC )} ; ::_thesis: f . b1 in (the_Values_of SCMPDS) . b1
then (the_Values_of SCMPDS) . x = Values (IC ) by TARSKI:def_1
.= NAT by MEMSTR_0:def_6 ;
hence f . x in (the_Values_of SCMPDS) . x by A11, A12, SCMPDS_2:2, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
then reconsider f = f as State of SCMPDS by A6, A8, FUNCT_1:def_14, PARTFUN1:def_2, RELAT_1:def_18;
consider m being Element of NAT such that
A13: ( ( IC = IC & f . (IC ) = F2() ) or ( IC = DataLoc (m,0) & f . (IC ) = F1(m) ) ) by A7;
take f ; ::_thesis: ( IC f = F2() & ( for i being Element of NAT holds f . (DataLoc (i,0)) = F1(i) ) )
thus IC f = F2() by A13, SCMPDS_2:43; ::_thesis: for i being Element of NAT holds f . (DataLoc (i,0)) = F1(i)
let i be Element of NAT ; ::_thesis: f . (DataLoc (i,0)) = F1(i)
ex m being Element of NAT st
( ( DataLoc (i,0) = IC & f . (DataLoc (i,0)) = F2() ) or ( DataLoc (i,0) = DataLoc (m,0) & f . (DataLoc (i,0)) = F1(m) ) ) by A7;
hence f . (DataLoc (i,0)) = F1(i) by Th3, SCMPDS_2:43; ::_thesis: verum
end;
theorem :: SCMPDS_4:5
for s being State of SCMPDS holds dom s = {(IC )} \/ SCM-Data-Loc
proof
let s be State of SCMPDS; ::_thesis: dom s = {(IC )} \/ SCM-Data-Loc
dom s = the carrier of SCMPDS by PARTFUN1:def_2;
hence dom s = {(IC )} \/ SCM-Data-Loc by SCMPDS_2:84, STRUCT_0:4; ::_thesis: verum
end;
theorem :: SCMPDS_4:6
for s being State of SCMPDS
for x being set holds
( not x in dom s or x is Int_position or x = IC )
proof
set S1 = {(IC )};
set S2 = SCM-Data-Loc ;
set S3 = NAT ;
let s be State of SCMPDS; ::_thesis: for x being set holds
( not x in dom s or x is Int_position or x = IC )
let x be set ; ::_thesis: ( not x in dom s or x is Int_position or x = IC )
assume A1: x in dom s ; ::_thesis: ( x is Int_position or x = IC )
dom s = the carrier of SCMPDS by PARTFUN1:def_2;
then dom s = {(IC )} \/ SCM-Data-Loc by SCMPDS_2:84, STRUCT_0:4;
then x in {(IC )} \/ SCM-Data-Loc by A1;
then ( x in {(IC )} or x in SCM-Data-Loc ) by XBOOLE_0:def_3;
hence ( x is Int_position or x = IC ) by AMI_2:def_16, TARSKI:def_1; ::_thesis: verum
end;
theorem :: SCMPDS_4:7
canceled;
theorem Th8: :: SCMPDS_4:8
for s1, s2 being State of SCMPDS holds
( ( for a being Int_position holds s1 . a = s2 . a ) iff DataPart s1 = DataPart s2 )
proof
set T1 = {(IC )};
set T2 = SCM-Data-Loc ;
set T3 = NAT ;
let s1, s2 be State of SCMPDS; ::_thesis: ( ( for a being Int_position holds s1 . a = s2 . a ) iff DataPart s1 = DataPart s2 )
A1: now__::_thesis:_(_(_for_a_being_Int_position_holds_s1_._a_=_s2_._a_)_implies_for_x_being_set_st_x_in_SCM-Data-Loc_holds_
s1_._x_=_s2_._x_)
assume A2: for a being Int_position holds s1 . a = s2 . a ; ::_thesis: for x being set st x in SCM-Data-Loc holds
s1 . x = s2 . x
hereby ::_thesis: verum
let x be set ; ::_thesis: ( x in SCM-Data-Loc implies s1 . x = s2 . x )
assume x in SCM-Data-Loc ; ::_thesis: s1 . x = s2 . x
then x is Int_position by AMI_2:def_16;
hence s1 . x = s2 . x by A2; ::_thesis: verum
end;
end;
A3: now__::_thesis:_(_(_for_x_being_set_st_x_in_SCM-Data-Loc_holds_
s1_._x_=_s2_._x_)_implies_for_a_being_Int_position_holds_s1_._a_=_s2_._a_)
assume A4: for x being set st x in SCM-Data-Loc holds
s1 . x = s2 . x ; ::_thesis: for a being Int_position holds s1 . a = s2 . a
hereby ::_thesis: verum
let a be Int_position; ::_thesis: s1 . a = s2 . a
a in SCM-Data-Loc by AMI_2:def_16;
hence s1 . a = s2 . a by A4; ::_thesis: verum
end;
end;
dom s2 = the carrier of SCMPDS by PARTFUN1:def_2;
then dom s2 = {(IC )} \/ SCM-Data-Loc by SCMPDS_2:84, STRUCT_0:4;
then A5: SCM-Data-Loc c= dom s2 by XBOOLE_1:7;
dom s1 = the carrier of SCMPDS by PARTFUN1:def_2;
then dom s1 = {(IC )} \/ SCM-Data-Loc by SCMPDS_2:84, STRUCT_0:4;
then SCM-Data-Loc c= dom s1 by XBOOLE_1:7;
hence ( ( for a being Int_position holds s1 . a = s2 . a ) iff DataPart s1 = DataPart s2 ) by A5, A1, A3, FUNCT_1:95, SCMPDS_2:84; ::_thesis: verum
end;
begin
notation
let I, J be Program of SCMPDS;
synonym I ';' J for I ^ J;
end;
definition
let I, J be Program of SCMPDS;
:: original: ';'
redefine funcI ';' J -> Program of SCMPDS equals :: SCMPDS_4:def 1
I +* (Shift (J,(card I)));
compatibility
for b1 being Program of SCMPDS holds
( b1 = I ';' J iff b1 = I +* (Shift (J,(card I))) ) by AFINSQ_1:77;
coherence
I ';' J is Program of SCMPDS ;
end;
:: deftheorem defines ';' SCMPDS_4:def_1_:_
for I, J being Program of SCMPDS holds I ';' J = I +* (Shift (J,(card I)));
begin
definition
let i be Instruction of SCMPDS;
let J be Program of SCMPDS;
funci ';' J -> Program of SCMPDS equals :: SCMPDS_4:def 2
(Load i) ';' J;
correctness
coherence
(Load i) ';' J is Program of SCMPDS;
;
end;
:: deftheorem defines ';' SCMPDS_4:def_2_:_
for i being Instruction of SCMPDS
for J being Program of SCMPDS holds i ';' J = (Load i) ';' J;
definition
let I be Program of SCMPDS;
let j be Instruction of SCMPDS;
funcI ';' j -> Program of SCMPDS equals :: SCMPDS_4:def 3
I ';' (Load j);
correctness
coherence
I ';' (Load j) is Program of SCMPDS;
;
end;
:: deftheorem defines ';' SCMPDS_4:def_3_:_
for I being Program of SCMPDS
for j being Instruction of SCMPDS holds I ';' j = I ';' (Load j);
definition
let i, j be Instruction of SCMPDS;
funci ';' j -> Program of SCMPDS equals :: SCMPDS_4:def 4
(Load i) ';' (Load j);
correctness
coherence
(Load i) ';' (Load j) is Program of SCMPDS;
;
end;
:: deftheorem defines ';' SCMPDS_4:def_4_:_
for i, j being Instruction of SCMPDS holds i ';' j = (Load i) ';' (Load j);
theorem :: SCMPDS_4:9
for i, j being Instruction of SCMPDS holds i ';' j = (Load i) ';' j ;
theorem :: SCMPDS_4:10
for i, j being Instruction of SCMPDS holds i ';' j = i ';' (Load j) ;
theorem :: SCMPDS_4:11
for k being Instruction of SCMPDS
for I, J being Program of SCMPDS holds (I ';' J) ';' k = I ';' (J ';' k) by AFINSQ_1:27;
theorem :: SCMPDS_4:12
for j being Instruction of SCMPDS
for I, K being Program of SCMPDS holds (I ';' j) ';' K = I ';' (j ';' K) by AFINSQ_1:27;
theorem :: SCMPDS_4:13
for j, k being Instruction of SCMPDS
for I being Program of SCMPDS holds (I ';' j) ';' k = I ';' (j ';' k) by AFINSQ_1:27;
theorem :: SCMPDS_4:14
for i being Instruction of SCMPDS
for J, K being Program of SCMPDS holds (i ';' J) ';' K = i ';' (J ';' K) by AFINSQ_1:27;
theorem :: SCMPDS_4:15
for i, k being Instruction of SCMPDS
for J being Program of SCMPDS holds (i ';' J) ';' k = i ';' (J ';' k) by AFINSQ_1:27;
theorem :: SCMPDS_4:16
for i, j being Instruction of SCMPDS
for K being Program of SCMPDS holds (i ';' j) ';' K = i ';' (j ';' K) by AFINSQ_1:27;
theorem :: SCMPDS_4:17
for i, j, k being Instruction of SCMPDS holds (i ';' j) ';' k = i ';' (j ';' k) by AFINSQ_1:27;
theorem :: SCMPDS_4:18
for a being Int_position
for l being Element of NAT holds not a in dom (Start-At (l,SCMPDS))
proof
let a be Int_position; ::_thesis: for l being Element of NAT holds not a in dom (Start-At (l,SCMPDS))
let l be Element of NAT ; ::_thesis: not a in dom (Start-At (l,SCMPDS))
A1: dom (Start-At (l,SCMPDS)) = {(IC )} by FUNCOP_1:13;
assume a in dom (Start-At (l,SCMPDS)) ; ::_thesis: contradiction
then a = IC by A1, TARSKI:def_1;
hence contradiction by SCMPDS_2:43; ::_thesis: verum
end;
definition
let s be State of SCMPDS;
let li be Int_position;
let k be Integer;
:: original: +*
redefine funcs +* (li,k) -> PartState of SCMPDS;
coherence
s +* (li,k) is PartState of SCMPDS
proof
A1: dom s = the carrier of SCMPDS by PARTFUN1:def_2;
now__::_thesis:_for_x_being_set_st_x_in_dom_(s_+*_(li,k))_holds_
(s_+*_(li,k))_._x_in_(the_Values_of_SCMPDS)_._x
let x be set ; ::_thesis: ( x in dom (s +* (li,k)) implies (s +* (li,k)) . b1 in (the_Values_of SCMPDS) . b1 )
assume x in dom (s +* (li,k)) ; ::_thesis: (s +* (li,k)) . b1 in (the_Values_of SCMPDS) . b1
then A2: x in dom s by A1, PARTFUN1:def_2;
percases ( x = li or x <> li ) ;
supposeA3: x = li ; ::_thesis: (s +* (li,k)) . b1 in (the_Values_of SCMPDS) . b1
then A4: (the_Values_of SCMPDS) . x = Values li
.= INT by SCMPDS_2:5 ;
(s +* (li,k)) . x = k by A1, A3, FUNCT_7:31;
hence (s +* (li,k)) . x in (the_Values_of SCMPDS) . x by A4, INT_1:def_2; ::_thesis: verum
end;
suppose x <> li ; ::_thesis: (s +* (li,k)) . b1 in (the_Values_of SCMPDS) . b1
then (s +* (li,k)) . x = s . x by FUNCT_7:32;
hence (s +* (li,k)) . x in (the_Values_of SCMPDS) . x by A2, FUNCT_1:def_14; ::_thesis: verum
end;
end;
end;
hence s +* (li,k) is PartState of SCMPDS by FUNCT_1:def_14; ::_thesis: verum
end;
end;
begin
definition
let I be Program of SCMPDS;
let s be State of SCMPDS;
let P be Instruction-Sequence of SCMPDS;
func IExec (I,P,s) -> State of SCMPDS equals :: SCMPDS_4:def 5
Result ((P +* (stop I)),s);
coherence
Result ((P +* (stop I)),s) is State of SCMPDS ;
end;
:: deftheorem defines IExec SCMPDS_4:def_5_:_
for I being Program of SCMPDS
for s being State of SCMPDS
for P being Instruction-Sequence of SCMPDS holds IExec (I,P,s) = Result ((P +* (stop I)),s);
definition
let I be Program of SCMPDS;
attrI is paraclosed means :Def6: :: SCMPDS_4:def 6
for s being 0 -started State of SCMPDS
for n being Element of NAT
for P being Instruction-Sequence of SCMPDS st stop I c= P holds
IC (Comput (P,s,n)) in dom (stop I);
attrI is parahalting means :Def7: :: SCMPDS_4:def 7
for s being 0 -started State of SCMPDS
for P being Instruction-Sequence of SCMPDS st stop I c= P holds
P halts_on s;
end;
:: deftheorem Def6 defines paraclosed SCMPDS_4:def_6_:_
for I being Program of SCMPDS holds
( I is paraclosed iff for s being 0 -started State of SCMPDS
for n being Element of NAT
for P being Instruction-Sequence of SCMPDS st stop I c= P holds
IC (Comput (P,s,n)) in dom (stop I) );
:: deftheorem Def7 defines parahalting SCMPDS_4:def_7_:_
for I being Program of SCMPDS holds
( I is parahalting iff for s being 0 -started State of SCMPDS
for P being Instruction-Sequence of SCMPDS st stop I c= P holds
P halts_on s );
Lm1: Load (halt SCMPDS) is parahalting
proof
let s be 0 -started State of SCMPDS; :: according to SCMPDS_4:def_7 ::_thesis: for P being Instruction-Sequence of SCMPDS st stop (Load (halt SCMPDS)) c= P holds
P halts_on s
let P be Instruction-Sequence of SCMPDS; ::_thesis: ( stop (Load (halt SCMPDS)) c= P implies P halts_on s )
set m = Load (halt SCMPDS);
set m0 = stop (Load (halt SCMPDS));
assume A1: stop (Load (halt SCMPDS)) c= P ; ::_thesis: P halts_on s
A2: IC s = 0 by MEMSTR_0:def_11;
take 0 ; :: according to EXTPRO_1:def_8 ::_thesis: ( IC (Comput (P,s,0)) in proj1 P & CurInstr (P,(Comput (P,s,0))) = halt SCMPDS )
IC (Comput (P,s,0)) in NAT ;
hence IC (Comput (P,s,0)) in dom P by PARTFUN1:def_2; ::_thesis: CurInstr (P,(Comput (P,s,0))) = halt SCMPDS
A3: (Load (halt SCMPDS)) . 0 = halt SCMPDS by FUNCOP_1:72;
dom (Load (halt SCMPDS)) = {0} by FUNCOP_1:13;
then A4: 0 in dom (Load (halt SCMPDS)) by TARSKI:def_1;
then A5: 0 in dom (stop (Load (halt SCMPDS))) by FUNCT_4:12;
A6: P /. (IC s) = P . (IC s) by PBOOLE:143;
CurInstr (P,(Comput (P,s,0))) = (stop (Load (halt SCMPDS))) . 0 by A1, A5, A2, A6, GRFUNC_1:2
.= halt SCMPDS by A3, A4, AFINSQ_1:def_3 ;
hence CurInstr (P,(Comput (P,s,0))) = halt SCMPDS ; ::_thesis: verum
end;
registration
cluster non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() parahalting for set ;
existence
ex b1 being Program of SCMPDS st b1 is parahalting by Lm1;
end;
theorem :: SCMPDS_4:19
canceled;
theorem Th20: :: SCMPDS_4:20
for s being State of SCMPDS
for P, Q being Instruction-Sequence of SCMPDS st Q = P +* (((IC s),(succ (IC s))) --> ((goto 1),(goto (- 1)))) holds
not Q halts_on s
proof
let s be State of SCMPDS; ::_thesis: for P, Q being Instruction-Sequence of SCMPDS st Q = P +* (((IC s),(succ (IC s))) --> ((goto 1),(goto (- 1)))) holds
not Q halts_on s
let P, Q be Instruction-Sequence of SCMPDS; ::_thesis: ( Q = P +* (((IC s),(succ (IC s))) --> ((goto 1),(goto (- 1)))) implies not Q halts_on s )
assume A1: Q = P +* (((IC s),(succ (IC s))) --> ((goto 1),(goto (- 1)))) ; ::_thesis: not Q halts_on s
set m = ((IC s),(succ (IC s))) --> ((goto 1),(goto (- 1)));
A2: (((IC s),(succ (IC s))) --> ((goto 1),(goto (- 1)))) . (succ (IC s)) = goto (- 1) by FUNCT_4:63;
IC s <> succ (IC s) ;
then A3: (((IC s),(succ (IC s))) --> ((goto 1),(goto (- 1)))) . (IC s) = goto 1 by FUNCT_4:63;
defpred S1[ Nat] means ( IC (Comput (Q,s,$1)) = IC s or IC (Comput (Q,s,$1)) = succ (IC s) );
A4: dom (((IC s),(succ (IC s))) --> ((goto 1),(goto (- 1)))) = {(IC s),(succ (IC s))} by FUNCT_4:62;
then A5: succ (IC s) in dom (((IC s),(succ (IC s))) --> ((goto 1),(goto (- 1)))) by TARSKI:def_2;
A6: IC s in dom (((IC s),(succ (IC s))) --> ((goto 1),(goto (- 1)))) by A4, TARSKI:def_2;
now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_(_not_IC_(Comput_(Q,s,n))_=_IC_s_&_not_IC_(Comput_(Q,s,n))_=_succ_(IC_s)_)_or_(_IC_(Comput_(Q,s,n))_=_IC_s_&_IC_(Comput_(Q,s,(n_+_1)))_=_succ_(IC_s)_)_or_(_IC_(Comput_(Q,s,n))_=_succ_(IC_s)_&_IC_(Comput_(Q,s,(n_+_1)))_=_IC_s_)_)
let n be Element of NAT ; ::_thesis: ( ( not IC (Comput (Q,s,n)) = IC s & not IC (Comput (Q,s,n)) = succ (IC s) ) or ( IC (Comput (Q,s,b1)) = IC s & IC (Comput (Q,s,(b1 + 1))) = succ (IC s) ) or ( IC (Comput (Q,s,b1)) = succ (IC s) & IC (Comput (Q,s,(b1 + 1))) = IC s ) )
set Cn = Comput (Q,s,n);
assume A7: ( IC (Comput (Q,s,n)) = IC s or IC (Comput (Q,s,n)) = succ (IC s) ) ; ::_thesis: ( ( IC (Comput (Q,s,b1)) = IC s & IC (Comput (Q,s,(b1 + 1))) = succ (IC s) ) or ( IC (Comput (Q,s,b1)) = succ (IC s) & IC (Comput (Q,s,(b1 + 1))) = IC s ) )
A8: Q /. (IC (Comput (Q,s,n))) = Q . (IC (Comput (Q,s,n))) by PBOOLE:143;
percases ( IC (Comput (Q,s,n)) = IC s or IC (Comput (Q,s,n)) = succ (IC s) ) by A7;
caseA9: IC (Comput (Q,s,n)) = IC s ; ::_thesis: IC (Comput (Q,s,(n + 1))) = succ (IC s)
then A10: CurInstr (Q,(Comput (Q,s,n))) = Q . (IC s) by A8
.= goto 1 by A6, A3, A1, FUNCT_4:13 ;
thus IC (Comput (Q,s,(n + 1))) = IC (Following (Q,(Comput (Q,s,n)))) by EXTPRO_1:3
.= ICplusConst ((Comput (Q,s,n)),1) by A10, SCMPDS_2:54
.= succ (IC s) by A9, SCMPDS_3:10 ; ::_thesis: verum
end;
caseA11: IC (Comput (Q,s,n)) = succ (IC s) ; ::_thesis: IC (Comput (Q,s,(n + 1))) = IC s
reconsider i = IC s as Element of NAT ;
A12: ex j being Element of NAT st
( j = IC (Comput (Q,s,n)) & ICplusConst ((Comput (Q,s,n)),(- 1)) = abs (j + (- 1)) ) by SCMPDS_2:def_18;
A13: Q /. (IC (Comput (Q,s,n))) = Q . (IC (Comput (Q,s,n))) by PBOOLE:143;
A14: CurInstr (Q,(Comput (Q,s,n))) = Q . (succ (IC s)) by A11, A13
.= goto (- 1) by A5, A2, A1, FUNCT_4:13 ;
thus IC (Comput (Q,s,(n + 1))) = IC (Following (Q,(Comput (Q,s,n)))) by EXTPRO_1:3
.= abs ((i + 4) + (- 4)) by A11, A14, A12, SCMPDS_2:54
.= IC s by ABSVALUE:def_1 ; ::_thesis: verum
end;
end;
end;
then A15: for n being Element of NAT st S1[n] holds
S1[n + 1] ;
let nn be Nat; :: according to EXTPRO_1:def_8 ::_thesis: ( not IC (Comput (Q,s,nn)) in proj1 Q or not CurInstr (Q,(Comput (Q,s,nn))) = halt SCMPDS )
reconsider n = nn as Element of NAT by ORDINAL1:def_12;
assume IC (Comput (Q,s,nn)) in dom Q ; ::_thesis: not CurInstr (Q,(Comput (Q,s,nn))) = halt SCMPDS
A16: S1[ 0 ] ;
A17: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A16, A15);
A18: Q /. (IC (Comput (Q,s,n))) = Q . (IC (Comput (Q,s,n))) by PBOOLE:143;
percases ( IC (Comput (Q,s,n)) = IC s or IC (Comput (Q,s,n)) = succ (IC s) ) by A17;
suppose IC (Comput (Q,s,n)) = IC s ; ::_thesis: not CurInstr (Q,(Comput (Q,s,nn))) = halt SCMPDS
then CurInstr (Q,(Comput (Q,s,n))) = Q . (IC s) by A18
.= goto 1 by A6, A3, A1, FUNCT_4:13 ;
hence not CurInstr (Q,(Comput (Q,s,nn))) = halt SCMPDS by SCMPDS_2:73; ::_thesis: verum
end;
suppose IC (Comput (Q,s,n)) = succ (IC s) ; ::_thesis: not CurInstr (Q,(Comput (Q,s,nn))) = halt SCMPDS
then CurInstr (Q,(Comput (Q,s,n))) = Q . (succ (IC s)) by A18
.= goto (- 1) by A5, A2, A1, FUNCT_4:13 ;
hence not CurInstr (Q,(Comput (Q,s,nn))) = halt SCMPDS by SCMPDS_2:73; ::_thesis: verum
end;
end;
end;
theorem Th21: :: SCMPDS_4:21
for n being Element of NAT
for I being Program of SCMPDS
for s1, s2 being State of SCMPDS
for P1, P2 being Instruction-Sequence of SCMPDS st s1 = s2 & I c= P1 & I c= P2 & ( for m being Element of NAT st m < n holds
IC (Comput (P2,s2,m)) in dom I ) holds
for m being Element of NAT st m <= n holds
Comput (P1,s1,m) = Comput (P2,s2,m)
proof
let n be Element of NAT ; ::_thesis: for I being Program of SCMPDS
for s1, s2 being State of SCMPDS
for P1, P2 being Instruction-Sequence of SCMPDS st s1 = s2 & I c= P1 & I c= P2 & ( for m being Element of NAT st m < n holds
IC (Comput (P2,s2,m)) in dom I ) holds
for m being Element of NAT st m <= n holds
Comput (P1,s1,m) = Comput (P2,s2,m)
let I be Program of SCMPDS; ::_thesis: for s1, s2 being State of SCMPDS
for P1, P2 being Instruction-Sequence of SCMPDS st s1 = s2 & I c= P1 & I c= P2 & ( for m being Element of NAT st m < n holds
IC (Comput (P2,s2,m)) in dom I ) holds
for m being Element of NAT st m <= n holds
Comput (P1,s1,m) = Comput (P2,s2,m)
let s1, s2 be State of SCMPDS; ::_thesis: for P1, P2 being Instruction-Sequence of SCMPDS st s1 = s2 & I c= P1 & I c= P2 & ( for m being Element of NAT st m < n holds
IC (Comput (P2,s2,m)) in dom I ) holds
for m being Element of NAT st m <= n holds
Comput (P1,s1,m) = Comput (P2,s2,m)
let P1, P2 be Instruction-Sequence of SCMPDS; ::_thesis: ( s1 = s2 & I c= P1 & I c= P2 & ( for m being Element of NAT st m < n holds
IC (Comput (P2,s2,m)) in dom I ) implies for m being Element of NAT st m <= n holds
Comput (P1,s1,m) = Comput (P2,s2,m) )
assume that
A1: s1 = s2 and
A2: I c= P1 and
A3: I c= P2 and
A4: for m being Element of NAT st m < n holds
IC (Comput (P2,s2,m)) in dom I ; ::_thesis: for m being Element of NAT st m <= n holds
Comput (P1,s1,m) = Comput (P2,s2,m)
defpred S1[ Nat] means ( $1 <= n implies Comput (P1,s1,$1) = Comput (P2,s2,$1) );
A5: for m being Element of NAT st S1[m] holds
S1[m + 1]
proof
let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A6: ( m <= n implies Comput (P1,s1,m) = Comput (P2,s2,m) ) ; ::_thesis: S1[m + 1]
A7: Comput (P2,s2,(m + 1)) = Following (P2,(Comput (P2,s2,m))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,m)))),(Comput (P2,s2,m))) ;
A8: Comput (P1,s1,(m + 1)) = Following (P1,(Comput (P1,s1,m))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,m)))),(Comput (P1,s1,m))) ;
assume A9: m + 1 <= n ; ::_thesis: Comput (P1,s1,(m + 1)) = Comput (P2,s2,(m + 1))
then A10: IC (Comput (P1,s1,m)) = IC (Comput (P2,s2,m)) by A6, NAT_1:13;
m < n by A9, NAT_1:13;
then A11: IC (Comput (P2,s2,m)) in dom I by A4;
A12: P1 /. (IC (Comput (P1,s1,m))) = P1 . (IC (Comput (P1,s1,m))) by PBOOLE:143;
A13: P2 /. (IC (Comput (P2,s2,m))) = P2 . (IC (Comput (P2,s2,m))) by PBOOLE:143;
CurInstr (P1,(Comput (P1,s1,m))) = P1 . (IC (Comput (P1,s1,m))) by A12
.= I . (IC (Comput (P1,s1,m))) by A2, A11, A10, GRFUNC_1:2
.= P2 . (IC (Comput (P2,s2,m))) by A3, A11, A10, GRFUNC_1:2
.= CurInstr (P2,(Comput (P2,s2,m))) by A13 ;
hence Comput (P1,s1,(m + 1)) = Comput (P2,s2,(m + 1)) by A6, A8, A7, A9, NAT_1:13; ::_thesis: verum
end;
A14: S1[ 0 ] by A1;
thus for m being Element of NAT holds S1[m] from NAT_1:sch_1(A14, A5); ::_thesis: verum
end;
registration
cluster non empty Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V71() parahalting -> paraclosed for set ;
coherence
for b1 being Program of SCMPDS st b1 is parahalting holds
b1 is paraclosed
proof
let I be Program of SCMPDS; ::_thesis: ( I is parahalting implies I is paraclosed )
assume A1: I is parahalting ; ::_thesis: I is paraclosed
let s be 0 -started State of SCMPDS; :: according to SCMPDS_4:def_6 ::_thesis: for n being Element of NAT
for P being Instruction-Sequence of SCMPDS st stop I c= P holds
IC (Comput (P,s,n)) in dom (stop I)
let n be Element of NAT ; ::_thesis: for P being Instruction-Sequence of SCMPDS st stop I c= P holds
IC (Comput (P,s,n)) in dom (stop I)
let P be Instruction-Sequence of SCMPDS; ::_thesis: ( stop I c= P implies IC (Comput (P,s,n)) in dom (stop I) )
defpred S1[ Nat] means not IC (Comput (P,s,c1)) in dom (stop I);
assume A2: stop I c= P ; ::_thesis: IC (Comput (P,s,n)) in dom (stop I)
assume not IC (Comput (P,s,n)) in dom (stop I) ; ::_thesis: contradiction
then A3: ex n being Nat st S1[n] ;
consider n being Nat such that
A4: S1[n] and
A5: for m being Nat st S1[m] holds
n <= m from NAT_1:sch_5(A3);
reconsider n = n as Element of NAT by ORDINAL1:def_12;
A6: for m being Element of NAT st m < n holds
IC (Comput (P,s,m)) in dom (stop I) by A5;
set s2 = Comput (P,s,n);
set Ig = ((IC (Comput (P,s,n))),(succ (IC (Comput (P,s,n))))) --> ((goto 1),(goto (- 1)));
reconsider P0 = P +* (((IC (Comput (P,s,n))),(succ (IC (Comput (P,s,n))))) --> ((goto 1),(goto (- 1)))) as Instruction-Sequence of SCMPDS ;
reconsider P3 = P +* ((IC (Comput (P,s,n))),(goto 1)) as Instruction-Sequence of SCMPDS ;
reconsider P2 = P3 +* ((succ (IC (Comput (P,s,n)))),(goto (- 1))) as Instruction-Sequence of SCMPDS ;
reconsider P4 = P3 +* ((succ (IC (Comput (P,s,n)))),(goto (- 1))) as Instruction-Sequence of SCMPDS ;
A7: P0 = P4 by FUNCT_7:139;
A8: not succ (IC (Comput (P,s,n))) in dom (stop I) by A4, AFINSQ_1:73;
stop I c= P3 by A2, A4, FUNCT_7:89;
then stop I c= P4 by A8, FUNCT_7:89;
then A9: stop I c= P0 by A7;
then Comput (P0,s,n) = Comput (P,s,n) by A2, A6, Th21;
then A10: Comput (P0,s,n) = Comput (P,s,n) ;
A11: not P0 halts_on Comput (P,s,n) by Th20;
P0 halts_on s by A1, A9, Def7;
then P0 halts_on Comput (P0,s,n) by EXTPRO_1:22;
then P0 halts_on Comput (P,s,n) by A10;
hence contradiction by A11; ::_thesis: verum
end;
end;
begin
definition
let i be Instruction of SCMPDS;
let n be Element of NAT ;
predi valid_at n means :Def8: :: SCMPDS_4:def 8
( ( InsCode i = 14 implies ex k1 being Integer st
( i = goto k1 & n + k1 >= 0 ) ) & ( InsCode i = 4 implies ex a being Int_position ex k1, k2 being Integer st
( i = (a,k1) <>0_goto k2 & n + k2 >= 0 ) ) & ( InsCode i = 5 implies ex a being Int_position ex k1, k2 being Integer st
( i = (a,k1) <=0_goto k2 & n + k2 >= 0 ) ) & ( InsCode i = 6 implies ex a being Int_position ex k1, k2 being Integer st
( i = (a,k1) >=0_goto k2 & n + k2 >= 0 ) ) );
end;
:: deftheorem Def8 defines valid_at SCMPDS_4:def_8_:_
for i being Instruction of SCMPDS
for n being Element of NAT holds
( i valid_at n iff ( ( InsCode i = 14 implies ex k1 being Integer st
( i = goto k1 & n + k1 >= 0 ) ) & ( InsCode i = 4 implies ex a being Int_position ex k1, k2 being Integer st
( i = (a,k1) <>0_goto k2 & n + k2 >= 0 ) ) & ( InsCode i = 5 implies ex a being Int_position ex k1, k2 being Integer st
( i = (a,k1) <=0_goto k2 & n + k2 >= 0 ) ) & ( InsCode i = 6 implies ex a being Int_position ex k1, k2 being Integer st
( i = (a,k1) >=0_goto k2 & n + k2 >= 0 ) ) ) );
definition
let IT be NAT -defined the InstructionsF of SCMPDS -valued finite Function;
attrIT is shiftable means :Def9: :: SCMPDS_4:def 9
for n being Element of NAT
for i being Instruction of SCMPDS st n in dom IT & i = IT . n holds
( InsCode i <> 1 & InsCode i <> 3 & i valid_at n );
end;
:: deftheorem Def9 defines shiftable SCMPDS_4:def_9_:_
for IT being NAT -defined the InstructionsF of SCMPDS -valued finite Function holds
( IT is shiftable iff for n being Element of NAT
for i being Instruction of SCMPDS st n in dom IT & i = IT . n holds
( InsCode i <> 1 & InsCode i <> 3 & i valid_at n ) );
Lm2: Load (halt SCMPDS) is shiftable
proof
set m = Load (halt SCMPDS);
A1: dom (Load (halt SCMPDS)) = {0} by FUNCOP_1:13;
let n be Element of NAT ; :: according to SCMPDS_4:def_9 ::_thesis: for i being Instruction of SCMPDS st n in dom (Load (halt SCMPDS)) & i = (Load (halt SCMPDS)) . n holds
( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )
let i be Instruction of SCMPDS; ::_thesis: ( n in dom (Load (halt SCMPDS)) & i = (Load (halt SCMPDS)) . n implies ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n ) )
assume that
A2: n in dom (Load (halt SCMPDS)) and
A3: i = (Load (halt SCMPDS)) . n ; ::_thesis: ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )
A4: n = 0 by A1, A2, TARSKI:def_1;
i = halt SCMPDS by A3, A4, AFINSQ_1:34;
then i = [0,{},{}] by SCMPDS_2:80;
then A5: InsCode i = 0 by RECDEF_2:def_1;
hence ( InsCode i <> 1 & InsCode i <> 3 ) ; ::_thesis: i valid_at n
( InsCode i <> 4 & InsCode i <> 5 & InsCode i <> 6 & InsCode i <> 14 ) by A5;
hence i valid_at n by Def8; ::_thesis: verum
end;
theorem Th22: :: SCMPDS_4:22
for i being Instruction of SCMPDS
for m, n being Element of NAT st i valid_at m & m <= n holds
i valid_at n
proof
let i be Instruction of SCMPDS; ::_thesis: for m, n being Element of NAT st i valid_at m & m <= n holds
i valid_at n
let m, n be Element of NAT ; ::_thesis: ( i valid_at m & m <= n implies i valid_at n )
assume that
A1: i valid_at m and
A2: m <= n ; ::_thesis: i valid_at n
A3: now__::_thesis:_(_InsCode_i_=_4_implies_ex_a_being_Int_position_ex_k1,_k2_being_Integer_st_
(_i_=_(a,k1)_<>0_goto_k2_&_n_+_k2_>=_0_)_)
assume InsCode i = 4 ; ::_thesis: ex a being Int_position ex k1, k2 being Integer st
( i = (a,k1) <>0_goto k2 & n + k2 >= 0 )
then consider a being Int_position, k1, k2 being Integer such that
A4: i = (a,k1) <>0_goto k2 and
A5: m + k2 >= 0 by A1, Def8;
take a = a; ::_thesis: ex k1, k2 being Integer st
( i = (a,k1) <>0_goto k2 & n + k2 >= 0 )
take k1 = k1; ::_thesis: ex k2 being Integer st
( i = (a,k1) <>0_goto k2 & n + k2 >= 0 )
take k2 = k2; ::_thesis: ( i = (a,k1) <>0_goto k2 & n + k2 >= 0 )
thus i = (a,k1) <>0_goto k2 by A4; ::_thesis: n + k2 >= 0
thus n + k2 >= 0 by A2, A5, XREAL_1:6; ::_thesis: verum
end;
A6: now__::_thesis:_(_InsCode_i_=_6_implies_ex_a_being_Int_position_ex_k1,_k2_being_Integer_st_
(_i_=_(a,k1)_>=0_goto_k2_&_n_+_k2_>=_0_)_)
assume InsCode i = 6 ; ::_thesis: ex a being Int_position ex k1, k2 being Integer st
( i = (a,k1) >=0_goto k2 & n + k2 >= 0 )
then consider a being Int_position, k1, k2 being Integer such that
A7: i = (a,k1) >=0_goto k2 and
A8: m + k2 >= 0 by A1, Def8;
take a = a; ::_thesis: ex k1, k2 being Integer st
( i = (a,k1) >=0_goto k2 & n + k2 >= 0 )
take k1 = k1; ::_thesis: ex k2 being Integer st
( i = (a,k1) >=0_goto k2 & n + k2 >= 0 )
take k2 = k2; ::_thesis: ( i = (a,k1) >=0_goto k2 & n + k2 >= 0 )
thus i = (a,k1) >=0_goto k2 by A7; ::_thesis: n + k2 >= 0
thus n + k2 >= 0 by A2, A8, XREAL_1:6; ::_thesis: verum
end;
A9: now__::_thesis:_(_InsCode_i_=_5_implies_ex_a_being_Int_position_ex_k1,_k2_being_Integer_st_
(_i_=_(a,k1)_<=0_goto_k2_&_n_+_k2_>=_0_)_)
assume InsCode i = 5 ; ::_thesis: ex a being Int_position ex k1, k2 being Integer st
( i = (a,k1) <=0_goto k2 & n + k2 >= 0 )
then consider a being Int_position, k1, k2 being Integer such that
A10: i = (a,k1) <=0_goto k2 and
A11: m + k2 >= 0 by A1, Def8;
take a = a; ::_thesis: ex k1, k2 being Integer st
( i = (a,k1) <=0_goto k2 & n + k2 >= 0 )
take k1 = k1; ::_thesis: ex k2 being Integer st
( i = (a,k1) <=0_goto k2 & n + k2 >= 0 )
take k2 = k2; ::_thesis: ( i = (a,k1) <=0_goto k2 & n + k2 >= 0 )
thus i = (a,k1) <=0_goto k2 by A10; ::_thesis: n + k2 >= 0
thus n + k2 >= 0 by A2, A11, XREAL_1:6; ::_thesis: verum
end;
now__::_thesis:_(_InsCode_i_=_14_implies_ex_k1_being_Integer_st_
(_i_=_goto_k1_&_n_+_k1_>=_0_)_)
assume InsCode i = 14 ; ::_thesis: ex k1 being Integer st
( i = goto k1 & n + k1 >= 0 )
then consider k1 being Integer such that
A12: i = goto k1 and
A13: m + k1 >= 0 by A1, Def8;
take k1 = k1; ::_thesis: ( i = goto k1 & n + k1 >= 0 )
thus i = goto k1 by A12; ::_thesis: n + k1 >= 0
thus n + k1 >= 0 by A2, A13, XREAL_1:6; ::_thesis: verum
end;
hence i valid_at n by A3, A9, A6, Def8; ::_thesis: verum
end;
registration
cluster non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like finite V43() V71() V136() parahalting shiftable for set ;
existence
ex b1 being Program of SCMPDS st
( b1 is parahalting & b1 is shiftable ) by Lm1, Lm2;
end;
definition
let i be Instruction of SCMPDS;
attri is shiftable means :Def10: :: SCMPDS_4:def 10
( InsCode i = 2 or ( InsCode i <> 14 & InsCode i > 6 ) );
end;
:: deftheorem Def10 defines shiftable SCMPDS_4:def_10_:_
for i being Instruction of SCMPDS holds
( i is shiftable iff ( InsCode i = 2 or ( InsCode i <> 14 & InsCode i > 6 ) ) );
registration
cluster shiftable for Element of the InstructionsF of SCMPDS;
existence
ex b1 being Instruction of SCMPDS st b1 is shiftable
proof
take i = (DataLoc (0,0)) := 1; ::_thesis: i is shiftable
InsCode i = 2 by SCMPDS_2:14;
hence i is shiftable by Def10; ::_thesis: verum
end;
end;
registration
let a be Int_position;
let k1 be Integer;
clustera := k1 -> shiftable ;
coherence
a := k1 is shiftable
proof
InsCode (a := k1) = 2 by SCMPDS_2:14;
hence a := k1 is shiftable by Def10; ::_thesis: verum
end;
end;
registration
let a be Int_position;
let k1, k2 be Integer;
cluster(a,k1) := k2 -> shiftable ;
coherence
(a,k1) := k2 is shiftable
proof
InsCode ((a,k1) := k2) = 7 by SCMPDS_2:19;
hence (a,k1) := k2 is shiftable by Def10; ::_thesis: verum
end;
end;
registration
let a be Int_position;
let k1, k2 be Integer;
cluster AddTo (a,k1,k2) -> shiftable ;
coherence
AddTo (a,k1,k2) is shiftable
proof
InsCode (AddTo (a,k1,k2)) = 8 by SCMPDS_2:20;
hence AddTo (a,k1,k2) is shiftable by Def10; ::_thesis: verum
end;
end;
registration
let a, b be Int_position;
let k1, k2 be Integer;
cluster AddTo (a,k1,b,k2) -> shiftable ;
coherence
AddTo (a,k1,b,k2) is shiftable
proof
InsCode (AddTo (a,k1,b,k2)) = 9 by SCMPDS_2:21;
hence AddTo (a,k1,b,k2) is shiftable by Def10; ::_thesis: verum
end;
cluster SubFrom (a,k1,b,k2) -> shiftable ;
coherence
SubFrom (a,k1,b,k2) is shiftable
proof
InsCode (SubFrom (a,k1,b,k2)) = 10 by SCMPDS_2:22;
hence SubFrom (a,k1,b,k2) is shiftable by Def10; ::_thesis: verum
end;
cluster MultBy (a,k1,b,k2) -> shiftable ;
coherence
MultBy (a,k1,b,k2) is shiftable
proof
InsCode (MultBy (a,k1,b,k2)) = 11 by SCMPDS_2:23;
hence MultBy (a,k1,b,k2) is shiftable by Def10; ::_thesis: verum
end;
cluster Divide (a,k1,b,k2) -> shiftable ;
coherence
Divide (a,k1,b,k2) is shiftable
proof
InsCode (Divide (a,k1,b,k2)) = 12 by SCMPDS_2:24;
hence Divide (a,k1,b,k2) is shiftable by Def10; ::_thesis: verum
end;
cluster(a,k1) := (b,k2) -> shiftable ;
coherence
(a,k1) := (b,k2) is shiftable
proof
InsCode ((a,k1) := (b,k2)) = 13 by SCMPDS_2:25;
hence (a,k1) := (b,k2) is shiftable by Def10; ::_thesis: verum
end;
end;
registration
let I, J be shiftable Program of SCMPDS;
clusterI ';' J -> shiftable for Program of SCMPDS;
coherence
for b1 being Program of SCMPDS st b1 = I ';' J holds
b1 is shiftable
proof
set IJ = I ';' J;
now__::_thesis:_for_n_being_Element_of_NAT_
for_i_being_Instruction_of_SCMPDS_st_n_in_dom_(I_';'_J)_&_i_=_(I_';'_J)_._n_holds_
(_InsCode_i_<>_1_&_InsCode_i_<>_3_&_i_valid_at_n_)
set D = { (l + (card I)) where l is Element of NAT : l in dom J } ;
let n be Element of NAT ; ::_thesis: for i being Instruction of SCMPDS st n in dom (I ';' J) & i = (I ';' J) . n holds
( InsCode b3 <> 1 & InsCode b3 <> 3 & b3 valid_at b2 )
let i be Instruction of SCMPDS; ::_thesis: ( n in dom (I ';' J) & i = (I ';' J) . n implies ( InsCode b2 <> 1 & InsCode b2 <> 3 & b2 valid_at b1 ) )
assume that
A1: n in dom (I ';' J) and
A2: i = (I ';' J) . n ; ::_thesis: ( InsCode b2 <> 1 & InsCode b2 <> 3 & b2 valid_at b1 )
dom (Shift (J,(card I))) = { (l + (card I)) where l is Element of NAT : l in dom J } by VALUED_1:def_12;
then A3: dom (I ';' J) = (dom I) \/ { (l + (card I)) where l is Element of NAT : l in dom J } by FUNCT_4:def_1;
percases ( n in dom I or n in { (l + (card I)) where l is Element of NAT : l in dom J } ) by A1, A3, XBOOLE_0:def_3;
supposeA4: n in dom I ; ::_thesis: ( InsCode b2 <> 1 & InsCode b2 <> 3 & b2 valid_at b1 )
then I . n = i by A2, AFINSQ_1:def_3;
hence ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n ) by A4, Def9; ::_thesis: verum
end;
suppose n in { (l + (card I)) where l is Element of NAT : l in dom J } ; ::_thesis: ( InsCode b2 <> 1 & InsCode b2 <> 3 & b2 valid_at b1 )
then consider l being Element of NAT such that
A5: n = l + (card I) and
A6: l in dom J ;
A7: J . l = i by A2, A5, A6, AFINSQ_1:def_3;
hence ( InsCode i <> 1 & InsCode i <> 3 ) by A6, Def9; ::_thesis: i valid_at n
i valid_at l by A6, A7, Def9;
hence i valid_at n by A5, Th22, NAT_1:11; ::_thesis: verum
end;
end;
end;
hence for b1 being Program of SCMPDS st b1 = I ';' J holds
b1 is shiftable by Def9; ::_thesis: verum
end;
end;
registration
let i be shiftable Instruction of SCMPDS;
cluster Load -> shiftable for Program of SCMPDS;
coherence
for b1 being Program of SCMPDS st b1 = Load i holds
b1 is shiftable
proof
let p be Program of SCMPDS; ::_thesis: ( p = Load i implies p is shiftable )
assume A1: p = Load i ; ::_thesis: p is shiftable
let n be Element of NAT ; :: according to SCMPDS_4:def_9 ::_thesis: for i being Instruction of SCMPDS st n in dom p & i = p . n holds
( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )
let j be Instruction of SCMPDS; ::_thesis: ( n in dom p & j = p . n implies ( InsCode j <> 1 & InsCode j <> 3 & j valid_at n ) )
assume that
A2: n in dom p and
A3: j = p . n ; ::_thesis: ( InsCode j <> 1 & InsCode j <> 3 & j valid_at n )
dom p = {0} by A1, FUNCOP_1:13;
then n = 0 by A2, TARSKI:def_1;
then A4: j = i by A3, A1, FUNCOP_1:72;
hence InsCode j <> 1 by Def10; ::_thesis: ( InsCode j <> 3 & j valid_at n )
thus InsCode j <> 3 by A4, Def10; ::_thesis: j valid_at n
( InsCode j <> 4 & InsCode j <> 5 & InsCode j <> 6 & InsCode j <> 14 ) by A4, Def10;
hence j valid_at n by Def8; ::_thesis: verum
end;
end;
registration
let i be shiftable Instruction of SCMPDS;
let J be shiftable Program of SCMPDS;
clusteri ';' J -> shiftable ;
coherence
i ';' J is shiftable ;
end;
registration
let I be shiftable Program of SCMPDS;
let j be shiftable Instruction of SCMPDS;
clusterI ';' j -> shiftable ;
coherence
I ';' j is shiftable ;
end;
registration
let i, j be shiftable Instruction of SCMPDS;
clusteri ';' j -> shiftable ;
coherence
i ';' j is shiftable ;
end;
registration
cluster Stop SCMPDS -> parahalting shiftable ;
coherence
( Stop SCMPDS is parahalting & Stop SCMPDS is shiftable ) by Lm1, Lm2;
end;
registration
let I be shiftable Program of SCMPDS;
cluster stop I -> shiftable ;
coherence
stop I is shiftable ;
end;
theorem :: SCMPDS_4:23
for I being shiftable Program of SCMPDS
for k1 being Integer st (card I) + k1 >= 0 holds
I ';' (goto k1) is shiftable
proof
let I be shiftable Program of SCMPDS; ::_thesis: for k1 being Integer st (card I) + k1 >= 0 holds
I ';' (goto k1) is shiftable
let k1 be Integer; ::_thesis: ( (card I) + k1 >= 0 implies I ';' (goto k1) is shiftable )
set J = Load (goto k1);
set Ig = I ';' (goto k1);
assume A1: (card I) + k1 >= 0 ; ::_thesis: I ';' (goto k1) is shiftable
now__::_thesis:_for_n_being_Element_of_NAT_
for_i_being_Instruction_of_SCMPDS_st_n_in_dom_(I_';'_(goto_k1))_&_i_=_(I_';'_(goto_k1))_._n_holds_
(_InsCode_i_<>_1_&_InsCode_i_<>_3_&_i_valid_at_n_)
set D = { (l + (card I)) where l is Element of NAT : l in dom (Load (goto k1)) } ;
let n be Element of NAT ; ::_thesis: for i being Instruction of SCMPDS st n in dom (I ';' (goto k1)) & i = (I ';' (goto k1)) . n holds
( InsCode b3 <> 1 & InsCode b3 <> 3 & b3 valid_at b2 )
let i be Instruction of SCMPDS; ::_thesis: ( n in dom (I ';' (goto k1)) & i = (I ';' (goto k1)) . n implies ( InsCode b2 <> 1 & InsCode b2 <> 3 & b2 valid_at b1 ) )
assume that
A2: n in dom (I ';' (goto k1)) and
A3: i = (I ';' (goto k1)) . n ; ::_thesis: ( InsCode b2 <> 1 & InsCode b2 <> 3 & b2 valid_at b1 )
dom (Shift ((Load (goto k1)),(card I))) = { (l + (card I)) where l is Element of NAT : l in dom (Load (goto k1)) } by VALUED_1:def_12;
then A4: dom (I ';' (goto k1)) = (dom I) \/ { (l + (card I)) where l is Element of NAT : l in dom (Load (goto k1)) } by FUNCT_4:def_1;
percases ( n in dom I or n in { (l + (card I)) where l is Element of NAT : l in dom (Load (goto k1)) } ) by A2, A4, XBOOLE_0:def_3;
supposeA5: n in dom I ; ::_thesis: ( InsCode b2 <> 1 & InsCode b2 <> 3 & b2 valid_at b1 )
then I . n = i by A3, AFINSQ_1:def_3;
hence ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n ) by A5, Def9; ::_thesis: verum
end;
suppose n in { (l + (card I)) where l is Element of NAT : l in dom (Load (goto k1)) } ; ::_thesis: ( InsCode b2 <> 1 & InsCode b2 <> 3 & b2 valid_at b1 )
then consider l being Element of NAT such that
A6: n = l + (card I) and
A7: l in dom (Load (goto k1)) ;
dom (Load (goto k1)) = {0} by FUNCOP_1:13;
then A8: l = 0 by A7, TARSKI:def_1;
then A9: goto k1 = (Load (goto k1)) . l by FUNCOP_1:72
.= i by A3, A6, A7, AFINSQ_1:def_3 ;
hence ( InsCode i <> 1 & InsCode i <> 3 ) by SCMPDS_2:12; ::_thesis: i valid_at n
A10: InsCode i <> 6 by A9, SCMPDS_2:12;
( InsCode i <> 4 & InsCode i <> 5 ) by A9, SCMPDS_2:12;
hence i valid_at n by A1, A6, A8, A9, A10, Def8; ::_thesis: verum
end;
end;
end;
hence I ';' (goto k1) is shiftable by Def9; ::_thesis: verum
end;
registration
let n be Element of NAT ;
cluster Load -> shiftable for Program of SCMPDS;
coherence
for b1 being Program of SCMPDS st b1 = Load (goto n) holds
b1 is shiftable
proof
set k1 = n;
set J = Load (goto n);
now__::_thesis:_for_n_being_Element_of_NAT_
for_i_being_Instruction_of_SCMPDS_st_n_in_dom_(Load_(goto_n))_&_i_=_(Load_(goto_n))_._n_holds_
(_InsCode_i_<>_1_&_InsCode_i_<>_3_&_i_valid_at_n_)
let n be Element of NAT ; ::_thesis: for i being Instruction of SCMPDS st n in dom (Load (goto n)) & i = (Load (goto n)) . n holds
( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )
let i be Instruction of SCMPDS; ::_thesis: ( n in dom (Load (goto n)) & i = (Load (goto n)) . n implies ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n ) )
assume that
A1: n in dom (Load (goto n)) and
A2: i = (Load (goto n)) . n ; ::_thesis: ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )
dom (Load (goto n)) = {0} by FUNCOP_1:13;
then n = 0 by A1, TARSKI:def_1;
then A3: goto n = i by A2, FUNCOP_1:72;
hence ( InsCode i <> 1 & InsCode i <> 3 ) by SCMPDS_2:12; ::_thesis: i valid_at n
A4: ( n + n >= 0 & InsCode i <> 6 ) by A3, SCMPDS_2:12;
( InsCode i <> 4 & InsCode i <> 5 ) by A3, SCMPDS_2:12;
hence i valid_at n by A3, A4, Def8; ::_thesis: verum
end;
hence for b1 being Program of SCMPDS st b1 = Load (goto n) holds
b1 is shiftable by Def9; ::_thesis: verum
end;
end;
theorem :: SCMPDS_4:24
for I being shiftable Program of SCMPDS
for k1, k2 being Integer
for a being Int_position st (card I) + k2 >= 0 holds
I ';' ((a,k1) <>0_goto k2) is shiftable
proof
let I be shiftable Program of SCMPDS; ::_thesis: for k1, k2 being Integer
for a being Int_position st (card I) + k2 >= 0 holds
I ';' ((a,k1) <>0_goto k2) is shiftable
let k1, k2 be Integer; ::_thesis: for a being Int_position st (card I) + k2 >= 0 holds
I ';' ((a,k1) <>0_goto k2) is shiftable
let a be Int_position; ::_thesis: ( (card I) + k2 >= 0 implies I ';' ((a,k1) <>0_goto k2) is shiftable )
set ii = (a,k1) <>0_goto k2;
set J = Load ((a,k1) <>0_goto k2);
set Ig = I ';' ((a,k1) <>0_goto k2);
assume A1: (card I) + k2 >= 0 ; ::_thesis: I ';' ((a,k1) <>0_goto k2) is shiftable
now__::_thesis:_for_n_being_Element_of_NAT_
for_i_being_Instruction_of_SCMPDS_st_n_in_dom_(I_';'_((a,k1)_<>0_goto_k2))_&_i_=_(I_';'_((a,k1)_<>0_goto_k2))_._n_holds_
(_InsCode_i_<>_1_&_InsCode_i_<>_3_&_i_valid_at_n_)
set D = { (l + (card I)) where l is Element of NAT : l in dom (Load ((a,k1) <>0_goto k2)) } ;
let n be Element of NAT ; ::_thesis: for i being Instruction of SCMPDS st n in dom (I ';' ((a,k1) <>0_goto k2)) & i = (I ';' ((a,k1) <>0_goto k2)) . n holds
( InsCode b3 <> 1 & InsCode b3 <> 3 & b3 valid_at b2 )
let i be Instruction of SCMPDS; ::_thesis: ( n in dom (I ';' ((a,k1) <>0_goto k2)) & i = (I ';' ((a,k1) <>0_goto k2)) . n implies ( InsCode b2 <> 1 & InsCode b2 <> 3 & b2 valid_at b1 ) )
assume that
A2: n in dom (I ';' ((a,k1) <>0_goto k2)) and
A3: i = (I ';' ((a,k1) <>0_goto k2)) . n ; ::_thesis: ( InsCode b2 <> 1 & InsCode b2 <> 3 & b2 valid_at b1 )
dom (Shift ((Load ((a,k1) <>0_goto k2)),(card I))) = { (l + (card I)) where l is Element of NAT : l in dom (Load ((a,k1) <>0_goto k2)) } by VALUED_1:def_12;
then A4: dom (I ';' ((a,k1) <>0_goto k2)) = (dom I) \/ { (l + (card I)) where l is Element of NAT : l in dom (Load ((a,k1) <>0_goto k2)) } by FUNCT_4:def_1;
percases ( n in dom I or n in { (l + (card I)) where l is Element of NAT : l in dom (Load ((a,k1) <>0_goto k2)) } ) by A2, A4, XBOOLE_0:def_3;
supposeA5: n in dom I ; ::_thesis: ( InsCode b2 <> 1 & InsCode b2 <> 3 & b2 valid_at b1 )
then I . n = i by A3, AFINSQ_1:def_3;
hence ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n ) by A5, Def9; ::_thesis: verum
end;
suppose n in { (l + (card I)) where l is Element of NAT : l in dom (Load ((a,k1) <>0_goto k2)) } ; ::_thesis: ( InsCode b2 <> 1 & InsCode b2 <> 3 & b2 valid_at b1 )
then consider l being Element of NAT such that
A6: n = l + (card I) and
A7: l in dom (Load ((a,k1) <>0_goto k2)) ;
dom (Load ((a,k1) <>0_goto k2)) = {0} by FUNCOP_1:13;
then A8: l = 0 by A7, TARSKI:def_1;
then A9: (a,k1) <>0_goto k2 = (Load ((a,k1) <>0_goto k2)) . l by FUNCOP_1:72
.= i by A3, A6, A7, AFINSQ_1:def_3 ;
hence ( InsCode i <> 1 & InsCode i <> 3 ) by SCMPDS_2:16; ::_thesis: i valid_at n
A10: ( InsCode i <> 6 & InsCode i <> 14 ) by A9, SCMPDS_2:16;
( InsCode i <> 0 & InsCode i <> 5 ) by A9, SCMPDS_2:16;
hence i valid_at n by A1, A6, A8, A9, A10, Def8; ::_thesis: verum
end;
end;
end;
hence I ';' ((a,k1) <>0_goto k2) is shiftable by Def9; ::_thesis: verum
end;
registration
let k1 be Integer;
let a be Int_position;
let n be Element of NAT ;
cluster Load -> shiftable for Program of SCMPDS;
coherence
for b1 being Program of SCMPDS st b1 = Load ((a,k1) <>0_goto n) holds
b1 is shiftable
proof
set k2 = n;
set ii = (a,k1) <>0_goto n;
set J = Load ((a,k1) <>0_goto n);
now__::_thesis:_for_n_being_Element_of_NAT_
for_i_being_Instruction_of_SCMPDS_st_n_in_dom_(Load_((a,k1)_<>0_goto_n))_&_i_=_(Load_((a,k1)_<>0_goto_n))_._n_holds_
(_InsCode_i_<>_1_&_InsCode_i_<>_3_&_i_valid_at_n_)
let n be Element of NAT ; ::_thesis: for i being Instruction of SCMPDS st n in dom (Load ((a,k1) <>0_goto n)) & i = (Load ((a,k1) <>0_goto n)) . n holds
( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )
let i be Instruction of SCMPDS; ::_thesis: ( n in dom (Load ((a,k1) <>0_goto n)) & i = (Load ((a,k1) <>0_goto n)) . n implies ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n ) )
assume that
A1: n in dom (Load ((a,k1) <>0_goto n)) and
A2: i = (Load ((a,k1) <>0_goto n)) . n ; ::_thesis: ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )
dom (Load ((a,k1) <>0_goto n)) = {0} by FUNCOP_1:13;
then n = 0 by A1, TARSKI:def_1;
then A3: (a,k1) <>0_goto n = i by A2, FUNCOP_1:72;
hence ( InsCode i <> 1 & InsCode i <> 3 ) by SCMPDS_2:16; ::_thesis: i valid_at n
A4: ( n + n >= 0 & InsCode i <> 6 & InsCode i <> 14 ) by A3, SCMPDS_2:16;
( InsCode i <> 0 & InsCode i <> 5 ) by A3, SCMPDS_2:16;
hence i valid_at n by A3, A4, Def8; ::_thesis: verum
end;
hence for b1 being Program of SCMPDS st b1 = Load ((a,k1) <>0_goto n) holds
b1 is shiftable by Def9; ::_thesis: verum
end;
end;
theorem :: SCMPDS_4:25
for I being shiftable Program of SCMPDS
for k1, k2 being Integer
for a being Int_position st (card I) + k2 >= 0 holds
I ';' ((a,k1) <=0_goto k2) is shiftable
proof
let I be shiftable Program of SCMPDS; ::_thesis: for k1, k2 being Integer
for a being Int_position st (card I) + k2 >= 0 holds
I ';' ((a,k1) <=0_goto k2) is shiftable
let k1, k2 be Integer; ::_thesis: for a being Int_position st (card I) + k2 >= 0 holds
I ';' ((a,k1) <=0_goto k2) is shiftable
let a be Int_position; ::_thesis: ( (card I) + k2 >= 0 implies I ';' ((a,k1) <=0_goto k2) is shiftable )
set ii = (a,k1) <=0_goto k2;
set J = Load ((a,k1) <=0_goto k2);
set Ig = I ';' ((a,k1) <=0_goto k2);
assume A1: (card I) + k2 >= 0 ; ::_thesis: I ';' ((a,k1) <=0_goto k2) is shiftable
now__::_thesis:_for_n_being_Element_of_NAT_
for_i_being_Instruction_of_SCMPDS_st_n_in_dom_(I_';'_((a,k1)_<=0_goto_k2))_&_i_=_(I_';'_((a,k1)_<=0_goto_k2))_._n_holds_
(_InsCode_i_<>_1_&_InsCode_i_<>_3_&_i_valid_at_n_)
set D = { (l + (card I)) where l is Element of NAT : l in dom (Load ((a,k1) <=0_goto k2)) } ;
let n be Element of NAT ; ::_thesis: for i being Instruction of SCMPDS st n in dom (I ';' ((a,k1) <=0_goto k2)) & i = (I ';' ((a,k1) <=0_goto k2)) . n holds
( InsCode b3 <> 1 & InsCode b3 <> 3 & b3 valid_at b2 )
let i be Instruction of SCMPDS; ::_thesis: ( n in dom (I ';' ((a,k1) <=0_goto k2)) & i = (I ';' ((a,k1) <=0_goto k2)) . n implies ( InsCode b2 <> 1 & InsCode b2 <> 3 & b2 valid_at b1 ) )
assume that
A2: n in dom (I ';' ((a,k1) <=0_goto k2)) and
A3: i = (I ';' ((a,k1) <=0_goto k2)) . n ; ::_thesis: ( InsCode b2 <> 1 & InsCode b2 <> 3 & b2 valid_at b1 )
dom (Shift ((Load ((a,k1) <=0_goto k2)),(card I))) = { (l + (card I)) where l is Element of NAT : l in dom (Load ((a,k1) <=0_goto k2)) } by VALUED_1:def_12;
then A4: dom (I ';' ((a,k1) <=0_goto k2)) = (dom I) \/ { (l + (card I)) where l is Element of NAT : l in dom (Load ((a,k1) <=0_goto k2)) } by FUNCT_4:def_1;
percases ( n in dom I or n in { (l + (card I)) where l is Element of NAT : l in dom (Load ((a,k1) <=0_goto k2)) } ) by A2, A4, XBOOLE_0:def_3;
supposeA5: n in dom I ; ::_thesis: ( InsCode b2 <> 1 & InsCode b2 <> 3 & b2 valid_at b1 )
then I . n = i by A3, AFINSQ_1:def_3;
hence ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n ) by A5, Def9; ::_thesis: verum
end;
suppose n in { (l + (card I)) where l is Element of NAT : l in dom (Load ((a,k1) <=0_goto k2)) } ; ::_thesis: ( InsCode b2 <> 1 & InsCode b2 <> 3 & b2 valid_at b1 )
then consider l being Element of NAT such that
A6: n = l + (card I) and
A7: l in dom (Load ((a,k1) <=0_goto k2)) ;
dom (Load ((a,k1) <=0_goto k2)) = {0} by FUNCOP_1:13;
then A8: l = 0 by A7, TARSKI:def_1;
then A9: (a,k1) <=0_goto k2 = (Load ((a,k1) <=0_goto k2)) . l by FUNCOP_1:72
.= i by A3, A6, A7, AFINSQ_1:def_3 ;
hence ( InsCode i <> 1 & InsCode i <> 3 ) by SCMPDS_2:17; ::_thesis: i valid_at n
A10: ( InsCode i <> 6 & InsCode i <> 14 ) by A9, SCMPDS_2:17;
( InsCode i <> 0 & InsCode i <> 4 ) by A9, SCMPDS_2:17;
hence i valid_at n by A1, A6, A8, A9, A10, Def8; ::_thesis: verum
end;
end;
end;
hence I ';' ((a,k1) <=0_goto k2) is shiftable by Def9; ::_thesis: verum
end;
registration
let k1 be Integer;
let a be Int_position;
let n be Element of NAT ;
cluster Load -> shiftable for Program of SCMPDS;
coherence
for b1 being Program of SCMPDS st b1 = Load ((a,k1) <=0_goto n) holds
b1 is shiftable
proof
set k2 = n;
set ii = (a,k1) <=0_goto n;
set J = Load ((a,k1) <=0_goto n);
now__::_thesis:_for_n_being_Element_of_NAT_
for_i_being_Instruction_of_SCMPDS_st_n_in_dom_(Load_((a,k1)_<=0_goto_n))_&_i_=_(Load_((a,k1)_<=0_goto_n))_._n_holds_
(_InsCode_i_<>_1_&_InsCode_i_<>_3_&_i_valid_at_n_)
let n be Element of NAT ; ::_thesis: for i being Instruction of SCMPDS st n in dom (Load ((a,k1) <=0_goto n)) & i = (Load ((a,k1) <=0_goto n)) . n holds
( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )
let i be Instruction of SCMPDS; ::_thesis: ( n in dom (Load ((a,k1) <=0_goto n)) & i = (Load ((a,k1) <=0_goto n)) . n implies ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n ) )
assume that
A1: n in dom (Load ((a,k1) <=0_goto n)) and
A2: i = (Load ((a,k1) <=0_goto n)) . n ; ::_thesis: ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )
dom (Load ((a,k1) <=0_goto n)) = {0} by FUNCOP_1:13;
then n = 0 by A1, TARSKI:def_1;
then A3: (a,k1) <=0_goto n = i by A2, FUNCOP_1:72;
hence ( InsCode i <> 1 & InsCode i <> 3 ) by SCMPDS_2:17; ::_thesis: i valid_at n
A4: ( n + n >= 0 & InsCode i <> 6 & InsCode i <> 14 ) by A3, SCMPDS_2:17;
( InsCode i <> 0 & InsCode i <> 4 ) by A3, SCMPDS_2:17;
hence i valid_at n by A3, A4, Def8; ::_thesis: verum
end;
hence for b1 being Program of SCMPDS st b1 = Load ((a,k1) <=0_goto n) holds
b1 is shiftable by Def9; ::_thesis: verum
end;
end;
theorem :: SCMPDS_4:26
for I being shiftable Program of SCMPDS
for k1, k2 being Integer
for a being Int_position st (card I) + k2 >= 0 holds
I ';' ((a,k1) >=0_goto k2) is shiftable
proof
let I be shiftable Program of SCMPDS; ::_thesis: for k1, k2 being Integer
for a being Int_position st (card I) + k2 >= 0 holds
I ';' ((a,k1) >=0_goto k2) is shiftable
let k1, k2 be Integer; ::_thesis: for a being Int_position st (card I) + k2 >= 0 holds
I ';' ((a,k1) >=0_goto k2) is shiftable
let a be Int_position; ::_thesis: ( (card I) + k2 >= 0 implies I ';' ((a,k1) >=0_goto k2) is shiftable )
set ii = (a,k1) >=0_goto k2;
set J = Load ((a,k1) >=0_goto k2);
set Ig = I ';' ((a,k1) >=0_goto k2);
assume A1: (card I) + k2 >= 0 ; ::_thesis: I ';' ((a,k1) >=0_goto k2) is shiftable
now__::_thesis:_for_n_being_Element_of_NAT_
for_i_being_Instruction_of_SCMPDS_st_n_in_dom_(I_';'_((a,k1)_>=0_goto_k2))_&_i_=_(I_';'_((a,k1)_>=0_goto_k2))_._n_holds_
(_InsCode_i_<>_1_&_InsCode_i_<>_3_&_i_valid_at_n_)
set D = { (l + (card I)) where l is Element of NAT : l in dom (Load ((a,k1) >=0_goto k2)) } ;
let n be Element of NAT ; ::_thesis: for i being Instruction of SCMPDS st n in dom (I ';' ((a,k1) >=0_goto k2)) & i = (I ';' ((a,k1) >=0_goto k2)) . n holds
( InsCode b3 <> 1 & InsCode b3 <> 3 & b3 valid_at b2 )
let i be Instruction of SCMPDS; ::_thesis: ( n in dom (I ';' ((a,k1) >=0_goto k2)) & i = (I ';' ((a,k1) >=0_goto k2)) . n implies ( InsCode b2 <> 1 & InsCode b2 <> 3 & b2 valid_at b1 ) )
assume that
A2: n in dom (I ';' ((a,k1) >=0_goto k2)) and
A3: i = (I ';' ((a,k1) >=0_goto k2)) . n ; ::_thesis: ( InsCode b2 <> 1 & InsCode b2 <> 3 & b2 valid_at b1 )
dom (Shift ((Load ((a,k1) >=0_goto k2)),(card I))) = { (l + (card I)) where l is Element of NAT : l in dom (Load ((a,k1) >=0_goto k2)) } by VALUED_1:def_12;
then A4: dom (I ';' ((a,k1) >=0_goto k2)) = (dom I) \/ { (l + (card I)) where l is Element of NAT : l in dom (Load ((a,k1) >=0_goto k2)) } by FUNCT_4:def_1;
percases ( n in dom I or n in { (l + (card I)) where l is Element of NAT : l in dom (Load ((a,k1) >=0_goto k2)) } ) by A2, A4, XBOOLE_0:def_3;
supposeA5: n in dom I ; ::_thesis: ( InsCode b2 <> 1 & InsCode b2 <> 3 & b2 valid_at b1 )
then I . n = i by A3, AFINSQ_1:def_3;
hence ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n ) by A5, Def9; ::_thesis: verum
end;
suppose n in { (l + (card I)) where l is Element of NAT : l in dom (Load ((a,k1) >=0_goto k2)) } ; ::_thesis: ( InsCode b2 <> 1 & InsCode b2 <> 3 & b2 valid_at b1 )
then consider l being Element of NAT such that
A6: n = l + (card I) and
A7: l in dom (Load ((a,k1) >=0_goto k2)) ;
dom (Load ((a,k1) >=0_goto k2)) = {0} by FUNCOP_1:13;
then A8: l = 0 by A7, TARSKI:def_1;
then A9: (a,k1) >=0_goto k2 = (Load ((a,k1) >=0_goto k2)) . l by FUNCOP_1:72
.= i by A3, A6, A7, AFINSQ_1:def_3 ;
hence ( InsCode i <> 1 & InsCode i <> 3 ) by SCMPDS_2:18; ::_thesis: i valid_at n
A10: ( InsCode i <> 5 & InsCode i <> 14 ) by A9, SCMPDS_2:18;
( InsCode i <> 0 & InsCode i <> 4 ) by A9, SCMPDS_2:18;
hence i valid_at n by A1, A6, A8, A9, A10, Def8; ::_thesis: verum
end;
end;
end;
hence I ';' ((a,k1) >=0_goto k2) is shiftable by Def9; ::_thesis: verum
end;
registration
let k1 be Integer;
let a be Int_position;
let n be Element of NAT ;
cluster Load -> shiftable for Program of SCMPDS;
coherence
for b1 being Program of SCMPDS st b1 = Load ((a,k1) >=0_goto n) holds
b1 is shiftable
proof
set k2 = n;
set ii = (a,k1) >=0_goto n;
set J = Load ((a,k1) >=0_goto n);
now__::_thesis:_for_n_being_Element_of_NAT_
for_i_being_Instruction_of_SCMPDS_st_n_in_dom_(Load_((a,k1)_>=0_goto_n))_&_i_=_(Load_((a,k1)_>=0_goto_n))_._n_holds_
(_InsCode_i_<>_1_&_InsCode_i_<>_3_&_i_valid_at_n_)
let n be Element of NAT ; ::_thesis: for i being Instruction of SCMPDS st n in dom (Load ((a,k1) >=0_goto n)) & i = (Load ((a,k1) >=0_goto n)) . n holds
( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )
let i be Instruction of SCMPDS; ::_thesis: ( n in dom (Load ((a,k1) >=0_goto n)) & i = (Load ((a,k1) >=0_goto n)) . n implies ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n ) )
assume that
A1: n in dom (Load ((a,k1) >=0_goto n)) and
A2: i = (Load ((a,k1) >=0_goto n)) . n ; ::_thesis: ( InsCode i <> 1 & InsCode i <> 3 & i valid_at n )
dom (Load ((a,k1) >=0_goto n)) = {0} by FUNCOP_1:13;
then n = 0 by A1, TARSKI:def_1;
then A3: (a,k1) >=0_goto n = i by A2, FUNCOP_1:72;
hence ( InsCode i <> 1 & InsCode i <> 3 ) by SCMPDS_2:18; ::_thesis: i valid_at n
A4: ( n + n >= 0 & InsCode i <> 5 & InsCode i <> 14 ) by A3, SCMPDS_2:18;
( InsCode i <> 0 & InsCode i <> 4 ) by A3, SCMPDS_2:18;
hence i valid_at n by A3, A4, Def8; ::_thesis: verum
end;
hence for b1 being Program of SCMPDS st b1 = Load ((a,k1) >=0_goto n) holds
b1 is shiftable by Def9; ::_thesis: verum
end;
end;
theorem Th27: :: SCMPDS_4:27
for s1, s2 being State of SCMPDS
for n, m being Element of NAT
for k1 being Integer st IC s1 = m & m + k1 >= 0 & (IC s1) + n = IC s2 holds
(ICplusConst (s1,k1)) + n = ICplusConst (s2,k1)
proof
let s1, s2 be State of SCMPDS; ::_thesis: for n, m being Element of NAT
for k1 being Integer st IC s1 = m & m + k1 >= 0 & (IC s1) + n = IC s2 holds
(ICplusConst (s1,k1)) + n = ICplusConst (s2,k1)
let n, m be Element of NAT ; ::_thesis: for k1 being Integer st IC s1 = m & m + k1 >= 0 & (IC s1) + n = IC s2 holds
(ICplusConst (s1,k1)) + n = ICplusConst (s2,k1)
let k1 be Integer; ::_thesis: ( IC s1 = m & m + k1 >= 0 & (IC s1) + n = IC s2 implies (ICplusConst (s1,k1)) + n = ICplusConst (s2,k1) )
assume that
A1: IC s1 = m and
A2: m + k1 >= 0 and
A3: (IC s1) + n = IC s2 ; ::_thesis: (ICplusConst (s1,k1)) + n = ICplusConst (s2,k1)
reconsider nk = ICplusConst (s1,k1) as Element of NAT ;
reconsider mk = m + k1 as Element of NAT by A2, INT_1:3;
ex n1 being Element of NAT st
( n1 = IC s1 & ICplusConst (s1,k1) = abs (n1 + k1) ) by SCMPDS_2:def_18;
then ( ex n2 being Element of NAT st
( n2 = IC s2 & ICplusConst (s2,k1) = abs (n2 + k1) ) & nk = mk ) by A1, ABSVALUE:def_1, SCMPDS_2:def_18;
hence (ICplusConst (s1,k1)) + n = ICplusConst (s2,k1) by A1, A3, ABSVALUE:def_1; ::_thesis: verum
end;
theorem Th28: :: SCMPDS_4:28
for s1, s2 being State of SCMPDS
for n, m being Element of NAT
for i being Instruction of SCMPDS st IC s1 = m & i valid_at m & InsCode i <> 1 & InsCode i <> 3 & (IC s1) + n = IC s2 & DataPart s1 = DataPart s2 holds
( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
proof
let s1, s2 be State of SCMPDS; ::_thesis: for n, m being Element of NAT
for i being Instruction of SCMPDS st IC s1 = m & i valid_at m & InsCode i <> 1 & InsCode i <> 3 & (IC s1) + n = IC s2 & DataPart s1 = DataPart s2 holds
( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
let n, m be Element of NAT ; ::_thesis: for i being Instruction of SCMPDS st IC s1 = m & i valid_at m & InsCode i <> 1 & InsCode i <> 3 & (IC s1) + n = IC s2 & DataPart s1 = DataPart s2 holds
( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
let i be Instruction of SCMPDS; ::_thesis: ( IC s1 = m & i valid_at m & InsCode i <> 1 & InsCode i <> 3 & (IC s1) + n = IC s2 & DataPart s1 = DataPart s2 implies ( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) ) )
assume that
A1: IC s1 = m and
A2: i valid_at m and
A3: ( InsCode i <> 1 & InsCode i <> 3 ) and
A4: (IC s1) + n = IC s2 and
A5: DataPart s1 = DataPart s2 ; ::_thesis: ( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
A6: now__::_thesis:_for_a_being_Int_position
for_k1_being_Integer_holds_s1_._(DataLoc_((s1_._a),k1))_=_s2_._(DataLoc_((s2_._a),k1))
let a be Int_position; ::_thesis: for k1 being Integer holds s1 . (DataLoc ((s1 . a),k1)) = s2 . (DataLoc ((s2 . a),k1))
let k1 be Integer; ::_thesis: s1 . (DataLoc ((s1 . a),k1)) = s2 . (DataLoc ((s2 . a),k1))
thus s1 . (DataLoc ((s1 . a),k1)) = s1 . (DataLoc ((s2 . a),k1)) by A5, Th8
.= s2 . (DataLoc ((s2 . a),k1)) by A5, Th8 ; ::_thesis: verum
end;
reconsider k1 = IC s1 as Element of NAT ;
set Ci = InsCode i;
A7: (succ (IC s1)) + n = succ (IC s2) by A4;
A8: now__::_thesis:_(_InsCode_i_<>_0_&_InsCode_i_<>_14_&_InsCode_i_<>_1_&_InsCode_i_<>_4_&_InsCode_i_<>_5_&_InsCode_i_<>_6_implies_(IC_(Exec_(i,s1)))_+_n_=_IC_(Exec_(i,s2))_)
assume ( InsCode i <> 0 & InsCode i <> 14 & InsCode i <> 1 & InsCode i <> 4 & InsCode i <> 5 & InsCode i <> 6 ) ; ::_thesis: (IC (Exec (i,s1))) + n = IC (Exec (i,s2))
then A9: not InsCode i in {0,1,4,5,6,14} by ENUMSET1:def_4;
then IC (Exec (i,s1)) = succ (IC s1) by Th1;
hence (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) by A7, A9, Th1; ::_thesis: verum
end;
percases ( InsCode i = 0 or InsCode i = 14 or InsCode i = 2 or InsCode i = 4 or InsCode i = 5 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or InsCode i = 13 ) by A3, NAT_1:60, SCMPDS_2:6;
suppose InsCode i = 0 ; ::_thesis: ( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
then A10: ( Exec (i,s1) = s1 & Exec (i,s2) = s2 ) by SCMPDS_2:86;
hence (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) by A4; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
thus DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by A5, A10; ::_thesis: verum
end;
suppose InsCode i = 14 ; ::_thesis: ( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
then consider k1 being Integer such that
A11: i = goto k1 and
A12: m + k1 >= 0 by A2, Def8;
IC (Exec (i,s1)) = ICplusConst (s1,k1) by A11, SCMPDS_2:54;
hence (IC (Exec (i,s1))) + n = ICplusConst (s2,k1) by A1, A4, A12, Th27
.= IC (Exec (i,s2)) by A11, SCMPDS_2:54 ;
::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
now__::_thesis:_for_a_being_Int_position_holds_(Exec_(i,s1))_._a_=_(Exec_(i,s2))_._a
let a be Int_position; ::_thesis: (Exec (i,s1)) . a = (Exec (i,s2)) . a
thus (Exec (i,s1)) . a = s1 . a by A11, SCMPDS_2:54
.= s2 . a by A5, Th8
.= (Exec (i,s2)) . a by A11, SCMPDS_2:54 ; ::_thesis: verum
end;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by Th8; ::_thesis: verum
end;
supposeA13: InsCode i = 2 ; ::_thesis: ( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
hence (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) by A8; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
consider a being Int_position, k1 being Integer such that
A14: i = a := k1 by A13, SCMPDS_2:28;
now__::_thesis:_for_b_being_Int_position_holds_(Exec_(i,s1))_._b_=_(Exec_(i,s2))_._b
let b be Int_position; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
percases ( a = b or a <> b ) ;
supposeA15: a = b ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
hence (Exec (i,s1)) . b = k1 by A14, SCMPDS_2:45
.= (Exec (i,s2)) . b by A14, A15, SCMPDS_2:45 ;
::_thesis: verum
end;
supposeA16: a <> b ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
hence (Exec (i,s1)) . b = s1 . b by A14, SCMPDS_2:45
.= s2 . b by A5, Th8
.= (Exec (i,s2)) . b by A14, A16, SCMPDS_2:45 ;
::_thesis: verum
end;
end;
end;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by Th8; ::_thesis: verum
end;
suppose InsCode i = 4 ; ::_thesis: ( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
then consider a being Int_position, k1, k2 being Integer such that
A17: i = (a,k1) <>0_goto k2 and
A18: m + k2 >= 0 by A2, Def8;
hereby ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
percases ( s1 . (DataLoc ((s1 . a),k1)) <> 0 or s1 . (DataLoc ((s1 . a),k1)) = 0 ) ;
supposeA19: s1 . (DataLoc ((s1 . a),k1)) <> 0 ; ::_thesis: (IC (Exec (i,s1))) + n = IC (Exec (i,s2))
then A20: s2 . (DataLoc ((s2 . a),k1)) <> 0 by A6;
IC (Exec (i,s1)) = ICplusConst (s1,k2) by A17, A19, SCMPDS_2:55;
hence (IC (Exec (i,s1))) + n = ICplusConst (s2,k2) by A1, A4, A18, Th27
.= IC (Exec (i,s2)) by A17, A20, SCMPDS_2:55 ;
::_thesis: verum
end;
suppose s1 . (DataLoc ((s1 . a),k1)) = 0 ; ::_thesis: (IC (Exec (i,s1))) + n = IC (Exec (i,s2))
then ( s2 . (DataLoc ((s2 . a),k1)) = 0 & IC (Exec (i,s1)) = succ (IC s1) ) by A6, A17, SCMPDS_2:55;
hence (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) by A7, A17, SCMPDS_2:55; ::_thesis: verum
end;
end;
end;
now__::_thesis:_for_a_being_Int_position_holds_(Exec_(i,s1))_._a_=_(Exec_(i,s2))_._a
let a be Int_position; ::_thesis: (Exec (i,s1)) . a = (Exec (i,s2)) . a
thus (Exec (i,s1)) . a = s1 . a by A17, SCMPDS_2:55
.= s2 . a by A5, Th8
.= (Exec (i,s2)) . a by A17, SCMPDS_2:55 ; ::_thesis: verum
end;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by Th8; ::_thesis: verum
end;
suppose InsCode i = 5 ; ::_thesis: ( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
then consider a being Int_position, k1, k2 being Integer such that
A21: i = (a,k1) <=0_goto k2 and
A22: m + k2 >= 0 by A2, Def8;
hereby ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
percases ( s1 . (DataLoc ((s1 . a),k1)) <= 0 or s1 . (DataLoc ((s1 . a),k1)) > 0 ) ;
supposeA23: s1 . (DataLoc ((s1 . a),k1)) <= 0 ; ::_thesis: (IC (Exec (i,s1))) + n = IC (Exec (i,s2))
then A24: s2 . (DataLoc ((s2 . a),k1)) <= 0 by A6;
IC (Exec (i,s1)) = ICplusConst (s1,k2) by A21, A23, SCMPDS_2:56;
hence (IC (Exec (i,s1))) + n = ICplusConst (s2,k2) by A1, A4, A22, Th27
.= IC (Exec (i,s2)) by A21, A24, SCMPDS_2:56 ;
::_thesis: verum
end;
suppose s1 . (DataLoc ((s1 . a),k1)) > 0 ; ::_thesis: (IC (Exec (i,s1))) + n = IC (Exec (i,s2))
then ( s2 . (DataLoc ((s2 . a),k1)) > 0 & IC (Exec (i,s1)) = succ (IC s1) ) by A6, A21, SCMPDS_2:56;
hence (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) by A7, A21, SCMPDS_2:56; ::_thesis: verum
end;
end;
end;
now__::_thesis:_for_a_being_Int_position_holds_(Exec_(i,s1))_._a_=_(Exec_(i,s2))_._a
let a be Int_position; ::_thesis: (Exec (i,s1)) . a = (Exec (i,s2)) . a
thus (Exec (i,s1)) . a = s1 . a by A21, SCMPDS_2:56
.= s2 . a by A5, Th8
.= (Exec (i,s2)) . a by A21, SCMPDS_2:56 ; ::_thesis: verum
end;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by Th8; ::_thesis: verum
end;
suppose InsCode i = 6 ; ::_thesis: ( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
then consider a being Int_position, k1, k2 being Integer such that
A25: i = (a,k1) >=0_goto k2 and
A26: m + k2 >= 0 by A2, Def8;
hereby ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
percases ( s1 . (DataLoc ((s1 . a),k1)) >= 0 or s1 . (DataLoc ((s1 . a),k1)) < 0 ) ;
supposeA27: s1 . (DataLoc ((s1 . a),k1)) >= 0 ; ::_thesis: (IC (Exec (i,s1))) + n = IC (Exec (i,s2))
then A28: s2 . (DataLoc ((s2 . a),k1)) >= 0 by A6;
IC (Exec (i,s1)) = ICplusConst (s1,k2) by A25, A27, SCMPDS_2:57;
hence (IC (Exec (i,s1))) + n = ICplusConst (s2,k2) by A1, A4, A26, Th27
.= IC (Exec (i,s2)) by A25, A28, SCMPDS_2:57 ;
::_thesis: verum
end;
suppose s1 . (DataLoc ((s1 . a),k1)) < 0 ; ::_thesis: (IC (Exec (i,s1))) + n = IC (Exec (i,s2))
then ( s2 . (DataLoc ((s2 . a),k1)) < 0 & IC (Exec (i,s1)) = succ (IC s1) ) by A6, A25, SCMPDS_2:57;
hence (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) by A7, A25, SCMPDS_2:57; ::_thesis: verum
end;
end;
end;
now__::_thesis:_for_a_being_Int_position_holds_(Exec_(i,s1))_._a_=_(Exec_(i,s2))_._a
let a be Int_position; ::_thesis: (Exec (i,s1)) . a = (Exec (i,s2)) . a
thus (Exec (i,s1)) . a = s1 . a by A25, SCMPDS_2:57
.= s2 . a by A5, Th8
.= (Exec (i,s2)) . a by A25, SCMPDS_2:57 ; ::_thesis: verum
end;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by Th8; ::_thesis: verum
end;
supposeA29: InsCode i = 7 ; ::_thesis: ( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
hence (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) by A8; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
consider a being Int_position, k1, k2 being Integer such that
A30: i = (a,k1) := k2 by A29, SCMPDS_2:33;
now__::_thesis:_for_b_being_Int_position_holds_(Exec_(i,s1))_._b_=_(Exec_(i,s2))_._b
let b be Int_position; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
percases ( DataLoc ((s1 . a),k1) = b or DataLoc ((s1 . a),k1) <> b ) ;
supposeA31: DataLoc ((s1 . a),k1) = b ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A32: DataLoc ((s2 . a),k1) = b by A5, Th8;
thus (Exec (i,s1)) . b = k2 by A30, A31, SCMPDS_2:46
.= (Exec (i,s2)) . b by A30, A32, SCMPDS_2:46 ; ::_thesis: verum
end;
supposeA33: DataLoc ((s1 . a),k1) <> b ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A34: DataLoc ((s2 . a),k1) <> b by A5, Th8;
thus (Exec (i,s1)) . b = s1 . b by A30, A33, SCMPDS_2:46
.= s2 . b by A5, Th8
.= (Exec (i,s2)) . b by A30, A34, SCMPDS_2:46 ; ::_thesis: verum
end;
end;
end;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by Th8; ::_thesis: verum
end;
supposeA35: InsCode i = 8 ; ::_thesis: ( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
hence (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) by A8; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
consider a being Int_position, k1, k2 being Integer such that
A36: i = AddTo (a,k1,k2) by A35, SCMPDS_2:34;
now__::_thesis:_for_b_being_Int_position_holds_(Exec_(i,s1))_._b_=_(Exec_(i,s2))_._b
let b be Int_position; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
percases ( DataLoc ((s1 . a),k1) = b or DataLoc ((s1 . a),k1) <> b ) ;
supposeA37: DataLoc ((s1 . a),k1) = b ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A38: DataLoc ((s2 . a),k1) = b by A5, Th8;
thus (Exec (i,s1)) . b = (s1 . (DataLoc ((s1 . a),k1))) + k2 by A36, A37, SCMPDS_2:48
.= (s2 . (DataLoc ((s2 . a),k1))) + k2 by A6
.= (Exec (i,s2)) . b by A36, A38, SCMPDS_2:48 ; ::_thesis: verum
end;
supposeA39: DataLoc ((s1 . a),k1) <> b ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A40: DataLoc ((s2 . a),k1) <> b by A5, Th8;
thus (Exec (i,s1)) . b = s1 . b by A36, A39, SCMPDS_2:48
.= s2 . b by A5, Th8
.= (Exec (i,s2)) . b by A36, A40, SCMPDS_2:48 ; ::_thesis: verum
end;
end;
end;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by Th8; ::_thesis: verum
end;
supposeA41: InsCode i = 9 ; ::_thesis: ( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
hence (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) by A8; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
consider a, b being Int_position, k1, k2 being Integer such that
A42: i = AddTo (a,k1,b,k2) by A41, SCMPDS_2:35;
now__::_thesis:_for_c_being_Int_position_holds_(Exec_(i,s1))_._c_=_(Exec_(i,s2))_._c
let c be Int_position; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
percases ( DataLoc ((s1 . a),k1) = c or DataLoc ((s1 . a),k1) <> c ) ;
supposeA43: DataLoc ((s1 . a),k1) = c ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A44: DataLoc ((s2 . a),k1) = c by A5, Th8;
thus (Exec (i,s1)) . c = (s1 . (DataLoc ((s1 . a),k1))) + (s1 . (DataLoc ((s1 . b),k2))) by A42, A43, SCMPDS_2:49
.= (s2 . (DataLoc ((s2 . a),k1))) + (s1 . (DataLoc ((s1 . b),k2))) by A6
.= (s2 . (DataLoc ((s2 . a),k1))) + (s2 . (DataLoc ((s2 . b),k2))) by A6
.= (Exec (i,s2)) . c by A42, A44, SCMPDS_2:49 ; ::_thesis: verum
end;
supposeA45: DataLoc ((s1 . a),k1) <> c ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A46: DataLoc ((s2 . a),k1) <> c by A5, Th8;
thus (Exec (i,s1)) . c = s1 . c by A42, A45, SCMPDS_2:49
.= s2 . c by A5, Th8
.= (Exec (i,s2)) . c by A42, A46, SCMPDS_2:49 ; ::_thesis: verum
end;
end;
end;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by Th8; ::_thesis: verum
end;
supposeA47: InsCode i = 10 ; ::_thesis: ( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
hence (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) by A8; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
consider a, b being Int_position, k1, k2 being Integer such that
A48: i = SubFrom (a,k1,b,k2) by A47, SCMPDS_2:36;
now__::_thesis:_for_c_being_Int_position_holds_(Exec_(i,s1))_._c_=_(Exec_(i,s2))_._c
let c be Int_position; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
percases ( DataLoc ((s1 . a),k1) = c or DataLoc ((s1 . a),k1) <> c ) ;
supposeA49: DataLoc ((s1 . a),k1) = c ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A50: DataLoc ((s2 . a),k1) = c by A5, Th8;
thus (Exec (i,s1)) . c = (s1 . (DataLoc ((s1 . a),k1))) - (s1 . (DataLoc ((s1 . b),k2))) by A48, A49, SCMPDS_2:50
.= (s2 . (DataLoc ((s2 . a),k1))) - (s1 . (DataLoc ((s1 . b),k2))) by A6
.= (s2 . (DataLoc ((s2 . a),k1))) - (s2 . (DataLoc ((s2 . b),k2))) by A6
.= (Exec (i,s2)) . c by A48, A50, SCMPDS_2:50 ; ::_thesis: verum
end;
supposeA51: DataLoc ((s1 . a),k1) <> c ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A52: DataLoc ((s2 . a),k1) <> c by A5, Th8;
thus (Exec (i,s1)) . c = s1 . c by A48, A51, SCMPDS_2:50
.= s2 . c by A5, Th8
.= (Exec (i,s2)) . c by A48, A52, SCMPDS_2:50 ; ::_thesis: verum
end;
end;
end;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by Th8; ::_thesis: verum
end;
supposeA53: InsCode i = 11 ; ::_thesis: ( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
hence (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) by A8; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
consider a, b being Int_position, k1, k2 being Integer such that
A54: i = MultBy (a,k1,b,k2) by A53, SCMPDS_2:37;
now__::_thesis:_for_c_being_Int_position_holds_(Exec_(i,s1))_._c_=_(Exec_(i,s2))_._c
let c be Int_position; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
percases ( DataLoc ((s1 . a),k1) = c or DataLoc ((s1 . a),k1) <> c ) ;
supposeA55: DataLoc ((s1 . a),k1) = c ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A56: DataLoc ((s2 . a),k1) = c by A5, Th8;
thus (Exec (i,s1)) . c = (s1 . (DataLoc ((s1 . a),k1))) * (s1 . (DataLoc ((s1 . b),k2))) by A54, A55, SCMPDS_2:51
.= (s2 . (DataLoc ((s2 . a),k1))) * (s1 . (DataLoc ((s1 . b),k2))) by A6
.= (s2 . (DataLoc ((s2 . a),k1))) * (s2 . (DataLoc ((s2 . b),k2))) by A6
.= (Exec (i,s2)) . c by A54, A56, SCMPDS_2:51 ; ::_thesis: verum
end;
supposeA57: DataLoc ((s1 . a),k1) <> c ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A58: DataLoc ((s2 . a),k1) <> c by A5, Th8;
thus (Exec (i,s1)) . c = s1 . c by A54, A57, SCMPDS_2:51
.= s2 . c by A5, Th8
.= (Exec (i,s2)) . c by A54, A58, SCMPDS_2:51 ; ::_thesis: verum
end;
end;
end;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by Th8; ::_thesis: verum
end;
supposeA59: InsCode i = 12 ; ::_thesis: ( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
hence (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) by A8; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
consider a, b being Int_position, k1, k2 being Integer such that
A60: i = Divide (a,k1,b,k2) by A59, SCMPDS_2:38;
now__::_thesis:_for_c_being_Int_position_holds_(Exec_(i,s1))_._c_=_(Exec_(i,s2))_._c
let c be Int_position; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
percases ( DataLoc ((s1 . b),k2) = c or DataLoc ((s1 . b),k2) <> c ) ;
supposeA61: DataLoc ((s1 . b),k2) = c ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A62: DataLoc ((s2 . b),k2) = c by A5, Th8;
thus (Exec (i,s1)) . c = (s1 . (DataLoc ((s1 . a),k1))) mod (s1 . (DataLoc ((s1 . b),k2))) by A60, A61, SCMPDS_2:52
.= (s2 . (DataLoc ((s2 . a),k1))) mod (s1 . (DataLoc ((s1 . b),k2))) by A6
.= (s2 . (DataLoc ((s2 . a),k1))) mod (s2 . (DataLoc ((s2 . b),k2))) by A6
.= (Exec (i,s2)) . c by A60, A62, SCMPDS_2:52 ; ::_thesis: verum
end;
supposeA63: DataLoc ((s1 . b),k2) <> c ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A64: DataLoc ((s2 . b),k2) <> c by A5, Th8;
hereby ::_thesis: verum
percases ( DataLoc ((s1 . a),k1) <> c or DataLoc ((s1 . a),k1) = c ) ;
supposeA65: DataLoc ((s1 . a),k1) <> c ; ::_thesis: (Exec (i,s1)) . c = (Exec (i,s2)) . c
then A66: DataLoc ((s2 . a),k1) <> c by A5, Th8;
thus (Exec (i,s1)) . c = s1 . c by A60, A63, A65, SCMPDS_2:52
.= s2 . c by A5, Th8
.= (Exec (i,s2)) . c by A60, A64, A66, SCMPDS_2:52 ; ::_thesis: verum
end;
supposeA67: DataLoc ((s1 . a),k1) = c ; ::_thesis: (Exec (i,s1)) . c = (Exec (i,s2)) . c
then A68: DataLoc ((s2 . a),k1) = c by A5, Th8;
thus (Exec (i,s1)) . c = (s1 . (DataLoc ((s1 . a),k1))) div (s1 . (DataLoc ((s1 . b),k2))) by A60, A63, A67, SCMPDS_2:52
.= (s2 . (DataLoc ((s2 . a),k1))) div (s1 . (DataLoc ((s1 . b),k2))) by A6
.= (s2 . (DataLoc ((s2 . a),k1))) div (s2 . (DataLoc ((s2 . b),k2))) by A6
.= (Exec (i,s2)) . c by A60, A64, A68, SCMPDS_2:52 ; ::_thesis: verum
end;
end;
end;
end;
end;
end;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by Th8; ::_thesis: verum
end;
supposeA69: InsCode i = 13 ; ::_thesis: ( (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) & DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) )
hence (IC (Exec (i,s1))) + n = IC (Exec (i,s2)) by A8; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))
consider a, b being Int_position, k1, k2 being Integer such that
A70: i = (a,k1) := (b,k2) by A69, SCMPDS_2:39;
now__::_thesis:_for_c_being_Int_position_holds_(Exec_(i,s1))_._c_=_(Exec_(i,s2))_._c
let c be Int_position; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
percases ( DataLoc ((s1 . a),k1) = c or DataLoc ((s1 . a),k1) <> c ) ;
supposeA71: DataLoc ((s1 . a),k1) = c ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A72: DataLoc ((s2 . a),k1) = c by A5, Th8;
thus (Exec (i,s1)) . c = s1 . (DataLoc ((s1 . b),k2)) by A70, A71, SCMPDS_2:47
.= s2 . (DataLoc ((s2 . b),k2)) by A6
.= (Exec (i,s2)) . c by A70, A72, SCMPDS_2:47 ; ::_thesis: verum
end;
supposeA73: DataLoc ((s1 . a),k1) <> c ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1
then A74: DataLoc ((s2 . a),k1) <> c by A5, Th8;
thus (Exec (i,s1)) . c = s1 . c by A70, A73, SCMPDS_2:47
.= s2 . c by A5, Th8
.= (Exec (i,s2)) . c by A70, A74, SCMPDS_2:47 ; ::_thesis: verum
end;
end;
end;
hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by Th8; ::_thesis: verum
end;
end;
end;
theorem :: SCMPDS_4:29
for s2 being State of SCMPDS
for P1, P2 being Instruction-Sequence of SCMPDS
for s1 being 0 -started State of SCMPDS
for J being parahalting shiftable Program of SCMPDS st stop J c= P1 holds
for n being Element of NAT st Shift ((stop J),n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
proof
let s2 be State of SCMPDS; ::_thesis: for P1, P2 being Instruction-Sequence of SCMPDS
for s1 being 0 -started State of SCMPDS
for J being parahalting shiftable Program of SCMPDS st stop J c= P1 holds
for n being Element of NAT st Shift ((stop J),n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
let P1, P2 be Instruction-Sequence of SCMPDS; ::_thesis: for s1 being 0 -started State of SCMPDS
for J being parahalting shiftable Program of SCMPDS st stop J c= P1 holds
for n being Element of NAT st Shift ((stop J),n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
let s1 be 0 -started State of SCMPDS; ::_thesis: for J being parahalting shiftable Program of SCMPDS st stop J c= P1 holds
for n being Element of NAT st Shift ((stop J),n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
let I be parahalting shiftable Program of SCMPDS; ::_thesis: ( stop I c= P1 implies for n being Element of NAT st Shift ((stop I),n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) )
set SI = stop I;
assume A1: stop I c= P1 ; ::_thesis: for n being Element of NAT st Shift ((stop I),n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
let n be Element of NAT ; ::_thesis: ( Shift ((stop I),n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 implies for i being Element of NAT holds
( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) )
assume that
A2: Shift ((stop I),n) c= P2 and
A3: IC s2 = n and
A4: DataPart s1 = DataPart s2 ; ::_thesis: for i being Element of NAT holds
( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
A5: 0 in dom (stop I) by COMPOS_1:36;
then A6: 0 + n in dom (Shift ((stop I),n)) by VALUED_1:24;
defpred S1[ Nat] means ( (IC (Comput (P1,s1,$1))) + n = IC (Comput (P2,s2,$1)) & CurInstr (P1,(Comput (P1,s1,$1))) = CurInstr (P2,(Comput (P2,s2,$1))) & DataPart (Comput (P1,s1,$1)) = DataPart (Comput (P2,s2,$1)) );
A7: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A8: S1[k] ; ::_thesis: S1[k + 1]
reconsider m = IC (Comput (P1,s1,k)) as Element of NAT ;
set i = CurInstr (P1,(Comput (P1,s1,k)));
A9: Comput (P1,s1,(k + 1)) = Following (P1,(Comput (P1,s1,k))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,k)))),(Comput (P1,s1,k))) ;
reconsider l = IC (Comput (P1,s1,(k + 1))) as Element of NAT ;
A10: IC (Comput (P1,s1,(k + 1))) in dom (stop I) by A1, Def6;
then A11: l + n in dom (Shift ((stop I),n)) by VALUED_1:24;
A12: Comput (P2,s2,(k + 1)) = Following (P2,(Comput (P2,s2,k))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,k)))),(Comput (P2,s2,k))) ;
A13: IC (Comput (P1,s1,k)) in dom (stop I) by A1, Def6;
A14: CurInstr (P1,(Comput (P1,s1,k))) = P1 . (IC (Comput (P1,s1,k))) by PBOOLE:143
.= (stop I) . (IC (Comput (P1,s1,k))) by A1, A13, GRFUNC_1:2 ;
then A15: ( InsCode (CurInstr (P1,(Comput (P1,s1,k)))) <> 1 & InsCode (CurInstr (P1,(Comput (P1,s1,k)))) <> 3 ) by A13, Def9;
A16: CurInstr (P1,(Comput (P1,s1,k))) valid_at m by A13, A14, Def9;
hence A17: (IC (Comput (P1,s1,(k + 1)))) + n = IC (Comput (P2,s2,(k + 1))) by A8, A9, A12, A15, Th28; ::_thesis: ( CurInstr (P1,(Comput (P1,s1,(k + 1)))) = CurInstr (P2,(Comput (P2,s2,(k + 1)))) & DataPart (Comput (P1,s1,(k + 1))) = DataPart (Comput (P2,s2,(k + 1))) )
CurInstr (P1,(Comput (P1,s1,(k + 1)))) = P1 . l by PBOOLE:143
.= (stop I) . l by A1, A10, GRFUNC_1:2 ;
hence CurInstr (P1,(Comput (P1,s1,(k + 1)))) = (Shift ((stop I),n)) . (IC (Comput (P2,s2,(k + 1)))) by A17, A10, VALUED_1:def_12
.= P2 . (IC (Comput (P2,s2,(k + 1)))) by A2, A17, A11, GRFUNC_1:2
.= CurInstr (P2,(Comput (P2,s2,(k + 1)))) by PBOOLE:143 ;
::_thesis: DataPart (Comput (P1,s1,(k + 1))) = DataPart (Comput (P2,s2,(k + 1)))
thus DataPart (Comput (P1,s1,(k + 1))) = DataPart (Comput (P2,s2,(k + 1))) by A8, A9, A12, A15, A16, Th28; ::_thesis: verum
end;
A18: P1 . (IC s1) = P1 . 0 by MEMSTR_0:def_11
.= (stop I) . 0 by A1, A5, GRFUNC_1:2 ;
let i be Element of NAT ; ::_thesis: ( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
A19: DataPart (Comput (P1,s1,0)) = DataPart s2 by A4
.= DataPart (Comput (P2,s2,0)) ;
A20: IC (Comput (P1,s1,0)) = IC s1
.= 0 by MEMSTR_0:def_11 ;
A21: P2 /. (IC s2) = P2 . (IC s2) by PBOOLE:143;
A22: P1 /. (IC s1) = P1 . (IC s1) by PBOOLE:143;
CurInstr (P1,(Comput (P1,s1,0))) = (Shift ((stop I),n)) . (0 + n) by A5, A18, A22, VALUED_1:def_12
.= CurInstr (P2,(Comput (P2,s2,0))) by A2, A3, A6, A21, GRFUNC_1:2 ;
then A23: S1[ 0 ] by A3, A20, A19;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A23, A7);
hence ( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) ; ::_thesis: verum
end;