:: Computation of Two Consecutive Program Blocks for SCMPDS
:: by JingChao Chen
::
:: Received June 15, 1999
:: Copyright (c) 1999 Association of Mizar Users

begin

theorem :: SCMPDS_5:1

canceled;

LL: card (Stop SCMPDS ) = 1
by COMPOS_1:46;

theorem Th2: :: SCMPDS_5:2

for x being set
for i being Instruction of SCMPDS holds
( x in dom (Load i) iff x = 0 )

proof end;

theorem Th3: :: SCMPDS_5:3

for loc being Element of NAT
for I being Program of SCMPDS st loc in dom (stop I) & (stop I) . loc <> halt SCMPDS holds
loc in dom I

proof end;

theorem :: SCMPDS_5:4

for i being Instruction of SCMPDS holds
( dom (Load i) = {0 } & (Load i) . 0 = i ) by FUNCOP_1:19, FUNCOP_1:87;

theorem Th5: :: SCMPDS_5:5

for i being Instruction of SCMPDS holds 0 in dom (Load i)

proof end;

theorem Th6: :: SCMPDS_5:6

for i being Instruction of SCMPDS holds card (Load i) = 1

proof end;

theorem :: SCMPDS_5:7

for I being Program of SCMPDS holds card (stop I) = (card I) + 1 by LL, SCMPDS_4:45;

theorem Th8: :: SCMPDS_5:8

for i being Instruction of SCMPDS holds card (stop (Load i)) = 2

proof end;

theorem Th9: :: SCMPDS_5:9

for i being Instruction of SCMPDS holds
( 0 in dom (stop (Load i)) & 1 in dom (stop (Load i)) )

proof end;

theorem Th10: :: SCMPDS_5:10

for i being Instruction of SCMPDS holds
( (stop (Load i)) . 0 = i & (stop (Load i)) . 1 = halt SCMPDS )

proof end;

theorem Th11: :: SCMPDS_5:11

for x being set
for i being Instruction of SCMPDS holds
( x in dom (stop (Load i)) iff ( x = 0 or x = 1 ) )

proof end;

theorem :: SCMPDS_5:12

for i being Instruction of SCMPDS holds dom (stop (Load i)) = {0 ,1}

proof end;

theorem Th13: :: SCMPDS_5:13

for i being Instruction of SCMPDS holds
( 0 in dom (Initialize (stop (Load i))) & 1 in dom (Initialize (stop (Load i))) & (Initialize (stop (Load i))) . 0 = i & (Initialize (stop (Load i))) . 1 = halt SCMPDS )

proof end;

theorem :: SCMPDS_5:14

canceled;

theorem Th15: :: SCMPDS_5:15

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

proof end;

theorem Th16: :: SCMPDS_5:16

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

proof end;

theorem Th17: :: SCMPDS_5:17

for I, J being Program of SCMPDS holds (Initialize (stop I)) +* (Initialize (stop (I ';' J))) = Initialize (stop (I ';' J))

proof end;

theorem Th18: :: SCMPDS_5:18

for s being State of SCMPDS
for I being Program of SCMPDS st Initialize I c= s holds
IC s = 0

proof end;

theorem Th19: :: SCMPDS_5:19

for a being Int_position
for s being State of SCMPDS
for I being Program of SCMPDS holds ((Initialize s) +* I) . a = s . a

proof end;

theorem Th20: :: SCMPDS_5:20

for s1, s2 being State of SCMPDS
for I being parahalting Program of SCMPDS st Initialize (stop I) c= s1 & Initialize (stop I) c= s2 & s1,s2 equal_outside NAT holds
for k being Element of NAT holds
( Comput (ProgramPart s1),s1,k, Comput (ProgramPart s2),s2,k equal_outside NAT & CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,k) = CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,k) )

proof end;

theorem Th21: :: SCMPDS_5:21

for s1, s2 being State of SCMPDS
for I being parahalting Program of SCMPDS st Initialize (stop I) c= s1 & Initialize (stop I) c= s2 & s1,s2 equal_outside NAT holds
( LifeSpan (ProgramPart s1),s1 = LifeSpan (ProgramPart s2),s2 & Result (ProgramPart s1),s1, Result (ProgramPart s2),s2 equal_outside NAT )

proof end;

theorem Th22: :: SCMPDS_5:22

for s being State of SCMPDS
for I being Program of SCMPDS holds IC (IExec I,s) = IC (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))

proof end;

theorem Th23: :: SCMPDS_5:23

for s being State of SCMPDS
for I being parahalting Program of SCMPDS
for J being Program of SCMPDS st Initialize (stop I) c= s holds
for m being Element of NAT st m <= LifeSpan (ProgramPart s),s holds
Comput (ProgramPart s),s,m, Comput (ProgramPart (s +* (I ';' J))),(s +* (I ';' J)),m equal_outside NAT

proof end;

theorem Th24: :: SCMPDS_5:24

for s being State of SCMPDS
for I being parahalting Program of SCMPDS
for J being Program of SCMPDS st Initialize (stop I) c= s holds
for m being Element of NAT st m <= LifeSpan (ProgramPart s),s holds
Comput (ProgramPart s),s,m, Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),m equal_outside NAT

proof end;

Lm1: Load ((DataLoc 0 ,0 ) := 0 ) is parahalting

proof end;

begin

definition

let i be Instruction of SCMPDS ;
attr i is No-StopCode means :Def1: :: SCMPDS_5:def 1
i <> halt SCMPDS ;

end;

:: deftheorem Def1 defines No-StopCode SCMPDS_5:def 1 :
for i being Instruction of SCMPDS holds
( i is No-StopCode iff i <> halt SCMPDS );

definition

let i be Instruction of SCMPDS ;
attr i is parahalting means :Def2: :: SCMPDS_5:def 2
Load i is parahalting ;

end;

:: deftheorem Def2 defines parahalting SCMPDS_5:def 2 :
for i being Instruction of SCMPDS holds
( i is parahalting iff Load i is parahalting );

registration

cluster shiftable No-StopCode parahalting Element of the Instructions of SCMPDS ;
existence
ex b₁ being Instruction of SCMPDS st
( b₁ is No-StopCode & b₁ is shiftable & b₁ is parahalting )

proof end;

end;

theorem :: SCMPDS_5:25

for k1 being Integer st k1 <> 0 holds
goto k1 is No-StopCode

proof end;

registration

let a be Int_position ;
cluster return a -> No-StopCode ;
coherence
return a is No-StopCode

proof end;

end;

registration

let a be Int_position ;
let k1 be Integer;
cluster a := k1 -> No-StopCode ;
coherence
a := k1 is No-StopCode

proof end;

cluster saveIC a,k1 -> No-StopCode ;
coherence
saveIC a,k1 is No-StopCode

proof end;

end;

registration

let a be Int_position ;
let k1, k2 be Integer;
cluster a,k1 <>0_goto k2 -> No-StopCode ;
coherence
a,k1 <>0_goto k2 is No-StopCode

proof end;

cluster a,k1 <=0_goto k2 -> No-StopCode ;
coherence
a,k1 <=0_goto k2 is No-StopCode

proof end;

cluster a,k1 >=0_goto k2 -> No-StopCode ;
coherence
a,k1 >=0_goto k2 is No-StopCode

proof end;

cluster a,k1 := k2 -> No-StopCode ;
coherence
a,k1 := k2 is No-StopCode

proof end;

end;

registration

let a be Int_position ;
let k1, k2 be Integer;
cluster AddTo a,k1,k2 -> No-StopCode ;
coherence
AddTo a,k1,k2 is No-StopCode

proof end;

end;

registration

let a, b be Int_position ;
let k1, k2 be Integer;
cluster AddTo a,k1,b,k2 -> No-StopCode ;
coherence
AddTo a,k1,b,k2 is No-StopCode

proof end;

cluster SubFrom a,k1,b,k2 -> No-StopCode ;
coherence
SubFrom a,k1,b,k2 is No-StopCode

proof end;

cluster MultBy a,k1,b,k2 -> No-StopCode ;
coherence
MultBy a,k1,b,k2 is No-StopCode

proof end;

cluster Divide a,k1,b,k2 -> No-StopCode ;
coherence
Divide a,k1,b,k2 is No-StopCode

proof end;

cluster a,k1 := b,k2 -> No-StopCode ;
coherence
a,k1 := b,k2 is No-StopCode

proof end;

end;

registration

cluster halt SCMPDS -> parahalting ;
coherence
halt SCMPDS is parahalting

proof end;

end;

registration

let i be parahalting Instruction of SCMPDS ;
cluster Load i -> parahalting Program of SCMPDS ;
coherence
for b₁ being Program of SCMPDS st b₁ = Load i holds
b₁ is parahalting by Def2;

end;

Lm2: for i being Instruction of SCMPDS st ( for s being State of SCMPDS holds (Exec i,s) . (IC SCMPDS ) = succ (IC s) ) holds
Load i is parahalting

proof end;

registration

let a be Int_position ;
let k1 be Integer;
cluster a := k1 -> parahalting ;
coherence
a := k1 is parahalting

proof end;

end;

registration

let a be Int_position ;
let k1, k2 be Integer;
cluster a,k1 := k2 -> parahalting ;
coherence
a,k1 := k2 is parahalting

proof end;

cluster AddTo a,k1,k2 -> parahalting ;
coherence
AddTo a,k1,k2 is parahalting

proof end;

end;

registration

let a, b be Int_position ;
let k1, k2 be Integer;
cluster AddTo a,k1,b,k2 -> parahalting ;
coherence
AddTo a,k1,b,k2 is parahalting

proof end;

cluster SubFrom a,k1,b,k2 -> parahalting ;
coherence
SubFrom a,k1,b,k2 is parahalting

proof end;

cluster MultBy a,k1,b,k2 -> parahalting ;
coherence
MultBy a,k1,b,k2 is parahalting

proof end;

cluster Divide a,k1,b,k2 -> parahalting ;
coherence
Divide a,k1,b,k2 is parahalting

proof end;

cluster a,k1 := b,k2 -> parahalting ;
coherence
a,k1 := b,k2 is parahalting

proof end;

end;

theorem Th26: :: SCMPDS_5:26

for i being Instruction of SCMPDS st InsCode i = 1 holds
not i is parahalting

proof end;

definition

let N be with_non-empty_elements set ;
let S be halting AMI-Struct of N;
let IT be NAT -defined the Instructions of S -valued Function;
redefine attr IT is halt-free means :Def3: :: SCMPDS_5:def 3
for x being Element of NAT st x in dom IT holds
IT . x <> halt S;
compatibility
( IT is halt-free iff for x being Element of NAT st x in dom IT holds
IT . x <> halt S )

proof end;

end;

:: deftheorem Def3 defines halt-free SCMPDS_5:def 3 :
for N being with_non-empty_elements set
for S being halting AMI-Struct of N
for IT being NAT -defined the Instructions of b₂ -valued Function holds
( IT is halt-free iff for x being Element of NAT st x in dom IT holds
IT . x <> halt S );

registration

cluster V11() Relation-like NAT -defined the carrier of SCMPDS -defined the Instructions of SCMPDS -valued Function-like the Object-Kind of SCMPDS -compatible V32() V68() halt-free parahalting shiftable set ;
existence
ex b₁ being Program of SCMPDS st
( b₁ is parahalting & b₁ is shiftable & b₁ is halt-free )

proof end;

end;

registration

let I, J be halt-free Program of SCMPDS ;
cluster I ';' J -> halt-free ;
coherence
I ';' J is halt-free

proof end;

end;

registration

let i be No-StopCode Instruction of SCMPDS ;
cluster Load i -> halt-free ;
coherence
Load i is halt-free

proof end;

end;

registration

let i be No-StopCode Instruction of SCMPDS ;
let J be halt-free Program of SCMPDS ;
cluster i ';' J -> halt-free ;
coherence
i ';' J is halt-free ;

end;

registration

let I be halt-free Program of SCMPDS ;
let j be No-StopCode Instruction of SCMPDS ;
cluster I ';' j -> halt-free ;
coherence
I ';' j is halt-free ;

end;

registration

let i, j be No-StopCode Instruction of SCMPDS ;
cluster i ';' j -> halt-free ;
coherence
i ';' j is halt-free ;

end;

theorem Th27: :: SCMPDS_5:27

for s being State of SCMPDS
for I being halt-free parahalting Program of SCMPDS st Initialize (stop I) c= s holds
IC (Comput (ProgramPart s),s,(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = card I

proof end;

theorem Th28: :: SCMPDS_5:28

for s being State of SCMPDS
for I being parahalting Program of SCMPDS
for k being Element of NAT st k < LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)) holds
IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k) in dom I

proof end;

theorem Th29: :: SCMPDS_5:29

for s being State of SCMPDS
for I being parahalting Program of SCMPDS
for k being Element of NAT st Initialize I c= s & k <= LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)) holds
Comput (ProgramPart s),s,k, Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k equal_outside NAT

proof end;

theorem Th30: :: SCMPDS_5:30

for s being State of SCMPDS
for I being halt-free parahalting Program of SCMPDS st Initialize I c= s holds
IC (Comput (ProgramPart s),s,(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = card I

proof end;

theorem Th31: :: SCMPDS_5:31

for s being State of SCMPDS
for I being parahalting Program of SCMPDS holds
( not Initialize I c= s or CurInstr (ProgramPart (Comput (ProgramPart s),s,(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))),(Comput (ProgramPart s),s,(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = halt SCMPDS or IC (Comput (ProgramPart s),s,(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = card I )

proof end;

theorem Th32: :: SCMPDS_5:32

for s being State of SCMPDS
for I being halt-free parahalting Program of SCMPDS
for k being Element of NAT st Initialize I c= s & k < LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)) holds
CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) <> halt SCMPDS

proof end;

theorem Th33: :: SCMPDS_5:33

for s being State of SCMPDS
for I being parahalting Program of SCMPDS
for J being Program of SCMPDS
for k being Element of NAT st k <= LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)) holds
Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k, Comput (ProgramPart (s +* ((I ';' J) +* (Start-At 0 ,SCMPDS )))),(s +* ((I ';' J) +* (Start-At 0 ,SCMPDS ))),k equal_outside NAT

proof end;

theorem Th34: :: SCMPDS_5:34

for s being State of SCMPDS
for I being parahalting Program of SCMPDS
for J being Program of SCMPDS
for k being Element of NAT st k <= LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)) holds
Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k, Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k equal_outside NAT

proof end;

registration

let I be parahalting Program of SCMPDS ;
let J be parahalting shiftable Program of SCMPDS ;
cluster I ';' J -> parahalting ;
coherence
I ';' J is parahalting

proof end;

end;

registration

let i be parahalting Instruction of SCMPDS ;
let J be parahalting shiftable Program of SCMPDS ;
cluster i ';' J -> parahalting ;
coherence
i ';' J is parahalting ;

end;

registration

let I be parahalting Program of SCMPDS ;
let j be shiftable parahalting Instruction of SCMPDS ;
cluster I ';' j -> parahalting ;
coherence
I ';' j is parahalting ;

end;

registration

let i be parahalting Instruction of SCMPDS ;
let j be shiftable parahalting Instruction of SCMPDS ;
cluster i ';' j -> parahalting ;
coherence
i ';' j is parahalting ;

end;

theorem Th35: :: SCMPDS_5:35

for m, n being Element of NAT
for s, s1 being State of SCMPDS
for J being parahalting shiftable Program of SCMPDS st s = Comput (ProgramPart (s1 +* (Initialize (stop J)))),(s1 +* (Initialize (stop J))),m holds
Exec (CurInstr (ProgramPart s),s),(s +* (Start-At ((IC s) + n),SCMPDS )) = (Following (ProgramPart s),s) +* (Start-At ((IC (Following (ProgramPart s),s)) + n),SCMPDS )

proof end;

begin

theorem :: SCMPDS_5:36

for s being State of SCMPDS
for I being halt-free parahalting Program of SCMPDS
for J being parahalting shiftable Program of SCMPDS
for k being Element of NAT st Initialize (stop (I ';' J)) c= s holds
(Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)),k)) + (card I)),SCMPDS ), Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + k) equal_outside NAT

proof end;

Lm3: for I being halt-free parahalting Program of SCMPDS
for J being parahalting shiftable Program of SCMPDS
for s, s1 being State of SCMPDS st Initialize (stop (I ';' J)) c= s & s1 = (Initialize s) +* (stop I) holds
( IC (Comput (ProgramPart s),s,(LifeSpan (ProgramPart s1),s1)) = card I & DataPart (Comput (ProgramPart s),s,(LifeSpan (ProgramPart s1),s1)) = DataPart ((Initialize (Comput (ProgramPart s1),s1,(LifeSpan (ProgramPart s1),s1))) +* (stop J)) & Shift (stop J),(card I) c= Comput (ProgramPart s),s,(LifeSpan (ProgramPart s1),s1) & LifeSpan (ProgramPart s),s = (LifeSpan (ProgramPart s1),s1) + (LifeSpan (ProgramPart ((Initialize (Result (ProgramPart s1),s1)) +* (stop J))),((Initialize (Result (ProgramPart s1),s1)) +* (stop J))) )

proof end;

theorem Th37: :: SCMPDS_5:37

for s being State of SCMPDS
for I being halt-free parahalting Program of SCMPDS
for J being parahalting shiftable Program of SCMPDS holds LifeSpan (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))) = (LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + (LifeSpan (ProgramPart ((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J))),((Initialize (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (stop J)))

proof end;

theorem Th38: :: SCMPDS_5:38

for s being State of SCMPDS
for I being halt-free parahalting Program of SCMPDS
for J being parahalting shiftable Program of SCMPDS holds IExec (I ';' J),s = (IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)),SCMPDS )

proof end;

theorem :: SCMPDS_5:39

for a being Int_position
for s being State of SCMPDS
for I being halt-free parahalting Program of SCMPDS
for J being parahalting shiftable Program of SCMPDS holds (IExec (I ';' J),s) . a = (IExec J,(IExec I,s)) . a

proof end;

begin

theorem Th40: :: SCMPDS_5:40

for a being Int_position
for s being State of SCMPDS
for loc being Element of NAT holds
( IC (Initialize s) = 0 & (Initialize s) . a = s . a & (Initialize s) . loc = s . loc )

proof end;

theorem Th41: :: SCMPDS_5:41

for s1, s2 being State of SCMPDS holds
( s1,s2 equal_outside NAT iff s1 | (SCM-Data-Loc \/ {(IC SCMPDS )}) = s2 | (SCM-Data-Loc \/ {(IC SCMPDS )}) )

proof end;

theorem :: SCMPDS_5:42

canceled;

theorem Th43: :: SCMPDS_5:43

for i being Instruction of SCMPDS
for s1, s2 being State of SCMPDS st DataPart s1 = DataPart s2 & InsCode i <> 3 holds
DataPart (Exec i,s1) = DataPart (Exec i,s2)

proof end;

theorem Th44: :: SCMPDS_5:44

for s1, s2 being State of SCMPDS
for i being shiftable Instruction of SCMPDS st DataPart s1 = DataPart s2 holds
DataPart (Exec i,s1) = DataPart (Exec i,s2)

proof end;

theorem Th45: :: SCMPDS_5:45

for s being State of SCMPDS
for i being parahalting Instruction of SCMPDS holds Exec i,(Initialize s) = IExec (Load i),s

proof end;

theorem Th46: :: SCMPDS_5:46

for a being Int_position
for s being State of SCMPDS
for I being halt-free parahalting Program of SCMPDS
for j being shiftable parahalting Instruction of SCMPDS holds (IExec (I ';' j),s) . a = (Exec j,(IExec I,s)) . a

proof end;

theorem :: SCMPDS_5:47

for a being Int_position
for s being State of SCMPDS
for i being No-StopCode parahalting Instruction of SCMPDS
for j being shiftable parahalting Instruction of SCMPDS holds (IExec (i ';' j),s) . a = (Exec j,(Exec i,(Initialize s))) . a

proof end;