:: The {\bf loop} and {\bf Times} Macroinstruction for {\SCMFSA}
:: by Noriko Asamoto
::
:: Received October 29, 1997
:: Copyright (c) 1997-2016 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, FSM_1, SCMFSA_2, CAT_1, AMI_1, SCMFSA8A,
XXREAL_0, CIRCUIT2, FUNCT_4, CARD_1, RELAT_1, ARYTM_3, AMISTD_2, GRAPHSP,
AMI_3, EXTPRO_1, TARSKI, FUNCT_1, ARYTM_1, SCMFSA6C, FUNCOP_1, SCMFSA6A,
SCMFSA6B, MSUALG_1, SCMFSA7B, SF_MASTR, STRUCT_0, NAT_1, SCMFSA8B,
SCMFSA8C, COMPOS_1, PARTFUN1, RELOC, SCMPDS_4, AMISTD_1, TURING_1,
SCMFSA_9;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
XCMPLX_0, NAT_1, FUNCOP_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_4, FUNCT_7,
PBOOLE, VALUED_1, AFINSQ_1, STRUCT_0, COMPOS_0, COMPOS_1, COMPOS_2,
MEMSTR_0, EXTPRO_1, AMISTD_1, AMISTD_2, SCMFSA_2, SF_MASTR, SCMFSA6A,
SCMFSA6B, SCMFSA6C, SCMFSA7B, SCMFSA8A, SCMFSA8B, NAT_D, XXREAL_0,
SCMFSA_M, SCMFSA_X;
constructors DOMAIN_1, XXREAL_0, REAL_1, SCMFSA6A, SF_MASTR, SCMFSA6B,
SCMFSA6C, SCMFSA8A, SCMFSA8B, AMISTD_2, NAT_D, AMI_3, RELSET_1, PRE_POLY,
SCMFSA7B, AMISTD_1, PBOOLE, SCMFSA_7, MEMSTR_0, WELLORD2, INT_2,
SCMFSA_2, VALUED_1, SCMFSA_M, FUNCT_7, SCMFSA_X, AMISTD_4, COMPOS_2;
registrations FUNCT_1, FUNCOP_1, XXREAL_0, XREAL_0, NAT_1, INT_1, SCMFSA_2,
SCMFSA6A, SCMFSA6B, SCMFSA6C, SCMFSA7B, SCMFSA8A, SCMFSA8B, ORDINAL1,
XBOOLE_0, AFINSQ_1, RELAT_1, SCMFSA10, COMPOS_1, EXTPRO_1, FUNCT_4,
MEMSTR_0, STRUCT_0, AMI_3, COMPOS_0, SCMFSA_M, FINSET_1, AMISTD_1,
SCMFSA_X, COMPOS_2, VALUED_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin :: Preliminaries
reserve m for Nat;
reserve P,PP,P1,P2 for Instruction-Sequence of SCM+FSA;
theorem :: SCMFSA8C:1
for s being State of SCM+FSA,I being initial Program of SCM+FSA
st I is_pseudo-closed_on s,P
for k being Nat st
for n being Nat st n <= k
holds IC Comput(P +* I,Initialize s,n) in dom I
holds k < pseudo-LifeSpan(s,P,I);
theorem :: SCMFSA8C:2
for I,J being Program of SCM+FSA, k being Nat
st card I <= k & k < card I + card J
for i being Instruction of SCM+FSA st i = J.(k -' card I)
holds (I ";" J). k = IncAddr(i,card I);
theorem :: SCMFSA8C:3
for s being State of SCM+FSA, I being Program of SCM+FSA holds
IExec(I,P,s) = IExec(I,P,Initialized s);
::$CT
theorem :: SCMFSA8C:5
for I being Program of SCM+FSA st
for s being State of SCM+FSA, P holds I is_halting_on Initialized s,P
holds Initialize((intloc 0).-->1) is I-halted;
theorem :: SCMFSA8C:6
for I being Program of SCM+FSA holds (for s being State of
SCM+FSA, P holds I is_halting_on Initialized s,P)
implies Initialize((intloc 0).-->1) is I-halted;
::$CT 5
theorem :: SCMFSA8C:12
for s being State of SCM+FSA, i being Instruction of SCM+FSA st
InsCode i in {0,6,7,8} holds DataPart Exec(i,s) = DataPart s;
::$CT
theorem :: SCMFSA8C:14
for s being State of SCM+FSA holds IExec(Stop SCM+FSA,P,s) = Initialized s;
::$CT
theorem :: SCMFSA8C:16
for s1 being 0-started State of SCM+FSA,
s2 being State of SCM+FSA,I being really-closed Program of SCM+FSA
st I c= P1
for n being Nat st
Reloc(I,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 :: SCMFSA8C:17
for s1,s2 being 0-started State of SCM+FSA,
I being really-closed Program of SCM+FSA
st I c= P1 & I c= P2 & DataPart s1 = DataPart s2
for i being Nat
holds IC Comput(P1, s1,i) = IC Comput(P2, s2,i) &
CurInstr(P1,Comput(P1,s1,i)) = CurInstr(P2,Comput(P2,s2,i)) &
DataPart Comput(P1, s1,i) = DataPart Comput(P2,s2,i);
theorem :: SCMFSA8C:18
for s1,s2 being 0-started State of SCM+FSA,
I being really-closed Program of SCM+FSA
st I is_halting_on s1,P1 & I c= P1 & I c= P2 &
DataPart s1 = DataPart s2
holds LifeSpan(P1,s1) = LifeSpan(P2,s2);
theorem :: SCMFSA8C:19
for s1,s2 being State of SCM+FSA,I being really-closed Program of SCM+FSA st
s1.intloc 0 = 1 & I is_halting_on s1,P1 &
((for a being read-write Int-Location holds s1.a = s2.a) &
for f being FinSeq-Location holds s1.f = s2.f)
holds DataPart IExec(I,P1,s1) = DataPart IExec(I,P2,s2);
theorem :: SCMFSA8C:20
for s1,s2 being State of SCM+FSA,
I being really-closed Program of SCM+FSA
st s1.intloc 0 = 1 & I is_halting_on s1,P1 &
DataPart s1 = DataPart s2
holds DataPart IExec(I,P1,s1) = DataPart IExec(I,P2,s2);
theorem :: SCMFSA8C:21
for s being State of SCM+FSA,
I being Program of SCM+FSA
st I is_pseudo-closed_on s,P
holds I is_pseudo-closed_on Initialize s,P+*I &
pseudo-LifeSpan(s,P,I) = pseudo-LifeSpan(Initialize s,P+*I,I);
theorem :: SCMFSA8C:22
for s1 being 0-started State of SCM+FSA,
s2 being State of SCM+FSA, I being Program of SCM+FSA st
I c= P1 & I is_pseudo-closed_on s1,P1
for n being Nat st Reloc(I,n) c= P2 &
IC s2 = n & DataPart s1 =
DataPart s2 holds ((for i being Nat
st i < pseudo-LifeSpan(s1,P1,I)
holds IncAddr(CurInstr(P1,Comput(P1,s1,i)),n)
= CurInstr(P2,Comput(P2,s2,i))) &
for i being Nat st i <= pseudo-LifeSpan(s1,P1,I)
holds IC Comput(P1, s1,i) + n = IC Comput(P2, s2,i) &
DataPart Comput(P1, s1,i) = DataPart Comput(P2, s2,i));
theorem :: SCMFSA8C:23
for s1,s2 being State of SCM+FSA, I being Program of SCM+FSA st
DataPart s1 = DataPart s2 holds I is_pseudo-closed_on s1,P1 implies I
is_pseudo-closed_on s2,P2;
theorem :: SCMFSA8C:24
for s being State of SCM+FSA, I being Program of SCM+FSA st s.
intloc 0 = 1 holds I is_pseudo-closed_on s,P iff
I is_pseudo-closed_on Initialized s,P;
theorem :: SCMFSA8C:25
for a being Int-Location, I,J being MacroInstruction of SCM+FSA holds
::: 0 in dom if=0(a,I,J) &
1 in dom if=0(a,I,J) &
::: 0 in dom if>0(a,I,J) &
1 in dom if>0(a,I,J);
theorem :: SCMFSA8C:26
for a being Int-Location, I,J being MacroInstruction of SCM+FSA
holds
if=0(a,I,J). 0 = a =0_goto (card J + 3) & if=0(a,I,J). 1 =
goto 2 & if>0(a,I,J). 0 = a >0_goto (card J + 3) & if>0(a,I
,J). 1 = goto 2;
theorem :: SCMFSA8C:27
for a being Int-Location, I,J being MacroInstruction of SCM+FSA, n being
Element of NAT st n < card I + card J + 3 holds n in dom if=0(a,I,J) & if=0(a,I
,J).n <> halt SCM+FSA;
theorem :: SCMFSA8C:28
for a being Int-Location, I,J being MacroInstruction of SCM+FSA, n being
Element of NAT st n < card I + card J + 3 holds n in dom if>0(a,I,J) & if>0(a,I
,J).n <> halt SCM+FSA;
theorem :: SCMFSA8C:29
for s being State of SCM+FSA, I being Program of SCM+FSA st
Directed I is_pseudo-closed_on s,P
holds I ";" Stop SCM+FSA is_halting_on s,P &
LifeSpan(P +* (I ";" Stop SCM+FSA),
Initialize s) =
pseudo-LifeSpan(s,P,Directed I) &
(for n being Nat st n < pseudo-LifeSpan(s,P,Directed I) holds
IC Comput(P +* I, (Initialize s),n)
= IC Comput(P +* (I ";" Stop SCM+FSA),
(Initialize s),n)) &
for n being Nat st n <= pseudo-LifeSpan(s,P,Directed I)
holds DataPart Comput(P +* I, (Initialize s),n)
= DataPart Comput(P+* (I ";" Stop SCM+FSA),
Initialize s,n);
theorem :: SCMFSA8C:30
for s being State of SCM+FSA, I being Program of SCM+FSA st
Directed I is_pseudo-closed_on s,P holds
DataPart Result(P +* (I ";" Stop SCM+FSA),
Initialize s) =
DataPart Comput(P +* I, (Initialize s),
pseudo-LifeSpan(s,P,Directed I));
theorem :: SCMFSA8C:31
for s being State of SCM+FSA, I being Program of SCM+FSA st s.intloc 0
= 1 & Directed I is_pseudo-closed_on s,P
holds DataPart IExec(I ";" Stop SCM+FSA,P,s)
= DataPart Comput(P +* I, (Initialize s),
pseudo-LifeSpan(s,P,Directed I));
theorem :: SCMFSA8C:32
for I,J being MacroInstruction of SCM+FSA,a being Int-Location
holds if=0
(a,I,J). (card I + card J + 3) = halt SCM+FSA;
theorem :: SCMFSA8C:33
for I,J being MacroInstruction of SCM+FSA,a being Int-Location holds if>0
(a,I,J). (card I + card J + 3) = halt SCM+FSA;
theorem :: SCMFSA8C:34
for I,J being MacroInstruction of SCM+FSA,a being Int-Location holds if=0
(a,I,J). (card J + 2) = goto (card I + card J + 3);
theorem :: SCMFSA8C:35
for I,J being MacroInstruction of SCM+FSA,a being Int-Location holds if>0
(a,I,J). (card J + 2) = goto (card I + card J + 3);
::$CT
theorem :: SCMFSA8C:37
for s being State of SCM+FSA, I,J being MacroInstruction of SCM+FSA,
a being read-write Int-Location st
s.a = 0 & Directed I is_pseudo-closed_on s,P
holds if=0(a,I,J) is_halting_on s,P &
LifeSpan(P +* if=0(a,I,J),Initialize s)
= LifeSpan(P +* (I ";" Stop SCM+FSA),
Initialize s) + 1;
theorem :: SCMFSA8C:38
for s being State of SCM+FSA, I,J being MacroInstruction of SCM+FSA,
a being
read-write Int-Location st s.intloc 0 = 1 & s.a = 0 & Directed I
is_pseudo-closed_on s,P holds DataPart IExec(if=0(a,I,J),P,s)
= DataPart IExec(I ";" Stop SCM+FSA,P,s);
theorem :: SCMFSA8C:39
for s being State of SCM+FSA, I,J being MacroInstruction of SCM+FSA, a
being read-write Int-Location
st s.a > 0 & Directed I is_pseudo-closed_on s,P
holds if>0(a,I,J) is_halting_on s,P &
LifeSpan(P+* if>0(a,I,J),Initialize s)
= LifeSpan(P +* (I ";" Stop SCM+FSA),Initialize s) + 1;
theorem :: SCMFSA8C:40
for s being State of SCM+FSA, I,J being MacroInstruction of SCM+FSA, a
being read-write Int-Location st s.intloc 0 = 1 & s.a > 0 & Directed I
is_pseudo-closed_on s,P holds DataPart IExec(if>0(a,I,J),P,s)
= DataPart IExec(I ";" Stop SCM+FSA,P,s);
theorem :: SCMFSA8C:41
for s being State of SCM+FSA, I,J being MacroInstruction of SCM+FSA, a
being read-write Int-Location st s.a <> 0 &
Directed J is_pseudo-closed_on s,P
holds if=0(a,I,J) is_halting_on s,P &
LifeSpan(P +* if=0(a,I,J),Initialize s)
= LifeSpan(P +* (J ";" Stop SCM+FSA),
Initialize s) + 3;
theorem :: SCMFSA8C:42
for s being State of SCM+FSA, I,J being MacroInstruction of SCM+FSA,
a being
read-write Int-Location st s.intloc 0 = 1 & s.a <> 0 & Directed J
is_pseudo-closed_on s,P holds
DataPart IExec(if=0(a,I,J),P,s) = DataPart IExec(J ";" Stop SCM+FSA,P,s);
theorem :: SCMFSA8C:43
for s being State of SCM+FSA, I,J being MacroInstruction of SCM+FSA, a
being read-write Int-Location st s.a <= 0 &
Directed J is_pseudo-closed_on s,P
holds if>0(a,I,J) is_halting_on s,P &
LifeSpan(P +* if>0(a,I,J),s +* (Start-At(0,SCM+FSA))) =
LifeSpan(P +* (J ";" Stop SCM+FSA),
Initialize s) + 3;
theorem :: SCMFSA8C:44
for s being State of SCM+FSA, I,J being MacroInstruction of SCM+FSA, a
being read-write Int-Location st s.intloc 0 = 1 & s.a <= 0 & Directed J
is_pseudo-closed_on s,P holds
DataPart IExec(if>0(a,I,J),P,s) = DataPart IExec(J
";" Stop SCM+FSA,P,s);
theorem :: SCMFSA8C:45
for s being State of SCM+FSA, I,J being MacroInstruction of SCM+FSA,
a being
read-write Int-Location st Directed I is_pseudo-closed_on s,P & Directed J
is_pseudo-closed_on s,P holds
if=0(a,I,J)
is_halting_on s,P;
theorem :: SCMFSA8C:46
for s being State of SCM+FSA, I,J being MacroInstruction of SCM+FSA, a being
read-write Int-Location st Directed I is_pseudo-closed_on s,P & Directed J
is_pseudo-closed_on s,P holds if>0(a,I,J) is_halting_on s,P;
theorem :: SCMFSA8C:47
for I being Program of SCM+FSA, a being Int-Location holds I
does not destroy a implies Directed I does not destroy a;
theorem :: SCMFSA8C:48
for i being Instruction of SCM+FSA, a being Int-Location holds i
does not destroy a implies Macro i does not destroy a;
theorem :: SCMFSA8C:49
for a being Int-Location holds halt SCM+FSA does not refer a;
theorem :: SCMFSA8C:50
for a,b,c being Int-Location holds a <> b implies AddTo(c,b)
does not refer a;
theorem :: SCMFSA8C:51
for i being Instruction of SCM+FSA, a being Int-Location holds
i does not refer a implies Macro i does not refer a;
theorem :: SCMFSA8C:52
for I,J being Program of SCM+FSA, a being Int-Location holds I
does not destroy a & J does not destroy a implies I ";" J does not destroy a;
theorem :: SCMFSA8C:53
for J being Program of SCM+FSA, i being Instruction of SCM+FSA,
a being Int-Location st i does not destroy a & J does not destroy a holds i ";"
J does not destroy a;
theorem :: SCMFSA8C:54
for I being Program of SCM+FSA, j being Instruction of SCM+FSA, a
being Int-Location st I does not destroy a & j does not destroy a holds I ";" j
does not destroy a;
theorem :: SCMFSA8C:55
for i,j being Instruction of SCM+FSA, a being Int-Location st i
does not destroy a & j does not destroy a holds i ";" j does not destroy a;
theorem :: SCMFSA8C:56
for a being Int-Location holds Stop SCM+FSA does not destroy a;
theorem :: SCMFSA8C:57
for a being Int-Location, l being Nat
holds Goto l does not destroy a;
theorem :: SCMFSA8C:58
for s being State of SCM+FSA, I being Program of SCM+FSA st I
is_halting_on Initialized s,P holds
(for 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) &
for f being FinSeq-Location
holds IExec(I,P,s).f = Comput(P +* I,Initialize Initialized s,
LifeSpan(P +* I,Initialize Initialized s)).f;
theorem :: SCMFSA8C:59
for s being State of SCM+FSA, I being parahalting 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 :: SCMFSA8C:60
for s being State of SCM+FSA,
I being really-closed Program of SCM+FSA, a
being Int-Location,k being Element of NAT
st I is_halting_on Initialized s,P & I does not destroy a
holds IExec(I,P,s).a = Comput(P +* I, (Initialize Initialized s),k).a;
theorem :: SCMFSA8C:61
for s being State of SCM+FSA,
I being parahalting 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 :: SCMFSA8C:62
for s being State of SCM+FSA,
I being parahalting 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 :: SCMFSA8C:63
for s being State of SCM+FSA, I being keeping_0 Program of
SCM+FSA st I is_halting_on Initialized s,P
holds IExec(I,P,s).intloc 0 = 1 & for k
being Nat holds Comput(P +* I,
(Initialize Initialized s),k).intloc 0 = 1;
theorem :: SCMFSA8C:64
for s being State of SCM+FSA, I being Program of SCM+FSA, a
being Int-Location st I does not destroy a holds for k being Element of NAT st
IC Comput(P +* I, (Initialize s),k) in dom I
holds Comput(P +* I,
(Initialize s),k + 1).a =
Comput(P +* I, (Initialize s),k).a;
theorem :: SCMFSA8C:65
for s being State of SCM+FSA, I being Program of SCM+FSA, a
being Int-Location st I does not destroy a for m being Nat st
(for n being Nat st n < m
holds IC Comput(P +* I, (Initialize s),n) in dom I)
for n being Nat st n <= m holds
Comput(P +* I, (Initialize s),n).a = s.a;
theorem :: SCMFSA8C:66
for s being State of SCM+FSA, I being good Program of SCM+FSA
for m being Nat st (for n being Nat st n < m holds IC
Comput(P +* I, (Initialize s),n) in dom I) holds
for n being Nat st n <= m
holds Comput(P +* I, (Initialize s),n).intloc 0 = s.intloc 0;
registration
cluster good keeping_0 really-closed parahalting
for MacroInstruction of SCM+FSA;
end;
theorem :: SCMFSA8C:67
for s being State of SCM+FSA,
I being good really-closed Program of SCM+FSA st
I is_halting_on Initialized s,P
holds IExec(I,P,s).intloc 0 = 1 & for k being Nat
holds Comput(P +* I, (Initialize Initialized s),k).intloc 0 = 1;
theorem :: SCMFSA8C:68
for s being State of SCM+FSA,
I being good really-closed Program of SCM+FSA
for k being Nat
holds Comput(P +* I, Initialize s,k).intloc 0 = s.intloc 0;
theorem :: SCMFSA8C:69
for P
for s being State of SCM+FSA,
I being keeping_0 parahalting 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;
theorem :: SCMFSA8C:70
for i being Instruction of SCM+FSA st i does not destroy intloc
0 holds Macro i is good;
theorem :: SCMFSA8C:71
for s1,s2 being State of SCM+FSA,
I being really-closed Program of SCM+FSA st
I is_halting_on s1,P1 & DataPart s1 = DataPart s2
for k being Nat holds
Comput(P1 +* I,Initialize s1,k)
= Comput(P2 +* I,Initialize s2,k)
& CurInstr(P1 +* I,Comput(P1 +* I,Initialize s1,k))
= CurInstr(P2 +* I,Comput(P2 +* I,Initialize s2,k));
theorem :: SCMFSA8C:72
for s1,s2 being State of SCM+FSA,
I being really-closed Program of SCM+FSA
st I is_halting_on s1,P1 & DataPart s1 = DataPart s2
holds
LifeSpan(P1 +* I,Initialize s1) =
LifeSpan(P2 +* I,Initialize s2) &
Result(P1 +* I,Initialize s1)
= Result(P2 +* I,Initialize s2);
theorem :: SCMFSA8C:73
for s1,s2 being 0-started State of SCM+FSA,
I being really-closed Program of SCM+FSA st
I is_halting_on s1,P1 &
I c= P1 & I c= P2 &
ex k being Nat st Comput(P1, s1,k) = s2
holds Result(P1,s1) = Result(P2,s2);
begin :: loop
::$CD
::$CT 8
begin :: Times
definition
let a be Int-Location;
let I be MacroInstruction of SCM+FSA;
func Times(a,I) -> Program of SCM+FSA equals
:: SCMFSA8C:def 2
while>0 (a,I ";" SubFrom(a, intloc 0));
end;
registration
let a be Int-Location;
let I be MacroInstruction of SCM+FSA;
cluster Times(a,I) -> halt-ending unique-halt;
end;
::$CT 6
theorem :: SCMFSA8C:88
for I,J being MacroInstruction of SCM+FSA, a,c being Int-Location st I
does not destroy c & J does not destroy c holds if=0(a,I,J) does not destroy c
& if>0(a,I,J) does not destroy c;
::$CT 2
theorem :: SCMFSA8C:91
for s being State of SCM+FSA,
I being good parahalting really-closed Program
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;
begin :: Example
reserve aa,bb for Int-Location;
theorem :: SCMFSA8C:92
for I being MacroInstruction of SCM+FSA holds
I does not destroy aa implies while>0(bb, I) does not destroy aa;
theorem :: SCMFSA8C:93
for I being MacroInstruction of SCM+FSA
for a,b being Int-Location st
I does not destroy b & a<>b holds Times(a,I) does not destroy b;
theorem :: SCMFSA8C:94
for a being Int-Location,I being MacroInstruction of SCM+FSA holds
card Times(a,I) = card I + 7;
reserve s for State of SCM+FSA,
a for Int-Location,
I for Program of SCM+FSA,
p for Instruction-Sequence of SCM+FSA;
theorem :: SCMFSA8C:95
for I being really-closed Program of SCM+FSA
st I is_halting_on Initialized s,p & I does not destroy a
holds IExec(I,p,s).a = (Initialized s).a;
theorem :: SCMFSA8C:96
for I,J being MacroInstruction of SCM+FSA st
I does not destroy aa & J does not destroy aa
holds I ';' J does not destroy aa;
theorem :: SCMFSA8C:97
for I being MacroInstruction of SCM+FSA st I does not destroy aa
holds I ';' goto 0 does not destroy aa;
theorem :: SCMFSA8C:98
for I being MacroInstruction of SCM+FSA holds
I does not destroy aa implies
if>0(bb, I ';' goto 0) does not destroy aa;
theorem :: SCMFSA8C:99
for I being MacroInstruction of SCM+FSA holds
I does not destroy aa implies
if=0(bb, I ';' goto 0) does not destroy aa;