:: Initialization Halting Concepts and Their Basic Properties of SCM+FSA
:: by JingChao Chen and Yatsuka Nakamura
::
:: Received June 17, 1998
:: Copyright (c) 1998-2017 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, AMI_1, SCMFSA_2, FSM_1, SCMFSA6A, TARSKI,
CIRCUIT2, RELAT_1, FUNCT_1, CARD_1, FUNCOP_1, FUNCT_4, XBOOLE_0,
SCMFSA6B, NAT_1, XXREAL_0, ARYTM_3, AMI_3, SF_MASTR, GRAPHSP, MSUALG_1,
AMISTD_2, STRUCT_0, VALUED_1, SCMFSA6C, SCMFSA7B, SCMFSA8B, ARYTM_1,
SCMFSA8C, SCM_HALT, PARTFUN1, EXTPRO_1, RELOC, COMPOS_1, AMISTD_1,
SFMASTR2, SCMFSA_9, FRECHET;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, CARD_1, ORDINAL1, CARD_3,
NUMBERS, XCMPLX_0, RELAT_1, FINSEQ_1, FUNCT_1, PARTFUN1, FUNCT_4,
FUNCT_7, PBOOLE, FUNCT_2, VALUED_1, NAT_1, NAT_D, STRUCT_0, MEMSTR_0,
COMPOS_0, COMPOS_1, EXTPRO_1, AMISTD_1, AMISTD_2, SCMFSA_2, FUNCOP_1,
SCMFSA6B, SCMFSA6A, SF_MASTR, SCMFSA8B, SFMASTR1, SCMFSA8C, SCMFSA7B,
SCMFSA_3, SCMFSA6C, XXREAL_0, SCMFSA_M, SCMFSA_X, SCMFSA_9, SCMFSA9A;
constructors SFMASTR1, DOMAIN_1, XXREAL_0, REAL_1, SCM_1, SCMFSA_3, SCMFSA6A,
SF_MASTR, SCMFSA6B, SCMFSA6C, SCMFSA8A, SCMFSA8B, SCMFSA8C, AMISTD_1,
AMISTD_2, NAT_D, RELSET_1, VALUED_1, SCMFSA7B, SCMFSA_9, AMISTD_5,
PBOOLE, PRE_POLY, MEMSTR_0, SCMFSA_1, SCMFSA_M, FUNCT_7, SCMFSA_X,
SCMFSA9A, CARD_3;
registrations XBOOLE_0, FUNCT_1, XREAL_0, NAT_1, INT_1, SCMFSA_2, SCMFSA6A,
SF_MASTR, SCMFSA6B, SCMFSA6C, SCMFSA7B, SCMFSA8A, SCMFSA_9, ORDINAL1,
RELAT_1, COMPOS_1, SFMASTR1, EXTPRO_1, SCMFSA_4, FUNCT_4, FUNCT_7,
PRE_POLY, STRUCT_0, FUNCOP_1, MEMSTR_0, AMI_3, COMPOS_0, SCMFSA_M,
SCMFSA8C, SCMFSA8B, CARD_3, RELSET_1, AMISTD_1, SCMFSA9A, SCMFSA10,
SCMFSA_X, COMPOS_2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin
reserve m,n for Nat,
I for Program of SCM+FSA,
s,s1,s2 for State of SCM+FSA,
a for Int-Location,
f for FinSeq-Location,
p,p1,p2 for Instruction-Sequence of SCM+FSA;
::$CD
definition
let I be Program of SCM+FSA;
attr I is InitHalting means
:: SCM_HALT:def 2
for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s
for P being Instruction-Sequence of SCM+FSA
st I c= P
holds P halts_on s;
attr I is keepInt0_1 means
:: SCM_HALT:def 3
for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s
for p st I c= p
for k being Nat holds (Comput(p,s,k)).intloc 0 = 1;
end;
::$CT
theorem :: SCM_HALT:2
Macro halt SCM+FSA is InitHalting;
registration
cluster InitHalting for Program of SCM+FSA;
end;
registration
cluster parahalting -> InitHalting for Program of SCM+FSA;
end;
registration
cluster keeping_0 -> keepInt0_1 for Program of SCM+FSA;
end;
::$CT
theorem :: SCM_HALT:4
for I being InitHalting really-closed Program of SCM+FSA,
a being read-write
Int-Location holds not a in UsedILoc I implies (IExec(I,p,s)).a = s.a;
theorem :: SCM_HALT:5
for I being InitHalting really-closed Program of SCM+FSA,
f being FinSeq-Location
holds not f in UsedI*Loc I implies (IExec(I,p,s)).f = s.f;
registration
cluster InitHalting -> non empty for Program of SCM+FSA;
end;
theorem :: SCM_HALT:6
for J being InitHalting really-closed Program of SCM+FSA
st Initialize ((intloc 0) .--> 1) c= s1 & J c= p1
for n being Nat st
Reloc(J,n) c= p2 &
IC s2 = n & DataPart s1 = DataPart s2
for i being Nat holds
IC Comput(p1,s1,i) + n = IC Comput(p2,s2,i) &
IncAddr(CurInstr(p1,Comput(p1,s1,i)),n) = CurInstr(p2,Comput(p2,s2,i)) &
DataPart Comput(p1,s1,i) = DataPart Comput(p2,s2,i);
theorem :: SCM_HALT:7
for I being InitHalting really-closed Program of SCM+FSA st
Initialize ((intloc 0) .--> 1) c= s1 &
Initialize ((intloc 0) .--> 1) c= s2 &
I c= p1 & I c= p2 &
s1 = s2
for k being Nat holds
Comput(p1,s1,k) = Comput(p2,s2,k) &
CurInstr(p1,Comput(p1,s1,k)) = CurInstr(p2,Comput(p2,s2,k));
theorem :: SCM_HALT:8
for I being InitHalting really-closed Program of SCM+FSA
st Initialize ((intloc 0) .--> 1) c= s1 &
Initialize ((intloc 0) .--> 1) c= s2 & I c= p1 & I c= p2 &
s1 = s2
holds LifeSpan(p1,s1) = LifeSpan(p2,
s2) & Result(p1,s1) = Result(p2,s2);
registration
cluster keeping_0 InitHalting for Program of SCM+FSA;
end;
registration
cluster keepInt0_1 InitHalting for really-closed Program of SCM+FSA;
end;
theorem :: SCM_HALT:9
for I being keepInt0_1 InitHalting Program of SCM+FSA holds
IExec(I,p,s).intloc 0 = 1;
theorem :: SCM_HALT:10
for I being really-closed Program of SCM+FSA, J being Program of
SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= p &
p halts_on s
for m st m <= LifeSpan(p,s) holds
Comput(p,s,m) = Comput(p+*(I ";" J),s,m);
theorem :: SCM_HALT:11
for I being really-closed Program of SCM+FSA
st p+*I halts_on s &
Directed I c= p &
Initialize ((intloc 0) .--> 1) c= s
holds IC Comput(p, s,LifeSpan(p +* I,s) + 1) = card I;
theorem :: SCM_HALT:12
for I being really-closed Program of SCM+FSA
st p+*I halts_on s & Directed I c= p &
Initialize ((intloc 0) .--> 1) c= s
holds DataPart Comput(p, s,LifeSpan(p +* I,s))
= DataPart Comput(p,s,LifeSpan(p +* I,s) + 1);
theorem :: SCM_HALT:13
for I being InitHalting really-closed Program of SCM+FSA st
Initialize ((intloc 0) .--> 1) c= s & I c= p
for k being Nat st k <= LifeSpan(p,s)
holds CurInstr(p +* Directed I,
Comput(p +* Directed I, s,k)) <> halt SCM+FSA;
theorem :: SCM_HALT:14
for I being really-closed Program of SCM+FSA
st p+*I halts_on Initialized s
for J being Program of SCM+FSA, k being Nat
st k <= LifeSpan(p +* I,Initialized s )
holds Comput(p +* I, (Initialized s),k)
= Comput(p +* (I ";" J), (Initialized s),k);
theorem :: SCM_HALT:15
for I being keepInt0_1 InitHalting really-closed Program of SCM+FSA,
J being InitHalting really-closed Program of SCM+FSA,
s being State of SCM+FSA st
Initialize ((intloc 0) .--> 1) c= s & I ";" J c= p
holds IC Comput(p, s,LifeSpan(p +* I,s) + 1) = card I &
DataPart Comput(p, s,LifeSpan(p +* I,s) + 1) =
DataPart(Comput(p +* I, s,LifeSpan(p +* I,s))
+* Initialize ((intloc 0) .--> 1)) &
Reloc(J,card I) c= p &
Comput(p, s,LifeSpan(p +* I,s) + 1).intloc 0 = 1 & p halts_on s &
LifeSpan(p,s) = LifeSpan(p +* I,s) + 1 +
LifeSpan(p +* I +* J,
Result(p +* I,s) +*Initialize ((intloc 0) .--> 1)) & (J is keeping_0 implies
(Result(p,s)).intloc 0 = 1);
registration
let I be keepInt0_1 InitHalting really-closed Program of SCM+FSA,
J be InitHalting really-closed Program of SCM+FSA;
cluster I ";" J -> InitHalting;
end;
theorem :: SCM_HALT:16
for I being keepInt0_1 really-closed Program of SCM+FSA st p+*I halts_on s
for J being really-closed Program of SCM+FSA st
Initialize ((intloc 0) .--> 1) c= s & I ";" J c= p
for k being Element of NAT holds (Comput(p +* I +* J,
(Result(p +* I,s) +* Initialize ((intloc 0) .--> 1)),k) +*
Start-At (IC Comput(p +* I +* J, (
Result(p +* I,s) +* Initialize ((intloc 0) .--> 1)),k) + card I,SCM+FSA))
= Comput(p +* (I ";" J), s,LifeSpan(p +* I,s)+1+k);
theorem :: SCM_HALT:17
for I being keepInt0_1 really-closed Program of SCM+FSA
st not p+*I halts_on Initialized s
for J being Program of SCM+FSA, k being Nat
holds Comput(p +* I, Initialized s,k)
= Comput(p +* (I ";" J), Initialized s,k);
theorem :: SCM_HALT:18
for I being keepInt0_1 InitHalting really-closed Program of SCM+FSA,
J being InitHalting really-closed Program of SCM+FSA holds
LifeSpan(p +* (I ";" J),Initialized s)
= LifeSpan(p+*I,Initialized s) + 1 +
LifeSpan(p +* I +* J,
Result(p+*I,Initialized s)
+*Initialize ((intloc 0) .--> 1));
theorem :: SCM_HALT:19
for I being keepInt0_1 InitHalting really-closed Program of SCM+FSA,
J being InitHalting really-closed Program of SCM+FSA holds
IExec(I ";" J,p,s) = IncIC(IExec(J,p,IExec(I,p,s)),card I);
registration
let i be sequential Instruction of SCM+FSA;
cluster Macro i -> InitHalting;
end;
registration
let i be sequential Instruction of SCM+FSA,
J be parahalting really-closed Program of SCM+FSA;
cluster i ";" J -> InitHalting;
end;
registration
let i be keeping_0 sequential Instruction of SCM+FSA,
J be InitHalting really-closed Program of SCM+FSA;
cluster i ";" J -> InitHalting;
end;
registration
let I, J be keepInt0_1 really-closed Program of SCM+FSA;
cluster I ";" J -> keepInt0_1;
end;
registration
let j be keeping_0 sequential Instruction of SCM+FSA,
I be keepInt0_1 InitHalting really-closed Program of SCM+FSA;
cluster I ";" j -> InitHalting keepInt0_1;
end;
registration
let i be keeping_0 sequential Instruction of SCM+FSA,
J be keepInt0_1 InitHalting really-closed Program of SCM+FSA;
cluster i ";" J -> InitHalting keepInt0_1;
end;
registration
let j be sequential Instruction of SCM+FSA,
I be parahalting really-closed Program of SCM+FSA;
cluster I ";" j -> InitHalting;
end;
registration
let i,j be sequential Instruction of SCM+FSA;
cluster i ";" j -> InitHalting;
end;
theorem :: SCM_HALT:20
for I being keepInt0_1 InitHalting really-closed Program of SCM+FSA,
J being InitHalting really-closed Program of SCM+FSA
holds IExec(I ";" J,p,s).a = IExec(J,p,IExec(I,p,s)).a;
theorem :: SCM_HALT:21
for I being keepInt0_1 InitHalting really-closed Program of SCM+FSA,
J being InitHalting really-closed Program of SCM+FSA
holds IExec(I ";" J,p,s).f = IExec(J,p,IExec(I,p,s)).f;
theorem :: SCM_HALT:22
for I be keepInt0_1 InitHalting Program of SCM+FSA, s be State
of SCM+FSA holds DataPart(Initialized IExec(I,p,s)) = DataPart IExec(I,p,s);
theorem :: SCM_HALT:23
for I being keepInt0_1 InitHalting really-closed Program of SCM+FSA,
j being sequential Instruction of SCM+FSA
holds IExec(I ";" j,p,s).a = Exec(j,IExec(I,p,s)).a;
theorem :: SCM_HALT:24
for I being keepInt0_1 InitHalting really-closed Program of SCM+FSA,
j being sequential Instruction of SCM+FSA
holds IExec(I ";" j,p,s).f = Exec(j,IExec(I,p,s)).f;
definition
let I be Program of SCM+FSA;
let s be State of SCM+FSA;
let p;
pred I is_halting_onInit s,p means
:: SCM_HALT:def 4
p+*I halts_on Initialized s;
end;
::$CD
::$CT
theorem :: SCM_HALT:26
for I being Program of SCM+FSA holds I is InitHalting iff for s
being State of SCM+FSA,p holds I is_halting_onInit s,p;
theorem :: SCM_HALT:27
for s being State of SCM+FSA, I being really-closed Program of SCM+FSA, a
being Int-Location st I does not destroy a &
:::I is_closed_onInit s,p &
Initialize ((intloc 0) .--> 1) c= s & I c= p
holds for k being Nat holds Comput(p,s,k).a = s.a;
registration
cluster InitHalting good for Program of SCM+FSA;
end;
registration
cluster really-closed good -> keepInt0_1 for Program of SCM+FSA;
end;
registration
cluster Stop SCM+FSA -> InitHalting good;
end;
theorem :: SCM_HALT:28
for s being State of SCM+FSA, i being keeping_0 sequential
Instruction of SCM+FSA, J being InitHalting really-closed Program of SCM+FSA,
a being
Int-Location holds IExec(i ";" J,p,s).a
= IExec(J,p,Exec(i,Initialized s)).a;
theorem :: SCM_HALT:29
for s being State of SCM+FSA, i being keeping_0 sequential
Instruction of SCM+FSA, J being InitHalting really-closed Program of SCM+FSA,
f being
FinSeq-Location holds IExec(i ";" J,p,s).f
= IExec(J,p,Exec(i,Initialized s)).f;
::$CT
theorem :: SCM_HALT:31
for s being State of SCM+FSA, I being Program of SCM+FSA holds I
is_halting_onInit s,p iff I is_halting_on Initialized s,p;
theorem :: SCM_HALT:32
for I be Program of SCM+FSA, s be State of SCM+FSA holds IExec(I,p,s) =
IExec(I,p,Initialized s);
theorem :: SCM_HALT:33
for s being State of SCM+FSA,
I being really-closed MacroInstruction of SCM+FSA,
J being MacroInstruction of SCM+FSA,
a being read-write Int-Location st s.a = 0 &
:::I is_closed_onInit s,p &
I is_halting_onInit s,p holds
:::if=0(a,I,J) is_closed_onInit s,p &
if=0(a,I,J) is_halting_onInit s,p;
theorem :: SCM_HALT:34
for s being State of SCM+FSA,
I being really-closed MacroInstruction of SCM+FSA,
J being MacroInstruction of SCM+FSA,
a being read-write Int-Location st s.a = 0 &
I is_halting_onInit s,p
holds IExec(if=0(a,I,J),p,s)
= IExec(I,p,s) +* Start-At( (card I + card J + 3),SCM+FSA);
theorem :: SCM_HALT:35
for s being State of SCM+FSA,
I,J being really-closed MacroInstruction of SCM+FSA,
a being read-write Int-Location st s.a <> 0
:::& J is_closed_onInit s,p
& J is_halting_onInit s,p
holds
:::if=0(a,I,J) is_closed_onInit s,p &
if=0(a,I,J)
is_halting_onInit s,p;
theorem :: SCM_HALT:36
for I,J being really-closed MacroInstruction of SCM+FSA, a being read-write
Int-Location holds for s being State of SCM+FSA st s.a <> 0 &
:::Jis_closed_onInit s,p &
J is_halting_onInit s,p
holds IExec(if=0(a,I,J),p,s)
= IExec(J,p,s) +* Start-At((card I + card J + 3),SCM+FSA);
theorem :: SCM_HALT:37
for s being State of SCM+FSA,
I,J being really-closed InitHalting MacroInstruction of
SCM+FSA, a being read-write Int-Location holds if=0(a,I,J) is InitHalting & (s.
a = 0 implies IExec(if=0(a,I,J),p,s) = IExec(I,p,s) +* Start-At((card I +
card J + 3),SCM+FSA)) &
(s.a <> 0 implies IExec(if=0(a,I,J),p,s) = IExec(J,p,s) +* Start-At(
(card I + card J + 3),SCM+FSA));
theorem :: SCM_HALT:38
for s being State of SCM+FSA,
I,J being InitHalting really-closed MacroInstruction of SCM+FSA,
a being read-write Int-Location holds IC IExec(if=0(a,I,J),p,s) = (card
I + card J + 3) & (s.a = 0 implies ((for d being Int-Location
holds IExec(if=0(a,I,J),p,s).d = IExec(I,p,s).d) &
for f being FinSeq-Location
holds IExec(if=0(a,I,J),p,s).f = IExec(I,p,s).f)) & (s.a <> 0 implies
((for d being Int-Location holds
IExec(if=0(a,I,J),p,s).d = IExec(J,p,s).d) &
for f being FinSeq-Location holds
IExec(if=0(a,I,J),p,s).f = IExec(J,p,s).f));
theorem :: SCM_HALT:39
for s being State of SCM+FSA,
I,J being really-closed MacroInstruction of SCM+FSA, a
being read-write Int-Location st s.a > 0 &
:::I is_closed_onInit s,p &
I
is_halting_onInit s,p holds
:::if>0(a,I,J) is_closed_onInit s,p &
if>0(a,I,J)
is_halting_onInit s,p;
theorem :: SCM_HALT:40
for s being State of SCM+FSA,
I,J being really-closed MacroInstruction of SCM+FSA,
a being read-write Int-Location st s.a > 0 &
:::I is_closed_onInit s,p &
I
is_halting_onInit s,p holds IExec(if>0(a,I,J),p,s)
= IExec(I,p,s) +* Start-At((card I + card J + 3),SCM+FSA);
theorem :: SCM_HALT:41
for s being State of SCM+FSA,
I,J being really-closed MacroInstruction of SCM+FSA,
a being read-write Int-Location st s.a <= 0 &
:::J is_closed_onInit s,p &
J
is_halting_onInit s,p holds
:::if>0(a,I,J) is_closed_onInit s,p &
if>0(a,I,J) is_halting_onInit s,p;
theorem :: SCM_HALT:42
for I,J being really-closed MacroInstruction of SCM+FSA, a being read-write
Int-Location holds for s being State of SCM+FSA st s.a <= 0 &
:::Jis_closed_onInit s,p &
J is_halting_onInit s,p
holds IExec(if>0(a,I,J),p,s)
= IExec(J,p,s) +* Start-At((card I + card J + 3),SCM+FSA);
theorem :: SCM_HALT:43
for s being State of SCM+FSA,
I,J being InitHalting really-closed MacroInstruction of
SCM+FSA, a being read-write Int-Location holds if>0(a,I,J) is InitHalting & (s.
a > 0 implies IExec(if>0(a,I,J),p,s) = IExec(I,p,s) +* Start-At((card I +
card J + 3),SCM+FSA)) &
(s.a <= 0 implies IExec(if>0(a,I,J),p,s) = IExec(J,p,s) +* Start-At(
(card I + card J + 3),SCM+FSA));
theorem :: SCM_HALT:44
for s being State of SCM+FSA,
I,J being InitHalting really-closed MacroInstruction of SCM+FSA
, a being read-write Int-Location holds IC IExec(if>0(a,I,J),p,s) = (card
I + card J + 3) & (s.a > 0 implies ((for d being Int-Location
holds IExec(if>0(a,I,J),p,s).d = IExec(I,p,s).d) &
for f being FinSeq-Location
holds IExec(if>0(a,I,J),p,s).f
= IExec(I,p,s).f)) & (s.a <= 0 implies ((for d being Int-Location
holds
IExec(if>0(a,I,J),p,s).d = IExec(J,p,s).d) & for f being FinSeq-Location
holds
IExec(if>0(a,I,J),p,s).f = IExec(J,p,s).f));
::$CT 4
registration
let I,J be InitHalting really-closed MacroInstruction of SCM+FSA;
let a be read-write Int-Location;
cluster if=0(a,I,J) -> InitHalting;
cluster if>0(a,I,J) -> InitHalting;
:: cluster if<0(a,I,J) -> InitHalting;
:: correctness by Th46;
end;
theorem :: SCM_HALT:49
for I being Program of SCM+FSA holds I is InitHalting iff for s
being State of SCM+FSA,p holds I is_halting_on Initialized s,p;
::$CT
theorem :: SCM_HALT:51
for s being State of SCM+FSA, I being InitHalting Program of
SCM+FSA, a being read-write Int-Location holds IExec(I,p,s).a
= Comput(p +* I, Initialize Initialized s,
LifeSpan(p +* I,Initialize Initialized s)).a;
theorem :: SCM_HALT:52
for s being State of SCM+FSA, I being InitHalting really-closed Program of
SCM+FSA, a being Int-Location,k being Element of NAT st I does not destroy a
holds IExec(I,p,s).a = Comput(p +* I,
Initialize Initialized s,k).a;
theorem :: SCM_HALT:53
for s being State of SCM+FSA, I being InitHalting really-closed Program of
SCM+FSA, a being Int-Location st I does not destroy a
holds IExec(I,p,s).a = (Initialized s).a;
theorem :: SCM_HALT:54
for s be State of SCM+FSA,
I be keepInt0_1 InitHalting really-closed Program of
SCM+FSA, a being read-write Int-Location st I does not destroy a holds
Comput(p +* (I ";" SubFrom(a,intloc 0)),
Initialize Initialized s,
LifeSpan(p +* (I ";" SubFrom(a,intloc 0)),
Initialize Initialized s)).a
= s.a - 1;
::$CT 7
theorem :: SCM_HALT:62
for s being 0-started State of SCM+FSA,
I being good InitHalting really-closed MacroInstruction of
SCM+FSA, a being read-write Int-Location
st I does not destroy a & s.intloc 0 = 1
holds Times(a,I) is_halting_on s,p;
registration
let a be read-write Int-Location,I be good MacroInstruction of SCM+FSA;
cluster Times(a,I) -> good;
end;
::$CT 2
theorem :: SCM_HALT:65
for s being State of SCM+FSA,
I being good InitHalting really-closed MacroInstruction
of SCM+FSA, a being read-write Int-Location st s.intloc 0 = 1 & s.a <= 0 holds
DataPart IExec(Times(a,I),p,s) = DataPart s;
reserve P,P1,P2,Q for Instruction-Sequence of SCM+FSA;
theorem :: SCM_HALT:66
for s being State of SCM+FSA,
I being good InitHalting really-closed MacroInstruction
of SCM+FSA, a being read-write Int-Location st I does not destroy a
holds IExec(I ";" SubFrom(a,intloc 0),p,s).a = s.a - 1 &
(s.a > 0 implies DataPart IExec(Times(a,I),p,s)
= DataPart IExec(Times(a,I),p,IExec(I ";" SubFrom(a,intloc 0),p,s)));
theorem :: SCM_HALT:67
for s be State of SCM+FSA,
I be good InitHalting really-closed MacroInstruction of SCM+FSA,
f be FinSeq-Location,a be read-write Int-Location st s.a <= 0
holds IExec(Times(a,I),p,s).f=s.f;
theorem :: SCM_HALT:68
for s be State of SCM+FSA,
I be good InitHalting really-closed MacroInstruction of SCM+FSA,
b be Int-Location,a be read-write Int-Location st s.a <= 0
holds IExec(Times(a,I),p,s).b=(Initialized s).b;
theorem :: SCM_HALT:69
for s be State of SCM+FSA,
I be good InitHalting really-closed MacroInstruction of SCM+FSA,
f be FinSeq-Location,a be read-write Int-Location
st I does not destroy a & s.a > 0
holds IExec(Times(a,I),p,s).f
=IExec(Times(a,I),p,IExec(I ";" SubFrom(a,intloc 0),p,s)).f;
theorem :: SCM_HALT:70
for s be State of SCM+FSA,
I be good InitHalting really-closed MacroInstruction of SCM+FSA, b
be Int-Location,a be read-write Int-Location st I does not destroy a & s.a > 0
holds IExec(Times(a,I),p,s).b
=IExec(Times(a,I),p,IExec(I ";" SubFrom(a,intloc 0),p,s)).b;
definition
let i be Instruction of SCM+FSA;
redefine attr i is good means
:: SCM_HALT:def 6
i does not destroy intloc 0;
end;
theorem :: SCM_HALT:71
for s be State of SCM+FSA,I be InitHalting really-closed Program of SCM+FSA
st Initialize ((intloc 0) .--> 1) c= s & I c= P1 & I c= P2
for k be Nat
holds Comput(P1, s,k) = Comput(P2, s,k) &
CurInstr(P1,Comput(P1,s,k)) = CurInstr(P2,Comput(P2,s,k));
theorem :: SCM_HALT:72
for s be State of SCM+FSA,I be InitHalting really-closed Program of SCM+FSA
st Initialize ((intloc 0) .--> 1) c= s &
I c= P1 & I c= P2
holds LifeSpan(P1,s) = LifeSpan(P2,s) &
Result(P1,s) = Result(P2,s);
theorem :: SCM_HALT:73
for s being State of SCM+FSA,
I being really-closed MacroInstruction of SCM+FSA,
a being read-write Int-Location st s.a <= 0
holds while>0(a,I) is_halting_onInit s,P;
theorem :: SCM_HALT:74
for s being State of SCM+FSA,
I be really-closed MacroInstruction of SCM+FSA,
a be read-write Int-Location st
I is_halting_onInit s,P & s.a >
0 holds IC Comput(P +* while>0(a,I), Initialized s,
LifeSpan(P +* I,Initialized s) + 2) = 0 &
DataPart Comput(P +* while>0(a,I), Initialized s,
LifeSpan(P +* I,Initialized s) + 2)
= DataPart Comput(P +* I, Initialized s,LifeSpan(P +* I,Initialized s));
theorem :: SCM_HALT:75
for s be State of SCM+FSA,
I be good InitHalting really-closed MacroInstruction of
SCM+FSA, a be read-write Int-Location st s.a > 0 & while>0(a,I) is InitHalting
holds DataPart IExec(while>0(a,I),P,s) =
DataPart IExec(while>0(a,I),P,IExec(I,P,s));
theorem :: SCM_HALT:76
for I be good InitHalting really-closed MacroInstruction of SCM+FSA,
a be read-write
Int-Location st (for s be State of SCM+FSA,P holds (s.a > 0
implies IExec(I,P,s).a < s.a )) holds while>0(a,I) is InitHalting;