:: by JingChao Chen

::

:: Received June 15, 1999

:: Copyright (c) 1999-2012 Association of Mizar Users

begin

set A = NAT ;

set D = SCM-Data-Loc ;

Lm1: (Stop SCMPDS) . 0 = halt SCMPDS

by AFINSQ_1:34;

Lm2: 0 in dom (Stop SCMPDS)

by COMPOS_1:3;

theorem Th11: :: SCMPDS_6:11

for i being Instruction of SCMPDS

for s being State of SCMPDS

for I being Program of SCMPDS

for P being Instruction-Sequence of SCMPDS holds CurInstr ((P +* (stop (i ';' I))),(Initialize s)) = i

for s being State of SCMPDS

for I being Program of SCMPDS

for P being Instruction-Sequence of SCMPDS holds CurInstr ((P +* (stop (i ';' I))),(Initialize s)) = i

proof end;

theorem Th12: :: SCMPDS_6:12

for s being State of SCMPDS

for m1, m2 being Element of NAT st IC s = m1 holds

ICplusConst (s,m2) = m1 + m2

for m1, m2 being Element of NAT st IC s = m1 holds

ICplusConst (s,m2) = m1 + m2

proof end;

theorem :: SCMPDS_6:15

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 parahalting shiftable Program of SCMPDS

for a being Int_position holds (IExec ((i ';' J),P,s)) . a = (IExec (J,P,(Initialize (Exec (i,s))))) . a

for s being 0 -started State of SCMPDS

for i being No-StopCode parahalting Instruction of SCMPDS

for J being parahalting shiftable Program of SCMPDS

for a being Int_position holds (IExec ((i ';' J),P,s)) . a = (IExec (J,P,(Initialize (Exec (i,s))))) . a

proof end;

registration

let n be Element of NAT ;

correctness

coherence

goto (n + 1) is No-StopCode ;

by SCMPDS_5:21;

correctness

coherence

goto (- (n + 1)) is No-StopCode ;

by SCMPDS_5:21;

end;
correctness

coherence

goto (n + 1) is No-StopCode ;

by SCMPDS_5:21;

correctness

coherence

goto (- (n + 1)) is No-StopCode ;

by SCMPDS_5:21;

registration

let n be Element of NAT ;

correctness

coherence

Goto (n + 1) is halt-free ;

;

correctness

coherence

Goto (- (n + 1)) is halt-free ;

;

end;
correctness

coherence

Goto (n + 1) is halt-free ;

;

correctness

coherence

Goto (- (n + 1)) is halt-free ;

;

begin

definition

let I be Program of SCMPDS;

let s be State of SCMPDS;

let P be Instruction-Sequence of SCMPDS;

end;
let s be State of SCMPDS;

let P be Instruction-Sequence of SCMPDS;

pred I is_closed_on s,P means :Def2: :: SCMPDS_6:def 2

for k being Element of NAT holds IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom (stop I);

for k being Element of NAT holds IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom (stop I);

:: deftheorem Def2 defines is_closed_on SCMPDS_6:def 2 :

for I being Program of SCMPDS

for s being State of SCMPDS

for P being Instruction-Sequence of SCMPDS holds

( I is_closed_on s,P iff for k being Element of NAT holds IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom (stop I) );

for I being Program of SCMPDS

for s being State of SCMPDS

for P being Instruction-Sequence of SCMPDS holds

( I is_closed_on s,P iff for k being Element of NAT holds IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom (stop I) );

:: deftheorem Def3 defines is_halting_on SCMPDS_6:def 3 :

for I being Program of SCMPDS

for s being State of SCMPDS

for P being Instruction-Sequence of SCMPDS holds

( I is_halting_on s,P iff P +* (stop I) halts_on Initialize s );

for I being Program of SCMPDS

for s being State of SCMPDS

for P being Instruction-Sequence of SCMPDS holds

( I is_halting_on s,P iff P +* (stop I) halts_on Initialize s );

theorem Th20: :: SCMPDS_6:20

for I being Program of SCMPDS holds

( I is paraclosed iff for s being State of SCMPDS

for P being Instruction-Sequence of SCMPDS holds I is_closed_on s,P )

( I is paraclosed iff for s being State of SCMPDS

for P being Instruction-Sequence of SCMPDS holds I is_closed_on s,P )

proof end;

theorem Th21: :: SCMPDS_6:21

for I being Program of SCMPDS holds

( I is parahalting iff for s being State of SCMPDS

for P being Instruction-Sequence of SCMPDS holds I is_halting_on s,P )

( I is parahalting iff for s being State of SCMPDS

for P being Instruction-Sequence of SCMPDS holds I is_halting_on s,P )

proof end;

theorem Th22: :: SCMPDS_6:22

for P1, P2 being Instruction-Sequence of SCMPDS

for s1, s2 being State of SCMPDS

for I being Program of SCMPDS st DataPart s1 = DataPart s2 & I is_closed_on s1,P1 holds

I is_closed_on s2,P2

for s1, s2 being State of SCMPDS

for I being Program of SCMPDS st DataPart s1 = DataPart s2 & I is_closed_on s1,P1 holds

I is_closed_on s2,P2

proof end;

theorem :: SCMPDS_6:23

for P1, P2 being Instruction-Sequence of SCMPDS

for s1, s2 being State of SCMPDS

for I being Program of SCMPDS st DataPart s1 = DataPart s2 & I is_closed_on s1,P1 & I is_halting_on s1,P1 holds

( I is_closed_on s2,P2 & I is_halting_on s2,P2 )

for s1, s2 being State of SCMPDS

for I being Program of SCMPDS st DataPart s1 = DataPart s2 & I is_closed_on s1,P1 & I is_halting_on s1,P1 holds

( I is_closed_on s2,P2 & I is_halting_on s2,P2 )

proof end;

theorem Th24: :: SCMPDS_6:24

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I, J being Program of SCMPDS holds

( I is_closed_on s,P iff I is_closed_on Initialize s,P +* J )

for s being State of SCMPDS

for I, J being Program of SCMPDS holds

( I is_closed_on s,P iff I is_closed_on Initialize s,P +* J )

proof end;

theorem Th25: :: SCMPDS_6:25

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I, J being Program of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds

( ( for k being Element of NAT st k <= LifeSpan ((P +* (stop I)),s) holds

IC (Comput ((P +* (stop I)),s,k)) = IC (Comput ((P +* (stop (I ';' J))),s,k)) ) & DataPart (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = DataPart (Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),s)))) )

for s being 0 -started State of SCMPDS

for I, J being Program of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds

( ( for k being Element of NAT st k <= LifeSpan ((P +* (stop I)),s) holds

IC (Comput ((P +* (stop I)),s,k)) = IC (Comput ((P +* (stop (I ';' J))),s,k)) ) & DataPart (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = DataPart (Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),s)))) )

proof end;

theorem Th26: :: SCMPDS_6:26

for s being State of SCMPDS

for P being Instruction-Sequence of SCMPDS

for I being Program of SCMPDS

for k being Element of NAT st I is_closed_on s,P & I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),(Initialize s)) holds

IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom I

for P being Instruction-Sequence of SCMPDS

for I being Program of SCMPDS

for k being Element of NAT st I is_closed_on s,P & I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),(Initialize s)) holds

IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom I

proof end;

theorem Th27: :: SCMPDS_6:27

for P being Instruction-Sequence of SCMPDS

for I, J being Program of SCMPDS

for s being 0 -started State of SCMPDS

for k being Element of NAT st I is_closed_on s,P & I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),s) holds

CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),s,k))) = CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,k)))

for I, J being Program of SCMPDS

for s being 0 -started State of SCMPDS

for k being Element of NAT st I is_closed_on s,P & I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),s) holds

CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),s,k))) = CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,k)))

proof end;

theorem Th28: :: SCMPDS_6:28

for P being Instruction-Sequence of SCMPDS

for I being halt-free Program of SCMPDS

for s being State of SCMPDS

for k being Element of NAT st I is_closed_on s,P & I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),(Initialize s)) holds

CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k))) <> halt SCMPDS

for I being halt-free Program of SCMPDS

for s being State of SCMPDS

for k being Element of NAT st I is_closed_on s,P & I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),(Initialize s)) holds

CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k))) <> halt SCMPDS

proof end;

theorem Th29: :: SCMPDS_6:29

for P being Instruction-Sequence of SCMPDS

for I being halt-free Program of SCMPDS

for s being State of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds

IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I

for I being halt-free Program of SCMPDS

for s being State of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds

IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I

proof end;

Lm3: for P being Instruction-Sequence of SCMPDS

for I being halt-free Program of SCMPDS

for J being Program of SCMPDS

for s being 0 -started State of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds

( IC (Comput ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + 1))) = ((card I) + (card J)) + 1 & DataPart (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = DataPart (Comput ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + 1))) & ( for k being Element of NAT st k <= LifeSpan ((P +* (stop I)),s) holds

CurInstr ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(Comput ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s,k))) <> halt SCMPDS ) & IC (Comput ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s,(LifeSpan ((P +* (stop I)),s)))) = card I & P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)) halts_on s & LifeSpan ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),s) = (LifeSpan ((P +* (stop I)),s)) + 1 )

proof end;

theorem Th30: :: SCMPDS_6:30

for P being Instruction-Sequence of SCMPDS

for I, J being Program of SCMPDS

for s being 0 -started State of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds

( (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s,P & (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s,P )

for I, J being Program of SCMPDS

for s being 0 -started State of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds

( (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s,P & (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s,P )

proof end;

theorem Th31: :: SCMPDS_6:31

for s2 being State of SCMPDS

for P1, P2 being Instruction-Sequence of SCMPDS

for s1 being 0 -started State of SCMPDS

for I being shiftable Program of SCMPDS st stop I c= P1 & I is_closed_on s1,P1 holds

for n being Element of NAT st Shift ((stop I),n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds

for i being Element of NAT holds

( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )

for P1, P2 being Instruction-Sequence of SCMPDS

for s1 being 0 -started State of SCMPDS

for I being shiftable Program of SCMPDS st stop I c= P1 & I is_closed_on s1,P1 holds

for n being Element of NAT st Shift ((stop I),n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds

for i being Element of NAT holds

( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )

proof end;

theorem Th32: :: SCMPDS_6:32

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being halt-free Program of SCMPDS

for J being Program of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds

IC (IExec (((I ';' (Goto ((card J) + 1))) ';' J),P,s)) = ((card I) + (card J)) + 1

for s being 0 -started State of SCMPDS

for I being halt-free Program of SCMPDS

for J being Program of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds

IC (IExec (((I ';' (Goto ((card J) + 1))) ';' J),P,s)) = ((card I) + (card J)) + 1

proof end;

theorem Th33: :: SCMPDS_6:33

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being halt-free Program of SCMPDS

for J being Program of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds

IExec (((I ';' (Goto ((card J) + 1))) ';' J),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 1),SCMPDS))

for s being 0 -started State of SCMPDS

for I being halt-free Program of SCMPDS

for J being Program of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds

IExec (((I ';' (Goto ((card J) + 1))) ';' J),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 1),SCMPDS))

proof end;

theorem Th34: :: SCMPDS_6:34

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being halt-free Program of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds

IC (IExec (I,P,(Initialize s))) = card I

for s being State of SCMPDS

for I being halt-free Program of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds

IC (IExec (I,P,(Initialize s))) = card I

proof end;

begin

definition

let a be Int_position;

let k be Integer;

let I, J be Program of SCMPDS;

((((a,k) <>0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J is Program of SCMPDS ;

((((a,k) <=0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J is Program of SCMPDS ;

((((a,k) >=0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J is Program of SCMPDS ;

end;
let k be Integer;

let I, J be Program of SCMPDS;

func if=0 (a,k,I,J) -> Program of SCMPDS equals :: SCMPDS_6:def 4

((((a,k) <>0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J;

coherence ((((a,k) <>0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J;

((((a,k) <>0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J is Program of SCMPDS ;

func if>0 (a,k,I,J) -> Program of SCMPDS equals :: SCMPDS_6:def 5

((((a,k) <=0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J;

coherence ((((a,k) <=0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J;

((((a,k) <=0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J is Program of SCMPDS ;

func if<0 (a,k,I,J) -> Program of SCMPDS equals :: SCMPDS_6:def 6

((((a,k) >=0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J;

coherence ((((a,k) >=0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J;

((((a,k) >=0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J is Program of SCMPDS ;

:: deftheorem defines if=0 SCMPDS_6:def 4 :

for a being Int_position

for k being Integer

for I, J being Program of SCMPDS holds if=0 (a,k,I,J) = ((((a,k) <>0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J;

for a being Int_position

for k being Integer

for I, J being Program of SCMPDS holds if=0 (a,k,I,J) = ((((a,k) <>0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J;

:: deftheorem defines if>0 SCMPDS_6:def 5 :

for a being Int_position

for k being Integer

for I, J being Program of SCMPDS holds if>0 (a,k,I,J) = ((((a,k) <=0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J;

for a being Int_position

for k being Integer

for I, J being Program of SCMPDS holds if>0 (a,k,I,J) = ((((a,k) <=0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J;

:: deftheorem defines if<0 SCMPDS_6:def 6 :

for a being Int_position

for k being Integer

for I, J being Program of SCMPDS holds if<0 (a,k,I,J) = ((((a,k) >=0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J;

for a being Int_position

for k being Integer

for I, J being Program of SCMPDS holds if<0 (a,k,I,J) = ((((a,k) >=0_goto ((card I) + 2)) ';' I) ';' (Goto ((card J) + 1))) ';' J;

definition

let a be Int_position;

let k be Integer;

let I be Program of SCMPDS;

((a,k) <>0_goto ((card I) + 1)) ';' I is Program of SCMPDS ;

(((a,k) <>0_goto 2) ';' (goto ((card I) + 1))) ';' I is Program of SCMPDS ;

((a,k) <=0_goto ((card I) + 1)) ';' I is Program of SCMPDS ;

(((a,k) <=0_goto 2) ';' (goto ((card I) + 1))) ';' I is Program of SCMPDS ;

((a,k) >=0_goto ((card I) + 1)) ';' I is Program of SCMPDS ;

(((a,k) >=0_goto 2) ';' (goto ((card I) + 1))) ';' I is Program of SCMPDS ;

end;
let k be Integer;

let I be Program of SCMPDS;

func if=0 (a,k,I) -> Program of SCMPDS equals :: SCMPDS_6:def 7

((a,k) <>0_goto ((card I) + 1)) ';' I;

coherence ((a,k) <>0_goto ((card I) + 1)) ';' I;

((a,k) <>0_goto ((card I) + 1)) ';' I is Program of SCMPDS ;

func if<>0 (a,k,I) -> Program of SCMPDS equals :: SCMPDS_6:def 8

(((a,k) <>0_goto 2) ';' (goto ((card I) + 1))) ';' I;

coherence (((a,k) <>0_goto 2) ';' (goto ((card I) + 1))) ';' I;

(((a,k) <>0_goto 2) ';' (goto ((card I) + 1))) ';' I is Program of SCMPDS ;

func if>0 (a,k,I) -> Program of SCMPDS equals :: SCMPDS_6:def 9

((a,k) <=0_goto ((card I) + 1)) ';' I;

coherence ((a,k) <=0_goto ((card I) + 1)) ';' I;

((a,k) <=0_goto ((card I) + 1)) ';' I is Program of SCMPDS ;

func if<=0 (a,k,I) -> Program of SCMPDS equals :: SCMPDS_6:def 10

(((a,k) <=0_goto 2) ';' (goto ((card I) + 1))) ';' I;

coherence (((a,k) <=0_goto 2) ';' (goto ((card I) + 1))) ';' I;

(((a,k) <=0_goto 2) ';' (goto ((card I) + 1))) ';' I is Program of SCMPDS ;

func if<0 (a,k,I) -> Program of SCMPDS equals :: SCMPDS_6:def 11

((a,k) >=0_goto ((card I) + 1)) ';' I;

coherence ((a,k) >=0_goto ((card I) + 1)) ';' I;

((a,k) >=0_goto ((card I) + 1)) ';' I is Program of SCMPDS ;

func if>=0 (a,k,I) -> Program of SCMPDS equals :: SCMPDS_6:def 12

(((a,k) >=0_goto 2) ';' (goto ((card I) + 1))) ';' I;

coherence (((a,k) >=0_goto 2) ';' (goto ((card I) + 1))) ';' I;

(((a,k) >=0_goto 2) ';' (goto ((card I) + 1))) ';' I is Program of SCMPDS ;

:: deftheorem defines if=0 SCMPDS_6:def 7 :

for a being Int_position

for k being Integer

for I being Program of SCMPDS holds if=0 (a,k,I) = ((a,k) <>0_goto ((card I) + 1)) ';' I;

for a being Int_position

for k being Integer

for I being Program of SCMPDS holds if=0 (a,k,I) = ((a,k) <>0_goto ((card I) + 1)) ';' I;

:: deftheorem defines if<>0 SCMPDS_6:def 8 :

for a being Int_position

for k being Integer

for I being Program of SCMPDS holds if<>0 (a,k,I) = (((a,k) <>0_goto 2) ';' (goto ((card I) + 1))) ';' I;

for a being Int_position

for k being Integer

for I being Program of SCMPDS holds if<>0 (a,k,I) = (((a,k) <>0_goto 2) ';' (goto ((card I) + 1))) ';' I;

:: deftheorem defines if>0 SCMPDS_6:def 9 :

for a being Int_position

for k being Integer

for I being Program of SCMPDS holds if>0 (a,k,I) = ((a,k) <=0_goto ((card I) + 1)) ';' I;

for a being Int_position

for k being Integer

for I being Program of SCMPDS holds if>0 (a,k,I) = ((a,k) <=0_goto ((card I) + 1)) ';' I;

:: deftheorem defines if<=0 SCMPDS_6:def 10 :

for a being Int_position

for k being Integer

for I being Program of SCMPDS holds if<=0 (a,k,I) = (((a,k) <=0_goto 2) ';' (goto ((card I) + 1))) ';' I;

for a being Int_position

for k being Integer

for I being Program of SCMPDS holds if<=0 (a,k,I) = (((a,k) <=0_goto 2) ';' (goto ((card I) + 1))) ';' I;

:: deftheorem defines if<0 SCMPDS_6:def 11 :

for a being Int_position

for k being Integer

for I being Program of SCMPDS holds if<0 (a,k,I) = ((a,k) >=0_goto ((card I) + 1)) ';' I;

for a being Int_position

for k being Integer

for I being Program of SCMPDS holds if<0 (a,k,I) = ((a,k) >=0_goto ((card I) + 1)) ';' I;

:: deftheorem defines if>=0 SCMPDS_6:def 12 :

for a being Int_position

for k being Integer

for I being Program of SCMPDS holds if>=0 (a,k,I) = (((a,k) >=0_goto 2) ';' (goto ((card I) + 1))) ';' I;

for a being Int_position

for k being Integer

for I being Program of SCMPDS holds if>=0 (a,k,I) = (((a,k) >=0_goto 2) ';' (goto ((card I) + 1))) ';' I;

Lm4: for n being Element of NAT

for i being Instruction of SCMPDS

for I, J being Program of SCMPDS holds card (((i ';' I) ';' (Goto n)) ';' J) = ((card I) + (card J)) + 2

proof end;

begin

theorem :: SCMPDS_6:35

theorem :: SCMPDS_6:36

for a being Int_position

for k1 being Integer

for I, J being Program of SCMPDS holds

( 0 in dom (if=0 (a,k1,I,J)) & 1 in dom (if=0 (a,k1,I,J)) )

for k1 being Integer

for I, J being Program of SCMPDS holds

( 0 in dom (if=0 (a,k1,I,J)) & 1 in dom (if=0 (a,k1,I,J)) )

proof end;

Lm5: for i being Instruction of SCMPDS

for I, J, K being Program of SCMPDS holds (((i ';' I) ';' J) ';' K) . 0 = i

proof end;

theorem :: SCMPDS_6:37

Lm6: for i being Instruction of SCMPDS

for I being Program of SCMPDS

for P being Instruction-Sequence of SCMPDS holds Shift ((stop I),1) c= P +* (stop (i ';' I))

proof end;

Lm7: for i, j being Instruction of SCMPDS

for I being Program of SCMPDS

for P being Instruction-Sequence of SCMPDS holds Shift ((stop I),2) c= P +* (stop ((i ';' j) ';' I))

proof end;

theorem Th38: :: SCMPDS_6:38

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I, J being shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) = 0 & I is_closed_on s,P & I is_halting_on s,P holds

( if=0 (a,k1,I,J) is_closed_on s,P & if=0 (a,k1,I,J) is_halting_on s,P )

for s being 0 -started State of SCMPDS

for I, J being shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) = 0 & I is_closed_on s,P & I is_halting_on s,P holds

( if=0 (a,k1,I,J) is_closed_on s,P & if=0 (a,k1,I,J) is_halting_on s,P )

proof end;

theorem Th39: :: SCMPDS_6:39

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of SCMPDS

for J being shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <> 0 & J is_closed_on s,P & J is_halting_on s,P holds

( if=0 (a,k1,I,J) is_closed_on s,P & if=0 (a,k1,I,J) is_halting_on s,P )

for s being State of SCMPDS

for I being Program of SCMPDS

for J being shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <> 0 & J is_closed_on s,P & J is_halting_on s,P holds

( if=0 (a,k1,I,J) is_closed_on s,P & if=0 (a,k1,I,J) is_halting_on s,P )

proof end;

theorem Th40: :: SCMPDS_6:40

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for J being shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) = 0 & I is_closed_on s,P & I is_halting_on s,P holds

IExec ((if=0 (a,k1,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS))

for s being 0 -started State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for J being shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) = 0 & I is_closed_on s,P & I is_halting_on s,P holds

IExec ((if=0 (a,k1,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS))

proof end;

theorem Th41: :: SCMPDS_6:41

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of SCMPDS

for J being halt-free shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <> 0 & J is_closed_on s,P & J is_halting_on s,P holds

IExec ((if=0 (a,k1,I,J)),P,(Initialize s)) = (IExec (J,P,(Initialize s))) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS))

for s being State of SCMPDS

for I being Program of SCMPDS

for J being halt-free shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <> 0 & J is_closed_on s,P & J is_halting_on s,P holds

IExec ((if=0 (a,k1,I,J)),P,(Initialize s)) = (IExec (J,P,(Initialize s))) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS))

proof end;

registration

let I, J be parahalting shiftable Program of SCMPDS;

let a be Int_position;

let k1 be Integer;

correctness

coherence

( if=0 (a,k1,I,J) is shiftable & if=0 (a,k1,I,J) is parahalting );

end;
let a be Int_position;

let k1 be Integer;

correctness

coherence

( if=0 (a,k1,I,J) is shiftable & if=0 (a,k1,I,J) is parahalting );

proof end;

registration

let I, J be halt-free Program of SCMPDS;

let a be Int_position;

let k1 be Integer;

coherence

if=0 (a,k1,I,J) is halt-free ;

end;
let a be Int_position;

let k1 be Integer;

coherence

if=0 (a,k1,I,J) is halt-free ;

theorem :: SCMPDS_6:42

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I, J being halt-free parahalting shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer holds IC (IExec ((if=0 (a,k1,I,J)),P,s)) = ((card I) + (card J)) + 2

for s being 0 -started State of SCMPDS

for I, J being halt-free parahalting shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer holds IC (IExec ((if=0 (a,k1,I,J)),P,s)) = ((card I) + (card J)) + 2

proof end;

theorem :: SCMPDS_6:43

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being halt-free parahalting shiftable Program of SCMPDS

for J being shiftable Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) = 0 holds

(IExec ((if=0 (a,k1,I,J)),P,s)) . b = (IExec (I,P,s)) . b

for s being 0 -started State of SCMPDS

for I being halt-free parahalting shiftable Program of SCMPDS

for J being shiftable Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) = 0 holds

(IExec ((if=0 (a,k1,I,J)),P,s)) . b = (IExec (I,P,s)) . b

proof end;

theorem :: SCMPDS_6:44

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of SCMPDS

for J being halt-free parahalting shiftable Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <> 0 holds

(IExec ((if=0 (a,k1,I,J)),P,(Initialize s))) . b = (IExec (J,P,(Initialize s))) . b

for s being State of SCMPDS

for I being Program of SCMPDS

for J being halt-free parahalting shiftable Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <> 0 holds

(IExec ((if=0 (a,k1,I,J)),P,(Initialize s))) . b = (IExec (J,P,(Initialize s))) . b

proof end;

begin

theorem :: SCMPDS_6:45

theorem :: SCMPDS_6:46

for a being Int_position

for k1 being Integer

for I being Program of SCMPDS holds 0 in dom (if=0 (a,k1,I))

for k1 being Integer

for I being Program of SCMPDS holds 0 in dom (if=0 (a,k1,I))

proof end;

theorem :: SCMPDS_6:47

theorem Th48: :: SCMPDS_6:48

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) = 0 & I is_closed_on s,P & I is_halting_on s,P holds

( if=0 (a,k1,I) is_closed_on s,P & if=0 (a,k1,I) is_halting_on s,P )

for s being State of SCMPDS

for I being shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) = 0 & I is_closed_on s,P & I is_halting_on s,P holds

( if=0 (a,k1,I) is_closed_on s,P & if=0 (a,k1,I) is_halting_on s,P )

proof end;

theorem Th49: :: SCMPDS_6:49

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <> 0 holds

( if=0 (a,k1,I) is_closed_on s,P & if=0 (a,k1,I) is_halting_on s,P )

for s being State of SCMPDS

for I being Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <> 0 holds

( if=0 (a,k1,I) is_closed_on s,P & if=0 (a,k1,I) is_halting_on s,P )

proof end;

theorem Th50: :: SCMPDS_6:50

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) = 0 & I is_closed_on s,P & I is_halting_on s,P holds

IExec ((if=0 (a,k1,I)),P,(Initialize s)) = (IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 1),SCMPDS))

for s being State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) = 0 & I is_closed_on s,P & I is_halting_on s,P holds

IExec ((if=0 (a,k1,I)),P,(Initialize s)) = (IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 1),SCMPDS))

proof end;

theorem Th51: :: SCMPDS_6:51

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <> 0 holds

IExec ((if=0 (a,k1,I)),P,(Initialize s)) = s +* (Start-At (((card I) + 1),SCMPDS))

for s being State of SCMPDS

for I being Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <> 0 holds

IExec ((if=0 (a,k1,I)),P,(Initialize s)) = s +* (Start-At (((card I) + 1),SCMPDS))

proof end;

registration

let I be parahalting shiftable Program of SCMPDS;

let a be Int_position;

let k1 be Integer;

correctness

coherence

( if=0 (a,k1,I) is shiftable & if=0 (a,k1,I) is parahalting );

end;
let a be Int_position;

let k1 be Integer;

correctness

coherence

( if=0 (a,k1,I) is shiftable & if=0 (a,k1,I) is parahalting );

proof end;

registration

let I be halt-free Program of SCMPDS;

let a be Int_position;

let k1 be Integer;

coherence

if=0 (a,k1,I) is halt-free ;

end;
let a be Int_position;

let k1 be Integer;

coherence

if=0 (a,k1,I) is halt-free ;

theorem :: SCMPDS_6:52

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being halt-free parahalting shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer holds IC (IExec ((if=0 (a,k1,I)),P,s)) = (card I) + 1

for s being 0 -started State of SCMPDS

for I being halt-free parahalting shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer holds IC (IExec ((if=0 (a,k1,I)),P,s)) = (card I) + 1

proof end;

theorem :: SCMPDS_6:53

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being halt-free parahalting shiftable Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) = 0 holds

(IExec ((if=0 (a,k1,I)),P,(Initialize s))) . b = (IExec (I,P,(Initialize s))) . b

for s being State of SCMPDS

for I being halt-free parahalting shiftable Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) = 0 holds

(IExec ((if=0 (a,k1,I)),P,(Initialize s))) . b = (IExec (I,P,(Initialize s))) . b

proof end;

theorem :: SCMPDS_6:54

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <> 0 holds

(IExec ((if=0 (a,k1,I)),P,(Initialize s))) . b = s . b

for s being State of SCMPDS

for I being Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <> 0 holds

(IExec ((if=0 (a,k1,I)),P,(Initialize s))) . b = s . b

proof end;

Lm8: for i, j being Instruction of SCMPDS

for I being Program of SCMPDS holds card ((i ';' j) ';' I) = (card I) + 2

proof end;

begin

theorem :: SCMPDS_6:55

Lm9: for i, j being Instruction of SCMPDS

for I being Program of SCMPDS holds

( 0 in dom ((i ';' j) ';' I) & 1 in dom ((i ';' j) ';' I) )

proof end;

theorem :: SCMPDS_6:56

Lm10: for i, j being Instruction of SCMPDS

for I being Program of SCMPDS holds

( ((i ';' j) ';' I) . 0 = i & ((i ';' j) ';' I) . 1 = j )

proof end;

theorem :: SCMPDS_6:57

theorem Th58: :: SCMPDS_6:58

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <> 0 & I is_closed_on s,P & I is_halting_on s,P holds

( if<>0 (a,k1,I) is_closed_on s,P & if<>0 (a,k1,I) is_halting_on s,P )

for s being State of SCMPDS

for I being shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <> 0 & I is_closed_on s,P & I is_halting_on s,P holds

( if<>0 (a,k1,I) is_closed_on s,P & if<>0 (a,k1,I) is_halting_on s,P )

proof end;

theorem Th59: :: SCMPDS_6:59

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) = 0 holds

( if<>0 (a,k1,I) is_closed_on s,P & if<>0 (a,k1,I) is_halting_on s,P )

for s being State of SCMPDS

for I being Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) = 0 holds

( if<>0 (a,k1,I) is_closed_on s,P & if<>0 (a,k1,I) is_halting_on s,P )

proof end;

theorem Th60: :: SCMPDS_6:60

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <> 0 & I is_closed_on s,P & I is_halting_on s,P holds

IExec ((if<>0 (a,k1,I)),P,(Initialize s)) = (IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 2),SCMPDS))

for s being State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <> 0 & I is_closed_on s,P & I is_halting_on s,P holds

IExec ((if<>0 (a,k1,I)),P,(Initialize s)) = (IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 2),SCMPDS))

proof end;

theorem Th61: :: SCMPDS_6:61

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) = 0 holds

IExec ((if<>0 (a,k1,I)),P,(Initialize s)) = s +* (Start-At (((card I) + 2),SCMPDS))

for s being State of SCMPDS

for I being Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) = 0 holds

IExec ((if<>0 (a,k1,I)),P,(Initialize s)) = s +* (Start-At (((card I) + 2),SCMPDS))

proof end;

registration

let I be parahalting shiftable Program of SCMPDS;

let a be Int_position;

let k1 be Integer;

correctness

coherence

( if<>0 (a,k1,I) is shiftable & if<>0 (a,k1,I) is parahalting );

end;
let a be Int_position;

let k1 be Integer;

correctness

coherence

( if<>0 (a,k1,I) is shiftable & if<>0 (a,k1,I) is parahalting );

proof end;

registration

let I be halt-free Program of SCMPDS;

let a be Int_position;

let k1 be Integer;

coherence

if<>0 (a,k1,I) is halt-free ;

end;
let a be Int_position;

let k1 be Integer;

coherence

if<>0 (a,k1,I) is halt-free ;

theorem :: SCMPDS_6:62

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being halt-free parahalting shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer holds IC (IExec ((if<>0 (a,k1,I)),P,(Initialize s))) = (card I) + 2

for s being State of SCMPDS

for I being halt-free parahalting shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer holds IC (IExec ((if<>0 (a,k1,I)),P,(Initialize s))) = (card I) + 2

proof end;

theorem :: SCMPDS_6:63

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being halt-free parahalting shiftable Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <> 0 holds

(IExec ((if<>0 (a,k1,I)),P,(Initialize s))) . b = (IExec (I,P,(Initialize s))) . b

for s being State of SCMPDS

for I being halt-free parahalting shiftable Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <> 0 holds

(IExec ((if<>0 (a,k1,I)),P,(Initialize s))) . b = (IExec (I,P,(Initialize s))) . b

proof end;

theorem :: SCMPDS_6:64

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) = 0 holds

(IExec ((if<>0 (a,k1,I)),P,(Initialize s))) . b = s . b

for s being State of SCMPDS

for I being Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) = 0 holds

(IExec ((if<>0 (a,k1,I)),P,(Initialize s))) . b = s . b

proof end;

begin

theorem :: SCMPDS_6:65

theorem :: SCMPDS_6:66

for a being Int_position

for k1 being Integer

for I, J being Program of SCMPDS holds

( 0 in dom (if>0 (a,k1,I,J)) & 1 in dom (if>0 (a,k1,I,J)) )

for k1 being Integer

for I, J being Program of SCMPDS holds

( 0 in dom (if>0 (a,k1,I,J)) & 1 in dom (if>0 (a,k1,I,J)) )

proof end;

theorem :: SCMPDS_6:67

theorem Th68: :: SCMPDS_6:68

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I, J being shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) > 0 & I is_closed_on s,P & I is_halting_on s,P holds

( if>0 (a,k1,I,J) is_closed_on s,P & if>0 (a,k1,I,J) is_halting_on s,P )

for s being 0 -started State of SCMPDS

for I, J being shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) > 0 & I is_closed_on s,P & I is_halting_on s,P holds

( if>0 (a,k1,I,J) is_closed_on s,P & if>0 (a,k1,I,J) is_halting_on s,P )

proof end;

theorem Th69: :: SCMPDS_6:69

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of SCMPDS

for J being shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <= 0 & J is_closed_on s,P & J is_halting_on s,P holds

( if>0 (a,k1,I,J) is_closed_on s,P & if>0 (a,k1,I,J) is_halting_on s,P )

for s being State of SCMPDS

for I being Program of SCMPDS

for J being shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <= 0 & J is_closed_on s,P & J is_halting_on s,P holds

( if>0 (a,k1,I,J) is_closed_on s,P & if>0 (a,k1,I,J) is_halting_on s,P )

proof end;

theorem Th70: :: SCMPDS_6:70

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for J being shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) > 0 & I is_closed_on s,P & I is_halting_on s,P holds

IExec ((if>0 (a,k1,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS))

for s being 0 -started State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for J being shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) > 0 & I is_closed_on s,P & I is_halting_on s,P holds

IExec ((if>0 (a,k1,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS))

proof end;

theorem Th71: :: SCMPDS_6:71

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being Program of SCMPDS

for J being halt-free shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <= 0 & J is_closed_on s,P & J is_halting_on s,P holds

IExec ((if>0 (a,k1,I,J)),P,s) = (IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS))

for s being 0 -started State of SCMPDS

for I being Program of SCMPDS

for J being halt-free shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <= 0 & J is_closed_on s,P & J is_halting_on s,P holds

IExec ((if>0 (a,k1,I,J)),P,s) = (IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS))

proof end;

registration

let I, J be parahalting shiftable Program of SCMPDS;

let a be Int_position;

let k1 be Integer;

correctness

coherence

( if>0 (a,k1,I,J) is shiftable & if>0 (a,k1,I,J) is parahalting );

end;
let a be Int_position;

let k1 be Integer;

correctness

coherence

( if>0 (a,k1,I,J) is shiftable & if>0 (a,k1,I,J) is parahalting );

proof end;

registration

let I, J be halt-free Program of SCMPDS;

let a be Int_position;

let k1 be Integer;

coherence

if>0 (a,k1,I,J) is halt-free ;

end;
let a be Int_position;

let k1 be Integer;

coherence

if>0 (a,k1,I,J) is halt-free ;

theorem :: SCMPDS_6:72

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I, J being halt-free parahalting shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer holds IC (IExec ((if>0 (a,k1,I,J)),P,s)) = ((card I) + (card J)) + 2

for s being 0 -started State of SCMPDS

for I, J being halt-free parahalting shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer holds IC (IExec ((if>0 (a,k1,I,J)),P,s)) = ((card I) + (card J)) + 2

proof end;

theorem :: SCMPDS_6:73

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being halt-free parahalting shiftable Program of SCMPDS

for J being shiftable Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) > 0 holds

(IExec ((if>0 (a,k1,I,J)),P,s)) . b = (IExec (I,P,s)) . b

for s being 0 -started State of SCMPDS

for I being halt-free parahalting shiftable Program of SCMPDS

for J being shiftable Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) > 0 holds

(IExec ((if>0 (a,k1,I,J)),P,s)) . b = (IExec (I,P,s)) . b

proof end;

theorem :: SCMPDS_6:74

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being Program of SCMPDS

for J being halt-free parahalting shiftable Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <= 0 holds

(IExec ((if>0 (a,k1,I,J)),P,s)) . b = (IExec (J,P,s)) . b

for s being 0 -started State of SCMPDS

for I being Program of SCMPDS

for J being halt-free parahalting shiftable Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <= 0 holds

(IExec ((if>0 (a,k1,I,J)),P,s)) . b = (IExec (J,P,s)) . b

proof end;

begin

theorem :: SCMPDS_6:75

theorem :: SCMPDS_6:76

for a being Int_position

for k1 being Integer

for I being Program of SCMPDS holds 0 in dom (if>0 (a,k1,I))

for k1 being Integer

for I being Program of SCMPDS holds 0 in dom (if>0 (a,k1,I))

proof end;

theorem :: SCMPDS_6:77

theorem Th78: :: SCMPDS_6:78

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) > 0 & I is_closed_on s,P & I is_halting_on s,P holds

( if>0 (a,k1,I) is_closed_on s,P & if>0 (a,k1,I) is_halting_on s,P )

for s being State of SCMPDS

for I being shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) > 0 & I is_closed_on s,P & I is_halting_on s,P holds

( if>0 (a,k1,I) is_closed_on s,P & if>0 (a,k1,I) is_halting_on s,P )

proof end;

theorem Th79: :: SCMPDS_6:79

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <= 0 holds

( if>0 (a,k1,I) is_closed_on s,P & if>0 (a,k1,I) is_halting_on s,P )

for s being State of SCMPDS

for I being Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <= 0 holds

( if>0 (a,k1,I) is_closed_on s,P & if>0 (a,k1,I) is_halting_on s,P )

proof end;

theorem Th80: :: SCMPDS_6:80

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) > 0 & I is_closed_on s,P & I is_halting_on s,P holds

IExec ((if>0 (a,k1,I)),P,(Initialize s)) = (IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 1),SCMPDS))

for s being State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) > 0 & I is_closed_on s,P & I is_halting_on s,P holds

IExec ((if>0 (a,k1,I)),P,(Initialize s)) = (IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 1),SCMPDS))

proof end;

theorem Th81: :: SCMPDS_6:81

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <= 0 holds

IExec ((if>0 (a,k1,I)),P,(Initialize s)) = s +* (Start-At (((card I) + 1),SCMPDS))

for s being State of SCMPDS

for I being Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <= 0 holds

IExec ((if>0 (a,k1,I)),P,(Initialize s)) = s +* (Start-At (((card I) + 1),SCMPDS))

proof end;

registration

let I be parahalting shiftable Program of SCMPDS;

let a be Int_position;

let k1 be Integer;

correctness

coherence

( if>0 (a,k1,I) is shiftable & if>0 (a,k1,I) is parahalting );

end;
let a be Int_position;

let k1 be Integer;

correctness

coherence

( if>0 (a,k1,I) is shiftable & if>0 (a,k1,I) is parahalting );

proof end;

registration

let I be halt-free Program of SCMPDS;

let a be Int_position;

let k1 be Integer;

coherence

if>0 (a,k1,I) is halt-free ;

end;
let a be Int_position;

let k1 be Integer;

coherence

if>0 (a,k1,I) is halt-free ;

theorem :: SCMPDS_6:82

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being halt-free parahalting shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer holds IC (IExec ((if>0 (a,k1,I)),P,s)) = (card I) + 1

for s being 0 -started State of SCMPDS

for I being halt-free parahalting shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer holds IC (IExec ((if>0 (a,k1,I)),P,s)) = (card I) + 1

proof end;

theorem :: SCMPDS_6:83

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being halt-free parahalting shiftable Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) > 0 holds

(IExec ((if>0 (a,k1,I)),P,(Initialize s))) . b = (IExec (I,P,(Initialize s))) . b

for s being State of SCMPDS

for I being halt-free parahalting shiftable Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) > 0 holds

(IExec ((if>0 (a,k1,I)),P,(Initialize s))) . b = (IExec (I,P,(Initialize s))) . b

proof end;

theorem :: SCMPDS_6:84

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <= 0 holds

(IExec ((if>0 (a,k1,I)),P,(Initialize s))) . b = s . b

for s being State of SCMPDS

for I being Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <= 0 holds

(IExec ((if>0 (a,k1,I)),P,(Initialize s))) . b = s . b

proof end;

begin

theorem :: SCMPDS_6:85

theorem :: SCMPDS_6:86

theorem :: SCMPDS_6:87

theorem Th88: :: SCMPDS_6:88

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <= 0 & I is_closed_on s,P & I is_halting_on s,P holds

( if<=0 (a,k1,I) is_closed_on s,P & if<=0 (a,k1,I) is_halting_on s,P )

for s being State of SCMPDS

for I being shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <= 0 & I is_closed_on s,P & I is_halting_on s,P holds

( if<=0 (a,k1,I) is_closed_on s,P & if<=0 (a,k1,I) is_halting_on s,P )

proof end;

theorem Th89: :: SCMPDS_6:89

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) > 0 holds

( if<=0 (a,k1,I) is_closed_on s,P & if<=0 (a,k1,I) is_halting_on s,P )

for s being State of SCMPDS

for I being Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) > 0 holds

( if<=0 (a,k1,I) is_closed_on s,P & if<=0 (a,k1,I) is_halting_on s,P )

proof end;

theorem Th90: :: SCMPDS_6:90

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <= 0 & I is_closed_on s,P & I is_halting_on s,P holds

IExec ((if<=0 (a,k1,I)),P,(Initialize s)) = (IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 2),SCMPDS))

for s being State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <= 0 & I is_closed_on s,P & I is_halting_on s,P holds

IExec ((if<=0 (a,k1,I)),P,(Initialize s)) = (IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 2),SCMPDS))

proof end;

theorem Th91: :: SCMPDS_6:91

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) > 0 holds

IExec ((if<=0 (a,k1,I)),P,(Initialize s)) = s +* (Start-At (((card I) + 2),SCMPDS))

for s being State of SCMPDS

for I being Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) > 0 holds

IExec ((if<=0 (a,k1,I)),P,(Initialize s)) = s +* (Start-At (((card I) + 2),SCMPDS))

proof end;

registration

let I be parahalting shiftable Program of SCMPDS;

let a be Int_position;

let k1 be Integer;

correctness

coherence

( if<=0 (a,k1,I) is shiftable & if<=0 (a,k1,I) is parahalting );

end;
let a be Int_position;

let k1 be Integer;

correctness

coherence

( if<=0 (a,k1,I) is shiftable & if<=0 (a,k1,I) is parahalting );

proof end;

registration

let I be halt-free Program of SCMPDS;

let a be Int_position;

let k1 be Integer;

coherence

if<=0 (a,k1,I) is halt-free ;

end;
let a be Int_position;

let k1 be Integer;

coherence

if<=0 (a,k1,I) is halt-free ;

theorem :: SCMPDS_6:92

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being halt-free parahalting shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer holds IC (IExec ((if<=0 (a,k1,I)),P,s)) = (card I) + 2

for s being 0 -started State of SCMPDS

for I being halt-free parahalting shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer holds IC (IExec ((if<=0 (a,k1,I)),P,s)) = (card I) + 2

proof end;

theorem :: SCMPDS_6:93

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being halt-free parahalting shiftable Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <= 0 holds

(IExec ((if<=0 (a,k1,I)),P,(Initialize s))) . b = (IExec (I,P,(Initialize s))) . b

for s being State of SCMPDS

for I being halt-free parahalting shiftable Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) <= 0 holds

(IExec ((if<=0 (a,k1,I)),P,(Initialize s))) . b = (IExec (I,P,(Initialize s))) . b

proof end;

theorem :: SCMPDS_6:94

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) > 0 holds

(IExec ((if<=0 (a,k1,I)),P,(Initialize s))) . b = s . b

for s being State of SCMPDS

for I being Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) > 0 holds

(IExec ((if<=0 (a,k1,I)),P,(Initialize s))) . b = s . b

proof end;

begin

theorem :: SCMPDS_6:95

theorem :: SCMPDS_6:96

for a being Int_position

for k1 being Integer

for I, J being Program of SCMPDS holds

( 0 in dom (if<0 (a,k1,I,J)) & 1 in dom (if<0 (a,k1,I,J)) )

for k1 being Integer

for I, J being Program of SCMPDS holds

( 0 in dom (if<0 (a,k1,I,J)) & 1 in dom (if<0 (a,k1,I,J)) )

proof end;

theorem :: SCMPDS_6:97

theorem Th98: :: SCMPDS_6:98

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I, J being shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) < 0 & I is_closed_on s,P & I is_halting_on s,P holds

( if<0 (a,k1,I,J) is_closed_on s,P & if<0 (a,k1,I,J) is_halting_on s,P )

for s being 0 -started State of SCMPDS

for I, J being shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) < 0 & I is_closed_on s,P & I is_halting_on s,P holds

( if<0 (a,k1,I,J) is_closed_on s,P & if<0 (a,k1,I,J) is_halting_on s,P )

proof end;

theorem Th99: :: SCMPDS_6:99

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of SCMPDS

for J being shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) >= 0 & J is_closed_on s,P & J is_halting_on s,P holds

( if<0 (a,k1,I,J) is_closed_on s,P & if<0 (a,k1,I,J) is_halting_on s,P )

for s being State of SCMPDS

for I being Program of SCMPDS

for J being shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) >= 0 & J is_closed_on s,P & J is_halting_on s,P holds

( if<0 (a,k1,I,J) is_closed_on s,P & if<0 (a,k1,I,J) is_halting_on s,P )

proof end;

theorem Th100: :: SCMPDS_6:100

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for J being shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) < 0 & I is_closed_on s,P & I is_halting_on s,P holds

IExec ((if<0 (a,k1,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS))

for s being 0 -started State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for J being shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) < 0 & I is_closed_on s,P & I is_halting_on s,P holds

IExec ((if<0 (a,k1,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS))

proof end;

theorem Th101: :: SCMPDS_6:101

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of SCMPDS

for J being halt-free shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) >= 0 & J is_closed_on s,P & J is_halting_on s,P holds

IExec ((if<0 (a,k1,I,J)),P,(Initialize s)) = (IExec (J,P,(Initialize s))) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS))

for s being State of SCMPDS

for I being Program of SCMPDS

for J being halt-free shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) >= 0 & J is_closed_on s,P & J is_halting_on s,P holds

IExec ((if<0 (a,k1,I,J)),P,(Initialize s)) = (IExec (J,P,(Initialize s))) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS))

proof end;

registration

let I, J be parahalting shiftable Program of SCMPDS;

let a be Int_position;

let k1 be Integer;

correctness

coherence

( if<0 (a,k1,I,J) is shiftable & if<0 (a,k1,I,J) is parahalting );

end;
let a be Int_position;

let k1 be Integer;

correctness

coherence

( if<0 (a,k1,I,J) is shiftable & if<0 (a,k1,I,J) is parahalting );

proof end;

registration

let I, J be halt-free Program of SCMPDS;

let a be Int_position;

let k1 be Integer;

coherence

if<0 (a,k1,I,J) is halt-free ;

end;
let a be Int_position;

let k1 be Integer;

coherence

if<0 (a,k1,I,J) is halt-free ;

theorem :: SCMPDS_6:102

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I, J being halt-free parahalting shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer holds IC (IExec ((if<0 (a,k1,I,J)),P,s)) = ((card I) + (card J)) + 2

for s being 0 -started State of SCMPDS

for I, J being halt-free parahalting shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer holds IC (IExec ((if<0 (a,k1,I,J)),P,s)) = ((card I) + (card J)) + 2

proof end;

theorem :: SCMPDS_6:103

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being halt-free parahalting shiftable Program of SCMPDS

for J being shiftable Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) < 0 holds

(IExec ((if<0 (a,k1,I,J)),P,s)) . b = (IExec (I,P,s)) . b

for s being 0 -started State of SCMPDS

for I being halt-free parahalting shiftable Program of SCMPDS

for J being shiftable Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) < 0 holds

(IExec ((if<0 (a,k1,I,J)),P,s)) . b = (IExec (I,P,s)) . b

proof end;

theorem :: SCMPDS_6:104

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of SCMPDS

for J being halt-free parahalting shiftable Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) >= 0 holds

(IExec ((if<0 (a,k1,I,J)),P,(Initialize s))) . b = (IExec (J,P,(Initialize s))) . b

for s being State of SCMPDS

for I being Program of SCMPDS

for J being halt-free parahalting shiftable Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) >= 0 holds

(IExec ((if<0 (a,k1,I,J)),P,(Initialize s))) . b = (IExec (J,P,(Initialize s))) . b

proof end;

begin

theorem :: SCMPDS_6:105

theorem :: SCMPDS_6:106

for a being Int_position

for k1 being Integer

for I being Program of SCMPDS holds 0 in dom (if<0 (a,k1,I))

for k1 being Integer

for I being Program of SCMPDS holds 0 in dom (if<0 (a,k1,I))

proof end;

theorem :: SCMPDS_6:107

theorem Th108: :: SCMPDS_6:108

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) < 0 & I is_closed_on s,P & I is_halting_on s,P holds

( if<0 (a,k1,I) is_closed_on s,P & if<0 (a,k1,I) is_halting_on s,P )

for s being State of SCMPDS

for I being shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) < 0 & I is_closed_on s,P & I is_halting_on s,P holds

( if<0 (a,k1,I) is_closed_on s,P & if<0 (a,k1,I) is_halting_on s,P )

proof end;

theorem Th109: :: SCMPDS_6:109

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) >= 0 holds

( if<0 (a,k1,I) is_closed_on s,P & if<0 (a,k1,I) is_halting_on s,P )

for s being State of SCMPDS

for I being Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) >= 0 holds

( if<0 (a,k1,I) is_closed_on s,P & if<0 (a,k1,I) is_halting_on s,P )

proof end;

theorem Th110: :: SCMPDS_6:110

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) < 0 & I is_closed_on s,P & I is_halting_on s,P holds

IExec ((if<0 (a,k1,I)),P,(Initialize s)) = (IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 1),SCMPDS))

for s being State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) < 0 & I is_closed_on s,P & I is_halting_on s,P holds

IExec ((if<0 (a,k1,I)),P,(Initialize s)) = (IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 1),SCMPDS))

proof end;

theorem Th111: :: SCMPDS_6:111

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) >= 0 holds

IExec ((if<0 (a,k1,I)),P,(Initialize s)) = s +* (Start-At (((card I) + 1),SCMPDS))

for s being State of SCMPDS

for I being Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) >= 0 holds

IExec ((if<0 (a,k1,I)),P,(Initialize s)) = s +* (Start-At (((card I) + 1),SCMPDS))

proof end;

registration

let I be parahalting shiftable Program of SCMPDS;

let a be Int_position;

let k1 be Integer;

correctness

coherence

( if<0 (a,k1,I) is shiftable & if<0 (a,k1,I) is parahalting );

end;
let a be Int_position;

let k1 be Integer;

correctness

coherence

( if<0 (a,k1,I) is shiftable & if<0 (a,k1,I) is parahalting );

proof end;

registration

let I be halt-free Program of SCMPDS;

let a be Int_position;

let k1 be Integer;

coherence

if<0 (a,k1,I) is halt-free ;

end;
let a be Int_position;

let k1 be Integer;

coherence

if<0 (a,k1,I) is halt-free ;

theorem :: SCMPDS_6:112

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being halt-free parahalting shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer holds IC (IExec ((if<0 (a,k1,I)),P,(Initialize s))) = (card I) + 1

for s being State of SCMPDS

for I being halt-free parahalting shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer holds IC (IExec ((if<0 (a,k1,I)),P,(Initialize s))) = (card I) + 1

proof end;

theorem :: SCMPDS_6:113

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being halt-free parahalting shiftable Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) < 0 holds

(IExec ((if<0 (a,k1,I)),P,(Initialize s))) . b = (IExec (I,P,(Initialize s))) . b

for s being State of SCMPDS

for I being halt-free parahalting shiftable Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) < 0 holds

(IExec ((if<0 (a,k1,I)),P,(Initialize s))) . b = (IExec (I,P,(Initialize s))) . b

proof end;

theorem :: SCMPDS_6:114

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) >= 0 holds

(IExec ((if<0 (a,k1,I)),P,(Initialize s))) . b = s . b

for s being State of SCMPDS

for I being Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) >= 0 holds

(IExec ((if<0 (a,k1,I)),P,(Initialize s))) . b = s . b

proof end;

begin

theorem :: SCMPDS_6:115

theorem :: SCMPDS_6:116

theorem :: SCMPDS_6:117

theorem Th118: :: SCMPDS_6:118

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) >= 0 & I is_closed_on s,P & I is_halting_on s,P holds

( if>=0 (a,k1,I) is_closed_on s,P & if>=0 (a,k1,I) is_halting_on s,P )

for s being State of SCMPDS

for I being shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) >= 0 & I is_closed_on s,P & I is_halting_on s,P holds

( if>=0 (a,k1,I) is_closed_on s,P & if>=0 (a,k1,I) is_halting_on s,P )

proof end;

theorem Th119: :: SCMPDS_6:119

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) < 0 holds

( if>=0 (a,k1,I) is_closed_on s,P & if>=0 (a,k1,I) is_halting_on s,P )

for s being State of SCMPDS

for I being Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) < 0 holds

( if>=0 (a,k1,I) is_closed_on s,P & if>=0 (a,k1,I) is_halting_on s,P )

proof end;

theorem Th120: :: SCMPDS_6:120

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) >= 0 & I is_closed_on s,P & I is_halting_on s,P holds

IExec ((if>=0 (a,k1,I)),P,(Initialize s)) = (IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 2),SCMPDS))

for s being State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) >= 0 & I is_closed_on s,P & I is_halting_on s,P holds

IExec ((if>=0 (a,k1,I)),P,(Initialize s)) = (IExec (I,P,(Initialize s))) +* (Start-At (((card I) + 2),SCMPDS))

proof end;

theorem Th121: :: SCMPDS_6:121

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) < 0 holds

IExec ((if>=0 (a,k1,I)),P,(Initialize s)) = s +* (Start-At (((card I) + 2),SCMPDS))

for s being State of SCMPDS

for I being Program of SCMPDS

for a being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) < 0 holds

IExec ((if>=0 (a,k1,I)),P,(Initialize s)) = s +* (Start-At (((card I) + 2),SCMPDS))

proof end;

registration

let I be parahalting shiftable Program of SCMPDS;

let a be Int_position;

let k1 be Integer;

correctness

coherence

( if>=0 (a,k1,I) is shiftable & if>=0 (a,k1,I) is parahalting );

end;
let a be Int_position;

let k1 be Integer;

correctness

coherence

( if>=0 (a,k1,I) is shiftable & if>=0 (a,k1,I) is parahalting );

proof end;

registration

let I be halt-free Program of SCMPDS;

let a be Int_position;

let k1 be Integer;

coherence

if>=0 (a,k1,I) is halt-free ;

end;
let a be Int_position;

let k1 be Integer;

coherence

if>=0 (a,k1,I) is halt-free ;

theorem :: SCMPDS_6:122

for P being Instruction-Sequence of SCMPDS

for s being 0 -started State of SCMPDS

for I being halt-free parahalting shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer holds IC (IExec ((if>=0 (a,k1,I)),P,s)) = (card I) + 2

for s being 0 -started State of SCMPDS

for I being halt-free parahalting shiftable Program of SCMPDS

for a being Int_position

for k1 being Integer holds IC (IExec ((if>=0 (a,k1,I)),P,s)) = (card I) + 2

proof end;

theorem :: SCMPDS_6:123

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being halt-free parahalting shiftable Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) >= 0 holds

(IExec ((if>=0 (a,k1,I)),P,(Initialize s))) . b = (IExec (I,P,(Initialize s))) . b

for s being State of SCMPDS

for I being halt-free parahalting shiftable Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) >= 0 holds

(IExec ((if>=0 (a,k1,I)),P,(Initialize s))) . b = (IExec (I,P,(Initialize s))) . b

proof end;

theorem :: SCMPDS_6:124

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) < 0 holds

(IExec ((if>=0 (a,k1,I)),P,(Initialize s))) . b = s . b

for s being State of SCMPDS

for I being Program of SCMPDS

for a, b being Int_position

for k1 being Integer st s . (DataLoc ((s . a),k1)) < 0 holds

(IExec ((if>=0 (a,k1,I)),P,(Initialize s))) . b = s . b

proof end;

theorem :: SCMPDS_6:125

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of SCMPDS holds

( I is_closed_on s,P iff I is_closed_on Initialize s,P )

for s being State of SCMPDS

for I being Program of SCMPDS holds

( I is_closed_on s,P iff I is_closed_on Initialize s,P )

proof end;

theorem :: SCMPDS_6:126

for P being Instruction-Sequence of SCMPDS

for s being State of SCMPDS

for I being Program of SCMPDS holds

( I is_halting_on s,P iff I is_halting_on Initialize s,P )

for s being State of SCMPDS

for I being Program of SCMPDS holds

( I is_halting_on s,P iff I is_halting_on Initialize s,P )

proof end;