:: The Construction and Computation of Conditional Statements for SCMPDS
:: 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 :: SCMPDS_6:1
canceled;

theorem :: SCMPDS_6:2
canceled;

theorem :: SCMPDS_6:3
canceled;

theorem :: SCMPDS_6:4
canceled;

theorem :: SCMPDS_6:5
canceled;

theorem Th6: :: SCMPDS_6:6
for i being Instruction of SCMPDS
for I being Program of SCMPDS holds card (i ';' I) = (card I) + 1
proof end;

theorem Th7: :: SCMPDS_6:7
for i being Instruction of SCMPDS
for I being Program of SCMPDS holds (i ';' I) . 0 = i
proof end;

theorem :: SCMPDS_6:8
canceled;

theorem :: SCMPDS_6:9
canceled;

theorem :: SCMPDS_6:10
canceled;

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
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
proof end;

theorem Th13: :: SCMPDS_6:13
for I, J being Program of SCMPDS holds Shift ((stop J),(card I)) c= stop (I ';' J)
proof end;

theorem :: SCMPDS_6:14
canceled;

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
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 SCMPDS equals :: SCMPDS_6:def 1
Load (goto k1);
coherence
Load (goto k1) is Program of SCMPDS
;
end;

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

registration
let n be Element of 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 Element of 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 Th19: :: SCMPDS_6:19
for k1 being Integer holds
( 0 in dom (Goto k1) & (Goto k1) . 0 = goto k1 ) by AFINSQ_1:34, AFINSQ_1:65;

begin

definition
let I be Program of SCMPDS;
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);
pred I is_halting_on s,P means :Def3: :: SCMPDS_6:def 3
P +* (stop I) halts_on Initialize s;
end;

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

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

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 )
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 )
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
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 )
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 )
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)))) )
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
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)))
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
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
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 )
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)) )
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
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))
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
proof end;

begin

definition
let a be Int_position;
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 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 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 is Program of SCMPDS
;
end;

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

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

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

definition
let a be Int_position;
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 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 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 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 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 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 is Program of SCMPDS
;
end;

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

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

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

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

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

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

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
for a being Int_position
for k1 being Integer
for I, J being Program of SCMPDS 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 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
for a being Int_position
for k1 being Integer
for I, J being Program of SCMPDS 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 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 )
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 )
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))
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))
proof end;

registration
let I, J be parahalting shiftable Program of SCMPDS;
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 SCMPDS;
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 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
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
proof end;

begin

theorem :: SCMPDS_6:45
for a being Int_position
for k1 being Integer
for I being Program of SCMPDS holds card (if=0 (a,k1,I)) = (card I) + 1 by Th6;

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))
proof end;

theorem :: SCMPDS_6:47
for a being Int_position
for k1 being Integer
for I being Program of SCMPDS holds (if=0 (a,k1,I)) . 0 = (a,k1) <>0_goto ((card I) + 1) by Th7;

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 )
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 )
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))
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))
proof end;

registration
let I be parahalting shiftable Program of SCMPDS;
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 SCMPDS;
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 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
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
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
for a being Int_position
for k1 being Integer
for I being Program of SCMPDS 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 SCMPDS 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 SCMPDS 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 SCMPDS 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 SCMPDS 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 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 )
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 )
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))
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))
proof end;

registration
let I be parahalting shiftable Program of SCMPDS;
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 SCMPDS;
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 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
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
proof end;

begin

theorem :: SCMPDS_6:65
for a being Int_position
for k1 being Integer
for I, J being Program of SCMPDS 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 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
for a being Int_position
for k1 being Integer
for I, J being Program of SCMPDS holds (if>0 (a,k1,I,J)) . 0 = (a,k1) <=0_goto ((card I) + 2) by Lm5;

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 )
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 )
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))
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))
proof end;

registration
let I, J be parahalting shiftable Program of SCMPDS;
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 SCMPDS;
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 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
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
proof end;

begin

theorem :: SCMPDS_6:75
for a being Int_position
for k1 being Integer
for I being Program of SCMPDS holds card (if>0 (a,k1,I)) = (card I) + 1 by Th6;

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))
proof end;

theorem :: SCMPDS_6:77
for a being Int_position
for k1 being Integer
for I being Program of SCMPDS holds (if>0 (a,k1,I)) . 0 = (a,k1) <=0_goto ((card I) + 1) by Th7;

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 )
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 )
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))
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))
proof end;

registration
let I be parahalting shiftable Program of SCMPDS;
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 SCMPDS;
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 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
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
proof end;

begin

theorem :: SCMPDS_6:85
for a being Int_position
for k1 being Integer
for I being Program of SCMPDS 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 SCMPDS 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 SCMPDS 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 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 )
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 )
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))
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))
proof end;

registration
let I be parahalting shiftable Program of SCMPDS;
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 SCMPDS;
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 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
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
proof end;

begin

theorem :: SCMPDS_6:95
for a being Int_position
for k1 being Integer
for I, J being Program of SCMPDS 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 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
for a being Int_position
for k1 being Integer
for I, J being Program of SCMPDS holds (if<0 (a,k1,I,J)) . 0 = (a,k1) >=0_goto ((card I) + 2) by Lm5;

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 )
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 )
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))
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))
proof end;

registration
let I, J be parahalting shiftable Program of SCMPDS;
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 SCMPDS;
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 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
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
proof end;

begin

theorem :: SCMPDS_6:105
for a being Int_position
for k1 being Integer
for I being Program of SCMPDS holds card (if<0 (a,k1,I)) = (card I) + 1 by Th6;

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))
proof end;

theorem :: SCMPDS_6:107
for a being Int_position
for k1 being Integer
for I being Program of SCMPDS holds (if<0 (a,k1,I)) . 0 = (a,k1) >=0_goto ((card I) + 1) by Th7;

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 )
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 )
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))
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))
proof end;

registration
let I be parahalting shiftable Program of SCMPDS;
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 SCMPDS;
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 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
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
proof end;

begin

theorem :: SCMPDS_6:115
for a being Int_position
for k1 being Integer
for I being Program of SCMPDS 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 SCMPDS 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 SCMPDS 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 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 )
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 )
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))
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))
proof end;

registration
let I be parahalting shiftable Program of SCMPDS;
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 SCMPDS;
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 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
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
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 )
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 )
proof end;