:: 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;