:: The Construction and Computation of Conditional Statements for SCMPDS
:: by JingChao Chen
::
:: Received June 15, 1999
:: Copyright (c) 1999-2021 Association of Mizar Users

set A = NAT ;

set D = SCM-Data-Loc ;

Lm1: (Stop SCMPDS) . 0 = halt SCMPDS
;

Lm2: 0 in dom (Stop SCMPDS)
by COMPOS_1:3;

theorem :: SCMPDS_6:1

canceled;

theorem :: SCMPDS_6:2

canceled;

theorem :: SCMPDS_6:3

canceled;

theorem :: SCMPDS_6:4

canceled;

theorem :: SCMPDS_6:5

canceled;

::$CT 5

theorem Th1: :: SCMPDS_6:6

for i being Instruction of SCMPDS
for I being Program of holds card (i ';' I) = (card I) + 1

proof end;

theorem Th2: :: SCMPDS_6:7

for i being Instruction of SCMPDS
for I being Program of holds (i ';' I) . 0 = i

proof end;

theorem :: SCMPDS_6:8

canceled;

theorem :: SCMPDS_6:9

canceled;

theorem :: SCMPDS_6:10

canceled;

::$CT 3

theorem Th3: :: SCMPDS_6:11

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

proof end;

theorem Th4: :: SCMPDS_6:12

for s being State of SCMPDS
for m1, m2 being Nat st IC s = m1 holds
ICplusConst (s,m2) = m1 + m2

proof end;

theorem Th5: :: SCMPDS_6:13

for I, J being Program of holds Shift ((stop J),(card I)) c= stop (I ';' J)

proof end;

theorem :: SCMPDS_6:14

canceled;

::$CT

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
for a being Int_position holds (IExec ((i ';' J),P,s)) . a = (IExec (J,P,(Initialize (Exec (i,s))))) . a

proof end;

theorem :: SCMPDS_6:16

for a being Int_position
for k1, k2 being Integer holds (a,k1) <>0_goto k2 <> halt SCMPDS

proof end;

theorem :: SCMPDS_6:17

for a being Int_position
for k1, k2 being Integer holds (a,k1) <=0_goto k2 <> halt SCMPDS

proof end;

theorem :: SCMPDS_6:18

for a being Int_position
for k1, k2 being Integer holds (a,k1) >=0_goto k2 <> halt SCMPDS

proof end;

definition

let k1 be Integer;

func Goto k1 -> Program of equals :: SCMPDS_6:def 1
Load (goto k1);

coherence
Load (goto k1) is Program of ;

end;

:: deftheorem defines Goto SCMPDS_6:def 1 :
for k1 being Integer holds Goto k1 = Load (goto k1);

registration

let n be Nat;

cluster goto (n + 1) -> No-StopCode ;

correctness
coherence
goto (n + 1) is No-StopCode ;
by SCMPDS_5:21;

cluster goto (- (n + 1)) -> No-StopCode ;

correctness
coherence
goto (- (n + 1)) is No-StopCode ;
by SCMPDS_5:21;

end;

registration

let n be Nat;

cluster Goto (n + 1) -> halt-free ;

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

cluster Goto (- (n + 1)) -> halt-free ;

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

end;

theorem Th10: :: SCMPDS_6:19

for k1 being Integer holds
( 0 in dom (Goto k1) & (Goto k1) . 0 = goto k1 ) by AFINSQ_1:65;

definition

let I be Program of ;
let s be State of SCMPDS;
let P be Instruction-Sequence of SCMPDS;

pred I is_closed_on s,P means :: SCMPDS_6:def 2
for k being Nat holds IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom (stop I);

pred I is_halting_on s,P means :: SCMPDS_6:def 3
P +* (stop I) halts_on Initialize s;

end;

:: deftheorem defines is_closed_on SCMPDS_6:def 2 :
for I being Program of
for s being State of SCMPDS
for P being Instruction-Sequence of SCMPDS holds
( I is_closed_on s,P iff for k being Nat holds IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom (stop I) );

:: deftheorem defines is_halting_on SCMPDS_6:def 3 :
for I being Program of
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 Th11: :: SCMPDS_6:20

for I being Program of 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 )

proof end;

theorem Th12: :: SCMPDS_6:21

for I being Program of 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 )

proof end;

theorem Th13: :: SCMPDS_6:22

for P1, P2 being Instruction-Sequence of SCMPDS
for s1, s2 being State of SCMPDS
for I being Program of 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 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 :: SCMPDS_6:24

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I, J being Program of holds
( I is_closed_on s,P iff I is_closed_on Initialize s,P +* J )

proof end;

theorem Th16: :: SCMPDS_6:25

for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I, J being Program of st I is_closed_on s,P & I is_halting_on s,P holds
( ( for k being 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 Th17: :: SCMPDS_6:26

for s being State of SCMPDS
for P being Instruction-Sequence of SCMPDS
for I being Program of
for k being 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 Th18: :: SCMPDS_6:27

for P being Instruction-Sequence of SCMPDS
for I, J being Program of
for s being 0 -started State of SCMPDS
for k being 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 Th19: :: SCMPDS_6:28

for P being Instruction-Sequence of SCMPDS
for I being halt-free Program of
for s being State of SCMPDS
for k being 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 Th20: :: SCMPDS_6:29

for P being Instruction-Sequence of SCMPDS
for I being halt-free Program of
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
for J being Program of
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 Th21: :: SCMPDS_6:30

for P being Instruction-Sequence of SCMPDS
for I, J being Program of
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 Th22: :: 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 st stop I c= P1 & I is_closed_on s1,P1 holds
for n being Nat st Shift ((stop I),n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being 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 Th23: :: 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
for J being Program of 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 Th24: :: 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
for J being Program of 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 Th25: :: SCMPDS_6:34

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being halt-free Program of st I is_closed_on s,P & I is_halting_on s,P holds
IC (IExec (I,P,(Initialize s))) = card I

proof end;

definition

let a be Int_position;
let k be Integer;
let I, J be Program of ;

func if=0 (a,k,I,J) -> Program of 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 is Program of ;

func if>0 (a,k,I,J) -> Program of 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 is Program of ;

func if<0 (a,k,I,J) -> Program of 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 is Program of ;

end;

:: deftheorem defines if=0 SCMPDS_6:def 4 :
for a being Int_position
for k being Integer
for I, J being Program of 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 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 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 ;

func if=0 (a,k,I) -> Program of equals :: SCMPDS_6:def 7
((a,k) <>0_goto ((card I) + 1)) ';' I;

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

func if<>0 (a,k,I) -> Program of 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 is Program of ;

func if>0 (a,k,I) -> Program of equals :: SCMPDS_6:def 9
((a,k) <=0_goto ((card I) + 1)) ';' I;

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

func if<=0 (a,k,I) -> Program of 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 is Program of ;

func if<0 (a,k,I) -> Program of equals :: SCMPDS_6:def 11
((a,k) >=0_goto ((card I) + 1)) ';' I;

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

func if>=0 (a,k,I) -> Program of 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 is Program of ;

end;

:: deftheorem defines if=0 SCMPDS_6:def 7 :
for a being Int_position
for k being Integer
for I being Program of 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 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 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 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 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 holds if>=0 (a,k,I) = (((a,k) >=0_goto 2) ';' (goto ((card I) + 1))) ';' I;

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

proof end;

theorem :: SCMPDS_6:35

for a being Int_position
for k1 being Integer
for I, J being Program of holds card (if=0 (a,k1,I,J)) = ((card I) + (card J)) + 2 by Lm4;

theorem :: SCMPDS_6:36

for a being Int_position
for k1 being Integer
for I, J being Program of 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 holds (((i ';' I) ';' J) ';' K) . 0 = i

proof end;

theorem :: SCMPDS_6:37

for a being Int_position
for k1 being Integer
for I, J being Program of holds (if=0 (a,k1,I,J)) . 0 = (a,k1) <>0_goto ((card I) + 2) by Lm5;

Lm6: for i being Instruction of SCMPDS
for I being Program of
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
for P being Instruction-Sequence of SCMPDS holds Shift ((stop I),2) c= P +* (stop ((i ';' j) ';' I))

proof end;

theorem Th29: :: 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
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 Th30: :: SCMPDS_6:39

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of
for J being shiftable Program of
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 Th31: :: 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
for J being shiftable Program of
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 Th32: :: SCMPDS_6:41

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of
for J being halt-free shiftable Program of
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 ;
let a be Int_position;
let k1 be Integer;

cluster if=0 (a,k1,I,J) -> parahalting shiftable ;

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

proof end;

end;

registration

let I, J be halt-free Program of ;
let a be Int_position;
let k1 be Integer;

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

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

end;

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
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
for J being shiftable Program of
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
for J being halt-free parahalting shiftable Program of
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;

theorem :: SCMPDS_6:45

for a being Int_position
for k1 being Integer
for I being Program of holds card (if=0 (a,k1,I)) = (card I) + 1 by Th1;

theorem :: SCMPDS_6:46

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

proof end;

theorem :: SCMPDS_6:47

for a being Int_position
for k1 being Integer
for I being Program of holds (if=0 (a,k1,I)) . 0 = (a,k1) <>0_goto ((card I) + 1) by Th2;

theorem Th39: :: SCMPDS_6:48

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being shiftable Program of
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 Th40: :: SCMPDS_6:49

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of
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 Th41: :: SCMPDS_6:50

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being halt-free shiftable Program of
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 Th42: :: SCMPDS_6:51

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of
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 ;
let a be Int_position;
let k1 be Integer;

cluster if=0 (a,k1,I) -> parahalting shiftable ;

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

proof end;

end;

registration

let I be halt-free Program of ;
let a be Int_position;
let k1 be Integer;

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

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

end;

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
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
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
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 holds card ((i ';' j) ';' I) = (card I) + 2

proof end;

theorem :: SCMPDS_6:55

for a being Int_position
for k1 being Integer
for I being Program of holds card (if<>0 (a,k1,I)) = (card I) + 2 by Lm8;

Lm9: for i, j being Instruction of SCMPDS
for I being Program of holds
( 0 in dom ((i ';' j) ';' I) & 1 in dom ((i ';' j) ';' I) )

proof end;

theorem :: SCMPDS_6:56

for a being Int_position
for k1 being Integer
for I being Program of holds
( 0 in dom (if<>0 (a,k1,I)) & 1 in dom (if<>0 (a,k1,I)) ) by Lm9;

Lm10: for i, j being Instruction of SCMPDS
for I being Program of holds
( ((i ';' j) ';' I) . 0 = i & ((i ';' j) ';' I) . 1 = j )

proof end;

theorem :: SCMPDS_6:57

for a being Int_position
for k1 being Integer
for I being Program of holds
( (if<>0 (a,k1,I)) . 0 = (a,k1) <>0_goto 2 & (if<>0 (a,k1,I)) . 1 = goto ((card I) + 1) ) by Lm10;

theorem Th49: :: SCMPDS_6:58

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being shiftable Program of
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 Th50: :: SCMPDS_6:59

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of
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 Th51: :: SCMPDS_6:60

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being halt-free shiftable Program of
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 Th52: :: SCMPDS_6:61

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of
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 ;
let a be Int_position;
let k1 be Integer;

cluster if<>0 (a,k1,I) -> parahalting shiftable ;

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

proof end;

end;

registration

let I be halt-free Program of ;
let a be Int_position;
let k1 be Integer;

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

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

end;

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

for a being Int_position
for k1 being Integer
for I, J being Program of holds card (if>0 (a,k1,I,J)) = ((card I) + (card J)) + 2 by Lm4;

theorem :: SCMPDS_6:66

for a being Int_position
for k1 being Integer
for I, J being Program of 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

for a being Int_position
for k1 being Integer
for I, J being Program of holds (if>0 (a,k1,I,J)) . 0 = (a,k1) <=0_goto ((card I) + 2) by Lm5;

theorem Th59: :: 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
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 Th60: :: SCMPDS_6:69

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of
for J being shiftable Program of
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 Th61: :: 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
for J being shiftable Program of
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 Th62: :: SCMPDS_6:71

for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being Program of
for J being halt-free shiftable Program of
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 ;
let a be Int_position;
let k1 be Integer;

cluster if>0 (a,k1,I,J) -> parahalting shiftable ;

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

proof end;

end;

registration

let I, J be halt-free Program of ;
let a be Int_position;
let k1 be Integer;

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

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

end;

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
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
for J being shiftable Program of
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
for J being halt-free parahalting shiftable Program of
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;

theorem :: SCMPDS_6:75

for a being Int_position
for k1 being Integer
for I being Program of holds card (if>0 (a,k1,I)) = (card I) + 1 by Th1;

theorem :: SCMPDS_6:76

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

proof end;

theorem :: SCMPDS_6:77

for a being Int_position
for k1 being Integer
for I being Program of holds (if>0 (a,k1,I)) . 0 = (a,k1) <=0_goto ((card I) + 1) by Th2;

theorem Th69: :: SCMPDS_6:78

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being shiftable Program of
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 Th70: :: SCMPDS_6:79

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of
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 Th71: :: SCMPDS_6:80

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being halt-free shiftable Program of
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 Th72: :: SCMPDS_6:81

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of
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 ;
let a be Int_position;
let k1 be Integer;

cluster if>0 (a,k1,I) -> parahalting shiftable ;

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

proof end;

end;

registration

let I be halt-free Program of ;
let a be Int_position;
let k1 be Integer;

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

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

end;

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

for a being Int_position
for k1 being Integer
for I being Program of holds card (if<=0 (a,k1,I)) = (card I) + 2 by Lm8;

theorem :: SCMPDS_6:86

for a being Int_position
for k1 being Integer
for I being Program of holds
( 0 in dom (if<=0 (a,k1,I)) & 1 in dom (if<=0 (a,k1,I)) ) by Lm9;

theorem :: SCMPDS_6:87

for a being Int_position
for k1 being Integer
for I being Program of holds
( (if<=0 (a,k1,I)) . 0 = (a,k1) <=0_goto 2 & (if<=0 (a,k1,I)) . 1 = goto ((card I) + 1) ) by Lm10;

theorem Th79: :: SCMPDS_6:88

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being shiftable Program of
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 Th80: :: SCMPDS_6:89

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of
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 Th81: :: SCMPDS_6:90

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being halt-free shiftable Program of
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 Th82: :: SCMPDS_6:91

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of
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 ;
let a be Int_position;
let k1 be Integer;

cluster if<=0 (a,k1,I) -> parahalting shiftable ;

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

proof end;

end;

registration

let I be halt-free Program of ;
let a be Int_position;
let k1 be Integer;

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

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

end;

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

for a being Int_position
for k1 being Integer
for I, J being Program of holds card (if<0 (a,k1,I,J)) = ((card I) + (card J)) + 2 by Lm4;

theorem :: SCMPDS_6:96

for a being Int_position
for k1 being Integer
for I, J being Program of 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

for a being Int_position
for k1 being Integer
for I, J being Program of holds (if<0 (a,k1,I,J)) . 0 = (a,k1) >=0_goto ((card I) + 2) by Lm5;

theorem Th89: :: 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
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 Th90: :: SCMPDS_6:99

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of
for J being shiftable Program of
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 Th91: :: 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
for J being shiftable Program of
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 Th92: :: SCMPDS_6:101

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of
for J being halt-free shiftable Program of
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 ;
let a be Int_position;
let k1 be Integer;

cluster if<0 (a,k1,I,J) -> parahalting shiftable ;

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

proof end;

end;

registration

let I, J be halt-free Program of ;
let a be Int_position;
let k1 be Integer;

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

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

end;

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
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
for J being shiftable Program of
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
for J being halt-free parahalting shiftable Program of
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;

theorem :: SCMPDS_6:105

for a being Int_position
for k1 being Integer
for I being Program of holds card (if<0 (a,k1,I)) = (card I) + 1 by Th1;

theorem :: SCMPDS_6:106

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

proof end;

theorem :: SCMPDS_6:107

for a being Int_position
for k1 being Integer
for I being Program of holds (if<0 (a,k1,I)) . 0 = (a,k1) >=0_goto ((card I) + 1) by Th2;

theorem Th99: :: SCMPDS_6:108

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being shiftable Program of
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 Th100: :: SCMPDS_6:109

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of
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 Th101: :: SCMPDS_6:110

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being halt-free shiftable Program of
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 Th102: :: SCMPDS_6:111

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of
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 ;
let a be Int_position;
let k1 be Integer;

cluster if<0 (a,k1,I) -> parahalting shiftable ;

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

proof end;

end;

registration

let I be halt-free Program of ;
let a be Int_position;
let k1 be Integer;

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

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

end;

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

for a being Int_position
for k1 being Integer
for I being Program of holds card (if>=0 (a,k1,I)) = (card I) + 2 by Lm8;

theorem :: SCMPDS_6:116

for a being Int_position
for k1 being Integer
for I being Program of holds
( 0 in dom (if>=0 (a,k1,I)) & 1 in dom (if>=0 (a,k1,I)) ) by Lm9;

theorem :: SCMPDS_6:117

for a being Int_position
for k1 being Integer
for I being Program of holds
( (if>=0 (a,k1,I)) . 0 = (a,k1) >=0_goto 2 & (if>=0 (a,k1,I)) . 1 = goto ((card I) + 1) ) by Lm10;

theorem Th109: :: SCMPDS_6:118

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being shiftable Program of
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 Th110: :: SCMPDS_6:119

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of
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 Th111: :: SCMPDS_6:120

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being halt-free shiftable Program of
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 Th112: :: SCMPDS_6:121

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of
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 ;
let a be Int_position;
let k1 be Integer;

cluster if>=0 (a,k1,I) -> parahalting shiftable ;

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

proof end;

end;

registration

let I be halt-free Program of ;
let a be Int_position;
let k1 be Integer;

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

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

end;

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
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
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
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 holds
( I is_closed_on s,P iff I is_closed_on Initialize s,P ) ;

theorem :: SCMPDS_6:126

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of holds
( I is_halting_on s,P iff I is_halting_on Initialize s,P ) ;