:: Computation of Two Consecutive Program Blocks for SCMPDS
:: by JingChao Chen
::
:: Received June 15, 1999
:: Copyright (c) 1999-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, SCMPDS_2, AMI_1, FSM_1, INT_1, SETFAM_1,
RELAT_1, SCMFSA_7, CARD_1, SCMPDS_4, FUNCT_1, AMISTD_2, VALUED_1,
ARYTM_3, TARSKI, XXREAL_0, TURING_1, FUNCT_4, XBOOLE_0, SCMFSA6B,
CIRCUIT2, GRAPHSP, MSUALG_1, AMI_2, AMI_3, SCMPDS_1, COMPLEX1, STRUCT_0,
ARYTM_1, NAT_1, SCMPDS_5, PARTFUN1, EXTPRO_1, SCMFSA6C, COMPOS_1,
SCMFSA6A;
notations TARSKI, XBOOLE_0, XTUPLE_0, SETFAM_1, ENUMSET1, SUBSET_1, CARD_1,
ORDINAL1, NUMBERS, XCMPLX_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_4, INT_1,
NAT_1, STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, VALUED_1, AMI_2,
FUNCT_7, SCMPDS_I, SCMPDS_1, SCMPDS_2, INT_2, SCMPDS_4, XXREAL_0;
constructors ENUMSET1, XXREAL_0, REAL_1, INT_2, SCMPDS_1, SCMPDS_4, PRE_POLY,
DOMAIN_1, AMI_3, NAT_D, MEMSTR_0, RELSET_1, XTUPLE_0;
registrations XREAL_0, INT_1, SCMPDS_2, SCMPDS_4, ORDINAL1, AFINSQ_1,
COMPOS_1, EXTPRO_1, FUNCT_4, MEMSTR_0, AMI_3, COMPOS_0, XTUPLE_0, NAT_1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
begin :: Preliminaries
reserve x for set,
m,n for Nat,
a,b,c for Int_position,
i for Instruction of SCMPDS,
s,s1,s2 for State of SCMPDS,
k1,k2 for Integer,
loc,l1 for Nat,
I,J for Program of SCMPDS,
N for with_non-empty_elements set;
::$CT 11
theorem :: SCMPDS_5:12
for I,J being Program of SCMPDS holds I c= stop (I ';' J);
theorem :: SCMPDS_5:13
dom stop I c= dom stop (I ';' J);
theorem :: SCMPDS_5:14
for I,J being Program of SCMPDS holds
stop I +* stop (I ';' J) = stop (I ';' J);
theorem :: SCMPDS_5:15
(Initialize s).a = s.a;
reserve P,P1,P2,Q for Instruction-Sequence of SCMPDS;
theorem :: SCMPDS_5:16
for s being 0-started State of SCMPDS
for I being parahalting Program of SCMPDS
st stop I c= P1 & stop I c= P2
for k being Nat holds
Comput(P1,s,k) = Comput(P2,s,k) &
CurInstr(P1,Comput(P1,s,k)) = CurInstr(P2,Comput(P2,s,k));
theorem :: SCMPDS_5:17
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);
::$CT
theorem :: SCMPDS_5:19
for s being 0-started State of SCMPDS
for I being parahalting Program of SCMPDS, J being Program of SCMPDS
st stop I c= P
for m st m <= LifeSpan(P,s)
holds Comput(P,s,m) = Comput(P+*(I ';' J),s,m);
theorem :: SCMPDS_5:20
for s being 0-started State of SCMPDS
for I being parahalting Program of SCMPDS, J being Program of SCMPDS
st stop I c= P
for m st m <= LifeSpan(P,s)
holds Comput(P,s,m) = Comput(P+*stop(I ';' J), s,m);
begin :: Non halting instrutions and parahalting instrutions
definition
::$CD
let i be Instruction of SCMPDS;
attr i is parahalting means
:: SCMPDS_5:def 2
Load i is parahalting;
end;
registration
cluster No-StopCode shiftable parahalting for Instruction of SCMPDS;
end;
theorem :: SCMPDS_5:21
goto k1 is No-StopCode;
registration
let a;
cluster return a -> No-StopCode;
end;
registration
let a,k1;
cluster a := k1 -> No-StopCode;
cluster saveIC(a,k1) -> No-StopCode;
end;
registration
let a,k1,k2;
cluster (a,k1)<>0_goto k2 -> No-StopCode;
cluster (a,k1)<=0_goto k2 -> No-StopCode;
cluster (a,k1)>=0_goto k2 -> No-StopCode;
cluster (a,k1) := k2 -> No-StopCode;
end;
registration
let a,k1,k2;
cluster AddTo(a,k1,k2) -> No-StopCode;
end;
registration
let a,b,k1,k2;
cluster AddTo(a,k1,b,k2) -> No-StopCode;
cluster SubFrom(a,k1,b,k2) -> No-StopCode;
cluster MultBy(a,k1,b,k2) -> No-StopCode;
cluster Divide(a,k1,b,k2) -> No-StopCode;
cluster (a,k1) := (b,k2) -> No-StopCode;
end;
registration
cluster halt SCMPDS -> parahalting;
end;
registration
let i be parahalting Instruction of SCMPDS;
cluster Load i -> parahalting for Program of SCMPDS;
end;
registration
let a,k1;
cluster a := k1 -> parahalting;
end;
registration
let a,k1,k2;
cluster (a,k1) := k2 -> parahalting;
cluster AddTo(a,k1,k2) -> parahalting;
end;
registration
let a,b,k1,k2;
cluster AddTo(a,k1,b,k2) -> parahalting;
cluster SubFrom(a,k1,b,k2) -> parahalting;
cluster MultBy(a,k1,b,k2) -> parahalting;
cluster Divide(a,k1,b,k2) -> parahalting;
cluster (a,k1) := (b,k2) -> parahalting;
end;
theorem :: SCMPDS_5:22
InsCode i =1 implies i is not parahalting;
registration
cluster parahalting shiftable halt-free for Program of SCMPDS;
end;
registration
let I,J be halt-free Program of SCMPDS;
cluster I ';' J -> halt-free;
end;
registration :: musi byc do najmniej jedna instrukcja rozna of halt
:: nie moze to byc np. Trivial-AMI
let i be No-StopCode Instruction of SCMPDS;
cluster Load i -> halt-free;
end;
registration
let i be No-StopCode Instruction of SCMPDS, J be halt-free Program of
SCMPDS;
cluster i ';' J -> halt-free;
end;
registration
let I be halt-free Program of SCMPDS, j be No-StopCode Instruction of
SCMPDS;
cluster I ';' j -> halt-free;
end;
registration
let i,j be No-StopCode Instruction of SCMPDS;
cluster i ';' j -> halt-free;
end;
theorem :: SCMPDS_5:23
for s being 0-started State of SCMPDS
for I being parahalting halt-free Program of SCMPDS st stop I c= P
holds IC Comput(P, s,LifeSpan(P +* stop I,s)) = card I;
theorem :: SCMPDS_5:24
for s being 0-started State of SCMPDS
for I being parahalting Program of SCMPDS,k be Nat st
k < LifeSpan(P +* stop I,s)
holds IC Comput(P +* stop I,s,k) in dom I;
theorem :: SCMPDS_5:25
for s being 0-started State of SCMPDS
for I being parahalting Program of SCMPDS,k be Nat st
I c= P & k <= LifeSpan(P +* stop I,s)
holds Comput(P, s,k) = Comput(P +* stop I,s,k);
theorem :: SCMPDS_5:26
for s being 0-started State of SCMPDS
for I being parahalting halt-free Program of SCMPDS st I c= P
holds IC Comput(P,s,LifeSpan(P +* stop I,s)) = card I;
theorem :: SCMPDS_5:27
for s being 0-started State of SCMPDS
for I being parahalting Program of SCMPDS st I c= P
holds CurInstr(P,Comput(P, s,LifeSpan(P +* stop I,s))) = halt SCMPDS
or IC Comput(P, s,LifeSpan(P +* stop I,s)) = card I;
theorem :: SCMPDS_5:28
for s being 0-started State of SCMPDS
for I being parahalting halt-free Program of SCMPDS,k being Nat
st I c= P & k < LifeSpan(P +* stop I,s)
holds CurInstr(P,Comput(P,s,k)) <> halt SCMPDS;
theorem :: SCMPDS_5:29
for s being 0-started State of SCMPDS
for I being parahalting Program of SCMPDS,
J being Program of SCMPDS, k being Nat
st k <= LifeSpan(P +* stop I,s)
holds Comput(P +* stop I,s,k) = Comput(P+*(I ';' J),s,k);
theorem :: SCMPDS_5:30
for s being 0-started State of SCMPDS
for I being parahalting Program of SCMPDS,J being Program of SCMPDS,
k being Nat st k <= LifeSpan(P +* stop I,s)
holds Comput(P +* stop I, s,k) = Comput(P+*stop(I ';' J),s,k);
registration
let I be parahalting Program of SCMPDS,
J be parahalting shiftable Program of SCMPDS;
cluster I ';' J -> parahalting for Program of SCMPDS;
end;
registration
let i be parahalting Instruction of SCMPDS, J be parahalting shiftable
Program of SCMPDS;
cluster i ';' J -> parahalting;
end;
registration
let I be parahalting Program of SCMPDS, j be parahalting shiftable
Instruction of SCMPDS;
cluster I ';' j -> parahalting;
end;
registration
let i be parahalting Instruction of SCMPDS, j be parahalting shiftable
Instruction of SCMPDS;
cluster i ';' j -> parahalting;
end;
theorem :: SCMPDS_5:31
for s being State of SCMPDS, s1 being 0-started State of SCMPDS,
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);
begin :: Computation of two consecutive program blocks
theorem :: SCMPDS_5:32
for s being 0-started State of SCMPDS
for I being parahalting halt-free Program of SCMPDS,J being
parahalting shiftable Program of SCMPDS,k being 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);
theorem :: SCMPDS_5:33
for s being 0-started State of SCMPDS
for I being parahalting halt-free Program of SCMPDS,
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));
theorem :: SCMPDS_5:34
for s being 0-started State of SCMPDS
for I being parahalting halt-free Program of SCMPDS,J being
parahalting shiftable Program of SCMPDS holds IExec(I ';' J,P,s)
= IncIC(IExec(J,P,Initialize IExec(I,P,s)),card I);
theorem :: SCMPDS_5:35
for s being 0-started State of SCMPDS
for I being parahalting halt-free Program of SCMPDS,J being
parahalting shiftable Program of SCMPDS holds IExec(I ';' J,P,s).a
= IExec(J,P,Initialize IExec(I,P,s)).a;
begin :: Computation of the program consisting of a instruction and a block
::$CT
theorem :: SCMPDS_5:37
s1 | (SCM-Data-Loc \/ {IC SCMPDS})
= s2 | (SCM-Data-Loc \/ {IC SCMPDS}) implies s1 = s2;
theorem :: SCMPDS_5:38
DataPart s1 = DataPart s2 & InsCode i <> 3 implies
DataPart Exec(i,s1) = DataPart Exec(i,s2);
theorem :: SCMPDS_5:39
for i being shiftable Instruction of SCMPDS holds (DataPart s1 =
DataPart s2 implies DataPart Exec(i,s1) = DataPart Exec(i,s2));
theorem :: SCMPDS_5:40
for s being 0-started State of SCMPDS
for i being parahalting Instruction of SCMPDS
holds Exec(i,s) = IExec(Load i,P,s);
theorem :: SCMPDS_5:41
for s being 0-started State of SCMPDS
for I being parahalting halt-free Program of SCMPDS,
j being parahalting shiftable Instruction of SCMPDS
holds IExec(I ';' j,P,s).a = Exec(j,IExec(I,P,s)).a;
theorem :: SCMPDS_5:42
for s being 0-started State of SCMPDS
for i being No-StopCode parahalting Instruction of SCMPDS,
j being shiftable parahalting Instruction of SCMPDS
holds IExec(i ';' j,P,s).a = Exec(j,Exec(i, s)).a;