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

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

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

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

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

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)

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

:: deftheorem Def2 defines parahalting SCMPDS_5:def 2 :

for i being Instruction of SCMPDS holds

( i is parahalting iff Load i is parahalting );

for i being Instruction of SCMPDS holds

( i is parahalting iff Load i is parahalting );

registration

existence

ex b_{1} being Instruction of SCMPDS st

( b_{1} is No-StopCode & b_{1} is shiftable & b_{1} is parahalting )

end;
ex b

( b

proof end;

registration

let a be Int_position;

let k1 be Integer;

coherence

a := k1 is No-StopCode

saveIC (a,k1) is No-StopCode

end;
let k1 be Integer;

coherence

a := k1 is No-StopCode

proof end;

coherence saveIC (a,k1) is No-StopCode

proof end;

registration

let a be Int_position;

let k1, k2 be Integer;

coherence

(a,k1) <>0_goto k2 is No-StopCode

(a,k1) <=0_goto k2 is No-StopCode

(a,k1) >=0_goto k2 is No-StopCode

(a,k1) := k2 is No-StopCode

end;
let k1, k2 be Integer;

coherence

(a,k1) <>0_goto k2 is No-StopCode

proof end;

coherence (a,k1) <=0_goto k2 is No-StopCode

proof end;

coherence (a,k1) >=0_goto k2 is No-StopCode

proof end;

coherence (a,k1) := k2 is No-StopCode

proof end;

registration
end;

registration

let a, b be Int_position;

let k1, k2 be Integer;

coherence

AddTo (a,k1,b,k2) is No-StopCode

SubFrom (a,k1,b,k2) is No-StopCode

MultBy (a,k1,b,k2) is No-StopCode

Divide (a,k1,b,k2) is No-StopCode

(a,k1) := (b,k2) is No-StopCode

end;
let k1, k2 be Integer;

coherence

AddTo (a,k1,b,k2) is No-StopCode

proof end;

coherence SubFrom (a,k1,b,k2) is No-StopCode

proof end;

coherence MultBy (a,k1,b,k2) is No-StopCode

proof end;

coherence Divide (a,k1,b,k2) is No-StopCode

proof end;

coherence (a,k1) := (b,k2) is No-StopCode

proof end;

registration
end;

registration

let i be parahalting Instruction of SCMPDS;

coherence

for b_{1} being Program of SCMPDS st b_{1} = Load i holds

b_{1} is parahalting
by Def2;

end;
coherence

for b

b

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

registration

let a be Int_position;

let k1, k2 be Integer;

coherence

(a,k1) := k2 is parahalting

AddTo (a,k1,k2) is parahalting

end;
let k1, k2 be Integer;

coherence

(a,k1) := k2 is parahalting

proof end;

coherence AddTo (a,k1,k2) is parahalting

proof end;

registration

let a, b be Int_position;

let k1, k2 be Integer;

coherence

AddTo (a,k1,b,k2) is parahalting

SubFrom (a,k1,b,k2) is parahalting

MultBy (a,k1,b,k2) is parahalting

Divide (a,k1,b,k2) is parahalting

(a,k1) := (b,k2) is parahalting

end;
let k1, k2 be Integer;

coherence

AddTo (a,k1,b,k2) is parahalting

proof end;

coherence SubFrom (a,k1,b,k2) is parahalting

proof end;

coherence MultBy (a,k1,b,k2) is parahalting

proof end;

coherence Divide (a,k1,b,k2) is parahalting

proof end;

coherence (a,k1) := (b,k2) is parahalting

proof end;

registration

ex b_{1} being Program of SCMPDS st

( b_{1} is parahalting & b_{1} is shiftable & b_{1} is halt-free )
end;

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 b

( b

proof end;

registration
end;

registration
end;

registration

let i be No-StopCode Instruction of SCMPDS;

let J be halt-free Program of SCMPDS;

coherence

i ';' J is halt-free ;

end;
let J be halt-free Program of SCMPDS;

coherence

i ';' J is halt-free ;

registration

let I be halt-free Program of SCMPDS;

let j be No-StopCode Instruction of SCMPDS;

coherence

I ';' j is halt-free ;

end;
let j be No-StopCode Instruction of SCMPDS;

coherence

I ';' j is halt-free ;

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

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

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)

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

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 )

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

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)

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)

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;

coherence

for b_{1} being Program of SCMPDS st b_{1} = I ';' J holds

b_{1} is parahalting

end;
let J be parahalting shiftable Program of SCMPDS;

coherence

for b

b

proof end;

registration

let i be parahalting Instruction of SCMPDS;

let J be parahalting shiftable Program of SCMPDS;

coherence

i ';' J is parahalting ;

end;
let J be parahalting shiftable Program of SCMPDS;

coherence

i ';' J is parahalting ;

registration

let I be parahalting Program of SCMPDS;

let j be shiftable parahalting Instruction of SCMPDS;

coherence

I ';' j is parahalting ;

end;
let j be shiftable parahalting Instruction of SCMPDS;

coherence

I ';' j is parahalting ;

registration

let i be parahalting Instruction of SCMPDS;

let j be shiftable parahalting Instruction of SCMPDS;

coherence

i ';' j is parahalting ;

end;
let j be shiftable parahalting Instruction of SCMPDS;

coherence

i ';' j is parahalting ;

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)

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

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

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

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

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

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

s1 = s2

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

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

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)

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

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

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;