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