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

begin

set A = NAT ;

set D = SCM-Data-Loc ;

Lm1: (Stop SCMPDS) . 0 = halt SCMPDS
by AFINSQ_1:38;

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

theorem :: SCMPDS_6:1

canceled;

theorem Th2: :: SCMPDS_6:2

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being State of SCMPDS st P halts_on s holds
for k being Element of NAT st LifeSpan (P,s) <= k holds
CurInstr (P,(Comput (P,s,k))) = halt SCMPDS

proof end;

theorem Th3: :: SCMPDS_6:3

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being State of SCMPDS st P halts_on s holds
for k being Element of NAT st LifeSpan (P,s) <= k holds
IC (Comput (P,s,k)) = IC (Comput (P,s,(LifeSpan (P,s))))

proof end;

theorem Th4: :: SCMPDS_6:4

for s1, s2 being State of SCMPDS holds
( NPP s1 = NPP s2 iff ( IC s1 = IC s2 & DataPart s1 = DataPart s2 ) )

proof end;

theorem :: SCMPDS_6:5

canceled;

theorem :: SCMPDS_6:6

canceled;

theorem Th7: :: SCMPDS_6:7

for s being State of SCMPDS
for l being Element of NAT holds DataPart s = DataPart (s +* (Start-At (l,SCMPDS)))

proof end;

theorem :: SCMPDS_6:8

canceled;

theorem :: SCMPDS_6:9

canceled;

theorem :: SCMPDS_6:10

canceled;

theorem :: SCMPDS_6:11

canceled;

theorem Th12: :: SCMPDS_6:12

for s1, s2 being State of SCMPDS
for I, J being Program of SCMPDS st DataPart s1 = DataPart s2 holds
NPP (Initialize s1) = NPP (Initialize s2)

proof end;

theorem :: SCMPDS_6:13

canceled;

theorem :: SCMPDS_6:14

canceled;

theorem Th15: :: SCMPDS_6:15

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

proof end;

theorem Th16: :: SCMPDS_6:16

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

proof end;

theorem :: SCMPDS_6:17

canceled;

theorem Th18: :: SCMPDS_6:18

for loc being Element of NAT
for I being Program of SCMPDS st loc in dom I holds
loc in dom (stop I)

proof end;

theorem Th19: :: SCMPDS_6:19

for loc being Element of NAT
for I being Program of SCMPDS st loc in dom I holds
(stop I) . loc = I . loc

proof end;

theorem Th20: :: SCMPDS_6:20

for loc being Element of NAT
for I being Program of SCMPDS st loc in dom I holds
(stop I) . loc = I . loc

proof end;

theorem :: SCMPDS_6:21

canceled;

theorem Th22: :: SCMPDS_6:22

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

proof end;

theorem Th23: :: SCMPDS_6:23

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 Th24: :: SCMPDS_6:24

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

proof end;

theorem Th25: :: SCMPDS_6:25

for I being Program of SCMPDS holds
( card I in dom (stop I) & (stop I) . (card I) = halt SCMPDS )

proof end;

theorem Th26: :: SCMPDS_6:26

for s being State of SCMPDS
for J, I being Program of SCMPDS
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for x, l being Element of NAT holds (IExec (J,P,s)) . x = ((IExec (I,P,s)) +* (Start-At (l,SCMPDS))) . x

proof end;

theorem Th27: :: SCMPDS_6:27

for s being State of SCMPDS
for I being Program of SCMPDS
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for x, l being Element of NAT holds (IExec (I,P,s)) . x = (s +* (Start-At (l,SCMPDS))) . x

proof end;

theorem :: SCMPDS_6:28

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,(Exec (i,(Initialize s))))) . a

proof end;

theorem :: SCMPDS_6:29

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

proof end;

theorem :: SCMPDS_6:30

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

proof end;

theorem :: SCMPDS_6:31

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:25;
cluster goto (- (n + 1)) -> No-StopCode ;
correctness
coherence
goto (- (n + 1)) is No-StopCode ;

proof end;

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 :: SCMPDS_6:32

canceled;

theorem Th33: :: SCMPDS_6:33

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

begin

definition

let I be Program of SCMPDS;
let s be State of SCMPDS;
let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ;
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 the Instructions of SCMPDS -valued ManySortedSet of NAT 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 the Instructions of SCMPDS -valued ManySortedSet of NAT holds
( I is_halting_on s,P iff P +* (stop I) halts_on Initialize s );

theorem Th34: :: SCMPDS_6:34

for I being Program of SCMPDS holds
( I is paraclosed iff for s being State of SCMPDS
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT holds I is_closed_on s,P )

proof end;

theorem Th35: :: SCMPDS_6:35

for I being Program of SCMPDS holds
( I is parahalting iff for s being State of SCMPDS
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT holds I is_halting_on s,P )

proof end;

theorem Th36: :: SCMPDS_6:36

for P1, P2 being the Instructions of SCMPDS -valued ManySortedSet of NAT
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:37

for P1, P2 being the Instructions of SCMPDS -valued ManySortedSet of NAT
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 Th38: :: SCMPDS_6:38

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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 Th39: :: SCMPDS_6:39

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for I, J being Program of SCMPDS
for s being State 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)),(Initialize s)) holds
IC (Comput ((P +* (stop I)),(Initialize s),k)) = IC (Comput ((P +* (stop (I ';' J))),(Initialize s),k)) ) & DataPart (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = DataPart (Comput ((P +* (stop (I ';' J))),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) )

proof end;

theorem Th40: :: SCMPDS_6:40

for s being State of SCMPDS
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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 Th41: :: SCMPDS_6:41

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for I, J being 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))) = CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),(Initialize s),k)))

proof end;

theorem Th42: :: SCMPDS_6:42

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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 Th43: :: SCMPDS_6:43

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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 the Instructions of SCMPDS -valued ManySortedSet of NAT
for I being halt-free Program of SCMPDS
for J being 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 ';' (Goto ((card J) + 1))) ';' J))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 1))) = ((card I) + (card J)) + 1 & DataPart (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = DataPart (Comput ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 1))) & ( for k being Element of NAT st k <= LifeSpan ((P +* (stop I)),(Initialize s)) holds
CurInstr ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(Comput ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(Initialize s),k))) <> halt SCMPDS ) & IC (Comput ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I & P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J)) halts_on Initialize s & LifeSpan ((P +* (stop ((I ';' (Goto ((card J) + 1))) ';' J))),(Initialize s)) = (LifeSpan ((P +* (stop I)),(Initialize s))) + 1 )

proof end;

theorem Th44: :: SCMPDS_6:44

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for I, J being Program of SCMPDS
for s being 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 Th45: :: SCMPDS_6:45

for s1, s2 being State of SCMPDS
for P1, P2 being the Instructions of SCMPDS -valued ManySortedSet of NAT
for I being shiftable Program of SCMPDS st Start-At (0,SCMPDS) c= s1 & 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 Th46: :: SCMPDS_6:46

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being 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 Th47: :: SCMPDS_6:47

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being 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 Th48: :: SCMPDS_6:48

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,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:49

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

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

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 the Instructions of SCMPDS -valued ManySortedSet of NAT 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 the Instructions of SCMPDS -valued ManySortedSet of NAT holds Shift ((stop I),2) c= P +* (stop ((i ';' j) ';' I))

proof end;

theorem Th52: :: SCMPDS_6:52

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being 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 Th53: :: SCMPDS_6:53

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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 Th54: :: SCMPDS_6:54

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being 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 Th55: :: SCMPDS_6:55

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,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:56

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being 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:57

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being 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:58

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,s)) . b = (IExec (J,P,s)) . b

proof end;

begin

theorem :: SCMPDS_6:59

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

theorem :: SCMPDS_6:60

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

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

theorem Th62: :: SCMPDS_6:62

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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 Th63: :: SCMPDS_6:63

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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 Th64: :: SCMPDS_6:64

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,s) = (IExec (I,P,s)) +* (Start-At (((card I) + 1),SCMPDS))

proof end;

theorem Th65: :: SCMPDS_6:65

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,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:66

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,s)) = (card I) + 1

proof end;

theorem :: SCMPDS_6:67

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,s)) . b = (IExec (I,P,s)) . b

proof end;

theorem :: SCMPDS_6:68

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,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:69

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

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

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 Th72: :: SCMPDS_6:72

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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 Th73: :: SCMPDS_6:73

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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 Th74: :: SCMPDS_6:74

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,s) = (IExec (I,P,s)) +* (Start-At (((card I) + 2),SCMPDS))

proof end;

theorem Th75: :: SCMPDS_6:75

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,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:76

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,s)) = (card I) + 2

proof end;

theorem :: SCMPDS_6:77

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,s)) . b = (IExec (I,P,s)) . b

proof end;

theorem :: SCMPDS_6:78

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,s)) . b = s . b

proof end;

begin

theorem :: SCMPDS_6:79

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

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

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 Th82: :: SCMPDS_6:82

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being 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 Th83: :: SCMPDS_6:83

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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 Th84: :: SCMPDS_6:84

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being 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 Th85: :: SCMPDS_6:85

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,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:86

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being 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:87

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being 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:88

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,s)) . b = (IExec (J,P,s)) . b

proof end;

begin

theorem :: SCMPDS_6:89

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

theorem :: SCMPDS_6:90

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

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

theorem Th92: :: SCMPDS_6:92

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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 Th93: :: SCMPDS_6:93

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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 Th94: :: SCMPDS_6:94

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,s) = (IExec (I,P,s)) +* (Start-At (((card I) + 1),SCMPDS))

proof end;

theorem Th95: :: SCMPDS_6:95

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,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:96

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,s)) = (card I) + 1

proof end;

theorem :: SCMPDS_6:97

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,s)) . b = (IExec (I,P,s)) . b

proof end;

theorem :: SCMPDS_6:98

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,s)) . b = s . b

proof end;

begin

theorem :: SCMPDS_6:99

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

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

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 Th102: :: SCMPDS_6:102

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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 Th103: :: SCMPDS_6:103

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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 Th104: :: SCMPDS_6:104

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,s) = (IExec (I,P,s)) +* (Start-At (((card I) + 2),SCMPDS))

proof end;

theorem Th105: :: SCMPDS_6:105

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,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:106

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,s)) = (card I) + 2

proof end;

theorem :: SCMPDS_6:107

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,s)) . b = (IExec (I,P,s)) . b

proof end;

theorem :: SCMPDS_6:108

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,s)) . b = s . b

proof end;

begin

theorem :: SCMPDS_6:109

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

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

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 Th112: :: SCMPDS_6:112

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being 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 Th113: :: SCMPDS_6:113

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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 Th114: :: SCMPDS_6:114

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being 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 Th115: :: SCMPDS_6:115

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,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:116

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being 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:117

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for s being 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:118

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,s)) . b = (IExec (J,P,s)) . b

proof end;

begin

theorem :: SCMPDS_6:119

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

theorem :: SCMPDS_6:120

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

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

theorem Th122: :: SCMPDS_6:122

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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 Th123: :: SCMPDS_6:123

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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 Th124: :: SCMPDS_6:124

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,s) = (IExec (I,P,s)) +* (Start-At (((card I) + 1),SCMPDS))

proof end;

theorem Th125: :: SCMPDS_6:125

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,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:126

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,s)) = (card I) + 1

proof end;

theorem :: SCMPDS_6:127

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,s)) . b = (IExec (I,P,s)) . b

proof end;

theorem :: SCMPDS_6:128

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,s)) . b = s . b

proof end;

begin

theorem :: SCMPDS_6:129

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

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

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 Th132: :: SCMPDS_6:132

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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 Th133: :: SCMPDS_6:133

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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 Th134: :: SCMPDS_6:134

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,s) = (IExec (I,P,s)) +* (Start-At (((card I) + 2),SCMPDS))

proof end;

theorem Th135: :: SCMPDS_6:135

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,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:136

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,s)) = (card I) + 2

proof end;

theorem :: SCMPDS_6:137

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,s)) . b = (IExec (I,P,s)) . b

proof end;

theorem :: SCMPDS_6:138

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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,s)) . b = s . b

proof end;

theorem :: SCMPDS_6:139

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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:140

for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
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;