SCMPDS_6: The Construction and Computation of Conditional Statements for SCMPDS

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

begin

set A = NAT ;

set D = SCM-Data-Loc ;

theorem Th1: :: SCMPDS_6:1

for s being State of SCMPDS holds dom (s | NAT ) = NAT

proof end;

theorem Th2: :: SCMPDS_6:2

for s being State of SCMPDS st ProgramPart s halts_on s holds
for k being Element of NAT st LifeSpan s <= k holds
CurInstr (Computation s,k) = halt SCMPDS

proof end;

theorem Th3: :: SCMPDS_6:3

for s being State of SCMPDS st ProgramPart s halts_on s holds
for k being Element of NAT st LifeSpan s <= k holds
IC (Computation s,k) = IC (Computation s,(LifeSpan s))

proof end;

theorem Th4: :: SCMPDS_6:4

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

proof end;

theorem :: SCMPDS_6:5

for s being State of SCMPDS
for I being Program of SCMPDS holds (Initialized s) +* (Initialized I) = s +* (Initialized I)

proof end;

theorem :: SCMPDS_6:6

for I being Program of SCMPDS
for l being Instruction-Location of SCMPDS holds I c= I +* (Start-At l)

proof end;

theorem Th7: :: SCMPDS_6:7

for s being State of SCMPDS
for l being Instruction-Location of SCMPDS holds DataPart s = DataPart (s +* (Start-At l))

proof end;

theorem Th8: :: SCMPDS_6:8

for s being State of SCMPDS
for I being Program of SCMPDS
for l being Instruction-Location of SCMPDS holds DataPart s = DataPart (s +* (I +* (Start-At l)))

proof end;

theorem Th9: :: SCMPDS_6:9

for s being State of SCMPDS
for I being Program of SCMPDS holds DataPart s = DataPart (s +* (Initialized I))

proof end;

theorem Th10: :: SCMPDS_6:10

for s being State of SCMPDS
for l being Instruction-Location of SCMPDS holds dom (s | NAT ) misses dom (Start-At l)

proof end;

theorem :: SCMPDS_6:11

for s being State of SCMPDS
for I, J being Program of SCMPDS
for l being Instruction-Location of SCMPDS holds s +* (I +* (Start-At l)),s +* (J +* (Start-At l)) equal_outside NAT

proof end;

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
s1 +* (Initialized I),s2 +* (Initialized J) equal_outside NAT

proof end;

theorem :: SCMPDS_6:13

canceled;

theorem Th14: :: SCMPDS_6:14

for s being State of SCMPDS
for l1, l2 being Instruction-Location of SCMPDS holds (s +* (Start-At l1)) +* (Start-At l2) = s +* (Start-At l2)

proof end;

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) . (inspos 0 ) = i

proof end;

theorem Th17: :: SCMPDS_6:17

for I being Program of SCMPDS holds I c= Initialized (stop I)

proof end;

theorem Th18: :: SCMPDS_6:18

for loc being Instruction-Location of SCMPDS
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 Instruction-Location of SCMPDS
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 Instruction-Location of SCMPDS
for I being Program of SCMPDS st loc in dom I holds
(Initialized (stop I)) . loc = I . loc

proof end;

theorem :: SCMPDS_6:21

for s being State of SCMPDS
for I being Program of SCMPDS holds IC (s +* (Initialized I)) = inspos 0 by FUNCT_4:26, SCMPDS_5:18;

theorem Th22: :: SCMPDS_6:22

for i being Instruction of SCMPDS
for s being State of SCMPDS
for I being Program of SCMPDS holds CurInstr (s +* (Initialized (stop (i ';' I)))) = i

proof end;

theorem Th23: :: SCMPDS_6:23

for s being State of SCMPDS
for m1, m2 being Element of NAT st IC s = inspos m1 holds
ICplusConst s,m2 = inspos (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
( inspos (card I) in dom (stop I) & (stop I) . (inspos (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 x, l being Instruction-Location of SCMPDS holds (IExec J,s) . x = ((IExec I,s) +* (Start-At l)) . x

proof end;

theorem Th27: :: SCMPDS_6:27

for s being State of SCMPDS
for I being Program of SCMPDS
for x, l being Instruction-Location of SCMPDS holds (IExec I,s) . x = (s +* (Start-At l)) . x

proof end;

theorem :: SCMPDS_6:28

for s being 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),s) . a = (IExec J,(Exec i,(Initialized s))) . a

proof end;

theorem Th29: :: SCMPDS_6:29

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

proof end;

theorem Th30: :: SCMPDS_6:30

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

proof end;

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

end;

:: deftheorem defines Goto SCMPDS_6:def 1 :

registration

let n be Element of NAT ;
cluster goto (n + 1) -> No-StopCode ;
correctness by SCMPDS_5:25;
cluster goto (- (n + 1)) -> No-StopCode ;
correctness

proof end;

end;

registration

let n be Element of NAT ;
cluster Goto (n + 1) -> No-StopCode ;
correctness ;
cluster Goto (- (n + 1)) -> No-StopCode ;
correctness ;

end;

Lm1: for k1 being Integer holds
( inspos 0 in dom ((inspos 0 ) .--> (goto k1)) & ((inspos 0 ) .--> (goto k1)) . (inspos 0 ) = goto k1 )

proof end;

theorem :: SCMPDS_6:32

canceled;

theorem Th33: :: SCMPDS_6:33

for k1 being Integer holds
( inspos 0 in dom (Goto k1) & (Goto k1) . (inspos 0 ) = goto k1 )

proof end;

begin

definition

let I be Program of SCMPDS ;
let s be State of SCMPDS ;
pred I is_closed_on s means :Def2: :: SCMPDS_6:def 2
for k being Element of NAT holds IC (Computation (s +* (Initialized (stop I))),k) in dom (stop I);
pred I is_halting_on s means :Def3: :: SCMPDS_6:def 3
ProgramPart (s +* (Initialized (stop I))) halts_on s +* (Initialized (stop I));

end;

:: deftheorem Def2 defines is_closed_on SCMPDS_6:def 2 :

:: deftheorem Def3 defines is_halting_on SCMPDS_6:def 3 :

theorem Th34: :: SCMPDS_6:34

for I being Program of SCMPDS holds
( I is paraclosed iff for s being State of SCMPDS holds I is_closed_on s )

proof end;

theorem Th35: :: SCMPDS_6:35

for I being Program of SCMPDS holds
( I is parahalting iff for s being State of SCMPDS holds I is_halting_on s )

proof end;

theorem Th36: :: SCMPDS_6:36

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

proof end;

theorem :: SCMPDS_6:37

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

proof end;

theorem Th38: :: SCMPDS_6:38

for s being State of SCMPDS
for I, J being Program of SCMPDS holds
( I is_closed_on s iff I is_closed_on s +* (Initialized J) )

proof end;

theorem Th39: :: SCMPDS_6:39

for I, J being Program of SCMPDS
for s being State of SCMPDS st I is_closed_on s & I is_halting_on s holds
( ( for k being Element of NAT st k <= LifeSpan (s +* (Initialized (stop I))) holds
IC (Computation (s +* (Initialized (stop I))),k) = IC (Computation (s +* (Initialized (stop (I ';' J)))),k) ) & DataPart (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = DataPart (Computation (s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) )

proof end;

theorem Th40: :: SCMPDS_6:40

for s being State of SCMPDS
for I being Program of SCMPDS
for k being Element of NAT st I is_closed_on s & I is_halting_on s & k < LifeSpan (s +* (Initialized (stop I))) holds
IC (Computation (s +* (Initialized (stop I))),k) in dom I

proof end;

theorem Th41: :: SCMPDS_6:41

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 & I is_halting_on s & k < LifeSpan (s +* (Initialized (stop I))) holds
CurInstr (Computation (s +* (Initialized (stop I))),k) = CurInstr (Computation (s +* (Initialized (stop (I ';' J)))),k)

proof end;

theorem Th42: :: SCMPDS_6:42

for I being No-StopCode Program of SCMPDS
for s being State of SCMPDS
for k being Element of NAT st I is_closed_on s & I is_halting_on s & k < LifeSpan (s +* (Initialized (stop I))) holds
CurInstr (Computation (s +* (Initialized (stop I))),k) <> halt SCMPDS

proof end;

theorem Th43: :: SCMPDS_6:43

for I being No-StopCode Program of SCMPDS
for s being State of SCMPDS st I is_closed_on s & I is_halting_on s holds
IC (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = inspos (card I)

proof end;

proof end;

theorem Th44: :: SCMPDS_6:44

for I, J being Program of SCMPDS
for s being State of SCMPDS st I is_closed_on s & I is_halting_on s holds
( (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s & (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s )

proof end;

theorem Th45: :: SCMPDS_6:45

for s1, s2 being State of SCMPDS
for I being shiftable Program of SCMPDS st Initialized (stop I) c= s1 & I is_closed_on s1 holds
for n being Element of NAT st Shift (stop I),n c= s2 & IC s2 = inspos n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Computation s1,i)) + n = IC (Computation s2,i) & CurInstr (Computation s1,i) = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) )

proof end;

theorem Th46: :: SCMPDS_6:46

for s being State of SCMPDS
for I being No-StopCode Program of SCMPDS
for J being Program of SCMPDS st I is_closed_on s & I is_halting_on s holds
IC (IExec ((I ';' (Goto ((card J) + 1))) ';' J),s) = inspos (((card I) + (card J)) + 1)

proof end;

theorem Th47: :: SCMPDS_6:47

for s being State of SCMPDS
for I being No-StopCode Program of SCMPDS
for J being Program of SCMPDS st I is_closed_on s & I is_halting_on s holds
IExec ((I ';' (Goto ((card J) + 1))) ';' J),s = (IExec I,s) +* (Start-At (inspos (((card I) + (card J)) + 1)))

proof end;

theorem Th48: :: SCMPDS_6:48

for s being State of SCMPDS
for I being No-StopCode Program of SCMPDS st I is_closed_on s & I is_halting_on s holds
IC (IExec I,s) = inspos (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 ;
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 ;
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 ;

end;

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

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

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

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 ;
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 ;
func if>0 a,k,I -> Program of SCMPDS equals :: SCMPDS_6:def 9
(a,k <=0_goto ((card I) + 1)) ';' I;
coherence ;
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 ;
func if<0 a,k,I -> Program of SCMPDS equals :: SCMPDS_6:def 11
(a,k >=0_goto ((card I) + 1)) ';' I;
coherence ;
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 ;

end;

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

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

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

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

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

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

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

theorem :: SCMPDS_6:50

for a being Int_position
for k1 being Integer
for I, J being Program of SCMPDS holds
( inspos 0 in dom (if=0 a,k1,I,J) & inspos 1 in dom (if=0 a,k1,I,J) )

proof end;

Lm4: for i being Instruction of SCMPDS
for I, J, K being Program of SCMPDS holds (((i ';' I) ';' J) ';' K) . (inspos 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) . (inspos 0 ) = a,k1 <>0_goto ((card I) + 2) by Lm4;

Lm5: for n being Element of NAT
for i being Instruction of SCMPDS
for s being State of SCMPDS
for I being Program of SCMPDS holds Shift (stop I),1 c= Computation (s +* (Initialized (stop (i ';' I)))),n

proof end;

Lm6: for n being Element of NAT
for i, j being Instruction of SCMPDS
for s being State of SCMPDS
for I being Program of SCMPDS holds Shift (stop I),2 c= Computation (s +* (Initialized (stop ((i ';' j) ';' I)))),n

proof end;

theorem Th52: :: SCMPDS_6:52

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 & I is_halting_on s holds
( if=0 a,k1,I,J is_closed_on s & if=0 a,k1,I,J is_halting_on s )

proof end;

theorem Th53: :: SCMPDS_6:53

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 & J is_halting_on s holds
( if=0 a,k1,I,J is_closed_on s & if=0 a,k1,I,J is_halting_on s )

proof end;

theorem Th54: :: SCMPDS_6:54

for s being State of SCMPDS
for I being shiftable No-StopCode 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 & I is_halting_on s holds
IExec (if=0 a,k1,I,J),s = (IExec I,s) +* (Start-At (inspos (((card I) + (card J)) + 2)))

proof end;

theorem Th55: :: SCMPDS_6:55

for s being State of SCMPDS
for I being Program of SCMPDS
for J being shiftable No-StopCode Program of SCMPDS
for a being Int_position
for k1 being Integer st s . (DataLoc (s . a),k1) <> 0 & J is_closed_on s & J is_halting_on s holds
IExec (if=0 a,k1,I,J),s = (IExec J,s) +* (Start-At (inspos (((card I) + (card J)) + 2)))

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

proof end;

end;

registration

let I, J be No-StopCode Program of SCMPDS ;
let a be Int_position ;
let k1 be Integer;
cluster if=0 a,k1,I,J -> No-StopCode ;
coherence ;

end;

theorem :: SCMPDS_6:56

for s being State of SCMPDS
for I, J being parahalting shiftable No-StopCode Program of SCMPDS
for a being Int_position
for k1 being Integer holds IC (IExec (if=0 a,k1,I,J),s) = inspos (((card I) + (card J)) + 2)

proof end;

theorem :: SCMPDS_6:57

for s being State of SCMPDS
for I being parahalting shiftable No-StopCode 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),s) . b = (IExec I,s) . b

proof end;

theorem :: SCMPDS_6:58

for s being State of SCMPDS
for I being Program of SCMPDS
for J being parahalting shiftable No-StopCode 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),s) . b = (IExec J,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 inspos 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) . (inspos 0 ) = a,k1 <>0_goto ((card I) + 1) by Th16;

theorem Th62: :: SCMPDS_6:62

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 & I is_halting_on s holds
( if=0 a,k1,I is_closed_on s & if=0 a,k1,I is_halting_on s )

proof end;

theorem Th63: :: SCMPDS_6:63

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 & if=0 a,k1,I is_halting_on s )

proof end;

theorem Th64: :: SCMPDS_6:64

for s being State of SCMPDS
for I being shiftable No-StopCode Program of SCMPDS
for a being Int_position
for k1 being Integer st s . (DataLoc (s . a),k1) = 0 & I is_closed_on s & I is_halting_on s holds
IExec (if=0 a,k1,I),s = (IExec I,s) +* (Start-At (inspos ((card I) + 1)))

proof end;

Lm7: for s being State of SCMPDS
for loc being Instruction-Location of SCMPDS holds (s +* (Start-At loc)) . (IC SCMPDS ) = loc

proof end;

theorem Th65: :: SCMPDS_6:65

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),s = s +* (Start-At (inspos ((card I) + 1)))

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

proof end;

end;

registration

let I be No-StopCode Program of SCMPDS ;
let a be Int_position ;
let k1 be Integer;
cluster if=0 a,k1,I -> No-StopCode ;
coherence ;

end;

theorem :: SCMPDS_6:66

for s being State of SCMPDS
for I being parahalting shiftable No-StopCode Program of SCMPDS
for a being Int_position
for k1 being Integer holds IC (IExec (if=0 a,k1,I),s) = inspos ((card I) + 1)

proof end;

theorem :: SCMPDS_6:67

for s being State of SCMPDS
for I being parahalting shiftable No-StopCode 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),s) . b = (IExec I,s) . b

proof end;

theorem :: SCMPDS_6:68

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),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
( inspos 0 in dom ((i ';' j) ';' I) & inspos 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
( inspos 0 in dom (if<>0 a,k1,I) & inspos 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) . (inspos 0 ) = i & ((i ';' j) ';' I) . (inspos 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) . (inspos 0 ) = a,k1 <>0_goto 2 & (if<>0 a,k1,I) . (inspos 1) = goto ((card I) + 1) ) by Lm10;

theorem Th72: :: SCMPDS_6:72

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 & I is_halting_on s holds
( if<>0 a,k1,I is_closed_on s & if<>0 a,k1,I is_halting_on s )

proof end;

theorem Th73: :: SCMPDS_6:73

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 & if<>0 a,k1,I is_halting_on s )

proof end;

theorem Th74: :: SCMPDS_6:74

for s being State of SCMPDS
for I being shiftable No-StopCode Program of SCMPDS
for a being Int_position
for k1 being Integer st s . (DataLoc (s . a),k1) <> 0 & I is_closed_on s & I is_halting_on s holds
IExec (if<>0 a,k1,I),s = (IExec I,s) +* (Start-At (inspos ((card I) + 2)))

proof end;

theorem Th75: :: SCMPDS_6:75

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),s = s +* (Start-At (inspos ((card I) + 2)))

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

proof end;

end;

registration

let I be No-StopCode Program of SCMPDS ;
let a be Int_position ;
let k1 be Integer;
cluster if<>0 a,k1,I -> No-StopCode ;
coherence ;

end;

theorem :: SCMPDS_6:76

for s being State of SCMPDS
for I being parahalting shiftable No-StopCode Program of SCMPDS
for a being Int_position
for k1 being Integer holds IC (IExec (if<>0 a,k1,I),s) = inspos ((card I) + 2)

proof end;

theorem :: SCMPDS_6:77

for s being State of SCMPDS
for I being parahalting shiftable No-StopCode 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),s) . b = (IExec I,s) . b

proof end;

theorem :: SCMPDS_6:78

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),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 Lm3;

theorem :: SCMPDS_6:80

for a being Int_position
for k1 being Integer
for I, J being Program of SCMPDS holds
( inspos 0 in dom (if>0 a,k1,I,J) & inspos 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) . (inspos 0 ) = a,k1 <=0_goto ((card I) + 2) by Lm4;

theorem Th82: :: SCMPDS_6:82

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 & I is_halting_on s holds
( if>0 a,k1,I,J is_closed_on s & if>0 a,k1,I,J is_halting_on s )

proof end;

theorem Th83: :: SCMPDS_6:83

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 & J is_halting_on s holds
( if>0 a,k1,I,J is_closed_on s & if>0 a,k1,I,J is_halting_on s )

proof end;

theorem Th84: :: SCMPDS_6:84

for s being State of SCMPDS
for I being shiftable No-StopCode 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 & I is_halting_on s holds
IExec (if>0 a,k1,I,J),s = (IExec I,s) +* (Start-At (inspos (((card I) + (card J)) + 2)))

proof end;

theorem Th85: :: SCMPDS_6:85

for s being State of SCMPDS
for I being Program of SCMPDS
for J being shiftable No-StopCode Program of SCMPDS
for a being Int_position
for k1 being Integer st s . (DataLoc (s . a),k1) <= 0 & J is_closed_on s & J is_halting_on s holds
IExec (if>0 a,k1,I,J),s = (IExec J,s) +* (Start-At (inspos (((card I) + (card J)) + 2)))

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

proof end;

end;

registration

let I, J be No-StopCode Program of SCMPDS ;
let a be Int_position ;
let k1 be Integer;
cluster if>0 a,k1,I,J -> No-StopCode ;
coherence ;

end;

theorem :: SCMPDS_6:86

for s being State of SCMPDS
for I, J being parahalting shiftable No-StopCode Program of SCMPDS
for a being Int_position
for k1 being Integer holds IC (IExec (if>0 a,k1,I,J),s) = inspos (((card I) + (card J)) + 2)

proof end;

theorem :: SCMPDS_6:87

for s being State of SCMPDS
for I being parahalting shiftable No-StopCode 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),s) . b = (IExec I,s) . b

proof end;

theorem :: SCMPDS_6:88

for s being State of SCMPDS
for I being Program of SCMPDS
for J being parahalting shiftable No-StopCode 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),s) . b = (IExec J,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 inspos 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) . (inspos 0 ) = a,k1 <=0_goto ((card I) + 1) by Th16;

theorem Th92: :: SCMPDS_6:92

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 & I is_halting_on s holds
( if>0 a,k1,I is_closed_on s & if>0 a,k1,I is_halting_on s )

proof end;

theorem Th93: :: SCMPDS_6:93

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 & if>0 a,k1,I is_halting_on s )

proof end;

theorem Th94: :: SCMPDS_6:94

for s being State of SCMPDS
for I being shiftable No-StopCode Program of SCMPDS
for a being Int_position
for k1 being Integer st s . (DataLoc (s . a),k1) > 0 & I is_closed_on s & I is_halting_on s holds
IExec (if>0 a,k1,I),s = (IExec I,s) +* (Start-At (inspos ((card I) + 1)))

proof end;

theorem Th95: :: SCMPDS_6:95

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),s = s +* (Start-At (inspos ((card I) + 1)))

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

proof end;

end;

registration

let I be No-StopCode Program of SCMPDS ;
let a be Int_position ;
let k1 be Integer;
cluster if>0 a,k1,I -> No-StopCode ;
coherence ;

end;

theorem :: SCMPDS_6:96

for s being State of SCMPDS
for I being parahalting shiftable No-StopCode Program of SCMPDS
for a being Int_position
for k1 being Integer holds IC (IExec (if>0 a,k1,I),s) = inspos ((card I) + 1)

proof end;

theorem :: SCMPDS_6:97

for s being State of SCMPDS
for I being parahalting shiftable No-StopCode 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),s) . b = (IExec I,s) . b

proof end;

theorem :: SCMPDS_6:98

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),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
( inspos 0 in dom (if<=0 a,k1,I) & inspos 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) . (inspos 0 ) = a,k1 <=0_goto 2 & (if<=0 a,k1,I) . (inspos 1) = goto ((card I) + 1) ) by Lm10;

theorem Th102: :: SCMPDS_6:102

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 & I is_halting_on s holds
( if<=0 a,k1,I is_closed_on s & if<=0 a,k1,I is_halting_on s )

proof end;

theorem Th103: :: SCMPDS_6:103

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 & if<=0 a,k1,I is_halting_on s )

proof end;

theorem Th104: :: SCMPDS_6:104

for s being State of SCMPDS
for I being shiftable No-StopCode Program of SCMPDS
for a being Int_position
for k1 being Integer st s . (DataLoc (s . a),k1) <= 0 & I is_closed_on s & I is_halting_on s holds
IExec (if<=0 a,k1,I),s = (IExec I,s) +* (Start-At (inspos ((card I) + 2)))

proof end;

theorem Th105: :: SCMPDS_6:105

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),s = s +* (Start-At (inspos ((card I) + 2)))

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

proof end;

end;

registration

let I be No-StopCode Program of SCMPDS ;
let a be Int_position ;
let k1 be Integer;
cluster if<=0 a,k1,I -> No-StopCode ;
coherence ;

end;

theorem :: SCMPDS_6:106

for s being State of SCMPDS
for I being parahalting shiftable No-StopCode Program of SCMPDS
for a being Int_position
for k1 being Integer holds IC (IExec (if<=0 a,k1,I),s) = inspos ((card I) + 2)

proof end;

theorem :: SCMPDS_6:107

for s being State of SCMPDS
for I being parahalting shiftable No-StopCode 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),s) . b = (IExec I,s) . b

proof end;

theorem :: SCMPDS_6:108

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),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 Lm3;

theorem :: SCMPDS_6:110

for a being Int_position
for k1 being Integer
for I, J being Program of SCMPDS holds
( inspos 0 in dom (if<0 a,k1,I,J) & inspos 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) . (inspos 0 ) = a,k1 >=0_goto ((card I) + 2) by Lm4;

theorem Th112: :: SCMPDS_6:112

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 & I is_halting_on s holds
( if<0 a,k1,I,J is_closed_on s & if<0 a,k1,I,J is_halting_on s )

proof end;

theorem Th113: :: SCMPDS_6:113

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 & J is_halting_on s holds
( if<0 a,k1,I,J is_closed_on s & if<0 a,k1,I,J is_halting_on s )

proof end;

theorem Th114: :: SCMPDS_6:114

for s being State of SCMPDS
for I being shiftable No-StopCode 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 & I is_halting_on s holds
IExec (if<0 a,k1,I,J),s = (IExec I,s) +* (Start-At (inspos (((card I) + (card J)) + 2)))

proof end;

theorem Th115: :: SCMPDS_6:115

for s being State of SCMPDS
for I being Program of SCMPDS
for J being shiftable No-StopCode Program of SCMPDS
for a being Int_position
for k1 being Integer st s . (DataLoc (s . a),k1) >= 0 & J is_closed_on s & J is_halting_on s holds
IExec (if<0 a,k1,I,J),s = (IExec J,s) +* (Start-At (inspos (((card I) + (card J)) + 2)))

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

proof end;

end;

registration

let I, J be No-StopCode Program of SCMPDS ;
let a be Int_position ;
let k1 be Integer;
cluster if<0 a,k1,I,J -> No-StopCode ;
coherence ;

end;

theorem :: SCMPDS_6:116

for s being State of SCMPDS
for I, J being parahalting shiftable No-StopCode Program of SCMPDS
for a being Int_position
for k1 being Integer holds IC (IExec (if<0 a,k1,I,J),s) = inspos (((card I) + (card J)) + 2)

proof end;

theorem :: SCMPDS_6:117

for s being State of SCMPDS
for I being parahalting shiftable No-StopCode 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),s) . b = (IExec I,s) . b

proof end;

theorem :: SCMPDS_6:118

for s being State of SCMPDS
for I being Program of SCMPDS
for J being parahalting shiftable No-StopCode 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),s) . b = (IExec J,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 inspos 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) . (inspos 0 ) = a,k1 >=0_goto ((card I) + 1) by Th16;

theorem Th122: :: SCMPDS_6:122

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 & I is_halting_on s holds
( if<0 a,k1,I is_closed_on s & if<0 a,k1,I is_halting_on s )

proof end;

theorem Th123: :: SCMPDS_6:123

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 & if<0 a,k1,I is_halting_on s )

proof end;

theorem Th124: :: SCMPDS_6:124

for s being State of SCMPDS
for I being shiftable No-StopCode Program of SCMPDS
for a being Int_position
for k1 being Integer st s . (DataLoc (s . a),k1) < 0 & I is_closed_on s & I is_halting_on s holds
IExec (if<0 a,k1,I),s = (IExec I,s) +* (Start-At (inspos ((card I) + 1)))

proof end;

theorem Th125: :: SCMPDS_6:125

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),s = s +* (Start-At (inspos ((card I) + 1)))

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

proof end;

end;

registration

let I be No-StopCode Program of SCMPDS ;
let a be Int_position ;
let k1 be Integer;
cluster if<0 a,k1,I -> No-StopCode ;
coherence ;

end;

theorem :: SCMPDS_6:126

for s being State of SCMPDS
for I being parahalting shiftable No-StopCode Program of SCMPDS
for a being Int_position
for k1 being Integer holds IC (IExec (if<0 a,k1,I),s) = inspos ((card I) + 1)

proof end;

theorem :: SCMPDS_6:127

for s being State of SCMPDS
for I being parahalting shiftable No-StopCode 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),s) . b = (IExec I,s) . b

proof end;

theorem :: SCMPDS_6:128

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),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
( inspos 0 in dom (if>=0 a,k1,I) & inspos 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) . (inspos 0 ) = a,k1 >=0_goto 2 & (if>=0 a,k1,I) . (inspos 1) = goto ((card I) + 1) ) by Lm10;

theorem Th132: :: SCMPDS_6:132

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 & I is_halting_on s holds
( if>=0 a,k1,I is_closed_on s & if>=0 a,k1,I is_halting_on s )

proof end;

theorem Th133: :: SCMPDS_6:133

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 & if>=0 a,k1,I is_halting_on s )

proof end;

theorem Th134: :: SCMPDS_6:134

for s being State of SCMPDS
for I being shiftable No-StopCode Program of SCMPDS
for a being Int_position
for k1 being Integer st s . (DataLoc (s . a),k1) >= 0 & I is_closed_on s & I is_halting_on s holds
IExec (if>=0 a,k1,I),s = (IExec I,s) +* (Start-At (inspos ((card I) + 2)))

proof end;

theorem Th135: :: SCMPDS_6:135

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),s = s +* (Start-At (inspos ((card I) + 2)))

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

proof end;

end;

registration

let I be No-StopCode Program of SCMPDS ;
let a be Int_position ;
let k1 be Integer;
cluster if>=0 a,k1,I -> No-StopCode ;
coherence ;

end;

theorem :: SCMPDS_6:136

for s being State of SCMPDS
for I being parahalting shiftable No-StopCode Program of SCMPDS
for a being Int_position
for k1 being Integer holds IC (IExec (if>=0 a,k1,I),s) = inspos ((card I) + 2)

proof end;

theorem :: SCMPDS_6:137

for s being State of SCMPDS
for I being parahalting shiftable No-StopCode 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),s) . b = (IExec I,s) . b

proof end;

theorem :: SCMPDS_6:138

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),s) . b = s . b

proof end;