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


begin

Lm1: card (Stop SCMPDS) = 1
by AFINSQ_1:33;

theorem :: SCMPDS_5:1
canceled;

theorem :: SCMPDS_5:2
canceled;

theorem :: SCMPDS_5:3
canceled;

theorem :: SCMPDS_5:4
canceled;

theorem :: SCMPDS_5:5
canceled;

theorem :: SCMPDS_5:6
canceled;

theorem :: SCMPDS_5:7
canceled;

theorem :: SCMPDS_5:8
canceled;

theorem :: SCMPDS_5:9
canceled;

theorem :: SCMPDS_5:10
canceled;

theorem :: SCMPDS_5:11
canceled;

theorem Th12: :: SCMPDS_5:12
for I, J being Program of SCMPDS holds I c= stop (I ';' J)
proof end;

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

theorem Th14: :: SCMPDS_5:14
for I, J being Program of SCMPDS holds (stop I) +* (stop (I ';' J)) = stop (I ';' J)
proof end;

set SA0 = Start-At (0,SCMPDS);

theorem Th15: :: SCMPDS_5:15
for a being Int_position
for s being State of SCMPDS holds (Initialize s) . a = s . a
proof end;

theorem Th16: :: SCMPDS_5:16
for P1, P2 being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being parahalting Program of SCMPDS st stop I c= P1 & stop I c= P2 holds
for k being Element of NAT holds
( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )
proof end;

theorem Th17: :: SCMPDS_5:17
for P1, P2 being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being parahalting Program of SCMPDS st stop I c= P1 & stop I c= P2 holds
( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )
proof end;

theorem :: SCMPDS_5:18
canceled;

theorem Th19: :: SCMPDS_5:19
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being parahalting Program of SCMPDS
for J being Program of SCMPDS st stop I c= P holds
for m being Element of NAT st m <= LifeSpan (P,s) holds
Comput (P,s,m) = Comput ((P +* (I ';' J)),s,m)
proof end;

theorem Th20: :: SCMPDS_5:20
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being parahalting Program of SCMPDS
for J being Program of SCMPDS st stop I c= P holds
for m being Element of NAT st m <= LifeSpan (P,s) holds
Comput (P,s,m) = Comput ((P +* (stop (I ';' J))),s,m)
proof end;

Lm2: Load ((DataLoc (0,0)) := 0) is parahalting
proof end;

begin

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

:: deftheorem SCMPDS_5:def 1 :
canceled;

:: 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 No-StopCode shiftable parahalting for Element of the InstructionsF of SCMPDS;
existence
ex b1 being Instruction of SCMPDS st
( b1 is No-StopCode & b1 is shiftable & b1 is parahalting )
proof end;
end;

theorem :: SCMPDS_5:21
for k1 being Integer 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 -> parahalting for Program of SCMPDS;
coherence
for b1 being Program of SCMPDS st b1 = Load i holds
b1 is parahalting by Def2;
end;

Lm3: for i being Instruction of SCMPDS st ( for s being State of SCMPDS holds (Exec (i,s)) . (IC ) = 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 Th22: :: SCMPDS_5:22
for i being Instruction of SCMPDS st InsCode i = 1 holds
not i is parahalting
proof end;

registration
cluster non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCMPDS -valued Function-like V35() V74() halt-free parahalting shiftable for set ;
existence
ex b1 being Program of SCMPDS st
( b1 is parahalting & b1 is shiftable & b1 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 -> 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 Th23: :: SCMPDS_5:23
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free parahalting Program of SCMPDS st stop I c= P holds
IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I
proof end;

theorem Th24: :: SCMPDS_5:24
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being parahalting Program of SCMPDS
for k being Element of NAT st k < LifeSpan ((P +* (stop I)),s) holds
IC (Comput ((P +* (stop I)),s,k)) in dom I
proof end;

theorem Th25: :: SCMPDS_5:25
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being parahalting Program of SCMPDS
for k being Element of NAT st I c= P & k <= LifeSpan ((P +* (stop I)),s) holds
Comput (P,s,k) = Comput ((P +* (stop I)),s,k)
proof end;

theorem Th26: :: SCMPDS_5:26
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free parahalting Program of SCMPDS st I c= P holds
IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I
proof end;

theorem Th27: :: SCMPDS_5:27
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being parahalting Program of SCMPDS holds
( not I c= P or CurInstr (P,(Comput (P,s,(LifeSpan ((P +* (stop I)),s))))) = halt SCMPDS or IC (Comput (P,s,(LifeSpan ((P +* (stop I)),s)))) = card I )
proof end;

theorem Th28: :: SCMPDS_5:28
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free parahalting Program of SCMPDS
for k being Element of NAT st I c= P & k < LifeSpan ((P +* (stop I)),s) holds
CurInstr (P,(Comput (P,s,k))) <> halt SCMPDS
proof end;

theorem Th29: :: SCMPDS_5:29
for P being Instruction-Sequence of SCMPDS
for s being 0 -started 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 ((P +* (stop I)),s) holds
Comput ((P +* (stop I)),s,k) = Comput ((P +* (I ';' J)),s,k)
proof end;

theorem Th30: :: SCMPDS_5:30
for P being Instruction-Sequence of SCMPDS
for s being 0 -started 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 ((P +* (stop I)),s) holds
Comput ((P +* (stop I)),s,k) = Comput ((P +* (stop (I ';' J))),s,k)
proof end;

registration
let I be parahalting Program of SCMPDS;
let J be parahalting shiftable Program of SCMPDS;
cluster I ';' J -> parahalting for Program of SCMPDS;
coherence
for b1 being Program of SCMPDS st b1 = I ';' J holds
b1 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 Th31: :: SCMPDS_5:31
for m, n being Element of NAT
for P, P1 being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for s1 being 0 -started State of SCMPDS
for J being parahalting shiftable Program of SCMPDS st stop J c= P & s = Comput ((P1 +* (stop J)),s1,m) holds
Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n)
proof end;

begin

theorem :: SCMPDS_5:32
for P being Instruction-Sequence of SCMPDS
for s being 0 -started 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 stop (I ';' J) c= P holds
IncIC ((Comput (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s))),k)),(card I)) = Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),s)) + k))
proof end;

Lm4: for P, P1 being Instruction-Sequence of SCMPDS
for I being halt-free parahalting Program of SCMPDS
for J being parahalting shiftable Program of SCMPDS
for s being 0 -started State of SCMPDS st stop (I ';' J) c= P & P1 = P +* (stop I) holds
( IC (Comput (P,s,(LifeSpan (P1,s)))) = card I & DataPart (Comput (P,s,(LifeSpan (P1,s)))) = DataPart (Initialize (Comput (P1,s,(LifeSpan (P1,s))))) & Shift ((stop J),(card I)) c= P & LifeSpan (P,s) = (LifeSpan (P1,s)) + (LifeSpan ((P1 +* (stop J)),(Initialize (Result (P1,s))))) )
proof end;

theorem Th33: :: SCMPDS_5:33
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free parahalting Program of SCMPDS
for J being parahalting shiftable Program of SCMPDS holds LifeSpan ((P +* (stop (I ';' J))),s) = (LifeSpan ((P +* (stop I)),s)) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),s)))))
proof end;

theorem Th34: :: SCMPDS_5:34
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free parahalting Program of SCMPDS
for J being parahalting shiftable Program of SCMPDS holds IExec ((I ';' J),P,s) = IncIC ((IExec (J,P,(Initialize (IExec (I,P,s))))),(card I))
proof end;

theorem :: SCMPDS_5:35
for a being Int_position
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free parahalting Program of SCMPDS
for J being parahalting shiftable Program of SCMPDS holds (IExec ((I ';' J),P,s)) . a = (IExec (J,P,(Initialize (IExec (I,P,s))))) . a
proof end;

begin

theorem :: SCMPDS_5:36
canceled;

theorem :: SCMPDS_5:37
for s1, s2 being State of SCMPDS st s1 | (SCM-Data-Loc \/ {(IC )}) = s2 | (SCM-Data-Loc \/ {(IC )}) holds
s1 = s2
proof end;

theorem Th38: :: SCMPDS_5:38
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 Th39: :: SCMPDS_5:39
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 Th40: :: SCMPDS_5:40
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for i being parahalting Instruction of SCMPDS holds Exec (i,s) = IExec ((Load i),P,s)
proof end;

theorem Th41: :: SCMPDS_5:41
for a being Int_position
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free parahalting Program of SCMPDS
for j being shiftable parahalting Instruction of SCMPDS holds (IExec ((I ';' j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a
proof end;

theorem :: SCMPDS_5:42
for a being Int_position
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for i being No-StopCode parahalting Instruction of SCMPDS
for j being shiftable parahalting Instruction of SCMPDS holds (IExec ((i ';' j),P,s)) . a = (Exec (j,(Exec (i,s)))) . a
proof end;