:: SCMPDS_5 semantic presentation begin Lm1: card (Stop SCMPDS) = 1 by AFINSQ_1:33; theorem :: SCMPDS_5:1 canceled; theorem :: SCMPDS_5:2 canceled; theorem :: SCMPDS_5:3 canceled; theorem :: SCMPDS_5:4 canceled; theorem :: SCMPDS_5:5 canceled; theorem :: SCMPDS_5:6 canceled; theorem :: SCMPDS_5:7 canceled; theorem :: SCMPDS_5:8 canceled; theorem :: SCMPDS_5:9 canceled; theorem :: SCMPDS_5:10 canceled; theorem :: SCMPDS_5:11 canceled; theorem Th12: :: SCMPDS_5:12 for I, J being Program of SCMPDS holds I c= stop (I ';' J) proof let I, J be Program of SCMPDS; ::_thesis: I c= stop (I ';' J) set IS = I ';' (J ';' (Stop SCMPDS)); set Ip = stop (I ';' J); A1: I c= I ';' (J ';' (Stop SCMPDS)) by AFINSQ_1:74; thus I c= stop (I ';' J) by A1, AFINSQ_1:27; ::_thesis: verum end; theorem Th13: :: SCMPDS_5:13 for I, J being Program of SCMPDS holds dom (stop I) c= dom (stop (I ';' J)) proof let I, J be Program of SCMPDS; ::_thesis: dom (stop I) c= dom (stop (I ';' J)) set sI = stop I; set sIJ = stop (I ';' J); A1: card (stop (I ';' J)) = (card (I ';' J)) + 1 by Lm1, AFINSQ_1:17 .= ((card I) + (card J)) + 1 by AFINSQ_1:17 .= ((card I) + 1) + (card J) ; card (stop I) = (card I) + 1 by Lm1, AFINSQ_1:17; then A2: card (stop I) <= card (stop (I ';' J)) by A1, NAT_1:11; now__::_thesis:_for_x_being_set_st_x_in_dom_(stop_I)_holds_ x_in_dom_(stop_(I_';'_J)) set A = NAT ; let x be set ; ::_thesis: ( x in dom (stop I) implies x in dom (stop (I ';' J)) ) assume A3: x in dom (stop I) ; ::_thesis: x in dom (stop (I ';' J)) dom (stop I) c= NAT by RELAT_1:def_18; then reconsider l = x as Element of NAT by A3; reconsider n = l as Element of NAT ; n < card (stop I) by A3, AFINSQ_1:66; then n < card (stop (I ';' J)) by A2, XXREAL_0:2; hence x in dom (stop (I ';' J)) by AFINSQ_1:66; ::_thesis: verum end; hence dom (stop I) c= dom (stop (I ';' J)) by TARSKI:def_3; ::_thesis: verum end; theorem Th14: :: SCMPDS_5:14 for I, J being Program of SCMPDS holds (stop I) +* (stop (I ';' J)) = stop (I ';' J) proof let I, J be Program of SCMPDS; ::_thesis: (stop I) +* (stop (I ';' J)) = stop (I ';' J) set sI = stop I; set IsI = stop I; set sIJ = stop (I ';' J); set IsIJ = stop (I ';' J); dom (stop I) c= dom (stop (I ';' J)) by Th13; hence (stop I) +* (stop (I ';' J)) = stop (I ';' J) by FUNCT_4:19; ::_thesis: verum end; set SA0 = Start-At (0,SCMPDS); theorem Th15: :: SCMPDS_5:15 for a being Int_position for s being State of SCMPDS holds (Initialize s) . a = s . a proof let a be Int_position; ::_thesis: for s being State of SCMPDS holds (Initialize s) . a = s . a let s be State of SCMPDS; ::_thesis: (Initialize s) . a = s . a not a in dom (Start-At (0,SCMPDS)) by SCMPDS_4:18; hence (Initialize s) . a = s . a by FUNCT_4:11; ::_thesis: verum end; theorem Th16: :: SCMPDS_5:16 for P1, P2 being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for I being parahalting Program of SCMPDS st stop I c= P1 & stop I c= P2 holds for k being Element of NAT holds ( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) ) proof let P1, P2 be Instruction-Sequence of SCMPDS; ::_thesis: for s being 0 -started State of SCMPDS for I being parahalting Program of SCMPDS st stop I c= P1 & stop I c= P2 holds for k being Element of NAT holds ( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) ) let s be 0 -started State of SCMPDS; ::_thesis: for I being parahalting Program of SCMPDS st stop I c= P1 & stop I c= P2 holds for k being Element of NAT holds ( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) ) let I be parahalting Program of SCMPDS; ::_thesis: ( stop I c= P1 & stop I c= P2 implies for k being Element of NAT holds ( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) ) ) set SI = stop I; assume that A1: stop I c= P1 and A2: stop I c= P2 ; ::_thesis: for k being Element of NAT holds ( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) ) let k be Element of NAT ; ::_thesis: ( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) ) A3: IC (Comput (P1,s,k)) in dom (stop I) by A1, SCMPDS_4:def_6; A4: IC (Comput (P2,s,k)) in dom (stop I) by A2, SCMPDS_4:def_6; for m being Element of NAT st m < k holds IC (Comput (P2,s,m)) in dom (stop I) by A2, SCMPDS_4:def_6; hence A5: Comput (P1,s,k) = Comput (P2,s,k) by A1, A2, SCMPDS_4:21; ::_thesis: CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) thus CurInstr (P2,(Comput (P2,s,k))) = P2 . (IC (Comput (P2,s,k))) by PBOOLE:143 .= (stop I) . (IC (Comput (P2,s,k))) by A2, A4, GRFUNC_1:2 .= P1 . (IC (Comput (P1,s,k))) by A1, A5, A3, GRFUNC_1:2 .= CurInstr (P1,(Comput (P1,s,k))) by PBOOLE:143 ; ::_thesis: verum end; theorem Th17: :: SCMPDS_5:17 for P1, P2 being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for I being parahalting Program of SCMPDS st stop I c= P1 & stop I c= P2 holds ( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) ) proof let P1, P2 be Instruction-Sequence of SCMPDS; ::_thesis: for s being 0 -started State of SCMPDS for I being parahalting Program of SCMPDS st stop I c= P1 & stop I c= P2 holds ( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) ) let s be 0 -started State of SCMPDS; ::_thesis: for I being parahalting Program of SCMPDS st stop I c= P1 & stop I c= P2 holds ( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) ) let I be parahalting Program of SCMPDS; ::_thesis: ( stop I c= P1 & stop I c= P2 implies ( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) ) ) set SI = stop I; assume that A1: stop I c= P1 and A2: stop I c= P2 ; ::_thesis: ( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) ) A3: P2 halts_on s by A2, SCMPDS_4:def_7; A4: P1 halts_on s by A1, SCMPDS_4:def_7; A5: now__::_thesis:_for_l_being_Element_of_NAT_st_CurInstr_(P2,(Comput_(P2,s,l)))_=_halt_SCMPDS_holds_ LifeSpan_(P1,s)_<=_l let l be Element of NAT ; ::_thesis: ( CurInstr (P2,(Comput (P2,s,l))) = halt SCMPDS implies LifeSpan (P1,s) <= l ) assume A6: CurInstr (P2,(Comput (P2,s,l))) = halt SCMPDS ; ::_thesis: LifeSpan (P1,s) <= l CurInstr (P1,(Comput (P1,s,l))) = CurInstr (P2,(Comput (P2,s,l))) by A1, A2, Th16; hence LifeSpan (P1,s) <= l by A4, A6, EXTPRO_1:def_15; ::_thesis: verum end; CurInstr (P2,(Comput (P2,s,(LifeSpan (P1,s))))) = CurInstr (P1,(Comput (P1,s,(LifeSpan (P1,s))))) by A1, A2, Th16 .= halt SCMPDS by A4, EXTPRO_1:def_15 ; hence A7: LifeSpan (P1,s) = LifeSpan (P2,s) by A5, A3, EXTPRO_1:def_15; ::_thesis: Result (P1,s) = Result (P2,s) P2 halts_on s by A2, SCMPDS_4:def_7; then A8: Result (P2,s) = Comput (P2,s,(LifeSpan (P1,s))) by A7, EXTPRO_1:23; P1 halts_on s by A1, SCMPDS_4:def_7; then Result (P1,s) = Comput (P1,s,(LifeSpan (P1,s))) by EXTPRO_1:23; hence Result (P1,s) = Result (P2,s) by A1, A2, A8, Th16; ::_thesis: verum end; theorem :: SCMPDS_5:18 canceled; theorem Th19: :: SCMPDS_5:19 for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for I being parahalting Program of SCMPDS for J being Program of SCMPDS st stop I c= P holds for m being Element of NAT st m <= LifeSpan (P,s) holds Comput (P,s,m) = Comput ((P +* (I ';' J)),s,m) proof let P be Instruction-Sequence of SCMPDS; ::_thesis: for s being 0 -started State of SCMPDS for I being parahalting Program of SCMPDS for J being Program of SCMPDS st stop I c= P holds for m being Element of NAT st m <= LifeSpan (P,s) holds Comput (P,s,m) = Comput ((P +* (I ';' J)),s,m) let s be 0 -started State of SCMPDS; ::_thesis: for I being parahalting Program of SCMPDS for J being Program of SCMPDS st stop I c= P holds for m being Element of NAT st m <= LifeSpan (P,s) holds Comput (P,s,m) = Comput ((P +* (I ';' J)),s,m) let I be parahalting Program of SCMPDS; ::_thesis: for J being Program of SCMPDS st stop I c= P holds for m being Element of NAT st m <= LifeSpan (P,s) holds Comput (P,s,m) = Comput ((P +* (I ';' J)),s,m) let J be Program of SCMPDS; ::_thesis: ( stop I c= P implies for m being Element of NAT st m <= LifeSpan (P,s) holds Comput (P,s,m) = Comput ((P +* (I ';' J)),s,m) ) set SI = stop I; defpred S1[ Element of NAT ] means ( $1 <= LifeSpan (P,s) implies Comput (P,s,$1) = Comput ((P +* (I ';' J)),s,$1) ); assume A2: stop I c= P ; ::_thesis: for m being Element of NAT st m <= LifeSpan (P,s) holds Comput (P,s,m) = Comput ((P +* (I ';' J)),s,m) then A3: P halts_on s by SCMPDS_4:def_7; A4: for m being Element of NAT st S1[m] holds S1[m + 1] proof dom (I ';' J) = (dom I) \/ (dom (Shift (J,(card I)))) by FUNCT_4:def_1; then A5: dom I c= dom (I ';' J) by XBOOLE_1:7; let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] ) assume A6: ( m <= LifeSpan (P,s) implies Comput (P,s,m) = Comput ((P +* (I ';' J)),s,m) ) ; ::_thesis: S1[m + 1] assume A7: m + 1 <= LifeSpan (P,s) ; ::_thesis: Comput (P,s,(m + 1)) = Comput ((P +* (I ';' J)),s,(m + 1)) A8: Comput ((P +* (I ';' J)),s,(m + 1)) = Following ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),s,m))) by EXTPRO_1:3; A9: Comput (P,s,(m + 1)) = Following (P,(Comput (P,s,m))) by EXTPRO_1:3; A10: I ';' J c= P +* (I ';' J) by FUNCT_4:25; A11: IC (Comput (P,s,m)) in dom (stop I) by A2, SCMPDS_4:def_6; A12: P /. (IC (Comput (P,s,m))) = P . (IC (Comput (P,s,m))) by PBOOLE:143; A13: CurInstr (P,(Comput (P,s,m))) = (stop I) . (IC (Comput (P,s,m))) by A11, A12, A2, GRFUNC_1:2; A14: (P +* (I ';' J)) /. (IC (Comput ((P +* (I ';' J)),s,m))) = (P +* (I ';' J)) . (IC (Comput ((P +* (I ';' J)),s,m))) by PBOOLE:143; m < LifeSpan (P,s) by A7, NAT_1:13; then (stop I) . (IC (Comput (P,s,m))) <> halt SCMPDS by A3, A13, EXTPRO_1:def_15; then A15: IC (Comput (P,s,m)) in dom I by A11, COMPOS_1:51; CurInstr (P,(Comput (P,s,m))) = I . (IC (Comput (P,s,m))) by A13, A15, AFINSQ_1:def_3 .= (I ';' J) . (IC (Comput (P,s,m))) by A15, AFINSQ_1:def_3 .= CurInstr ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),s,m))) by A7, A10, A15, A5, A14, A6, GRFUNC_1:2, NAT_1:13 ; hence Comput (P,s,(m + 1)) = Comput ((P +* (I ';' J)),s,(m + 1)) by A6, A7, A9, A8, NAT_1:13; ::_thesis: verum end; A16: S1[ 0 ] ; thus for m being Element of NAT holds S1[m] from NAT_1:sch_1(A16, A4); ::_thesis: verum end; theorem Th20: :: SCMPDS_5:20 for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for I being parahalting Program of SCMPDS for J being Program of SCMPDS st stop I c= P holds for m being Element of NAT st m <= LifeSpan (P,s) holds Comput (P,s,m) = Comput ((P +* (stop (I ';' J))),s,m) proof let P be Instruction-Sequence of SCMPDS; ::_thesis: for s being 0 -started State of SCMPDS for I being parahalting Program of SCMPDS for J being Program of SCMPDS st stop I c= P holds for m being Element of NAT st m <= LifeSpan (P,s) holds Comput (P,s,m) = Comput ((P +* (stop (I ';' J))),s,m) let s be 0 -started State of SCMPDS; ::_thesis: for I being parahalting Program of SCMPDS for J being Program of SCMPDS st stop I c= P holds for m being Element of NAT st m <= LifeSpan (P,s) holds Comput (P,s,m) = Comput ((P +* (stop (I ';' J))),s,m) let I be parahalting Program of SCMPDS; ::_thesis: for J being Program of SCMPDS st stop I c= P holds for m being Element of NAT st m <= LifeSpan (P,s) holds Comput (P,s,m) = Comput ((P +* (stop (I ';' J))),s,m) let J be Program of SCMPDS; ::_thesis: ( stop I c= P implies for m being Element of NAT st m <= LifeSpan (P,s) holds Comput (P,s,m) = Comput ((P +* (stop (I ';' J))),s,m) ) assume A1: stop I c= P ; ::_thesis: for m being Element of NAT st m <= LifeSpan (P,s) holds Comput (P,s,m) = Comput ((P +* (stop (I ';' J))),s,m) set sIJ = stop (I ';' J); set SS = Stop SCMPDS; let m be Element of NAT ; ::_thesis: ( m <= LifeSpan (P,s) implies Comput (P,s,m) = Comput ((P +* (stop (I ';' J))),s,m) ) assume A2: m <= LifeSpan (P,s) ; ::_thesis: Comput (P,s,m) = Comput ((P +* (stop (I ';' J))),s,m) P +* (stop (I ';' J)) = P +* (I ';' (J ';' (Stop SCMPDS))) by AFINSQ_1:27; hence Comput (P,s,m) = Comput ((P +* (stop (I ';' J))),s,m) by A1, A2, Th19; ::_thesis: verum end; Lm2: Load ((DataLoc (0,0)) := 0) is parahalting proof set ii = (DataLoc (0,0)) := 0; set m0 = stop (Load ((DataLoc (0,0)) := 0)); let s be 0 -started State of SCMPDS; :: according to SCMPDS_4:def_7 ::_thesis: for b1 being set holds ( not stop (Load ((DataLoc (0,0)) := 0)) c= b1 or b1 halts_on s ) let P be Instruction-Sequence of SCMPDS; ::_thesis: ( not stop (Load ((DataLoc (0,0)) := 0)) c= P or P halts_on s ) assume A1: stop (Load ((DataLoc (0,0)) := 0)) c= P ; ::_thesis: P halts_on s A2: stop (Load ((DataLoc (0,0)) := 0)) = Macro ((DataLoc (0,0)) := 0) ; take 1 ; :: according to EXTPRO_1:def_8 ::_thesis: ( IC (Comput (P,s,1)) in proj1 P & CurInstr (P,(Comput (P,s,1))) = halt SCMPDS ) IC (Comput (P,s,1)) in NAT ; hence IC (Comput (P,s,1)) in dom P by PARTFUN1:def_2; ::_thesis: CurInstr (P,(Comput (P,s,1))) = halt SCMPDS A3: IC s = 0 by MEMSTR_0:def_11; then A4: IC (Exec (((DataLoc (0,0)) := 0),s)) = succ 0 by SCMPDS_2:45 .= 0 + 1 ; 1 in dom (stop (Load ((DataLoc (0,0)) := 0))) by A2, COMPOS_1:57; then (stop (Load ((DataLoc (0,0)) := 0))) . 1 = P . 1 by A1, GRFUNC_1:2; then A5: P . 1 = halt SCMPDS by A2, COMPOS_1:59; 0 in dom (stop (Load ((DataLoc (0,0)) := 0))) by A2, COMPOS_1:57; then A6: (stop (Load ((DataLoc (0,0)) := 0))) . 0 = P . 0 by A1, GRFUNC_1:2; A7: P /. (IC s) = P . (IC s) by PBOOLE:143; Comput (P,s,(0 + 1)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:3 .= Following (P,s) .= Exec (((DataLoc (0,0)) := 0),s) by A3, A6, A7, A2, COMPOS_1:58 ; hence CurInstr (P,(Comput (P,s,1))) = halt SCMPDS by A5, A4, PBOOLE:143; ::_thesis: verum end; begin definition canceled; let i be Instruction of SCMPDS; attri is parahalting means :Def2: :: SCMPDS_5:def 2 Load i is parahalting ; end; :: deftheorem SCMPDS_5:def_1_:_ canceled; :: deftheorem Def2 defines parahalting SCMPDS_5:def_2_:_ for i being Instruction of SCMPDS holds ( i is parahalting iff Load i is parahalting ); registration cluster No-StopCode shiftable parahalting for Element of the InstructionsF of SCMPDS; existence ex b1 being Instruction of SCMPDS st ( b1 is No-StopCode & b1 is shiftable & b1 is parahalting ) proof take i = (DataLoc (0,0)) := 0; ::_thesis: ( i is No-StopCode & i is shiftable & i is parahalting ) A1: InsCode (halt SCMPDS) = 0 by COMPOS_1:70; InsCode i = 2 by SCMPDS_2:14; then i <> halt SCMPDS by A1; hence i is No-StopCode by COMPOS_0:def_12; ::_thesis: ( i is shiftable & i is parahalting ) thus ( i is shiftable & i is parahalting ) by Def2, Lm2; ::_thesis: verum end; end; theorem :: SCMPDS_5:21 for k1 being Integer holds goto k1 is No-StopCode proof let k1 be Integer; ::_thesis: goto k1 is No-StopCode A1: InsCode (goto k1) = 14 by SCMPDS_2:12; InsCode (halt SCMPDS) = 0 by COMPOS_1:70; hence goto k1 <> halt the InstructionsF of SCMPDS by A1; :: according to COMPOS_0:def_12 ::_thesis: verum end; registration let a be Int_position; cluster return a -> No-StopCode ; coherence return a is No-StopCode proof set i = return a; A1: InsCode (halt SCMPDS) = 0 by RECDEF_2:def_1; InsCode (return a) = 1 by SCMPDS_2:13; then return a <> halt SCMPDS by A1; hence return a is No-StopCode by COMPOS_0:def_12; ::_thesis: verum end; end; registration let a be Int_position; let k1 be Integer; clustera := k1 -> No-StopCode ; coherence a := k1 is No-StopCode proof set i = a := k1; A1: InsCode (halt SCMPDS) = 0 by RECDEF_2:def_1; InsCode (a := k1) = 2 by SCMPDS_2:14; then a := k1 <> halt SCMPDS by A1; hence a := k1 is No-StopCode by COMPOS_0:def_12; ::_thesis: verum end; cluster saveIC (a,k1) -> No-StopCode ; coherence saveIC (a,k1) is No-StopCode proof set i = saveIC (a,k1); A2: InsCode (halt SCMPDS) = 0 by RECDEF_2:def_1; InsCode (saveIC (a,k1)) = 3 by SCMPDS_2:15; then saveIC (a,k1) <> halt SCMPDS by A2; hence saveIC (a,k1) is No-StopCode by COMPOS_0:def_12; ::_thesis: verum end; end; registration let a be Int_position; let k1, k2 be Integer; cluster(a,k1) <>0_goto k2 -> No-StopCode ; coherence (a,k1) <>0_goto k2 is No-StopCode proof set i = (a,k1) <>0_goto k2; A1: InsCode (halt SCMPDS) = 0 by RECDEF_2:def_1; InsCode ((a,k1) <>0_goto k2) = 4 by SCMPDS_2:16; then (a,k1) <>0_goto k2 <> halt SCMPDS by A1; hence (a,k1) <>0_goto k2 is No-StopCode by COMPOS_0:def_12; ::_thesis: verum end; cluster(a,k1) <=0_goto k2 -> No-StopCode ; coherence (a,k1) <=0_goto k2 is No-StopCode proof set i = (a,k1) <=0_goto k2; A2: InsCode (halt SCMPDS) = 0 by RECDEF_2:def_1; InsCode ((a,k1) <=0_goto k2) = 5 by SCMPDS_2:17; then (a,k1) <=0_goto k2 <> halt SCMPDS by A2; hence (a,k1) <=0_goto k2 is No-StopCode by COMPOS_0:def_12; ::_thesis: verum end; cluster(a,k1) >=0_goto k2 -> No-StopCode ; coherence (a,k1) >=0_goto k2 is No-StopCode proof set i = (a,k1) >=0_goto k2; A3: InsCode (halt SCMPDS) = 0 by RECDEF_2:def_1; InsCode ((a,k1) >=0_goto k2) = 6 by SCMPDS_2:18; then (a,k1) >=0_goto k2 <> halt SCMPDS by A3; hence (a,k1) >=0_goto k2 is No-StopCode by COMPOS_0:def_12; ::_thesis: verum end; cluster(a,k1) := k2 -> No-StopCode ; coherence (a,k1) := k2 is No-StopCode proof set i = (a,k1) := k2; A4: InsCode (halt SCMPDS) = 0 by RECDEF_2:def_1; InsCode ((a,k1) := k2) = 7 by SCMPDS_2:19; then (a,k1) := k2 <> halt SCMPDS by A4; hence (a,k1) := k2 is No-StopCode by COMPOS_0:def_12; ::_thesis: verum end; end; registration let a be Int_position; let k1, k2 be Integer; cluster AddTo (a,k1,k2) -> No-StopCode ; coherence AddTo (a,k1,k2) is No-StopCode proof set i = AddTo (a,k1,k2); A1: InsCode (halt SCMPDS) = 0 by RECDEF_2:def_1; InsCode (AddTo (a,k1,k2)) = 8 by SCMPDS_2:20; then AddTo (a,k1,k2) <> halt SCMPDS by A1; hence AddTo (a,k1,k2) is No-StopCode by COMPOS_0:def_12; ::_thesis: verum end; end; registration let a, b be Int_position; let k1, k2 be Integer; cluster AddTo (a,k1,b,k2) -> No-StopCode ; coherence AddTo (a,k1,b,k2) is No-StopCode proof set i = AddTo (a,k1,b,k2); A1: InsCode (halt SCMPDS) = 0 by RECDEF_2:def_1; InsCode (AddTo (a,k1,b,k2)) = 9 by SCMPDS_2:21; then AddTo (a,k1,b,k2) <> halt SCMPDS by A1; hence AddTo (a,k1,b,k2) is No-StopCode by COMPOS_0:def_12; ::_thesis: verum end; cluster SubFrom (a,k1,b,k2) -> No-StopCode ; coherence SubFrom (a,k1,b,k2) is No-StopCode proof set i = SubFrom (a,k1,b,k2); A2: InsCode (halt SCMPDS) = 0 by RECDEF_2:def_1; InsCode (SubFrom (a,k1,b,k2)) = 10 by SCMPDS_2:22; then SubFrom (a,k1,b,k2) <> halt SCMPDS by A2; hence SubFrom (a,k1,b,k2) is No-StopCode by COMPOS_0:def_12; ::_thesis: verum end; cluster MultBy (a,k1,b,k2) -> No-StopCode ; coherence MultBy (a,k1,b,k2) is No-StopCode proof set i = MultBy (a,k1,b,k2); A3: InsCode (halt SCMPDS) = 0 by RECDEF_2:def_1; InsCode (MultBy (a,k1,b,k2)) = 11 by SCMPDS_2:23; then MultBy (a,k1,b,k2) <> halt SCMPDS by A3; hence MultBy (a,k1,b,k2) is No-StopCode by COMPOS_0:def_12; ::_thesis: verum end; cluster Divide (a,k1,b,k2) -> No-StopCode ; coherence Divide (a,k1,b,k2) is No-StopCode proof set i = Divide (a,k1,b,k2); A4: InsCode (halt SCMPDS) = 0 by RECDEF_2:def_1; InsCode (Divide (a,k1,b,k2)) = 12 by SCMPDS_2:24; then Divide (a,k1,b,k2) <> halt SCMPDS by A4; hence Divide (a,k1,b,k2) is No-StopCode by COMPOS_0:def_12; ::_thesis: verum end; cluster(a,k1) := (b,k2) -> No-StopCode ; coherence (a,k1) := (b,k2) is No-StopCode proof set i = (a,k1) := (b,k2); A5: InsCode (halt SCMPDS) = 0 by RECDEF_2:def_1; InsCode ((a,k1) := (b,k2)) = 13 by SCMPDS_2:25; then (a,k1) := (b,k2) <> halt SCMPDS by A5; hence (a,k1) := (b,k2) is No-StopCode by COMPOS_0:def_12; ::_thesis: verum end; end; registration cluster halt SCMPDS -> parahalting ; coherence halt SCMPDS is parahalting proof Stop SCMPDS = Load (halt SCMPDS) ; hence halt SCMPDS is parahalting by Def2; ::_thesis: verum end; end; registration let i be parahalting Instruction of SCMPDS; cluster Load -> parahalting for Program of SCMPDS; coherence for b1 being Program of SCMPDS st b1 = Load i holds b1 is parahalting by Def2; end; Lm3: for i being Instruction of SCMPDS st ( for s being State of SCMPDS holds (Exec (i,s)) . (IC ) = succ (IC s) ) holds Load i is parahalting proof let i be Instruction of SCMPDS; ::_thesis: ( ( for s being State of SCMPDS holds (Exec (i,s)) . (IC ) = succ (IC s) ) implies Load i is parahalting ) assume A1: for s being State of SCMPDS holds (Exec (i,s)) . (IC ) = succ (IC s) ; ::_thesis: Load i is parahalting set m0 = stop (Load i); let t be 0 -started State of SCMPDS; :: according to SCMPDS_4:def_7 ::_thesis: for b1 being set holds ( not stop (Load i) c= b1 or b1 halts_on t ) A2: stop (Load i) = Macro i ; let Q be Instruction-Sequence of SCMPDS; ::_thesis: ( not stop (Load i) c= Q or Q halts_on t ) assume A3: stop (Load i) c= Q ; ::_thesis: Q halts_on t take 1 ; :: according to EXTPRO_1:def_8 ::_thesis: ( IC (Comput (Q,t,1)) in proj1 Q & CurInstr (Q,(Comput (Q,t,1))) = halt SCMPDS ) IC (Comput (Q,t,1)) in NAT ; hence IC (Comput (Q,t,1)) in dom Q by PARTFUN1:def_2; ::_thesis: CurInstr (Q,(Comput (Q,t,1))) = halt SCMPDS A4: IC t = 0 by MEMSTR_0:def_11; then A5: IC (Exec (i,t)) = succ 0 by A1 .= 0 + 1 ; 1 in dom (stop (Load i)) by A2, COMPOS_1:57; then (stop (Load i)) . 1 = Q . 1 by A3, GRFUNC_1:2; then A6: Q . 1 = halt SCMPDS by A2, COMPOS_1:59; 0 in dom (stop (Load i)) by A2, COMPOS_1:57; then A7: (stop (Load i)) . 0 = Q . 0 by A3, GRFUNC_1:2; A8: Q /. (IC t) = Q . (IC t) by PBOOLE:143; Comput (Q,t,(0 + 1)) = Following (Q,(Comput (Q,t,0))) by EXTPRO_1:3 .= Following (Q,t) .= Exec (i,t) by A4, A7, A8, A2, COMPOS_1:58 ; hence CurInstr (Q,(Comput (Q,t,1))) = halt SCMPDS by A5, A6, PBOOLE:143; ::_thesis: verum end; registration let a be Int_position; let k1 be Integer; clustera := k1 -> parahalting ; coherence a := k1 is parahalting proof set i = a := k1; for s being State of SCMPDS holds (Exec ((a := k1),s)) . (IC ) = succ (IC s) by SCMPDS_2:45; then Load (a := k1) is parahalting by Lm3; hence a := k1 is parahalting by Def2; ::_thesis: verum end; end; registration let a be Int_position; let k1, k2 be Integer; cluster(a,k1) := k2 -> parahalting ; coherence (a,k1) := k2 is parahalting proof set i = (a,k1) := k2; for s being State of SCMPDS holds (Exec (((a,k1) := k2),s)) . (IC ) = succ (IC s) by SCMPDS_2:46; then Load ((a,k1) := k2) is parahalting by Lm3; hence (a,k1) := k2 is parahalting by Def2; ::_thesis: verum end; cluster AddTo (a,k1,k2) -> parahalting ; coherence AddTo (a,k1,k2) is parahalting proof set i = AddTo (a,k1,k2); for s being State of SCMPDS holds (Exec ((AddTo (a,k1,k2)),s)) . (IC ) = succ (IC s) by SCMPDS_2:48; then Load (AddTo (a,k1,k2)) is parahalting by Lm3; hence AddTo (a,k1,k2) is parahalting by Def2; ::_thesis: verum end; end; registration let a, b be Int_position; let k1, k2 be Integer; cluster AddTo (a,k1,b,k2) -> parahalting ; coherence AddTo (a,k1,b,k2) is parahalting proof set i = AddTo (a,k1,b,k2); for s being State of SCMPDS holds (Exec ((AddTo (a,k1,b,k2)),s)) . (IC ) = succ (IC s) by SCMPDS_2:49; then Load (AddTo (a,k1,b,k2)) is parahalting by Lm3; hence AddTo (a,k1,b,k2) is parahalting by Def2; ::_thesis: verum end; cluster SubFrom (a,k1,b,k2) -> parahalting ; coherence SubFrom (a,k1,b,k2) is parahalting proof set i = SubFrom (a,k1,b,k2); for s being State of SCMPDS holds (Exec ((SubFrom (a,k1,b,k2)),s)) . (IC ) = succ (IC s) by SCMPDS_2:50; then Load (SubFrom (a,k1,b,k2)) is parahalting by Lm3; hence SubFrom (a,k1,b,k2) is parahalting by Def2; ::_thesis: verum end; cluster MultBy (a,k1,b,k2) -> parahalting ; coherence MultBy (a,k1,b,k2) is parahalting proof set i = MultBy (a,k1,b,k2); for s being State of SCMPDS holds (Exec ((MultBy (a,k1,b,k2)),s)) . (IC ) = succ (IC s) by SCMPDS_2:51; then Load (MultBy (a,k1,b,k2)) is parahalting by Lm3; hence MultBy (a,k1,b,k2) is parahalting by Def2; ::_thesis: verum end; cluster Divide (a,k1,b,k2) -> parahalting ; coherence Divide (a,k1,b,k2) is parahalting proof set i = Divide (a,k1,b,k2); for s being State of SCMPDS holds (Exec ((Divide (a,k1,b,k2)),s)) . (IC ) = succ (IC s) by SCMPDS_2:52; then Load (Divide (a,k1,b,k2)) is parahalting by Lm3; hence Divide (a,k1,b,k2) is parahalting by Def2; ::_thesis: verum end; cluster(a,k1) := (b,k2) -> parahalting ; coherence (a,k1) := (b,k2) is parahalting proof set i = (a,k1) := (b,k2); for s being State of SCMPDS holds (Exec (((a,k1) := (b,k2)),s)) . (IC ) = succ (IC s) by SCMPDS_2:47; then Load ((a,k1) := (b,k2)) is parahalting by Lm3; hence (a,k1) := (b,k2) is parahalting by Def2; ::_thesis: verum end; end; theorem Th22: :: SCMPDS_5:22 for i being Instruction of SCMPDS st InsCode i = 1 holds not i is parahalting proof let i be Instruction of SCMPDS; ::_thesis: ( InsCode i = 1 implies not i is parahalting ) consider s being State of SCMPDS such that A1: for a being Int_position holds s . a = 2 by SCMPDS_2:61; set P = the Instruction-Sequence of SCMPDS; assume InsCode i = 1 ; ::_thesis: not i is parahalting then consider a being Int_position such that A2: i = return a by SCMPDS_2:27; assume i is parahalting ; ::_thesis: contradiction then reconsider Li = Load i as parahalting Program of SCMPDS ; set pi = Macro i; set s1 = Initialize s; set P1 = the Instruction-Sequence of SCMPDS +* (Macro i); (Initialize s) . (DataLoc (((Initialize s) . a),RetIC)) = s . (DataLoc (((Initialize s) . a),RetIC)) by Th15 .= 2 by A1 ; then A3: (Exec (i,(Initialize s))) . (IC ) = (abs 2) + 2 by A2, SCMPDS_2:58 .= 2 + 2 by ABSVALUE:def_1 .= 4 ; set C1 = Comput (( the Instruction-Sequence of SCMPDS +* (Macro i)),(Initialize s),1); stop Li c= the Instruction-Sequence of SCMPDS +* (Macro i) by FUNCT_4:25; then A4: IC (Comput (( the Instruction-Sequence of SCMPDS +* (Macro i)),(Initialize s),1)) in dom (Macro i) by SCMPDS_4:def_6; 0 in dom (Macro i) by COMPOS_1:57; then A5: ( the Instruction-Sequence of SCMPDS +* (Macro i)) . 0 = (Macro i) . 0 by FUNCT_4:13 .= i by COMPOS_1:58 ; A6: card (Macro i) = 2 by COMPOS_1:56; A7: ( the Instruction-Sequence of SCMPDS +* (Macro i)) /. (IC (Initialize s)) = ( the Instruction-Sequence of SCMPDS +* (Macro i)) . (IC (Initialize s)) by PBOOLE:143; Comput (( the Instruction-Sequence of SCMPDS +* (Macro i)),(Initialize s),(0 + 1)) = Following (( the Instruction-Sequence of SCMPDS +* (Macro i)),(Comput (( the Instruction-Sequence of SCMPDS +* (Macro i)),(Initialize s),0))) by EXTPRO_1:3 .= Following (( the Instruction-Sequence of SCMPDS +* (Macro i)),(Initialize s)) .= Exec (i,(Initialize s)) by A5, A7, MEMSTR_0:47 ; hence contradiction by A3, A4, A6, AFINSQ_1:66; ::_thesis: verum end; registration cluster non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() halt-free parahalting shiftable for set ; existence ex b1 being Program of SCMPDS st ( b1 is parahalting & b1 is shiftable & b1 is halt-free ) proof set ii = (DataLoc (0,0)) := 0; take II = Load ((DataLoc (0,0)) := 0); ::_thesis: ( II is parahalting & II is shiftable & II is halt-free ) now__::_thesis:_for_x_being_Nat_st_x_in_dom_II_holds_ II_._x_<>_halt_SCMPDS let x be Nat; ::_thesis: ( x in dom II implies II . x <> halt SCMPDS ) assume x in dom II ; ::_thesis: II . x <> halt SCMPDS then x in {0} by FUNCOP_1:13; then x = 0 by TARSKI:def_1; then A1: II . x = (DataLoc (0,0)) := 0 by FUNCOP_1:72; InsCode ((DataLoc (0,0)) := 0) = 2 by SCMPDS_2:14; hence II . x <> halt SCMPDS by A1, COMPOS_1:70; ::_thesis: verum end; hence ( II is parahalting & II is shiftable & II is halt-free ) by COMPOS_1:def_27; ::_thesis: verum end; end; registration let I, J be halt-free Program of SCMPDS; clusterI ';' J -> halt-free ; coherence I ';' J is halt-free proof set IJ = I ';' J; set D = { (n + (card I)) where n is Element of NAT : n in dom J } ; dom (Shift (J,(card I))) = { (n + (card I)) where n is Element of NAT : n in dom J } by VALUED_1:def_12; then A1: dom (I ';' J) = (dom I) \/ { (n + (card I)) where n is Element of NAT : n in dom J } by FUNCT_4:def_1; let x be Nat; :: according to COMPOS_1:def_27 ::_thesis: ( not x in proj1 (I ';' J) or not (I ';' J) . x = halt SCMPDS ) assume A2: x in dom (I ';' J) ; ::_thesis: not (I ';' J) . x = halt SCMPDS percases ( x in dom I or x in { (n + (card I)) where n is Element of NAT : n in dom J } ) by A2, A1, XBOOLE_0:def_3; supposeA3: x in dom I ; ::_thesis: not (I ';' J) . x = halt SCMPDS then I . x = (I ';' J) . x by AFINSQ_1:def_3; hence (I ';' J) . x <> halt SCMPDS by A3, COMPOS_1:def_27; ::_thesis: verum end; suppose x in { (n + (card I)) where n is Element of NAT : n in dom J } ; ::_thesis: not (I ';' J) . x = halt SCMPDS then consider n being Element of NAT such that A4: x = n + (card I) and A5: n in dom J ; J . n = (I ';' J) . x by A4, A5, AFINSQ_1:def_3; hence (I ';' J) . x <> halt SCMPDS by A5, COMPOS_1:def_27; ::_thesis: verum end; end; end; end; registration let i be No-StopCode Instruction of SCMPDS; cluster Load -> halt-free ; coherence Load i is halt-free proof set p = Load i; now__::_thesis:_for_x_being_Nat_st_x_in_dom_(Load_i)_holds_ (Load_i)_._x_<>_halt_SCMPDS let x be Nat; ::_thesis: ( x in dom (Load i) implies (Load i) . x <> halt SCMPDS ) assume x in dom (Load i) ; ::_thesis: (Load i) . x <> halt SCMPDS then x = 0 by COMPOS_1:50; then (Load i) . x = i by FUNCOP_1:72; hence (Load i) . x <> halt SCMPDS by COMPOS_0:def_12; ::_thesis: verum end; hence Load i is halt-free by COMPOS_1:def_27; ::_thesis: verum end; end; registration let i be No-StopCode Instruction of SCMPDS; let J be halt-free Program of SCMPDS; clusteri ';' J -> halt-free ; coherence i ';' J is halt-free ; end; registration let I be halt-free Program of SCMPDS; let j be No-StopCode Instruction of SCMPDS; clusterI ';' j -> halt-free ; coherence I ';' j is halt-free ; end; registration let i, j be No-StopCode Instruction of SCMPDS; clusteri ';' j -> halt-free ; coherence i ';' j is halt-free ; end; theorem Th23: :: SCMPDS_5:23 for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for I being halt-free parahalting Program of SCMPDS st stop I c= P holds IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I proof let P be Instruction-Sequence of SCMPDS; ::_thesis: for s being 0 -started State of SCMPDS for I being halt-free parahalting Program of SCMPDS st stop I c= P holds IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I let s be 0 -started State of SCMPDS; ::_thesis: for I being halt-free parahalting Program of SCMPDS st stop I c= P holds IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I let I be halt-free parahalting Program of SCMPDS; ::_thesis: ( stop I c= P implies IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I ) set Css = Comput (P,s,(LifeSpan (P,s))); reconsider n = IC (Comput (P,s,(LifeSpan (P,s)))) as Element of NAT ; assume A1: stop I c= P ; ::_thesis: IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I then A2: P halts_on s by SCMPDS_4:def_7; A3: P +* (stop I) = P by A1, FUNCT_4:98; I c= stop I by AFINSQ_1:74; then A4: I c= P by A1, XBOOLE_1:1; now__::_thesis:_not_IC_(Comput_(P,s,(LifeSpan_(P,s))))_in_dom_I assume A5: IC (Comput (P,s,(LifeSpan (P,s)))) in dom I ; ::_thesis: contradiction then I . (IC (Comput (P,s,(LifeSpan (P,s))))) = P . (IC (Comput (P,s,(LifeSpan (P,s))))) by A4, GRFUNC_1:2 .= CurInstr (P,(Comput (P,s,(LifeSpan (P,s))))) by PBOOLE:143 .= halt SCMPDS by A2, EXTPRO_1:def_15 ; hence contradiction by A5, COMPOS_1:def_27; ::_thesis: verum end; then A6: n >= card I by AFINSQ_1:66; A7: card (stop I) = (card I) + 1 by Lm1, AFINSQ_1:17; IC (Comput (P,s,(LifeSpan (P,s)))) in dom (stop I) by A1, SCMPDS_4:def_6; then n < (card I) + 1 by A7, AFINSQ_1:66; then n <= card I by NAT_1:13; hence IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I by A3, A6, XXREAL_0:1; ::_thesis: verum end; theorem Th24: :: SCMPDS_5:24 for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for I being parahalting Program of SCMPDS for k being Element of NAT st k < LifeSpan ((P +* (stop I)),s) holds IC (Comput ((P +* (stop I)),s,k)) in dom I proof let P be Instruction-Sequence of SCMPDS; ::_thesis: for s being 0 -started State of SCMPDS for I being parahalting Program of SCMPDS for k being Element of NAT st k < LifeSpan ((P +* (stop I)),s) holds IC (Comput ((P +* (stop I)),s,k)) in dom I let s be 0 -started State of SCMPDS; ::_thesis: for I being parahalting Program of SCMPDS for k being Element of NAT st k < LifeSpan ((P +* (stop I)),s) holds IC (Comput ((P +* (stop I)),s,k)) in dom I let I be parahalting Program of SCMPDS; ::_thesis: for k being Element of NAT st k < LifeSpan ((P +* (stop I)),s) holds IC (Comput ((P +* (stop I)),s,k)) in dom I let k be Element of NAT ; ::_thesis: ( k < LifeSpan ((P +* (stop I)),s) implies IC (Comput ((P +* (stop I)),s,k)) in dom I ) set ss = s; set PP = P +* (stop I); set m = LifeSpan ((P +* (stop I)),s); set Sk = Comput ((P +* (stop I)),s,k); set Ik = IC (Comput ((P +* (stop I)),s,k)); A1: stop I c= P +* (stop I) by FUNCT_4:25; then A2: P +* (stop I) halts_on s by SCMPDS_4:def_7; reconsider n = IC (Comput ((P +* (stop I)),s,k)) as Element of NAT ; A3: IC (Comput ((P +* (stop I)),s,k)) in dom (stop I) by A1, SCMPDS_4:def_6; A4: stop I c= P +* (stop I) by FUNCT_4:25; assume A5: k < LifeSpan ((P +* (stop I)),s) ; ::_thesis: IC (Comput ((P +* (stop I)),s,k)) in dom I A6: now__::_thesis:_not_n_=_card_I assume A7: n = card I ; ::_thesis: contradiction A8: 0 in dom (Stop SCMPDS) by COMPOS_1:3; A9: (Stop SCMPDS) . 0 = halt SCMPDS by AFINSQ_1:34; CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),s,k))) = (P +* (stop I)) . (IC (Comput ((P +* (stop I)),s,k))) by PBOOLE:143 .= (stop I) . (0 + n) by A3, A4, GRFUNC_1:2 .= halt SCMPDS by A7, A9, A8, AFINSQ_1:def_3 ; hence contradiction by A5, A2, EXTPRO_1:def_15; ::_thesis: verum end; card (stop I) = (card I) + 1 by Lm1, AFINSQ_1:17; then n < (card I) + 1 by A3, AFINSQ_1:66; then n <= card I by INT_1:7; then n < card I by A6, XXREAL_0:1; hence IC (Comput ((P +* (stop I)),s,k)) in dom I by AFINSQ_1:66; ::_thesis: verum end; theorem Th25: :: SCMPDS_5:25 for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for I being parahalting Program of SCMPDS for k being Element of NAT st I c= P & k <= LifeSpan ((P +* (stop I)),s) holds Comput (P,s,k) = Comput ((P +* (stop I)),s,k) proof let P be Instruction-Sequence of SCMPDS; ::_thesis: for s being 0 -started State of SCMPDS for I being parahalting Program of SCMPDS for k being Element of NAT st I c= P & k <= LifeSpan ((P +* (stop I)),s) holds Comput (P,s,k) = Comput ((P +* (stop I)),s,k) let s be 0 -started State of SCMPDS; ::_thesis: for I being parahalting Program of SCMPDS for k being Element of NAT st I c= P & k <= LifeSpan ((P +* (stop I)),s) holds Comput (P,s,k) = Comput ((P +* (stop I)),s,k) let I be parahalting Program of SCMPDS; ::_thesis: for k being Element of NAT st I c= P & k <= LifeSpan ((P +* (stop I)),s) holds Comput (P,s,k) = Comput ((P +* (stop I)),s,k) let k be Element of NAT ; ::_thesis: ( I c= P & k <= LifeSpan ((P +* (stop I)),s) implies Comput (P,s,k) = Comput ((P +* (stop I)),s,k) ) set m = LifeSpan ((P +* (stop I)),s); assume that A1: I c= P and A2: k <= LifeSpan ((P +* (stop I)),s) ; ::_thesis: Comput (P,s,k) = Comput ((P +* (stop I)),s,k) set s2 = s; set P2 = P +* (stop I); defpred S1[ Element of NAT ] means ( $1 <= LifeSpan ((P +* (stop I)),s) implies Comput (P,s,$1) = Comput ((P +* (stop I)),s,$1) ); A3: P = P +* I by A1, FUNCT_4:98; A4: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A5: S1[k] ; ::_thesis: S1[k + 1] now__::_thesis:_(_k_+_1_<=_LifeSpan_((P_+*_(stop_I)),s)_implies_Comput_(P,s,(k_+_1))_=_Comput_((P_+*_(stop_I)),s,(k_+_1))_) A6: Comput ((P +* (stop I)),s,(k + 1)) = Following ((P +* (stop I)),(Comput ((P +* (stop I)),s,k))) by EXTPRO_1:3; A7: Comput (P,s,(k + 1)) = Following (P,(Comput (P,s,k))) by EXTPRO_1:3; A8: k < k + 1 by XREAL_1:29; assume A9: k + 1 <= LifeSpan ((P +* (stop I)),s) ; ::_thesis: Comput (P,s,(k + 1)) = Comput ((P +* (stop I)),s,(k + 1)) then A10: k < LifeSpan ((P +* (stop I)),s) by A8, XXREAL_0:2; then IC (Comput ((P +* (stop I)),s,k)) in dom I by Th24; then A11: IC (Comput ((P +* (stop I)),s,k)) in dom (stop I) by FUNCT_4:12; A12: IC (Comput ((P +* (stop I)),s,k)) in dom I by A10, Th24; CurInstr (P,(Comput (P,s,k))) = P . (IC (Comput ((P +* (stop I)),s,k))) by A5, A9, A8, PBOOLE:143, XXREAL_0:2 .= I . (IC (Comput ((P +* (stop I)),s,k))) by A3, A10, Th24, FUNCT_4:13 .= (stop I) . (IC (Comput ((P +* (stop I)),s,k))) by A12, AFINSQ_1:def_3 .= (P +* (stop I)) . (IC (Comput ((P +* (stop I)),s,k))) by A11, FUNCT_4:13 .= CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),s,k))) by PBOOLE:143 ; hence Comput (P,s,(k + 1)) = Comput ((P +* (stop I)),s,(k + 1)) by A5, A9, A8, A7, A6, XXREAL_0:2; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; A13: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A13, A4); hence Comput (P,s,k) = Comput ((P +* (stop I)),s,k) by A2; ::_thesis: verum end; theorem Th26: :: SCMPDS_5:26 for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for I being halt-free parahalting Program of SCMPDS st I c= P holds IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I proof let P be Instruction-Sequence of SCMPDS; ::_thesis: for s being 0 -started State of SCMPDS for I being halt-free parahalting Program of SCMPDS st I c= P holds IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I let s be 0 -started State of SCMPDS; ::_thesis: for I being halt-free parahalting Program of SCMPDS st I c= P holds IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I let I be halt-free parahalting Program of SCMPDS; ::_thesis: ( I c= P implies IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I ) set PP = P +* (stop I); set m = LifeSpan ((P +* (stop I)),s); A1: stop I c= P +* (stop I) by FUNCT_4:25; A2: ( (stop I) +* (P +* (stop I)) = P +* (stop I) & (P +* (stop I)) +* (stop I) = P +* (stop I) ) by A1, FUNCT_4:97; assume I c= P ; ::_thesis: IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I hence IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = IC (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) by Th25 .= card I by Th23, A2, FUNCT_4:25 ; ::_thesis: verum end; theorem Th27: :: SCMPDS_5:27 for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for I being parahalting Program of SCMPDS holds ( not I c= P or CurInstr (P,(Comput (P,s,(LifeSpan ((P +* (stop I)),s))))) = halt SCMPDS or IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I ) proof let P be Instruction-Sequence of SCMPDS; ::_thesis: for s being 0 -started State of SCMPDS for I being parahalting Program of SCMPDS holds ( not I c= P or CurInstr (P,(Comput (P,s,(LifeSpan ((P +* (stop I)),s))))) = halt SCMPDS or IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I ) let s be 0 -started State of SCMPDS; ::_thesis: for I being parahalting Program of SCMPDS holds ( not I c= P or CurInstr (P,(Comput (P,s,(LifeSpan ((P +* (stop I)),s))))) = halt SCMPDS or IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I ) let I be parahalting Program of SCMPDS; ::_thesis: ( not I c= P or CurInstr (P,(Comput (P,s,(LifeSpan ((P +* (stop I)),s))))) = halt SCMPDS or IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I ) set PP = P +* (stop I); set m = LifeSpan ((P +* (stop I)),s); set s1 = Comput (P,s,(LifeSpan ((P +* (stop I)),s))); set s2 = Comput ((P +* (stop I)),s,(LifeSpan (((P +* (stop I)) +* (stop I)),(Initialize s)))); set Ik = IC (Comput ((P +* (stop I)),s,(LifeSpan (((P +* (stop I)) +* (stop I)),(Initialize s))))); A1: stop I c= P +* (stop I) by FUNCT_4:25; then A2: P +* (stop I) halts_on s by SCMPDS_4:def_7; reconsider n = IC (Comput ((P +* (stop I)),s,(LifeSpan (((P +* (stop I)) +* (stop I)),(Initialize s))))) as Element of NAT ; A3: IC (Comput ((P +* (stop I)),s,(LifeSpan (((P +* (stop I)) +* (stop I)),(Initialize s))))) in dom (stop I) by A1, SCMPDS_4:def_6; A4: Initialize s = s by MEMSTR_0:44; card (stop I) = (card I) + 1 by Lm1, AFINSQ_1:17; then n < (card I) + 1 by A3, AFINSQ_1:66; then A6: n <= card I by INT_1:7; A7: stop I c= P +* (stop I) by FUNCT_4:25; assume A8: I c= P ; ::_thesis: ( CurInstr (P,(Comput (P,s,(LifeSpan ((P +* (stop I)),s))))) = halt SCMPDS or IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I ) then A9: IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = IC (Comput ((P +* (stop I)),s,(LifeSpan (((P +* (stop I)) +* (stop I)),(Initialize s))))) by Th25, A4; now__::_thesis:_(_(_n_<_card_I_&_halt_SCMPDS_=_CurInstr_(P,(Comput_(P,s,(LifeSpan_((P_+*_(stop_I)),s)))))_)_or_(_n_=_card_I_&_IC_(Comput_(P,s,(LifeSpan_((P_+*_(stop_I)),s))))_=_card_I_)_) percases ( n < card I or n = card I ) by A6, XXREAL_0:1; case n < card I ; ::_thesis: halt SCMPDS = CurInstr (P,(Comput (P,s,(LifeSpan ((P +* (stop I)),s))))) then A10: n in dom I by AFINSQ_1:66; thus halt SCMPDS = CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),s,(LifeSpan (((P +* (stop I)) +* (stop I)),(Initialize s)))))) by A2, A4, EXTPRO_1:def_15 .= (P +* (stop I)) . (IC (Comput ((P +* (stop I)),s,(LifeSpan (((P +* (stop I)) +* (stop I)),(Initialize s)))))) by PBOOLE:143 .= (stop I) . (IC (Comput ((P +* (stop I)),s,(LifeSpan (((P +* (stop I)) +* (stop I)),(Initialize s)))))) by A3, A7, GRFUNC_1:2 .= I . (IC (Comput ((P +* (stop I)),s,(LifeSpan (((P +* (stop I)) +* (stop I)),(Initialize s)))))) by A10, AFINSQ_1:def_3 .= P . (IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s))))) by A8, A9, A10, GRFUNC_1:2 .= CurInstr (P,(Comput (P,s,(LifeSpan ((P +* (stop I)),s))))) by PBOOLE:143 ; ::_thesis: verum end; case n = card I ; ::_thesis: IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I hence IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I by A8, Th25, A4; ::_thesis: verum end; end; end; hence ( CurInstr (P,(Comput (P,s,(LifeSpan ((P +* (stop I)),s))))) = halt SCMPDS or IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I ) ; ::_thesis: verum end; theorem Th28: :: SCMPDS_5:28 for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for I being halt-free parahalting Program of SCMPDS for k being Element of NAT st I c= P & k < LifeSpan ((P +* (stop I)),s) holds CurInstr (P,(Comput (P,s,k))) <> halt SCMPDS proof let P be Instruction-Sequence of SCMPDS; ::_thesis: for s being 0 -started State of SCMPDS for I being halt-free parahalting Program of SCMPDS for k being Element of NAT st I c= P & k < LifeSpan ((P +* (stop I)),s) holds CurInstr (P,(Comput (P,s,k))) <> halt SCMPDS let s be 0 -started State of SCMPDS; ::_thesis: for I being halt-free parahalting Program of SCMPDS for k being Element of NAT st I c= P & k < LifeSpan ((P +* (stop I)),s) holds CurInstr (P,(Comput (P,s,k))) <> halt SCMPDS let I be halt-free parahalting Program of SCMPDS; ::_thesis: for k being Element of NAT st I c= P & k < LifeSpan ((P +* (stop I)),s) holds CurInstr (P,(Comput (P,s,k))) <> halt SCMPDS let k be Element of NAT ; ::_thesis: ( I c= P & k < LifeSpan ((P +* (stop I)),s) implies CurInstr (P,(Comput (P,s,k))) <> halt SCMPDS ) set PI = P +* (stop I); set s1 = Comput (P,s,k); set s2 = Comput ((P +* (stop I)),s,k); assume that A1: I c= P and A2: k < LifeSpan ((P +* (stop I)),s) ; ::_thesis: CurInstr (P,(Comput (P,s,k))) <> halt SCMPDS A3: IC (Comput ((P +* (stop I)),s,k)) in dom I by A2, Th24; A4: P /. (IC (Comput (P,s,k))) = P . (IC (Comput (P,s,k))) by PBOOLE:143; CurInstr (P,(Comput (P,s,k))) = P . (IC (Comput ((P +* (stop I)),s,k))) by A4, A1, A2, Th25 .= I . (IC (Comput ((P +* (stop I)),s,k))) by A1, A3, GRFUNC_1:2 ; hence CurInstr (P,(Comput (P,s,k))) <> halt SCMPDS by A3, COMPOS_1:def_27; ::_thesis: verum end; theorem Th29: :: SCMPDS_5:29 for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for I being parahalting Program of SCMPDS for J being Program of SCMPDS for k being Element of NAT st k <= LifeSpan ((P +* (stop I)),s) holds Comput ((P +* (stop I)),s,k) = Comput ((P +* (I ';' J)),s,k) proof let P be Instruction-Sequence of SCMPDS; ::_thesis: for s being 0 -started State of SCMPDS for I being parahalting Program of SCMPDS for J being Program of SCMPDS for k being Element of NAT st k <= LifeSpan ((P +* (stop I)),s) holds Comput ((P +* (stop I)),s,k) = Comput ((P +* (I ';' J)),s,k) let s be 0 -started State of SCMPDS; ::_thesis: for I being parahalting Program of SCMPDS for J being Program of SCMPDS for k being Element of NAT st k <= LifeSpan ((P +* (stop I)),s) holds Comput ((P +* (stop I)),s,k) = Comput ((P +* (I ';' J)),s,k) let I be parahalting Program of SCMPDS; ::_thesis: for J being Program of SCMPDS for k being Element of NAT st k <= LifeSpan ((P +* (stop I)),s) holds Comput ((P +* (stop I)),s,k) = Comput ((P +* (I ';' J)),s,k) let J be Program of SCMPDS; ::_thesis: for k being Element of NAT st k <= LifeSpan ((P +* (stop I)),s) holds Comput ((P +* (stop I)),s,k) = Comput ((P +* (I ';' J)),s,k) let k be Element of NAT ; ::_thesis: ( k <= LifeSpan ((P +* (stop I)),s) implies Comput ((P +* (stop I)),s,k) = Comput ((P +* (I ';' J)),s,k) ) set spI = stop I; set P1 = P +* (stop I); set P2 = P +* (I ';' J); set n = LifeSpan ((P +* (stop I)),s); defpred S1[ Element of NAT ] means ( $1 <= LifeSpan ((P +* (stop I)),s) implies Comput ((P +* (stop I)),s,$1) = Comput ((P +* (I ';' J)),s,$1) ); A1: for n being Element of NAT st S1[n] holds S1[n + 1] proof let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] ) assume A2: ( m <= LifeSpan ((P +* (stop I)),s) implies Comput ((P +* (stop I)),s,m) = Comput ((P +* (I ';' J)),s,m) ) ; ::_thesis: S1[m + 1] A3: Comput ((P +* (I ';' J)),s,(m + 1)) = Following ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),s,m))) by EXTPRO_1:3; stop I c= P +* (stop I) by FUNCT_4:25; then A4: IC (Comput ((P +* (stop I)),s,m)) in dom (stop I) by SCMPDS_4:def_6; A5: Comput ((P +* (stop I)),s,(m + 1)) = Following ((P +* (stop I)),(Comput ((P +* (stop I)),s,m))) by EXTPRO_1:3; assume A6: m + 1 <= LifeSpan ((P +* (stop I)),s) ; ::_thesis: Comput ((P +* (stop I)),s,(m + 1)) = Comput ((P +* (I ';' J)),s,(m + 1)) A7: m < LifeSpan ((P +* (stop I)),s) by A6, NAT_1:13; then IC (Comput ((P +* (stop I)),s,m)) in dom I by Th24; then A8: IC (Comput ((P +* (stop I)),s,m)) in dom (I ';' J) by FUNCT_4:12; A9: IC (Comput ((P +* (stop I)),s,m)) in dom I by A7, Th24; CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),s,m))) = (P +* (stop I)) . (IC (Comput ((P +* (stop I)),s,m))) by PBOOLE:143 .= (stop I) . (IC (Comput ((P +* (stop I)),s,m))) by A4, FUNCT_4:13 .= I . (IC (Comput ((P +* (stop I)),s,m))) by A9, AFINSQ_1:def_3 .= (I ';' J) . (IC (Comput ((P +* (stop I)),s,m))) by A9, AFINSQ_1:def_3 .= (P +* (I ';' J)) . (IC (Comput ((P +* (stop I)),s,m))) by A8, FUNCT_4:13 .= CurInstr ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),s,m))) by A6, A2, NAT_1:13, PBOOLE:143 ; hence Comput ((P +* (stop I)),s,(m + 1)) = Comput ((P +* (I ';' J)),s,(m + 1)) by A2, A6, A5, A3, NAT_1:13; ::_thesis: verum end; A11: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A11, A1); hence ( k <= LifeSpan ((P +* (stop I)),s) implies Comput ((P +* (stop I)),s,k) = Comput ((P +* (I ';' J)),s,k) ) ; ::_thesis: verum end; theorem Th30: :: SCMPDS_5:30 for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for I being parahalting Program of SCMPDS for J being Program of SCMPDS for k being Element of NAT st k <= LifeSpan ((P +* (stop I)),s) holds Comput ((P +* (stop I)),s,k) = Comput ((P +* (stop (I ';' J))),s,k) proof let P be Instruction-Sequence of SCMPDS; ::_thesis: for s being 0 -started State of SCMPDS for I being parahalting Program of SCMPDS for J being Program of SCMPDS for k being Element of NAT st k <= LifeSpan ((P +* (stop I)),s) holds Comput ((P +* (stop I)),s,k) = Comput ((P +* (stop (I ';' J))),s,k) let s be 0 -started State of SCMPDS; ::_thesis: for I being parahalting Program of SCMPDS for J being Program of SCMPDS for k being Element of NAT st k <= LifeSpan ((P +* (stop I)),s) holds Comput ((P +* (stop I)),s,k) = Comput ((P +* (stop (I ';' J))),s,k) let I be parahalting Program of SCMPDS; ::_thesis: for J being Program of SCMPDS for k being Element of NAT st k <= LifeSpan ((P +* (stop I)),s) holds Comput ((P +* (stop I)),s,k) = Comput ((P +* (stop (I ';' J))),s,k) let J be Program of SCMPDS; ::_thesis: for k being Element of NAT st k <= LifeSpan ((P +* (stop I)),s) holds Comput ((P +* (stop I)),s,k) = Comput ((P +* (stop (I ';' J))),s,k) let k be Element of NAT ; ::_thesis: ( k <= LifeSpan ((P +* (stop I)),s) implies Comput ((P +* (stop I)),s,k) = Comput ((P +* (stop (I ';' J))),s,k) ) A1: stop (I ';' J) = I ';' (J ';' (Stop SCMPDS)) by AFINSQ_1:27; thus ( k <= LifeSpan ((P +* (stop I)),s) implies Comput ((P +* (stop I)),s,k) = Comput ((P +* (stop (I ';' J))),s,k) ) by A1, Th29; ::_thesis: verum end; registration let I be parahalting Program of SCMPDS; let J be parahalting shiftable Program of SCMPDS; clusterI ';' J -> parahalting for Program of SCMPDS; coherence for b1 being Program of SCMPDS st b1 = I ';' J holds b1 is parahalting proof let p be Program of SCMPDS; ::_thesis: ( p = I ';' J implies p is parahalting ) assume A1: p = I ';' J ; ::_thesis: p is parahalting let s be 0 -started State of SCMPDS; :: according to SCMPDS_4:def_7 ::_thesis: for b1 being set holds ( not stop p c= b1 or b1 halts_on s ) let P be Instruction-Sequence of SCMPDS; ::_thesis: ( not stop p c= P or P halts_on s ) set sIJ = stop p; set spJ = stop J; set s1 = Initialize s; set P1 = P +* (stop I); set m1 = LifeSpan ((P +* (stop I)),(Initialize s)); set s3 = Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))); set P3 = (P +* (stop I)) +* (stop J); set m3 = LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))))); set D = SCM-Data-Loc ; A2: stop J c= (P +* (stop I)) +* (stop J) by FUNCT_4:25; then A3: (P +* (stop I)) +* (stop J) halts_on Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) by SCMPDS_4:def_7; A4: DataPart (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = DataPart (Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by MEMSTR_0:45; A5: I c= stop p by A1, Th12; set s4 = Comput (P,s,(LifeSpan ((P +* (stop I)),(Initialize s)))); set P4 = P; assume A6: stop p c= P ; ::_thesis: P halts_on s A7: p c= stop p by AFINSQ_1:74; A8: s = Initialize s by MEMSTR_0:44; P +* (I ';' J) = P by A7, A1, A6, FUNCT_4:98, XBOOLE_1:1; then A9: DataPart (Comput (P,s,(LifeSpan ((P +* (stop I)),(Initialize s))))) = DataPart (Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by A4, A8, Th29; percases ( CurInstr (P,(Comput (P,s,(LifeSpan ((P +* (stop I)),(Initialize s)))))) = halt SCMPDS or IC (Comput (P,s,(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I ) by A6, A5, Th27, A8, XBOOLE_1:1; supposeA10: CurInstr (P,(Comput (P,s,(LifeSpan ((P +* (stop I)),(Initialize s)))))) = halt SCMPDS ; ::_thesis: P halts_on s take LifeSpan ((P +* (stop I)),(Initialize s)) ; :: according to EXTPRO_1:def_8 ::_thesis: ( IC (Comput (P,s,(LifeSpan ((P +* (stop I)),(Initialize s))))) in proj1 P & CurInstr (P,(Comput (P,s,(LifeSpan ((P +* (stop I)),(Initialize s)))))) = halt SCMPDS ) IC (Comput (P,s,(LifeSpan ((P +* (stop I)),(Initialize s))))) in NAT ; hence IC (Comput (P,s,(LifeSpan ((P +* (stop I)),(Initialize s))))) in dom P by PARTFUN1:def_2; ::_thesis: CurInstr (P,(Comput (P,s,(LifeSpan ((P +* (stop I)),(Initialize s)))))) = halt SCMPDS thus CurInstr (P,(Comput (P,s,(LifeSpan ((P +* (stop I)),(Initialize s)))))) = halt SCMPDS by A10; ::_thesis: verum end; supposeA11: IC (Comput (P,s,(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I ; ::_thesis: P halts_on s reconsider m = (LifeSpan ((P +* (stop I)),(Initialize s))) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))))) as Element of NAT ; take m ; :: according to EXTPRO_1:def_8 ::_thesis: ( IC (Comput (P,s,m)) in proj1 P & CurInstr (P,(Comput (P,s,m))) = halt SCMPDS ) IC (Comput (P,s,m)) in NAT ; hence IC (Comput (P,s,m)) in dom P by PARTFUN1:def_2; ::_thesis: CurInstr (P,(Comput (P,s,m))) = halt SCMPDS A12: Comput (P,s,((LifeSpan ((P +* (stop I)),(Initialize s))) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))))))) = Comput (P,(Comput (P,s,(LifeSpan ((P +* (stop I)),(Initialize s))))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))))))) by EXTPRO_1:4; stop p = I ';' (J ';' (Stop SCMPDS)) by A1, AFINSQ_1:27 .= I +* (Shift ((stop J),(card I))) ; then Shift ((stop J),(card I)) c= stop p by FUNCT_4:25; then A13: Shift ((stop J),(card I)) c= P by A6, XBOOLE_1:1; CurInstr (((P +* (stop I)) +* (stop J)),(Comput (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))))))))) = CurInstr (P,(Comput (P,s,((LifeSpan ((P +* (stop I)),(Initialize s))) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))))))))) by A12, A2, A9, A11, A13, SCMPDS_4:29; hence CurInstr (P,(Comput (P,s,m))) = halt SCMPDS by A3, EXTPRO_1:def_15; ::_thesis: verum end; end; end; end; registration let i be parahalting Instruction of SCMPDS; let J be parahalting shiftable Program of SCMPDS; clusteri ';' J -> parahalting ; coherence i ';' J is parahalting ; end; registration let I be parahalting Program of SCMPDS; let j be shiftable parahalting Instruction of SCMPDS; clusterI ';' j -> parahalting ; coherence I ';' j is parahalting ; end; registration let i be parahalting Instruction of SCMPDS; let j be shiftable parahalting Instruction of SCMPDS; clusteri ';' j -> parahalting ; coherence i ';' j is parahalting ; end; theorem Th31: :: SCMPDS_5:31 for m, n being Element of NAT for P, P1 being Instruction-Sequence of SCMPDS for s being State of SCMPDS for s1 being 0 -started State of SCMPDS for J being parahalting shiftable Program of SCMPDS st stop J c= P & s = Comput ((P1 +* (stop J)),s1,m) holds Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) proof let m, n be Element of NAT ; ::_thesis: for P, P1 being Instruction-Sequence of SCMPDS for s being State of SCMPDS for s1 being 0 -started State of SCMPDS for J being parahalting shiftable Program of SCMPDS st stop J c= P & s = Comput ((P1 +* (stop J)),s1,m) holds Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) let P, P1 be Instruction-Sequence of SCMPDS; ::_thesis: for s being State of SCMPDS for s1 being 0 -started State of SCMPDS for J being parahalting shiftable Program of SCMPDS st stop J c= P & s = Comput ((P1 +* (stop J)),s1,m) holds Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) let s be State of SCMPDS; ::_thesis: for s1 being 0 -started State of SCMPDS for J being parahalting shiftable Program of SCMPDS st stop J c= P & s = Comput ((P1 +* (stop J)),s1,m) holds Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) let s1 be 0 -started State of SCMPDS; ::_thesis: for J being parahalting shiftable Program of SCMPDS st stop J c= P & s = Comput ((P1 +* (stop J)),s1,m) holds Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) let J be parahalting shiftable Program of SCMPDS; ::_thesis: ( stop J c= P & s = Comput ((P1 +* (stop J)),s1,m) implies Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) ) set pJ = stop J; set s2 = s1; set P2 = P1 +* (stop J); set i = CurInstr (P,s); set ss = s +* (Start-At (((IC s) + n),SCMPDS)); reconsider k = IC s as Element of NAT ; reconsider Nl = succ (IC s) as Element of NAT ; A1: succ (IC (s +* (Start-At (((IC s) + n),SCMPDS)))) = (k + n) + 1 by FUNCT_4:113 .= IC ((Exec ((CurInstr (P,s)),s)) +* (Start-At ((Nl + n),SCMPDS))) by FUNCT_4:113 ; assume A2: stop J c= P ; ::_thesis: ( not s = Comput ((P1 +* (stop J)),s1,m) or Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) ) assume A3: s = Comput ((P1 +* (stop J)),s1,m) ; ::_thesis: Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) stop J c= P1 +* (stop J) by FUNCT_4:25; then A4: IC s in dom (stop J) by A3, SCMPDS_4:def_6; reconsider n1 = IC s as Element of NAT ; set IEn = (IC (Exec ((CurInstr (P,s)),s))) + n; A5: IC (s +* (Start-At (((IC s) + n),SCMPDS))) = (IC s) + n by FUNCT_4:113; A6: P /. (IC s) = P . (IC s) by PBOOLE:143; A7: CurInstr (P,s) = (stop J) . n1 by A4, A6, A2, GRFUNC_1:2; then A8: InsCode (CurInstr (P,s)) <> 1 by A4, SCMPDS_4:def_9; A9: CurInstr (P,s) valid_at n1 by A4, A7, SCMPDS_4:def_9; A10: InsCode (CurInstr (P,s)) <> 3 by A4, A7, SCMPDS_4:def_9; InsCode (CurInstr (P,s)) <= 14 by SCMPDS_2:6; percasesthen ( InsCode (CurInstr (P,s)) = 0 or InsCode (CurInstr (P,s)) = 14 or InsCode (CurInstr (P,s)) = 2 or InsCode (CurInstr (P,s)) = 4 or InsCode (CurInstr (P,s)) = 5 or InsCode (CurInstr (P,s)) = 6 or InsCode (CurInstr (P,s)) = 7 or InsCode (CurInstr (P,s)) = 8 or InsCode (CurInstr (P,s)) = 9 or InsCode (CurInstr (P,s)) = 10 or InsCode (CurInstr (P,s)) = 11 or InsCode (CurInstr (P,s)) = 12 or InsCode (CurInstr (P,s)) = 13 ) by A8, A10, NAT_1:60; supposeA11: InsCode (CurInstr (P,s)) = 0 ; ::_thesis: Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) A12: Following (P,s) = s by A11, SCMPDS_2:86; thus Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC (s,n) by A11, SCMPDS_2:86 .= IncIC ((Following (P,s)),n) by A12 ; ::_thesis: verum end; suppose InsCode (CurInstr (P,s)) = 14 ; ::_thesis: Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) then consider k1 being Integer such that A13: CurInstr (P,s) = goto k1 and A14: n1 + k1 >= 0 by A9, SCMPDS_4:def_8; A15: IC (Exec ((CurInstr (P,s)),s)) = ICplusConst (s,k1) by A13, SCMPDS_2:54; A16: now__::_thesis:_for_b_being_Int_position_holds_(Exec_((CurInstr_(P,s)),(s_+*_(Start-At_(((IC_s)_+_n),SCMPDS)))))_._b_=_(IncIC_((Exec_((CurInstr_(P,s)),s)),n))_._b let b be Int_position; ::_thesis: (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b = (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b = (s +* (Start-At (((IC s) + n),SCMPDS))) . b by A13, SCMPDS_2:54 .= s . b by SCMPDS_3:6 .= (Exec ((CurInstr (P,s)),s)) . b by A13, SCMPDS_2:54 .= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b by SCMPDS_3:6 ; ::_thesis: verum end; IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = ICplusConst ((s +* (Start-At (((IC s) + n),SCMPDS))),k1) by A13, SCMPDS_2:54 .= (IC (Exec ((CurInstr (P,s)),s))) + n by A5, A14, A15, SCMPDS_4:27 .= IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by FUNCT_4:113 ; hence Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) by A16, SCMPDS_2:44; ::_thesis: verum end; suppose InsCode (CurInstr (P,s)) = 2 ; ::_thesis: Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) then consider a being Int_position, k1 being Integer such that A17: CurInstr (P,s) = a := k1 by SCMPDS_2:28; A18: now__::_thesis:_for_b_being_Int_position_holds_(Exec_((CurInstr_(P,s)),(s_+*_(Start-At_(((IC_s)_+_n),SCMPDS)))))_._b_=_(IncIC_((Exec_((CurInstr_(P,s)),s)),n))_._b let b be Int_position; ::_thesis: (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b1 = (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b1 percases ( a = b or a <> b ) ; supposeA19: a = b ; ::_thesis: (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b1 = (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b1 hence (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b = k1 by A17, SCMPDS_2:45 .= (Exec ((CurInstr (P,s)),s)) . b by A17, A19, SCMPDS_2:45 .= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b by SCMPDS_3:6 ; ::_thesis: verum end; supposeA20: a <> b ; ::_thesis: (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b1 = (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b1 hence (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b = (s +* (Start-At (((IC s) + n),SCMPDS))) . b by A17, SCMPDS_2:45 .= s . b by SCMPDS_3:6 .= (Exec ((CurInstr (P,s)),s)) . b by A17, A20, SCMPDS_2:45 .= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b by SCMPDS_3:6 ; ::_thesis: verum end; end; end; IC (Exec ((CurInstr (P,s)),s)) = Nl by A17, SCMPDS_2:45; then IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by A1, A17, SCMPDS_2:45; hence Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) by A18, SCMPDS_2:44; ::_thesis: verum end; suppose InsCode (CurInstr (P,s)) = 4 ; ::_thesis: Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) then consider a being Int_position, k1, k2 being Integer such that A21: CurInstr (P,s) = (a,k1) <>0_goto k2 and A22: n1 + k2 >= 0 by A9, SCMPDS_4:def_8; A23: now__::_thesis:_IC_(Exec_((CurInstr_(P,s)),(s_+*_(Start-At_(((IC_s)_+_n),SCMPDS)))))_=_IC_(IncIC_((Exec_((CurInstr_(P,s)),s)),n)) percases ( s . (DataLoc ((s . a),k1)) <> 0 or s . (DataLoc ((s . a),k1)) = 0 ) ; supposeA24: s . (DataLoc ((s . a),k1)) <> 0 ; ::_thesis: IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) then A25: IC (Exec ((CurInstr (P,s)),s)) = ICplusConst (s,k2) by A21, SCMPDS_2:55; (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc ((s . a),k1)) <> 0 by A24, SCMPDS_3:6; then (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) <> 0 by SCMPDS_3:6; hence IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = ICplusConst ((s +* (Start-At (((IC s) + n),SCMPDS))),k2) by A21, SCMPDS_2:55 .= (IC (Exec ((CurInstr (P,s)),s))) + n by A5, A22, A25, SCMPDS_4:27 .= IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by FUNCT_4:113 ; ::_thesis: verum end; supposeA26: s . (DataLoc ((s . a),k1)) = 0 ; ::_thesis: IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) then (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc ((s . a),k1)) = 0 by SCMPDS_3:6; then A27: (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) = 0 by SCMPDS_3:6; IC (Exec ((CurInstr (P,s)),s)) = Nl by A21, A26, SCMPDS_2:55; hence IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by A1, A21, A27, SCMPDS_2:55; ::_thesis: verum end; end; end; now__::_thesis:_for_b_being_Int_position_holds_(Exec_((CurInstr_(P,s)),(s_+*_(Start-At_(((IC_s)_+_n),SCMPDS)))))_._b_=_(IncIC_((Exec_((CurInstr_(P,s)),s)),n))_._b let b be Int_position; ::_thesis: (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b = (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b = (s +* (Start-At (((IC s) + n),SCMPDS))) . b by A21, SCMPDS_2:55 .= s . b by SCMPDS_3:6 .= (Exec ((CurInstr (P,s)),s)) . b by A21, SCMPDS_2:55 .= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b by SCMPDS_3:6 ; ::_thesis: verum end; hence Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) by A23, SCMPDS_2:44; ::_thesis: verum end; suppose InsCode (CurInstr (P,s)) = 5 ; ::_thesis: Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) then consider a being Int_position, k1, k2 being Integer such that A28: CurInstr (P,s) = (a,k1) <=0_goto k2 and A29: n1 + k2 >= 0 by A9, SCMPDS_4:def_8; A30: now__::_thesis:_IC_(Exec_((CurInstr_(P,s)),(s_+*_(Start-At_(((IC_s)_+_n),SCMPDS)))))_=_IC_(IncIC_((Exec_((CurInstr_(P,s)),s)),n)) percases ( s . (DataLoc ((s . a),k1)) <= 0 or s . (DataLoc ((s . a),k1)) > 0 ) ; supposeA31: s . (DataLoc ((s . a),k1)) <= 0 ; ::_thesis: IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) then A32: IC (Exec ((CurInstr (P,s)),s)) = ICplusConst (s,k2) by A28, SCMPDS_2:56; (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc ((s . a),k1)) <= 0 by A31, SCMPDS_3:6; then (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) <= 0 by SCMPDS_3:6; hence IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = ICplusConst ((s +* (Start-At (((IC s) + n),SCMPDS))),k2) by A28, SCMPDS_2:56 .= (IC (Exec ((CurInstr (P,s)),s))) + n by A5, A29, A32, SCMPDS_4:27 .= IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by FUNCT_4:113 ; ::_thesis: verum end; supposeA33: s . (DataLoc ((s . a),k1)) > 0 ; ::_thesis: IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) then (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc ((s . a),k1)) > 0 by SCMPDS_3:6; then A34: (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) > 0 by SCMPDS_3:6; IC (Exec ((CurInstr (P,s)),s)) = Nl by A28, A33, SCMPDS_2:56; hence IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by A1, A28, A34, SCMPDS_2:56; ::_thesis: verum end; end; end; now__::_thesis:_for_b_being_Int_position_holds_(Exec_((CurInstr_(P,s)),(s_+*_(Start-At_(((IC_s)_+_n),SCMPDS)))))_._b_=_(IncIC_((Exec_((CurInstr_(P,s)),s)),n))_._b let b be Int_position; ::_thesis: (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b = (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b = (s +* (Start-At (((IC s) + n),SCMPDS))) . b by A28, SCMPDS_2:56 .= s . b by SCMPDS_3:6 .= (Exec ((CurInstr (P,s)),s)) . b by A28, SCMPDS_2:56 .= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b by SCMPDS_3:6 ; ::_thesis: verum end; hence Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) by A30, SCMPDS_2:44; ::_thesis: verum end; suppose InsCode (CurInstr (P,s)) = 6 ; ::_thesis: Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) then consider a being Int_position, k1, k2 being Integer such that A35: CurInstr (P,s) = (a,k1) >=0_goto k2 and A36: n1 + k2 >= 0 by A9, SCMPDS_4:def_8; A37: now__::_thesis:_IC_(Exec_((CurInstr_(P,s)),(s_+*_(Start-At_(((IC_s)_+_n),SCMPDS)))))_=_IC_(IncIC_((Exec_((CurInstr_(P,s)),s)),n)) percases ( s . (DataLoc ((s . a),k1)) >= 0 or s . (DataLoc ((s . a),k1)) < 0 ) ; supposeA38: s . (DataLoc ((s . a),k1)) >= 0 ; ::_thesis: IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) then A39: IC (Exec ((CurInstr (P,s)),s)) = ICplusConst (s,k2) by A35, SCMPDS_2:57; (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc ((s . a),k1)) >= 0 by A38, SCMPDS_3:6; then (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) >= 0 by SCMPDS_3:6; hence IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = ICplusConst ((s +* (Start-At (((IC s) + n),SCMPDS))),k2) by A35, SCMPDS_2:57 .= (IC (Exec ((CurInstr (P,s)),s))) + n by A5, A36, A39, SCMPDS_4:27 .= IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by FUNCT_4:113 ; ::_thesis: verum end; supposeA40: s . (DataLoc ((s . a),k1)) < 0 ; ::_thesis: IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) then (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc ((s . a),k1)) < 0 by SCMPDS_3:6; then A41: (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) < 0 by SCMPDS_3:6; IC (Exec ((CurInstr (P,s)),s)) = Nl by A35, A40, SCMPDS_2:57; hence IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by A1, A35, A41, SCMPDS_2:57; ::_thesis: verum end; end; end; now__::_thesis:_for_b_being_Int_position_holds_(Exec_((CurInstr_(P,s)),(s_+*_(Start-At_(((IC_s)_+_n),SCMPDS)))))_._b_=_(IncIC_((Exec_((CurInstr_(P,s)),s)),n))_._b let b be Int_position; ::_thesis: (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b = (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b = (s +* (Start-At (((IC s) + n),SCMPDS))) . b by A35, SCMPDS_2:57 .= s . b by SCMPDS_3:6 .= (Exec ((CurInstr (P,s)),s)) . b by A35, SCMPDS_2:57 .= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b by SCMPDS_3:6 ; ::_thesis: verum end; hence Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) by A37, SCMPDS_2:44; ::_thesis: verum end; suppose InsCode (CurInstr (P,s)) = 7 ; ::_thesis: Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) then consider a being Int_position, k1, k2 being Integer such that A42: CurInstr (P,s) = (a,k1) := k2 by SCMPDS_2:33; A43: now__::_thesis:_for_b_being_Int_position_holds_(Exec_((CurInstr_(P,s)),(s_+*_(Start-At_(((IC_s)_+_n),SCMPDS)))))_._b_=_(IncIC_((Exec_((CurInstr_(P,s)),s)),n))_._b let b be Int_position; ::_thesis: (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b1 = (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b1 percases ( DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) = b or DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) <> b ) ; supposeA44: DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) = b ; ::_thesis: (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b1 = (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b1 then A45: DataLoc ((s . a),k1) = b by SCMPDS_3:6; thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b = k2 by A42, A44, SCMPDS_2:46 .= (Exec ((CurInstr (P,s)),s)) . b by A42, A45, SCMPDS_2:46 .= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b by SCMPDS_3:6 ; ::_thesis: verum end; supposeA46: DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) <> b ; ::_thesis: (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b1 = (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b1 then A47: DataLoc ((s . a),k1) <> b by SCMPDS_3:6; thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b = (s +* (Start-At (((IC s) + n),SCMPDS))) . b by A42, A46, SCMPDS_2:46 .= s . b by SCMPDS_3:6 .= (Exec ((CurInstr (P,s)),s)) . b by A42, A47, SCMPDS_2:46 .= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b by SCMPDS_3:6 ; ::_thesis: verum end; end; end; IC (Exec ((CurInstr (P,s)),s)) = Nl by A42, SCMPDS_2:46; then IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by A1, A42, SCMPDS_2:46; hence Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) by A43, SCMPDS_2:44; ::_thesis: verum end; suppose InsCode (CurInstr (P,s)) = 8 ; ::_thesis: Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) then consider a being Int_position, k1, k2 being Integer such that A48: CurInstr (P,s) = AddTo (a,k1,k2) by SCMPDS_2:34; A49: now__::_thesis:_for_b_being_Int_position_holds_(Exec_((CurInstr_(P,s)),(s_+*_(Start-At_(((IC_s)_+_n),SCMPDS)))))_._b_=_(IncIC_((Exec_((CurInstr_(P,s)),s)),n))_._b let b be Int_position; ::_thesis: (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b1 = (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b1 percases ( DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) = b or DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) <> b ) ; supposeA50: DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) = b ; ::_thesis: (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b1 = (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b1 then A51: DataLoc ((s . a),k1) = b by SCMPDS_3:6; thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b = ((s +* (Start-At (((IC s) + n),SCMPDS))) . b) + k2 by A48, A50, SCMPDS_2:48 .= (s . b) + k2 by SCMPDS_3:6 .= (Exec ((CurInstr (P,s)),s)) . b by A48, A51, SCMPDS_2:48 .= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b by SCMPDS_3:6 ; ::_thesis: verum end; supposeA52: DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) <> b ; ::_thesis: (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b1 = (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b1 then A53: DataLoc ((s . a),k1) <> b by SCMPDS_3:6; thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b = (s +* (Start-At (((IC s) + n),SCMPDS))) . b by A48, A52, SCMPDS_2:48 .= s . b by SCMPDS_3:6 .= (Exec ((CurInstr (P,s)),s)) . b by A48, A53, SCMPDS_2:48 .= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b by SCMPDS_3:6 ; ::_thesis: verum end; end; end; IC (Exec ((CurInstr (P,s)),s)) = Nl by A48, SCMPDS_2:48; then IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by A1, A48, SCMPDS_2:48; hence Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) by A49, SCMPDS_2:44; ::_thesis: verum end; suppose InsCode (CurInstr (P,s)) = 9 ; ::_thesis: Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) then consider a, b being Int_position, k1, k2 being Integer such that A54: CurInstr (P,s) = AddTo (a,k1,b,k2) by SCMPDS_2:35; A55: now__::_thesis:_for_c_being_Int_position_holds_(Exec_((CurInstr_(P,s)),(s_+*_(Start-At_(((IC_s)_+_n),SCMPDS)))))_._c_=_(IncIC_((Exec_((CurInstr_(P,s)),s)),n))_._c let c be Int_position; ::_thesis: (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b1 = (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b1 percases ( DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) = c or DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) <> c ) ; supposeA56: DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) = c ; ::_thesis: (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b1 = (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b1 then A57: DataLoc ((s . a),k1) = c by SCMPDS_3:6; A58: (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . b),k2)) = s . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . b),k2)) by SCMPDS_3:6 .= s . (DataLoc ((s . b),k2)) by SCMPDS_3:6 ; (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) = s . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) by SCMPDS_3:6 .= s . (DataLoc ((s . a),k1)) by SCMPDS_3:6 ; hence (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . c = (s . (DataLoc ((s . a),k1))) + (s . (DataLoc ((s . b),k2))) by A54, A56, A58, SCMPDS_2:49 .= (Exec ((CurInstr (P,s)),s)) . c by A54, A57, SCMPDS_2:49 .= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . c by SCMPDS_3:6 ; ::_thesis: verum end; supposeA59: DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) <> c ; ::_thesis: (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b1 = (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b1 then A60: DataLoc ((s . a),k1) <> c by SCMPDS_3:6; thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . c = (s +* (Start-At (((IC s) + n),SCMPDS))) . c by A54, A59, SCMPDS_2:49 .= s . c by SCMPDS_3:6 .= (Exec ((CurInstr (P,s)),s)) . c by A54, A60, SCMPDS_2:49 .= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . c by SCMPDS_3:6 ; ::_thesis: verum end; end; end; IC (Exec ((CurInstr (P,s)),s)) = Nl by A54, SCMPDS_2:49; then IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by A1, A54, SCMPDS_2:49; hence Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) by A55, SCMPDS_2:44; ::_thesis: verum end; suppose InsCode (CurInstr (P,s)) = 10 ; ::_thesis: Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) then consider a, b being Int_position, k1, k2 being Integer such that A61: CurInstr (P,s) = SubFrom (a,k1,b,k2) by SCMPDS_2:36; A62: now__::_thesis:_for_c_being_Int_position_holds_(Exec_((CurInstr_(P,s)),(s_+*_(Start-At_(((IC_s)_+_n),SCMPDS)))))_._c_=_(IncIC_((Exec_((CurInstr_(P,s)),s)),n))_._c let c be Int_position; ::_thesis: (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b1 = (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b1 percases ( DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) = c or DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) <> c ) ; supposeA63: DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) = c ; ::_thesis: (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b1 = (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b1 then A64: DataLoc ((s . a),k1) = c by SCMPDS_3:6; A65: (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . b),k2)) = s . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . b),k2)) by SCMPDS_3:6 .= s . (DataLoc ((s . b),k2)) by SCMPDS_3:6 ; (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) = s . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) by SCMPDS_3:6 .= s . (DataLoc ((s . a),k1)) by SCMPDS_3:6 ; hence (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . c = (s . (DataLoc ((s . a),k1))) - (s . (DataLoc ((s . b),k2))) by A61, A63, A65, SCMPDS_2:50 .= (Exec ((CurInstr (P,s)),s)) . c by A61, A64, SCMPDS_2:50 .= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . c by SCMPDS_3:6 ; ::_thesis: verum end; supposeA66: DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) <> c ; ::_thesis: (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b1 = (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b1 then A67: DataLoc ((s . a),k1) <> c by SCMPDS_3:6; thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . c = (s +* (Start-At (((IC s) + n),SCMPDS))) . c by A61, A66, SCMPDS_2:50 .= s . c by SCMPDS_3:6 .= (Exec ((CurInstr (P,s)),s)) . c by A61, A67, SCMPDS_2:50 .= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . c by SCMPDS_3:6 ; ::_thesis: verum end; end; end; IC (Exec ((CurInstr (P,s)),s)) = Nl by A61, SCMPDS_2:50; then IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by A1, A61, SCMPDS_2:50; hence Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) by A62, SCMPDS_2:44; ::_thesis: verum end; suppose InsCode (CurInstr (P,s)) = 11 ; ::_thesis: Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) then consider a, b being Int_position, k1, k2 being Integer such that A68: CurInstr (P,s) = MultBy (a,k1,b,k2) by SCMPDS_2:37; A69: now__::_thesis:_for_c_being_Int_position_holds_(Exec_((CurInstr_(P,s)),(s_+*_(Start-At_(((IC_s)_+_n),SCMPDS)))))_._c_=_(IncIC_((Exec_((CurInstr_(P,s)),s)),n))_._c let c be Int_position; ::_thesis: (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b1 = (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b1 percases ( DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) = c or DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) <> c ) ; supposeA70: DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) = c ; ::_thesis: (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b1 = (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b1 then A71: DataLoc ((s . a),k1) = c by SCMPDS_3:6; A72: (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . b),k2)) = s . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . b),k2)) by SCMPDS_3:6 .= s . (DataLoc ((s . b),k2)) by SCMPDS_3:6 ; (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) = s . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) by SCMPDS_3:6 .= s . (DataLoc ((s . a),k1)) by SCMPDS_3:6 ; hence (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . c = (s . (DataLoc ((s . a),k1))) * (s . (DataLoc ((s . b),k2))) by A68, A70, A72, SCMPDS_2:51 .= (Exec ((CurInstr (P,s)),s)) . c by A68, A71, SCMPDS_2:51 .= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . c by SCMPDS_3:6 ; ::_thesis: verum end; supposeA73: DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) <> c ; ::_thesis: (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b1 = (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b1 then A74: DataLoc ((s . a),k1) <> c by SCMPDS_3:6; thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . c = (s +* (Start-At (((IC s) + n),SCMPDS))) . c by A68, A73, SCMPDS_2:51 .= s . c by SCMPDS_3:6 .= (Exec ((CurInstr (P,s)),s)) . c by A68, A74, SCMPDS_2:51 .= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . c by SCMPDS_3:6 ; ::_thesis: verum end; end; end; IC (Exec ((CurInstr (P,s)),s)) = Nl by A68, SCMPDS_2:51; then IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by A1, A68, SCMPDS_2:51; hence Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) by A69, SCMPDS_2:44; ::_thesis: verum end; suppose InsCode (CurInstr (P,s)) = 12 ; ::_thesis: Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) then consider a, b being Int_position, k1, k2 being Integer such that A75: CurInstr (P,s) = Divide (a,k1,b,k2) by SCMPDS_2:38; A76: now__::_thesis:_for_c_being_Int_position_holds_(Exec_((CurInstr_(P,s)),(s_+*_(Start-At_(((IC_s)_+_n),SCMPDS)))))_._c_=_(IncIC_((Exec_((CurInstr_(P,s)),s)),n))_._c let c be Int_position; ::_thesis: (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b1 = (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b1 A77: (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) = s . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1)) by SCMPDS_3:6 .= s . (DataLoc ((s . a),k1)) by SCMPDS_3:6 ; A78: (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . b),k2)) = s . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . b),k2)) by SCMPDS_3:6 .= s . (DataLoc ((s . b),k2)) by SCMPDS_3:6 ; percases ( DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . b),k2) = c or DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . b),k2) <> c ) ; supposeA79: DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . b),k2) = c ; ::_thesis: (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b1 = (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b1 then A80: DataLoc ((s . b),k2) = c by SCMPDS_3:6; thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . c = (s . (DataLoc ((s . a),k1))) mod (s . (DataLoc ((s . b),k2))) by A75, A77, A78, A79, SCMPDS_2:52 .= (Exec ((CurInstr (P,s)),s)) . c by A75, A80, SCMPDS_2:52 .= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . c by SCMPDS_3:6 ; ::_thesis: verum end; supposeA81: DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . b),k2) <> c ; ::_thesis: (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b1 = (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b1 then A82: DataLoc ((s . b),k2) <> c by SCMPDS_3:6; hereby ::_thesis: verum percases ( DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) <> c or DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) = c ) ; supposeA83: DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) <> c ; ::_thesis: (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . c = (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . c then A84: DataLoc ((s . a),k1) <> c by SCMPDS_3:6; thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . c = (s +* (Start-At (((IC s) + n),SCMPDS))) . c by A75, A81, A83, SCMPDS_2:52 .= s . c by SCMPDS_3:6 .= (Exec ((CurInstr (P,s)),s)) . c by A75, A82, A84, SCMPDS_2:52 .= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . c by SCMPDS_3:6 ; ::_thesis: verum end; supposeA85: DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) = c ; ::_thesis: (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . c = (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . c then A86: DataLoc ((s . a),k1) = c by SCMPDS_3:6; thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . c = (s . (DataLoc ((s . a),k1))) div (s . (DataLoc ((s . b),k2))) by A75, A77, A78, A81, A85, SCMPDS_2:52 .= (Exec ((CurInstr (P,s)),s)) . c by A75, A82, A86, SCMPDS_2:52 .= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . c by SCMPDS_3:6 ; ::_thesis: verum end; end; end; end; end; end; IC (Exec ((CurInstr (P,s)),s)) = Nl by A75, SCMPDS_2:52; then IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by A1, A75, SCMPDS_2:52; hence Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) by A76, SCMPDS_2:44; ::_thesis: verum end; suppose InsCode (CurInstr (P,s)) = 13 ; ::_thesis: Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) then consider a, b being Int_position, k1, k2 being Integer such that A87: CurInstr (P,s) = (a,k1) := (b,k2) by SCMPDS_2:39; A88: now__::_thesis:_for_c_being_Int_position_holds_(Exec_((CurInstr_(P,s)),(s_+*_(Start-At_(((IC_s)_+_n),SCMPDS)))))_._c_=_(IncIC_((Exec_((CurInstr_(P,s)),s)),n))_._c let c be Int_position; ::_thesis: (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b1 = (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b1 percases ( DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) = c or DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) <> c ) ; supposeA89: DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) = c ; ::_thesis: (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b1 = (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b1 then A90: DataLoc ((s . a),k1) = c by SCMPDS_3:6; thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . c = (s +* (Start-At (((IC s) + n),SCMPDS))) . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . b),k2)) by A87, A89, SCMPDS_2:47 .= s . (DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . b),k2)) by SCMPDS_3:6 .= s . (DataLoc ((s . b),k2)) by SCMPDS_3:6 .= (Exec ((CurInstr (P,s)),s)) . c by A87, A90, SCMPDS_2:47 .= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . c by SCMPDS_3:6 ; ::_thesis: verum end; supposeA91: DataLoc (((s +* (Start-At (((IC s) + n),SCMPDS))) . a),k1) <> c ; ::_thesis: (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . b1 = (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . b1 then A92: DataLoc ((s . a),k1) <> c by SCMPDS_3:6; thus (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) . c = (s +* (Start-At (((IC s) + n),SCMPDS))) . c by A87, A91, SCMPDS_2:47 .= s . c by SCMPDS_3:6 .= (Exec ((CurInstr (P,s)),s)) . c by A87, A92, SCMPDS_2:47 .= (IncIC ((Exec ((CurInstr (P,s)),s)),n)) . c by SCMPDS_3:6 ; ::_thesis: verum end; end; end; IC (Exec ((CurInstr (P,s)),s)) = Nl by A87, SCMPDS_2:47; then IC (Exec ((CurInstr (P,s)),(s +* (Start-At (((IC s) + n),SCMPDS))))) = IC (IncIC ((Exec ((CurInstr (P,s)),s)),n)) by A1, A87, SCMPDS_2:47; hence Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n) by A88, SCMPDS_2:44; ::_thesis: verum end; end; end; begin theorem :: SCMPDS_5:32 for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for I being halt-free parahalting Program of SCMPDS for J being parahalting shiftable Program of SCMPDS for k being Element of NAT st stop (I ';' J) c= P holds IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I)) = Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k)) proof let P be Instruction-Sequence of SCMPDS; ::_thesis: for s being 0 -started State of SCMPDS for I being halt-free parahalting Program of SCMPDS for J being parahalting shiftable Program of SCMPDS for k being Element of NAT st stop (I ';' J) c= P holds IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I)) = Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k)) let s be 0 -started State of SCMPDS; ::_thesis: for I being halt-free parahalting Program of SCMPDS for J being parahalting shiftable Program of SCMPDS for k being Element of NAT st stop (I ';' J) c= P holds IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I)) = Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k)) let I be halt-free parahalting Program of SCMPDS; ::_thesis: for J being parahalting shiftable Program of SCMPDS for k being Element of NAT st stop (I ';' J) c= P holds IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I)) = Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k)) let J be parahalting shiftable Program of SCMPDS; ::_thesis: for k being Element of NAT st stop (I ';' J) c= P holds IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I)) = Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k)) let k be Element of NAT ; ::_thesis: ( stop (I ';' J) c= P implies IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I)) = Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k)) ) set sIsI = s; set PIPI = P +* (stop I); set RI = Result ((P +* (stop I)),s); set pJ = stop J; set RIJ = Initialize (Result ((P +* (stop I)),s)); set PRIJ = (P +* (stop I)) +* (stop J); set pIJ = stop (I ';' J); set sIsIJ = s; set PIPIJ = P +* (stop (I ';' J)); A1: stop J c= (P +* (stop I)) +* (stop J) by FUNCT_4:25; stop I c= P +* (stop I) by FUNCT_4:25; then A2: P +* (stop I) halts_on s by SCMPDS_4:def_7; set s2 = Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + 0)); set s1 = (Initialize (Result ((P +* (stop I)),s))) +* (Start-At (((IC (Initialize (Result ((P +* (stop I)),s)))) + (card I)),SCMPDS)); set m1 = LifeSpan ((P +* (stop I)),s); A3: I c= stop (I ';' J) by Th12; assume A4: stop (I ';' J) c= P ; ::_thesis: IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I)) = Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k)) A5: P +* (stop (I ';' J)) = P by A4, FUNCT_4:98; A6: now__::_thesis:_(_IC_((Initialize_(Result_((P_+*_(stop_I)),s)))_+*_(Start-At_(((IC_(Initialize_(Result_((P_+*_(stop_I)),s))))_+_(card_I)),SCMPDS)))_=_IC_(Comput_((P_+*_(stop_(I_';'_J))),s,((LifeSpan_((P_+*_(stop_I)),s))_+_0)))_&_(_for_a_being_Int_position_holds_((Initialize_(Result_((P_+*_(stop_I)),s)))_+*_(Start-At_(((IC_(Initialize_(Result_((P_+*_(stop_I)),s))))_+_(card_I)),SCMPDS)))_._a_=_(Comput_((P_+*_(stop_(I_';'_J))),s,((LifeSpan_((P_+*_(stop_I)),s))_+_0)))_._a_)_) thus IC ((Initialize (Result ((P +* (stop I)),s))) +* (Start-At (((IC (Initialize (Result ((P +* (stop I)),s)))) + (card I)),SCMPDS))) = (IC (Initialize (Result ((P +* (stop I)),s)))) + (card I) by FUNCT_4:113 .= 0 + (card I) by FUNCT_4:113 .= IC (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + 0))) by A4, A3, Th26, A5, XBOOLE_1:1 ; ::_thesis: for a being Int_position holds ((Initialize (Result ((P +* (stop I)),s))) +* (Start-At (((IC (Initialize (Result ((P +* (stop I)),s)))) + (card I)),SCMPDS))) . a = (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + 0))) . a hereby ::_thesis: verum let a be Int_position; ::_thesis: ((Initialize (Result ((P +* (stop I)),s))) +* (Start-At (((IC (Initialize (Result ((P +* (stop I)),s)))) + (card I)),SCMPDS))) . a = (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + 0))) . a A7: not a in dom (Start-At (0,SCMPDS)) by SCMPDS_4:18; not a in dom (Start-At (((IC (Initialize (Result ((P +* (stop I)),s)))) + (card I)),SCMPDS)) by SCMPDS_4:18; hence ((Initialize (Result ((P +* (stop I)),s))) +* (Start-At (((IC (Initialize (Result ((P +* (stop I)),s)))) + (card I)),SCMPDS))) . a = (Initialize (Result ((P +* (stop I)),s))) . a by FUNCT_4:11 .= (Result ((P +* (stop I)),s)) . a by A7, FUNCT_4:11 .= (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) . a by A2, EXTPRO_1:23 .= (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + 0))) . a by Th30 ; ::_thesis: verum end; end; defpred S1[ Element of NAT ] means IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),$1)),(card I)) = Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + $1)); A8: stop (I ';' J) c= P +* (stop (I ';' J)) by FUNCT_4:25; A9: 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] ) set k1 = k + 1; set CRk = Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k); set PCRk = (P +* (stop I)) +* (stop J); set CRSk = IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I)); set CIJk = Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k)); set PCIJk = P +* (stop (I ';' J)); set CRk1 = Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1)); set CRSk1 = (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1))) +* (Start-At (((IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1)))) + (card I)),SCMPDS)); set CIJk1 = Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + (k + 1))); assume A10: IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I)) = Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k)) ; ::_thesis: S1[k + 1] A11: CurInstr (((P +* (stop I)) +* (stop J)),(Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k))) = CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k)))) proof A12: CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k)))) = (P +* (stop (I ';' J))) . (IC (IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I)))) by A10, PBOOLE:143 .= (P +* (stop (I ';' J))) . ((IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k))) + (card I)) by FUNCT_4:113 ; reconsider n = IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)) as Element of NAT ; A13: stop (I ';' J) = I ';' (stop J) by AFINSQ_1:27; A14: IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)) in dom (stop J) by A1, SCMPDS_4:def_6; then n < card (stop J) by AFINSQ_1:66; then n + (card I) < (card (stop J)) + (card I) by XREAL_1:6; then n + (card I) < card (stop (I ';' J)) by A13, AFINSQ_1:17; then A15: (IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k))) + (card I) in dom (stop (I ';' J)) by AFINSQ_1:66; A16: ((P +* (stop I)) +* (stop J)) /. (IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k))) = ((P +* (stop I)) +* (stop J)) . (IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k))) by PBOOLE:143; stop J c= (P +* (stop I)) +* (stop J) by FUNCT_4:25; hence CurInstr (((P +* (stop I)) +* (stop J)),(Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k))) = (stop J) . (IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k))) by A14, A16, GRFUNC_1:2 .= (stop (I ';' J)) . ((IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k))) + (card I)) by A14, A13, AFINSQ_1:def_3 .= CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k)))) by A12, A8, A15, GRFUNC_1:2 ; ::_thesis: verum end; A17: Exec ((CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k))))),(Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k)))) = IncIC ((Following (((P +* (stop I)) +* (stop J)),(Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)))),(card I)) by A10, Th31, A11, FUNCT_4:25; Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + (k + 1))) = Comput ((P +* (stop (I ';' J))),s,(((LifeSpan ((P +* (stop I)),s)) + k) + 1)) ; then A18: Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + (k + 1))) = Following ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k)))) by EXTPRO_1:3; A19: now__::_thesis:_for_a_being_Int_position_holds_((Comput_(((P_+*_(stop_I))_+*_(stop_J)),(Initialize_(Result_((P_+*_(stop_I)),s))),(k_+_1)))_+*_(Start-At_(((IC_(Comput_(((P_+*_(stop_I))_+*_(stop_J)),(Initialize_(Result_((P_+*_(stop_I)),s))),(k_+_1))))_+_(card_I)),SCMPDS)))_._a_=_(Comput_((P_+*_(stop_(I_';'_J))),s,((LifeSpan_((P_+*_(stop_I)),s))_+_(k_+_1))))_._a let a be Int_position; ::_thesis: ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1))) +* (Start-At (((IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1)))) + (card I)),SCMPDS))) . a = (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + (k + 1)))) . a thus ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1))) +* (Start-At (((IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1)))) + (card I)),SCMPDS))) . a = (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1))) . a by SCMPDS_3:6 .= (Following (((P +* (stop I)) +* (stop J)),(Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)))) . a by EXTPRO_1:3 .= (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + (k + 1)))) . a by A18, A17, SCMPDS_3:6 ; ::_thesis: verum end; IC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1))) +* (Start-At (((IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1)))) + (card I)),SCMPDS))) = (IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1)))) + (card I) by FUNCT_4:113 .= (IC (Following (((P +* (stop I)) +* (stop J)),(Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k))))) + (card I) by EXTPRO_1:3 ; then IC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1))) +* (Start-At (((IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),(k + 1)))) + (card I)),SCMPDS))) = IC (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + (k + 1)))) by A18, A17, FUNCT_4:113; hence S1[k + 1] by A19, SCMPDS_4:2; ::_thesis: verum end; A20: S1[ 0 ] by A6, SCMPDS_4:2; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A20, A9); hence IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I)) = Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k)) ; ::_thesis: verum end; Lm4: for P, P1 being Instruction-Sequence of SCMPDS for I being halt-free parahalting Program of SCMPDS for J being parahalting shiftable Program of SCMPDS for s being 0 -started State of SCMPDS st stop (I ';' J) c= P & P1 = P +* (stop I) holds ( IC (Comput (P,s,(LifeSpan (P1,s)))) = card I & DataPart (Comput (P,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P & LifeSpan (P,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) ) proof let P, P1 be Instruction-Sequence of SCMPDS; ::_thesis: for I being halt-free parahalting Program of SCMPDS for J being parahalting shiftable Program of SCMPDS for s being 0 -started State of SCMPDS st stop (I ';' J) c= P & P1 = P +* (stop I) holds ( IC (Comput (P,s,(LifeSpan (P1,s)))) = card I & DataPart (Comput (P,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P & LifeSpan (P,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) ) set D = SCM-Data-Loc ; let I be halt-free parahalting Program of SCMPDS; ::_thesis: for J being parahalting shiftable Program of SCMPDS for s being 0 -started State of SCMPDS st stop (I ';' J) c= P & P1 = P +* (stop I) holds ( IC (Comput (P,s,(LifeSpan (P1,s)))) = card I & DataPart (Comput (P,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P & LifeSpan (P,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) ) let J be parahalting shiftable Program of SCMPDS; ::_thesis: for s being 0 -started State of SCMPDS st stop (I ';' J) c= P & P1 = P +* (stop I) holds ( IC (Comput (P,s,(LifeSpan (P1,s)))) = card I & DataPart (Comput (P,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P & LifeSpan (P,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) ) let s be 0 -started State of SCMPDS; ::_thesis: ( stop (I ';' J) c= P & P1 = P +* (stop I) implies ( IC (Comput (P,s,(LifeSpan (P1,s)))) = card I & DataPart (Comput (P,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P & LifeSpan (P,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) ) ) set spJ = stop J; set sIJ = stop (I ';' J); set m1 = LifeSpan (P1,s); set s3 = Initialize (Comput (P1,s,(LifeSpan (P1,s)))); set P3 = P1 +* (stop J); set m3 = LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s)))))); assume that A1: stop (I ';' J) c= P and A2: P1 = P +* (stop I) ; ::_thesis: ( IC (Comput (P,s,(LifeSpan (P1,s)))) = card I & DataPart (Comput (P,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P & LifeSpan (P,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) ) set s4 = Comput (P,s,(LifeSpan (P1,s))); set P4 = P; A3: I c= stop (I ';' J) by Th12; hence A4: IC (Comput (P,s,(LifeSpan (P1,s)))) = card I by A1, A2, Th26, XBOOLE_1:1; ::_thesis: ( DataPart (Comput (P,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P & LifeSpan (P,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) ) reconsider m = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s))))))) as Element of NAT ; stop (I ';' J) = I ';' (J ';' (Stop SCMPDS)) by AFINSQ_1:27 .= I +* (Shift ((stop J),(card I))) ; then A5: Shift ((stop J),(card I)) c= stop (I ';' J) by FUNCT_4:25; A6: stop J c= P1 +* (stop J) by FUNCT_4:25; then A7: P1 +* (stop J) halts_on Initialize (Comput (P1,s,(LifeSpan (P1,s)))) by SCMPDS_4:def_7; A8: DataPart (Comput (P1,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) by MEMSTR_0:45; I ';' J c= stop (I ';' J) by AFINSQ_1:74; then P +* (I ';' J) = P by A1, FUNCT_4:98, XBOOLE_1:1; hence A9: DataPart (Comput (P,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) by A8, A2, Th29; ::_thesis: ( Shift ((stop J),(card I)) c= P & LifeSpan (P,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) ) A10: Comput (P,s,((LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s))))))))) = Comput (P,(Comput (P,s,(LifeSpan (P1,s)))),(LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s)))))))) by EXTPRO_1:4; thus A11: Shift ((stop J),(card I)) c= P by A5, A1, XBOOLE_1:1; ::_thesis: LifeSpan (P,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) then CurInstr ((P1 +* (stop J)),(Comput ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s))))),(LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s)))))))))) = CurInstr (P,(Comput (P,s,((LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s))))))))))) by A10, A6, A4, A9, SCMPDS_4:29; then A12: CurInstr (P,(Comput (P,s,m))) = halt SCMPDS by A7, EXTPRO_1:def_15; A13: now__::_thesis:_for_k_being_Element_of_NAT_st_(LifeSpan_(P1,s))_+_k_<_m_holds_ not_CurInstr_(P,(Comput_(P,s,((LifeSpan_(P1,s))_+_k))))_=_halt_SCMPDS let k be Element of NAT ; ::_thesis: ( (LifeSpan (P1,s)) + k < m implies not CurInstr (P,(Comput (P,s,((LifeSpan (P1,s)) + k)))) = halt SCMPDS ) assume (LifeSpan (P1,s)) + k < m ; ::_thesis: not CurInstr (P,(Comput (P,s,((LifeSpan (P1,s)) + k)))) = halt SCMPDS then A14: k < LifeSpan ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s)))))) by XREAL_1:6; assume A15: CurInstr (P,(Comput (P,s,((LifeSpan (P1,s)) + k)))) = halt SCMPDS ; ::_thesis: contradiction A16: Comput (P,s,((LifeSpan (P1,s)) + k)) = Comput (P,(Comput (P,s,(LifeSpan (P1,s)))),k) by EXTPRO_1:4; CurInstr ((P1 +* (stop J)),(Comput ((P1 +* (stop J)),(Initialize (Comput (P1,s,(LifeSpan (P1,s))))),k))) = halt SCMPDS by A15, A16, A6, A4, A9, A11, SCMPDS_4:29; hence contradiction by A7, A14, EXTPRO_1:def_15; ::_thesis: verum end; now__::_thesis:_for_k_being_Element_of_NAT_st_k_<_m_holds_ CurInstr_(P,(Comput_(P,s,k)))_<>_halt_SCMPDS let k be Element of NAT ; ::_thesis: ( k < m implies CurInstr (P,(Comput (P,s,b1))) <> halt SCMPDS ) assume A17: k < m ; ::_thesis: CurInstr (P,(Comput (P,s,b1))) <> halt SCMPDS percases ( k < LifeSpan (P1,s) or LifeSpan (P1,s) <= k ) ; suppose k < LifeSpan (P1,s) ; ::_thesis: CurInstr (P,(Comput (P,s,b1))) <> halt SCMPDS hence CurInstr (P,(Comput (P,s,k))) <> halt SCMPDS by A2, Th28, A1, A3, XBOOLE_1:1; ::_thesis: verum end; suppose LifeSpan (P1,s) <= k ; ::_thesis: CurInstr (P,(Comput (P,s,b1))) <> halt SCMPDS then consider kk being Nat such that A18: (LifeSpan (P1,s)) + kk = k by NAT_1:10; kk in NAT by ORDINAL1:def_12; hence CurInstr (P,(Comput (P,s,k))) <> halt SCMPDS by A13, A17, A18; ::_thesis: verum end; end; end; then A19: for k being Element of NAT st CurInstr (P,(Comput (P,s,k))) = halt SCMPDS holds m <= k ; stop I c= P1 by A2, FUNCT_4:25; then P1 halts_on s by SCMPDS_4:def_7; then A20: Result (P1,s) = Comput (P1,s,(LifeSpan (P1,s))) by EXTPRO_1:23; P halts_on s by A1, SCMPDS_4:def_7; hence LifeSpan (P,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) by A20, A12, A19, EXTPRO_1:def_15; ::_thesis: verum end; theorem Th33: :: SCMPDS_5:33 for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for I being halt-free parahalting Program of SCMPDS for J being parahalting shiftable Program of SCMPDS holds LifeSpan ((P +* (stop (I ';' J))),s) = (LifeSpan ((P +* (stop I)),s)) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))))) proof let P be Instruction-Sequence of SCMPDS; ::_thesis: for s being 0 -started State of SCMPDS for I being halt-free parahalting Program of SCMPDS for J being parahalting shiftable Program of SCMPDS holds LifeSpan ((P +* (stop (I ';' J))),s) = (LifeSpan ((P +* (stop I)),s)) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))))) let s be 0 -started State of SCMPDS; ::_thesis: for I being halt-free parahalting Program of SCMPDS for J being parahalting shiftable Program of SCMPDS holds LifeSpan ((P +* (stop (I ';' J))),s) = (LifeSpan ((P +* (stop I)),s)) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))))) let I be halt-free parahalting Program of SCMPDS; ::_thesis: for J being parahalting shiftable Program of SCMPDS holds LifeSpan ((P +* (stop (I ';' J))),s) = (LifeSpan ((P +* (stop I)),s)) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))))) let J be parahalting shiftable Program of SCMPDS; ::_thesis: LifeSpan ((P +* (stop (I ';' J))),s) = (LifeSpan ((P +* (stop I)),s)) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))))) set sI = stop I; set sIJ = stop (I ';' J); set s1 = s; set s2 = s; set P1 = P +* (stop (I ';' J)); set P2 = P +* (stop I); A1: stop (I ';' J) c= P +* (stop (I ';' J)) by FUNCT_4:25; set s3 = Initialize (Result (((P +* (stop (I ';' J))) +* (stop I)),s)); set P3 = ((P +* (stop (I ';' J))) +* (stop I)) +* (stop J); set s4 = Initialize (Result ((P +* (stop I)),s)); set P4 = (P +* (stop I)) +* (stop J); A2: stop I c= P +* (stop I) by FUNCT_4:25; A3: stop J c= (P +* (stop I)) +* (stop J) by FUNCT_4:25; A4: stop J c= ((P +* (stop (I ';' J))) +* (stop I)) +* (stop J) by FUNCT_4:25; A5: stop I c= (P +* (stop (I ';' J))) +* (stop I) by FUNCT_4:25; then Initialize (Result ((P +* (stop I)),s)) = Initialize (Result (((P +* (stop (I ';' J))) +* (stop I)),s)) by A2, Th17; then A6: LifeSpan ((((P +* (stop (I ';' J))) +* (stop I)) +* (stop J)),(Initialize (Result (((P +* (stop (I ';' J))) +* (stop I)),s)))) = LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s)))) by A4, A3, Th17; LifeSpan (((P +* (stop (I ';' J))) +* (stop I)),s) = LifeSpan ((P +* (stop I)),s) by A5, A2, Th17; hence LifeSpan ((P +* (stop (I ';' J))),s) = (LifeSpan ((P +* (stop I)),s)) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))))) by A1, A6, Lm4; ::_thesis: verum end; theorem Th34: :: SCMPDS_5:34 for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for I being halt-free parahalting Program of SCMPDS for J being parahalting shiftable Program of SCMPDS holds IExec ((I ';' J),P,s) = IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I)) proof let P be Instruction-Sequence of SCMPDS; ::_thesis: for s being 0 -started State of SCMPDS for I being halt-free parahalting Program of SCMPDS for J being parahalting shiftable Program of SCMPDS holds IExec ((I ';' J),P,s) = IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I)) let s be 0 -started State of SCMPDS; ::_thesis: for I being halt-free parahalting Program of SCMPDS for J being parahalting shiftable Program of SCMPDS holds IExec ((I ';' J),P,s) = IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I)) let I be halt-free parahalting Program of SCMPDS; ::_thesis: for J being parahalting shiftable Program of SCMPDS holds IExec ((I ';' J),P,s) = IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I)) let J be parahalting shiftable Program of SCMPDS; ::_thesis: IExec ((I ';' J),P,s) = IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I)) set A = NAT ; set D = SCM-Data-Loc ; set sI = stop I; set sIJ = stop (I ';' J); set P1 = P +* (stop I); set m1 = LifeSpan ((P +* (stop I)),s); set P2 = P +* (stop (I ';' J)); set s3 = Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))); set P3 = (P +* (stop I)) +* (stop J); set m3 = LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))))); A1: stop J c= (P +* (stop I)) +* (stop J) by FUNCT_4:25; then A2: (P +* (stop I)) +* (stop J) halts_on Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) by SCMPDS_4:def_7; A3: stop J c= P +* (stop J) by FUNCT_4:25; A4: stop I c= P +* (stop I) by FUNCT_4:25; then P +* (stop I) halts_on s by SCMPDS_4:def_7; then A5: Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = Initialize (IExec (I,P,s)) by EXTPRO_1:23; A6: Result ((P +* (stop J)),(Initialize (IExec (I,P,s)))) = Result (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))))) by A1, A3, Th17, A5; A7: stop I c= (P +* (stop (I ';' J))) +* (stop I) by FUNCT_4:25; A8: ((P +* (stop (I ';' J))) +* (stop I)) +* (stop (I ';' J)) = (P +* (stop (I ';' J))) +* ((stop I) +* (stop (I ';' J))) by FUNCT_4:14 .= (P +* (stop (I ';' J))) +* (stop (I ';' J)) by Th14 ; A9: LifeSpan (((P +* (stop (I ';' J))) +* (stop I)),s) = LifeSpan ((P +* (stop I)),s) by A4, A7, Th17; set S1 = s; set E1 = (P +* (stop (I ';' J))) +* (stop I); A10: Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))) = Comput (((P +* (stop I)) +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),s))) by Th20, FUNCT_4:25; A11: (P +* (stop I)) +* (stop (I ';' J)) = P +* ((stop I) +* (stop (I ';' J))) by FUNCT_4:14 .= P +* ((stop (I ';' J)) +* (stop (I ';' J))) by Th14 .= ((P +* (stop (I ';' J))) +* (stop I)) +* (stop (I ';' J)) by A8 ; A12: DataPart (Comput (((P +* (stop (I ';' J))) +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = DataPart (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) by A11, A10, A9, Th20, FUNCT_4:25; A13: stop (I ';' J) c= P +* (stop (I ';' J)) by FUNCT_4:25; then A14: DataPart (Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),s)))) = DataPart (Initialize (Comput (((P +* (stop (I ';' J))) +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))) by A9, Lm4 .= DataPart (Comput (((P +* (stop (I ';' J))) +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) by MEMSTR_0:45 ; A15: Shift ((stop J),(card I)) c= P +* (stop (I ';' J)) by A13, A7, Lm4; A16: IC (Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),s)))) = card I by A13, A9, Lm4; A17: DataPart (Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))) = DataPart (Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),s)))) by A12, A14, MEMSTR_0:45; then A18: IC (Comput ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),s)))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))))))) = (IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))))))))) + (card I) by A15, A1, A16, SCMPDS_4:29; A19: DataPart (Comput ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),s)))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))))))) = DataPart (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))))))) by A16, A15, A1, A17, SCMPDS_4:29; A20: P +* (stop I) halts_on s by A4, SCMPDS_4:def_7; then A21: Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = Initialize (Result ((P +* (stop I)),s)) by EXTPRO_1:23; set SS1 = (Initialize (Result ((P +* (stop I)),s))) +* (stop J); set SS2 = (Initialize (IExec (I,P,s))) +* (stop J); A22: IC (Result (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))))) = IC (Result ((P +* (stop J)),(Initialize (IExec (I,P,s))))) by Th17, A1, A3; A23: P +* (stop (I ';' J)) halts_on s by A13, SCMPDS_4:def_7; A24: IC (IExec ((I ';' J),P,s)) = IC (Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop (I ';' J))),s)))) by A23, EXTPRO_1:23 .= IC (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))))))))) by A21, Th33 .= (IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))))))))) + (card I) by A18, EXTPRO_1:4 .= (IC (Result (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))))))) + (card I) by A2, EXTPRO_1:23 .= (IC (IExec (J,P,(Initialize (IExec (I,P,s)))))) + (card I) by A22, A20, EXTPRO_1:23 ; IExec ((I ';' J),P,s) = Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop (I ';' J))),s))) by A23, EXTPRO_1:23 .= Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))))))) by A21, Th33 ; then A25: DataPart (IExec ((I ';' J),P,s)) = DataPart (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))))))) by A19, EXTPRO_1:4 .= DataPart (IExec (J,P,(Initialize (IExec (I,P,s))))) by A6, A2, EXTPRO_1:23 ; hereby ::_thesis: verum reconsider l = (IC (IExec (J,P,(Initialize (IExec (I,P,s)))))) + (card I) as Element of NAT ; A26: dom (Start-At (l,SCMPDS)) = {(IC )} by FUNCOP_1:13; A27: now__::_thesis:_for_x_being_set_st_x_in_dom_(IExec_((I_';'_J),P,s))_holds_ (IExec_((I_';'_J),P,s))_._x_=_(IncIC_((IExec_(J,P,(Initialize_(IExec_(I,P,s))))),(card_I)))_._x let x be set ; ::_thesis: ( x in dom (IExec ((I ';' J),P,s)) implies (IExec ((I ';' J),P,s)) . b1 = (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) . b1 ) assume A28: x in dom (IExec ((I ';' J),P,s)) ; ::_thesis: (IExec ((I ';' J),P,s)) . b1 = (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) . b1 percases ( x is Int_position or x = IC ) by A28, SCMPDS_4:6; supposeA29: x is Int_position ; ::_thesis: (IExec ((I ';' J),P,s)) . b1 = (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) . b1 then x <> IC by SCMPDS_2:43; then A30: not x in dom (Start-At (l,SCMPDS)) by A26, TARSKI:def_1; (IExec ((I ';' J),P,s)) . x = (IExec (J,P,(Initialize (IExec (I,P,s))))) . x by A25, A29, SCMPDS_4:8; hence (IExec ((I ';' J),P,s)) . x = (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) . x by A30, FUNCT_4:11; ::_thesis: verum end; supposeA31: x = IC ; ::_thesis: (IExec ((I ';' J),P,s)) . b1 = (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) . b1 then x in {(IC )} by TARSKI:def_1; then A32: x in dom (Start-At (l,SCMPDS)) by FUNCOP_1:13; thus (IExec ((I ';' J),P,s)) . x = (Start-At (l,SCMPDS)) . (IC ) by A24, A31, FUNCOP_1:72 .= (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) . x by A31, A32, FUNCT_4:13 ; ::_thesis: verum end; end; end; dom (IExec ((I ';' J),P,s)) = the carrier of SCMPDS by PARTFUN1:def_2 .= dom (IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))) by PARTFUN1:def_2 ; hence IExec ((I ';' J),P,s) = IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I)) by A27, FUNCT_1:2; ::_thesis: verum end; end; theorem :: SCMPDS_5:35 for a being Int_position for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for I being halt-free parahalting Program of SCMPDS for J being parahalting shiftable Program of SCMPDS holds (IExec ((I ';' J),P,s)) . a = (IExec (J,P,(Initialize (IExec (I,P,s))))) . a proof let a be Int_position; ::_thesis: for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for I being halt-free parahalting Program of SCMPDS for J being parahalting shiftable Program of SCMPDS holds (IExec ((I ';' J),P,s)) . a = (IExec (J,P,(Initialize (IExec (I,P,s))))) . a let P be Instruction-Sequence of SCMPDS; ::_thesis: for s being 0 -started State of SCMPDS for I being halt-free parahalting Program of SCMPDS for J being parahalting shiftable Program of SCMPDS holds (IExec ((I ';' J),P,s)) . a = (IExec (J,P,(Initialize (IExec (I,P,s))))) . a let s be 0 -started State of SCMPDS; ::_thesis: for I being halt-free parahalting Program of SCMPDS for J being parahalting shiftable Program of SCMPDS holds (IExec ((I ';' J),P,s)) . a = (IExec (J,P,(Initialize (IExec (I,P,s))))) . a let I be halt-free parahalting Program of SCMPDS; ::_thesis: for J being parahalting shiftable Program of SCMPDS holds (IExec ((I ';' J),P,s)) . a = (IExec (J,P,(Initialize (IExec (I,P,s))))) . a let J be parahalting shiftable Program of SCMPDS; ::_thesis: (IExec ((I ';' J),P,s)) . a = (IExec (J,P,(Initialize (IExec (I,P,s))))) . a A1: not a in dom (Start-At (((IC (IExec (J,P,(Initialize (IExec (I,P,s)))))) + (card I)),SCMPDS)) by SCMPDS_4:18; IExec ((I ';' J),P,s) = IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I)) by Th34; hence (IExec ((I ';' J),P,s)) . a = (IExec (J,P,(Initialize (IExec (I,P,s))))) . a by A1, FUNCT_4:11; ::_thesis: verum end; begin theorem :: SCMPDS_5:36 canceled; theorem :: SCMPDS_5:37 for s1, s2 being State of SCMPDS st s1 | (SCM-Data-Loc \/ {(IC )}) = s2 | (SCM-Data-Loc \/ {(IC )}) holds s1 = s2 proof let s1, s2 be State of SCMPDS; ::_thesis: ( s1 | (SCM-Data-Loc \/ {(IC )}) = s2 | (SCM-Data-Loc \/ {(IC )}) implies s1 = s2 ) set Y = NAT ; set X = SCM-Data-Loc \/ {(IC )}; A1: ( s1 = s1 | ((Data-Locations ) \/ {(IC )}) & s2 = s2 | ((Data-Locations ) \/ {(IC )}) ) by MEMSTR_0:33; thus ( s1 | (SCM-Data-Loc \/ {(IC )}) = s2 | (SCM-Data-Loc \/ {(IC )}) implies s1 = s2 ) by A1, SCMPDS_2:84; ::_thesis: verum end; theorem Th38: :: SCMPDS_5:38 for i being Instruction of SCMPDS for s1, s2 being State of SCMPDS st DataPart s1 = DataPart s2 & InsCode i <> 3 holds DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) proof let i be Instruction of SCMPDS; ::_thesis: for s1, s2 being State of SCMPDS st DataPart s1 = DataPart s2 & InsCode i <> 3 holds DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) let s1, s2 be State of SCMPDS; ::_thesis: ( DataPart s1 = DataPart s2 & InsCode i <> 3 implies DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) ) assume that A1: DataPart s1 = DataPart s2 and A2: InsCode i <> 3 ; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) percases ( InsCode i = 0 or InsCode i = 14 or InsCode i = 1 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 A2, NAT_1:60, SCMPDS_2:6; suppose InsCode i = 0 ; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) then ( Exec (i,s1) = s1 & Exec (i,s2) = s2 ) by SCMPDS_2:86; hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by A1; ::_thesis: verum end; suppose InsCode i = 14 ; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) then A3: ex k1 being Integer st i = goto k1 by SCMPDS_2:26; 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 A3, SCMPDS_2:54 .= s2 . a by A1, SCMPDS_4:8 .= (Exec (i,s2)) . a by A3, SCMPDS_2:54 ; ::_thesis: verum end; hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by SCMPDS_4:8; ::_thesis: verum end; suppose InsCode i = 1 ; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) then consider a being Int_position such that A4: i = return a by SCMPDS_2:27; 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 ) ; supposeA5: a = b ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1 hence (Exec (i,s1)) . b = s1 . (DataLoc ((s1 . a),RetSP)) by A4, SCMPDS_2:58 .= s2 . (DataLoc ((s2 . a),RetSP)) by A1, SCMPDS_3:2 .= (Exec (i,s2)) . b by A4, A5, SCMPDS_2:58 ; ::_thesis: verum end; supposeA6: a <> b ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1 hence (Exec (i,s1)) . b = s1 . b by A4, SCMPDS_2:58 .= s2 . b by A1, SCMPDS_4:8 .= (Exec (i,s2)) . b by A4, A6, SCMPDS_2:58 ; ::_thesis: verum end; end; end; hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by SCMPDS_4:8; ::_thesis: verum end; suppose InsCode i = 2 ; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) then consider a being Int_position, k1 being Integer such that A7: i = a := k1 by 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 ) ; supposeA8: a = b ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1 hence (Exec (i,s1)) . b = k1 by A7, SCMPDS_2:45 .= (Exec (i,s2)) . b by A7, A8, SCMPDS_2:45 ; ::_thesis: verum end; supposeA9: a <> b ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1 hence (Exec (i,s1)) . b = s1 . b by A7, SCMPDS_2:45 .= s2 . b by A1, SCMPDS_4:8 .= (Exec (i,s2)) . b by A7, A9, SCMPDS_2:45 ; ::_thesis: verum end; end; end; hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by SCMPDS_4:8; ::_thesis: verum end; suppose InsCode i = 4 ; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) then A10: ex a being Int_position ex k1, k2 being Integer st i = (a,k1) <>0_goto k2 by SCMPDS_2:30; 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 A10, SCMPDS_2:55 .= s2 . a by A1, SCMPDS_4:8 .= (Exec (i,s2)) . a by A10, SCMPDS_2:55 ; ::_thesis: verum end; hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by SCMPDS_4:8; ::_thesis: verum end; suppose InsCode i = 5 ; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) then A11: ex a being Int_position ex k1, k2 being Integer st i = (a,k1) <=0_goto k2 by SCMPDS_2:31; 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:56 .= s2 . a by A1, SCMPDS_4:8 .= (Exec (i,s2)) . a by A11, SCMPDS_2:56 ; ::_thesis: verum end; hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by SCMPDS_4:8; ::_thesis: verum end; suppose InsCode i = 6 ; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) then A12: ex a being Int_position ex k1, k2 being Integer st i = (a,k1) >=0_goto k2 by SCMPDS_2:32; 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 A12, SCMPDS_2:57 .= s2 . a by A1, SCMPDS_4:8 .= (Exec (i,s2)) . a by A12, SCMPDS_2:57 ; ::_thesis: verum end; hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by SCMPDS_4:8; ::_thesis: verum end; suppose InsCode i = 7 ; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) then consider a being Int_position, k1, k2 being Integer such that A13: i = (a,k1) := k2 by 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 ) ; supposeA14: DataLoc ((s1 . a),k1) = b ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1 then A15: DataLoc ((s2 . a),k1) = b by A1, SCMPDS_4:8; thus (Exec (i,s1)) . b = k2 by A13, A14, SCMPDS_2:46 .= (Exec (i,s2)) . b by A13, A15, SCMPDS_2:46 ; ::_thesis: verum end; supposeA16: DataLoc ((s1 . a),k1) <> b ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1 then A17: DataLoc ((s2 . a),k1) <> b by A1, SCMPDS_4:8; thus (Exec (i,s1)) . b = s1 . b by A13, A16, SCMPDS_2:46 .= s2 . b by A1, SCMPDS_4:8 .= (Exec (i,s2)) . b by A13, A17, SCMPDS_2:46 ; ::_thesis: verum end; end; end; hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by SCMPDS_4:8; ::_thesis: verum end; suppose InsCode i = 8 ; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) then consider a being Int_position, k1, k2 being Integer such that A18: i = AddTo (a,k1,k2) by 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 ) ; supposeA19: DataLoc ((s1 . a),k1) = b ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1 then A20: DataLoc ((s2 . a),k1) = b by A1, SCMPDS_4:8; thus (Exec (i,s1)) . b = (s1 . (DataLoc ((s1 . a),k1))) + k2 by A18, A19, SCMPDS_2:48 .= (s2 . (DataLoc ((s2 . a),k1))) + k2 by A1, SCMPDS_3:2 .= (Exec (i,s2)) . b by A18, A20, SCMPDS_2:48 ; ::_thesis: verum end; supposeA21: DataLoc ((s1 . a),k1) <> b ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1 then A22: DataLoc ((s2 . a),k1) <> b by A1, SCMPDS_4:8; thus (Exec (i,s1)) . b = s1 . b by A18, A21, SCMPDS_2:48 .= s2 . b by A1, SCMPDS_4:8 .= (Exec (i,s2)) . b by A18, A22, SCMPDS_2:48 ; ::_thesis: verum end; end; end; hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by SCMPDS_4:8; ::_thesis: verum end; suppose InsCode i = 9 ; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) then consider a, b being Int_position, k1, k2 being Integer such that A23: i = AddTo (a,k1,b,k2) by 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 ) ; supposeA24: DataLoc ((s1 . a),k1) = c ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1 then A25: DataLoc ((s2 . a),k1) = c by A1, SCMPDS_4:8; thus (Exec (i,s1)) . c = (s1 . (DataLoc ((s1 . a),k1))) + (s1 . (DataLoc ((s1 . b),k2))) by A23, A24, SCMPDS_2:49 .= (s2 . (DataLoc ((s2 . a),k1))) + (s1 . (DataLoc ((s1 . b),k2))) by A1, SCMPDS_3:2 .= (s2 . (DataLoc ((s2 . a),k1))) + (s2 . (DataLoc ((s2 . b),k2))) by A1, SCMPDS_3:2 .= (Exec (i,s2)) . c by A23, A25, SCMPDS_2:49 ; ::_thesis: verum end; supposeA26: DataLoc ((s1 . a),k1) <> c ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1 then A27: DataLoc ((s2 . a),k1) <> c by A1, SCMPDS_4:8; thus (Exec (i,s1)) . c = s1 . c by A23, A26, SCMPDS_2:49 .= s2 . c by A1, SCMPDS_4:8 .= (Exec (i,s2)) . c by A23, A27, SCMPDS_2:49 ; ::_thesis: verum end; end; end; hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by SCMPDS_4:8; ::_thesis: verum end; suppose InsCode i = 10 ; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) then consider a, b being Int_position, k1, k2 being Integer such that A28: i = SubFrom (a,k1,b,k2) by 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 ) ; supposeA29: DataLoc ((s1 . a),k1) = c ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1 then A30: DataLoc ((s2 . a),k1) = c by A1, SCMPDS_4:8; thus (Exec (i,s1)) . c = (s1 . (DataLoc ((s1 . a),k1))) - (s1 . (DataLoc ((s1 . b),k2))) by A28, A29, SCMPDS_2:50 .= (s2 . (DataLoc ((s2 . a),k1))) - (s1 . (DataLoc ((s1 . b),k2))) by A1, SCMPDS_3:2 .= (s2 . (DataLoc ((s2 . a),k1))) - (s2 . (DataLoc ((s2 . b),k2))) by A1, SCMPDS_3:2 .= (Exec (i,s2)) . c by A28, A30, SCMPDS_2:50 ; ::_thesis: verum end; supposeA31: DataLoc ((s1 . a),k1) <> c ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1 then A32: DataLoc ((s2 . a),k1) <> c by A1, SCMPDS_4:8; thus (Exec (i,s1)) . c = s1 . c by A28, A31, SCMPDS_2:50 .= s2 . c by A1, SCMPDS_4:8 .= (Exec (i,s2)) . c by A28, A32, SCMPDS_2:50 ; ::_thesis: verum end; end; end; hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by SCMPDS_4:8; ::_thesis: verum end; suppose InsCode i = 11 ; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) then consider a, b being Int_position, k1, k2 being Integer such that A33: i = MultBy (a,k1,b,k2) by 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 ) ; supposeA34: DataLoc ((s1 . a),k1) = c ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1 then A35: DataLoc ((s2 . a),k1) = c by A1, SCMPDS_4:8; thus (Exec (i,s1)) . c = (s1 . (DataLoc ((s1 . a),k1))) * (s1 . (DataLoc ((s1 . b),k2))) by A33, A34, SCMPDS_2:51 .= (s2 . (DataLoc ((s2 . a),k1))) * (s1 . (DataLoc ((s1 . b),k2))) by A1, SCMPDS_3:2 .= (s2 . (DataLoc ((s2 . a),k1))) * (s2 . (DataLoc ((s2 . b),k2))) by A1, SCMPDS_3:2 .= (Exec (i,s2)) . c by A33, A35, SCMPDS_2:51 ; ::_thesis: verum end; supposeA36: DataLoc ((s1 . a),k1) <> c ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1 then A37: DataLoc ((s2 . a),k1) <> c by A1, SCMPDS_4:8; thus (Exec (i,s1)) . c = s1 . c by A33, A36, SCMPDS_2:51 .= s2 . c by A1, SCMPDS_4:8 .= (Exec (i,s2)) . c by A33, A37, SCMPDS_2:51 ; ::_thesis: verum end; end; end; hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by SCMPDS_4:8; ::_thesis: verum end; suppose InsCode i = 12 ; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) then consider a, b being Int_position, k1, k2 being Integer such that A38: i = Divide (a,k1,b,k2) by 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 ) ; supposeA39: DataLoc ((s1 . b),k2) = c ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1 then A40: DataLoc ((s2 . b),k2) = c by A1, SCMPDS_4:8; thus (Exec (i,s1)) . c = (s1 . (DataLoc ((s1 . a),k1))) mod (s1 . (DataLoc ((s1 . b),k2))) by A38, A39, SCMPDS_2:52 .= (s2 . (DataLoc ((s2 . a),k1))) mod (s1 . (DataLoc ((s1 . b),k2))) by A1, SCMPDS_3:2 .= (s2 . (DataLoc ((s2 . a),k1))) mod (s2 . (DataLoc ((s2 . b),k2))) by A1, SCMPDS_3:2 .= (Exec (i,s2)) . c by A38, A40, SCMPDS_2:52 ; ::_thesis: verum end; supposeA41: DataLoc ((s1 . b),k2) <> c ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1 then A42: DataLoc ((s2 . b),k2) <> c by A1, SCMPDS_4:8; hereby ::_thesis: verum percases ( DataLoc ((s1 . a),k1) <> c or DataLoc ((s1 . a),k1) = c ) ; supposeA43: DataLoc ((s1 . a),k1) <> c ; ::_thesis: (Exec (i,s1)) . c = (Exec (i,s2)) . c then A44: DataLoc ((s2 . a),k1) <> c by A1, SCMPDS_4:8; thus (Exec (i,s1)) . c = s1 . c by A38, A41, A43, SCMPDS_2:52 .= s2 . c by A1, SCMPDS_4:8 .= (Exec (i,s2)) . c by A38, A42, A44, SCMPDS_2:52 ; ::_thesis: verum end; supposeA45: DataLoc ((s1 . a),k1) = c ; ::_thesis: (Exec (i,s1)) . c = (Exec (i,s2)) . c then A46: DataLoc ((s2 . a),k1) = c by A1, SCMPDS_4:8; thus (Exec (i,s1)) . c = (s1 . (DataLoc ((s1 . a),k1))) div (s1 . (DataLoc ((s1 . b),k2))) by A38, A41, A45, SCMPDS_2:52 .= (s2 . (DataLoc ((s2 . a),k1))) div (s1 . (DataLoc ((s1 . b),k2))) by A1, SCMPDS_3:2 .= (s2 . (DataLoc ((s2 . a),k1))) div (s2 . (DataLoc ((s2 . b),k2))) by A1, SCMPDS_3:2 .= (Exec (i,s2)) . c by A38, A42, A46, SCMPDS_2:52 ; ::_thesis: verum end; end; end; end; end; end; hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by SCMPDS_4:8; ::_thesis: verum end; suppose InsCode i = 13 ; ::_thesis: DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) then consider a, b being Int_position, k1, k2 being Integer such that A47: i = (a,k1) := (b,k2) by 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 ) ; supposeA48: DataLoc ((s1 . a),k1) = c ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1 then A49: DataLoc ((s2 . a),k1) = c by A1, SCMPDS_4:8; thus (Exec (i,s1)) . c = s1 . (DataLoc ((s1 . b),k2)) by A47, A48, SCMPDS_2:47 .= s2 . (DataLoc ((s2 . b),k2)) by A1, SCMPDS_3:2 .= (Exec (i,s2)) . c by A47, A49, SCMPDS_2:47 ; ::_thesis: verum end; supposeA50: DataLoc ((s1 . a),k1) <> c ; ::_thesis: (Exec (i,s1)) . b1 = (Exec (i,s2)) . b1 then A51: DataLoc ((s2 . a),k1) <> c by A1, SCMPDS_4:8; thus (Exec (i,s1)) . c = s1 . c by A47, A50, SCMPDS_2:47 .= s2 . c by A1, SCMPDS_4:8 .= (Exec (i,s2)) . c by A47, A51, SCMPDS_2:47 ; ::_thesis: verum end; end; end; hence DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) by SCMPDS_4:8; ::_thesis: verum end; end; end; theorem Th39: :: SCMPDS_5:39 for s1, s2 being State of SCMPDS for i being shiftable Instruction of SCMPDS st DataPart s1 = DataPart s2 holds DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) proof let s1, s2 be State of SCMPDS; ::_thesis: for i being shiftable Instruction of SCMPDS st DataPart s1 = DataPart s2 holds DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) let i be shiftable Instruction of SCMPDS; ::_thesis: ( DataPart s1 = DataPart s2 implies DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) ) InsCode i <> 3 by SCMPDS_4:def_10; hence ( DataPart s1 = DataPart s2 implies DataPart (Exec (i,s1)) = DataPart (Exec (i,s2)) ) by Th38; ::_thesis: verum end; theorem Th40: :: SCMPDS_5:40 for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for i being parahalting Instruction of SCMPDS holds Exec (i,s) = IExec ((Load i),P,s) proof let P be Instruction-Sequence of SCMPDS; ::_thesis: for s being 0 -started State of SCMPDS for i being parahalting Instruction of SCMPDS holds Exec (i,s) = IExec ((Load i),P,s) let s be 0 -started State of SCMPDS; ::_thesis: for i being parahalting Instruction of SCMPDS holds Exec (i,s) = IExec ((Load i),P,s) let i be parahalting Instruction of SCMPDS; ::_thesis: Exec (i,s) = IExec ((Load i),P,s) set Li = Load i; set Mi = Macro i; set PI = P +* (Macro i); set IC1 = IC (Comput ((P +* (Macro i)),s,1)); A1: Initialize s = s by MEMSTR_0:44; Macro i c= P +* (Macro i) by FUNCT_4:25; then A2: P +* (Macro i) halts_on s by SCMPDS_4:def_7; A3: 1 in dom (Macro i) by COMPOS_1:57; A4: 0 in dom (Macro i) by COMPOS_1:57; A5: (Macro i) . 1 = halt SCMPDS by COMPOS_1:59; A6: (Macro i) . 0 = i by COMPOS_1:58; A7: Macro i c= P +* (Macro i) by FUNCT_4:25; then A8: IC (Comput ((P +* (Macro i)),s,1)) in dom (Macro i) by SCMPDS_4:def_6; A9: (P +* (Macro i)) /. (IC s) = (P +* (Macro i)) . (IC s) by PBOOLE:143; A10: Comput ((P +* (Macro i)),s,(0 + 1)) = Following ((P +* (Macro i)),(Comput ((P +* (Macro i)),s,0))) by EXTPRO_1:3 .= Following ((P +* (Macro i)),s) .= Exec (((P +* (Macro i)) . 0),s) by A9, A1, MEMSTR_0:47 .= Exec (i,s) by A4, A6, A7, GRFUNC_1:2 ; percases ( IC (Comput ((P +* (Macro i)),s,1)) = 0 or IC (Comput ((P +* (Macro i)),s,1)) = 1 ) by A8, COMPOS_1:60; supposeA11: IC (Comput ((P +* (Macro i)),s,1)) = 0 ; ::_thesis: Exec (i,s) = IExec ((Load i),P,s) set Ni = InsCode i; succ (IC s) = succ 0 by A1, MEMSTR_0:47 .= 1 ; then A12: InsCode i in {0,1,4,5,6,14} by A10, A11, SCMPDS_4:1; A13: CurInstr ((P +* (Macro i)),(Comput ((P +* (Macro i)),s,1))) = (P +* (Macro i)) . 0 by A11, PBOOLE:143 .= i by A4, A6, A7, GRFUNC_1:2 ; A14: InsCode i <> 1 by Th22; hereby ::_thesis: verum percases ( i = halt SCMPDS or i <> halt SCMPDS ) ; suppose i = halt SCMPDS ; ::_thesis: Exec (i,s) = IExec ((Load i),P,s) hence Exec (i,s) = IExec ((Load i),P,s) by A2, A10, A13, EXTPRO_1:def_9; ::_thesis: verum end; supposeA15: i <> halt SCMPDS ; ::_thesis: Exec (i,s) = IExec ((Load i),P,s) A16: now__::_thesis:_for_b_being_Int_position_holds_s_._b_=_(Exec_(i,s))_._b let b be Int_position; ::_thesis: s . b1 = (Exec (i,s)) . b1 percases ( InsCode i = 0 or InsCode i = 14 or InsCode i = 4 or InsCode i = 5 or InsCode i = 6 ) by A12, A14, ENUMSET1:def_4; suppose InsCode i = 0 ; ::_thesis: s . b1 = (Exec (i,s)) . b1 hence s . b = (Exec (i,s)) . b by SCMPDS_2:86; ::_thesis: verum end; suppose InsCode i = 14 ; ::_thesis: s . b1 = (Exec (i,s)) . b1 then ex k1 being Integer st i = goto k1 by SCMPDS_2:26; hence s . b = (Exec (i,s)) . b by SCMPDS_2:54; ::_thesis: verum end; suppose InsCode i = 4 ; ::_thesis: s . b1 = (Exec (i,s)) . b1 then ex a being Int_position ex k1, k2 being Integer st i = (a,k1) <>0_goto k2 by SCMPDS_2:30; hence s . b = (Exec (i,s)) . b by SCMPDS_2:55; ::_thesis: verum end; suppose InsCode i = 5 ; ::_thesis: s . b1 = (Exec (i,s)) . b1 then ex a being Int_position ex k1, k2 being Integer st i = (a,k1) <=0_goto k2 by SCMPDS_2:31; hence s . b = (Exec (i,s)) . b by SCMPDS_2:56; ::_thesis: verum end; suppose InsCode i = 6 ; ::_thesis: s . b1 = (Exec (i,s)) . b1 then ex a being Int_position ex k1, k2 being Integer st i = (a,k1) >=0_goto k2 by SCMPDS_2:32; hence s . b = (Exec (i,s)) . b by SCMPDS_2:57; ::_thesis: verum end; end; end; A17: Following ((P +* (Macro i)),s) = Following ((P +* (Macro i)),(Comput ((P +* (Macro i)),s,0))) .= Exec (i,s) by A10, EXTPRO_1:3 ; A18: IC s = IC (Exec (i,s)) by A10, A11, A1, MEMSTR_0:47; then A19: s = Exec (i,s) by A16, SCMPDS_2:44; now__::_thesis:_for_n_being_Element_of_NAT_holds_CurInstr_((P_+*_(Macro_i)),(Comput_((P_+*_(Macro_i)),s,n)))_<>_halt_SCMPDS let n be Element of NAT ; ::_thesis: CurInstr ((P +* (Macro i)),(Comput ((P +* (Macro i)),s,n))) <> halt SCMPDS Comput ((P +* (Macro i)),s,n) = s by A18, A16, A17, EXTPRO_1:27, SCMPDS_2:44 .= Following ((P +* (Macro i)),(Comput ((P +* (Macro i)),s,0))) by A19, A17 .= Comput ((P +* (Macro i)),s,(0 + 1)) by EXTPRO_1:3 ; hence CurInstr ((P +* (Macro i)),(Comput ((P +* (Macro i)),s,n))) <> halt SCMPDS by A13, A15; ::_thesis: verum end; then not P +* (Macro i) halts_on s by EXTPRO_1:29; hence Exec (i,s) = IExec ((Load i),P,s) by A7, SCMPDS_4:def_7; ::_thesis: verum end; end; end; end; supposeA20: IC (Comput ((P +* (Macro i)),s,1)) = 1 ; ::_thesis: Exec (i,s) = IExec ((Load i),P,s) CurInstr ((P +* (Macro i)),(Comput ((P +* (Macro i)),s,1))) = (P +* (Macro i)) . 1 by A20, PBOOLE:143 .= halt SCMPDS by A3, A5, A7, GRFUNC_1:2 ; hence Exec (i,s) = IExec ((Load i),P,s) by A2, A10, EXTPRO_1:def_9; ::_thesis: verum end; end; end; theorem Th41: :: SCMPDS_5:41 for a being Int_position for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for I being halt-free parahalting Program of SCMPDS for j being shiftable parahalting Instruction of SCMPDS holds (IExec ((I ';' j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a proof let a be Int_position; ::_thesis: for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for I being halt-free parahalting Program of SCMPDS for j being shiftable parahalting Instruction of SCMPDS holds (IExec ((I ';' j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a let P be Instruction-Sequence of SCMPDS; ::_thesis: for s being 0 -started State of SCMPDS for I being halt-free parahalting Program of SCMPDS for j being shiftable parahalting Instruction of SCMPDS holds (IExec ((I ';' j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a let s be 0 -started State of SCMPDS; ::_thesis: for I being halt-free parahalting Program of SCMPDS for j being shiftable parahalting Instruction of SCMPDS holds (IExec ((I ';' j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a let I be halt-free parahalting Program of SCMPDS; ::_thesis: for j being shiftable parahalting Instruction of SCMPDS holds (IExec ((I ';' j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a let j be shiftable parahalting Instruction of SCMPDS; ::_thesis: (IExec ((I ';' j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a set Mj = Load j; set SA = Start-At (((IC (IExec ((Load j),P,(Initialize (IExec (I,P,s)))))) + (card I)),SCMPDS); A1: not a in dom (Start-At (((IC (IExec ((Load j),P,(Initialize (IExec (I,P,s)))))) + (card I)),SCMPDS)) by SCMPDS_4:18; A2: a in SCM-Data-Loc by AMI_2:def_16; for a being Int_position holds (Initialize (IExec (I,P,s))) . a = (IExec (I,P,s)) . a by Th15; then A3: DataPart (Initialize (IExec (I,P,s))) = DataPart (IExec (I,P,s)) by SCMPDS_4:8; thus (IExec ((I ';' j),P,s)) . a = (IncIC ((IExec ((Load j),P,(Initialize (IExec (I,P,s))))),(card I))) . a by Th34 .= (IExec ((Load j),P,(Initialize (IExec (I,P,s))))) . a by A1, FUNCT_4:11 .= (Exec (j,(Initialize (IExec (I,P,s))))) . a by Th40 .= (DataPart (Exec (j,(Initialize (IExec (I,P,s)))))) . a by A2, FUNCT_1:49, SCMPDS_2:84 .= (DataPart (Exec (j,(IExec (I,P,s))))) . a by A3, Th39 .= (Exec (j,(IExec (I,P,s)))) . a by A2, FUNCT_1:49, SCMPDS_2:84 ; ::_thesis: verum end; theorem :: SCMPDS_5:42 for a being Int_position for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for i being No-StopCode parahalting Instruction of SCMPDS for j being shiftable parahalting Instruction of SCMPDS holds (IExec ((i ';' j),P,s)) . a = (Exec (j,(Exec (i,s)))) . a proof let a be Int_position; ::_thesis: for P being Instruction-Sequence of SCMPDS for s being 0 -started State of SCMPDS for i being No-StopCode parahalting Instruction of SCMPDS for j being shiftable parahalting Instruction of SCMPDS holds (IExec ((i ';' j),P,s)) . a = (Exec (j,(Exec (i,s)))) . a let P be Instruction-Sequence of SCMPDS; ::_thesis: for s being 0 -started State of SCMPDS for i being No-StopCode parahalting Instruction of SCMPDS for j being shiftable parahalting Instruction of SCMPDS holds (IExec ((i ';' j),P,s)) . a = (Exec (j,(Exec (i,s)))) . a let s be 0 -started State of SCMPDS; ::_thesis: for i being No-StopCode parahalting Instruction of SCMPDS for j being shiftable parahalting Instruction of SCMPDS holds (IExec ((i ';' j),P,s)) . a = (Exec (j,(Exec (i,s)))) . a let i be No-StopCode parahalting Instruction of SCMPDS; ::_thesis: for j being shiftable parahalting Instruction of SCMPDS holds (IExec ((i ';' j),P,s)) . a = (Exec (j,(Exec (i,s)))) . a let j be shiftable parahalting Instruction of SCMPDS; ::_thesis: (IExec ((i ';' j),P,s)) . a = (Exec (j,(Exec (i,s)))) . a set Mi = Load i; thus (IExec ((i ';' j),P,s)) . a = (IExec (((Load i) ';' j),P,s)) . a .= (Exec (j,(IExec ((Load i),P,s)))) . a by Th41 .= (Exec (j,(Exec (i,s)))) . a by Th40 ; ::_thesis: verum end;