:: Conditional branch macro instructions of SCM+FSA, Part II
:: by Noriko Asamoto
::
:: Received August 27, 1996
:: Copyright (c) 1996-2019 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, SCMFSA_2, AMI_1, AMISTD_2, CARD_1, TARSKI, SCMFSA6A,
FUNCT_4, FSM_1, RELAT_1, CIRCUIT2, FUNCT_1, SF_MASTR, SUBSET_1, ARYTM_3,
SCMFSA7B, SCMFSA6B, SCMFSA6C, AMI_3, SCMFSA8A, NAT_1, GRAPHSP, XXREAL_0,
MSUALG_1, STRUCT_0, ARYTM_1, INT_1, COMPLEX1, PARTFUN1, FINSEQ_1,
FINSEQ_2, SCMFSA8B, EXTPRO_1, RELOC, FUNCOP_1, COMPOS_1, AMISTD_1,
FRECHET;
notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0,
XXREAL_0, NAT_1, NAT_D, CARD_3, VALUED_1, INT_1, RELAT_1, FUNCT_1,
PARTFUN1, FUNCOP_1, FUNCT_4, PBOOLE, FUNCT_7, FINSEQ_1, FINSEQ_2,
STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1, COMPOS_2, EXTPRO_1, AMISTD_1,
AMISTD_2, SCMFSA_2, SCMFSA6A, SF_MASTR, SCMFSA6B, SCMFSA6C, SCMFSA7B,
SCMFSA8A, INT_2, SCMFSA_M;
constructors DOMAIN_1, XXREAL_0, NAT_1, INT_2, SCMFSA6A, SF_MASTR, SCMFSA6B,
SCMFSA6C, SCMFSA8A, AMISTD_2, RELSET_1, SCMFSA7B, PRE_POLY, AMISTD_1,
PBOOLE, FUNCOP_1, FUNCT_4, MEMSTR_0, SCMFSA_M, FUNCT_7, SCMFSA_X, NAT_D,
AMI_3, COMPOS_2;
registrations XXREAL_0, XREAL_0, NAT_1, INT_1, SCMFSA_2, SCMFSA6B, SCMFSA6C,
ORDINAL1, MEMSTR_0, RELSET_1, SCMFSA10, AMISTD_2, COMPOS_1, EXTPRO_1,
FUNCT_4, FUNCOP_1, STRUCT_0, AMI_3, COMPOS_0, SCMFSA_M, SCMFSA6A,
AMISTD_1, SCMFSA_X, AFINSQ_1, CARD_3, FUNCT_1, VALUED_1, RELAT_1, CARD_1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
begin
reserve P,P1,P2 for Instruction-Sequence of SCM+FSA;
::$CT 4
theorem :: SCMFSA8B:5
for s1,s2 being State of SCM+FSA, I being really-closed Program of SCM+FSA
st DataPart s1 = DataPart s2
holds
:::I is_closed_on s1,P1 &
I is_halting_on s1,P1
implies
::: I is_closed_on s2,P2 &
I is_halting_on s2,P2;
:: theorem Th5:
:: for s being State of SCM+FSA, I,J being Program of SCM+FSA holds
:: I is_closed_on Initialized s,P iff
:: I is_closed_on s +* Initialize((intloc 0).-->1),P+*J
:: proof
:: let s be State of SCM+FSA;
:: let I,J be Program of SCM+FSA;
:: DataPart Initialized s = DataPart(s +* Initialize((intloc 0).-->1));
:: hence thesis by Th2;
:: end;
:: theorem Th6:
:: for s being State of SCM+FSA, I,J being Program of SCM+FSA, l
:: being Element of NAT holds I is_closed_on s,P iff I is_closed_on
:: s +* (Start-At(0,SCM+FSA)),P+*I
:: proof
:: let s be State of SCM+FSA;
:: let I,J be Program of SCM+FSA;
:: let l be Element of NAT;
:: DataPart s = DataPart(Initialize s) by MEMSTR_0:79;
:: hence thesis by Th2;
:: end;
::$CT 2
theorem :: SCMFSA8B:8
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 is_closed_on s1,P1 &
I c= P1
for n being Nat st
IC s2 = n & DataPart s1 = DataPart s2 & Reloc(I,n) c= P2
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 :: SCMFSA8B:9
for s being State of SCM+FSA, i being keeping_0 sequential
Instruction of SCM+FSA,
J being parahalting 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 :: SCMFSA8B:10
for s being State of SCM+FSA, i being keeping_0 sequential
Instruction of SCM+FSA,
J being parahalting 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;
definition
let a be Int-Location;
let I,J be MacroInstruction of SCM+FSA;
func if=0(a,I,J) -> Program of SCM+FSA equals
:: SCMFSA8B:def 1
a =0_goto (card J + 3)
";" J ";" Goto (card I + 1) ";" I ";" Stop SCM+FSA;
func if>0(a,I,J) -> Program of SCM+FSA equals
:: SCMFSA8B:def 2
a >0_goto (card J + 3)
";" J ";" Goto (card I + 1) ";" I ";" Stop SCM+FSA;
end;
:: definition
:: let a be Int-Location;
:: let I,J be Program of SCM+FSA;
:: func if<0(a,I,J) -> Program of SCM+FSA equals
:: if=0(a,J,if>0(a,J,I));
:: coherence;
:: end;
:: definicjas w tym sensie jest niepoporawna, ze powtarza instrukcje J
::$CD
theorem :: SCMFSA8B:11
for I,J being MacroInstruction of SCM+FSA, a being Int-Location holds
card if=0(a,I,J) = card I + card J + 4;
theorem :: SCMFSA8B:12
for I,J being MacroInstruction of SCM+FSA, a being Int-Location holds
card if>0(a,I,J) = card I + card J + 4;
theorem :: SCMFSA8B:13
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_on s,P &
I is_halting_on s,P
holds
:::if=0(a,I,J) is_closed_on s,P &
if=0(a,I,J) is_halting_on s,P;
theorem :: SCMFSA8B:14
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_on Initialized s,P
& I is_halting_on Initialized s,P
holds IExec(if=0(a,I,J),P,s)
= IExec(I,P,s) +* Start-At((card I + card J + 3),SCM+FSA);
registration
let I,J be really-closed MacroInstruction of SCM+FSA,
a be Int-Location;
cluster if=0(a,I,J) -> really-closed;
cluster if>0(a,I,J) -> really-closed;
end;
theorem :: SCMFSA8B:15
for s being State of SCM+FSA,
::: I being Program 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_on s,P &
J is_halting_on s,P
holds
:::if=0(a,I,J) is_closed_on s,P &
if=0(a,I,J) is_halting_on s,P;
theorem :: SCMFSA8B:16
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 &
::: J is_closed_on Initialized s,P &
J is_halting_on Initialized 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 :: SCMFSA8B:17
for s being State of SCM+FSA,
I,J being parahalting really-closed MacroInstruction of SCM+FSA,
a being read-write Int-Location
holds if=0(a,I,J) is parahalting &
(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 :: SCMFSA8B:18
for s being State of SCM+FSA,
I,J being parahalting 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 :: SCMFSA8B:19
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_on s,P&
I is_halting_on s,P
holds
:::if>0(a,I,J) is_closed_on s,P &
if>0(a,I,J) is_halting_on s,P;
theorem :: SCMFSA8B:20
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 &
::: I is_closed_on Initialized s,P &
I is_halting_on Initialized 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 :: SCMFSA8B:21
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_on s,P &
J is_halting_on s,P
holds
:::if>0(a,I,J) is_closed_on s,P &
if>0(a,I,J) is_halting_on s,P;
theorem :: SCMFSA8B:22
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 &
::: J is_closed_on Initialized s,P &
J is_halting_on Initialized 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 :: SCMFSA8B:23
for s being State of SCM+FSA,
I,J being parahalting really-closed MacroInstruction of SCM+FSA,
a being read-write Int-Location holds if>0(a,I,J) is parahalting & (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 :: SCMFSA8B:24
for s being State of SCM+FSA,
I,J being parahalting 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 7
registration
let I,J be parahalting really-closed MacroInstruction of SCM+FSA;
let a be read-write Int-Location;
cluster if=0(a,I,J) -> parahalting;
cluster if>0(a,I,J) -> parahalting;
end;
definition
let a,b be Int-Location;
let I,J be MacroInstruction of SCM+FSA;
func if=0(a,b,I,J) -> Program of SCM+FSA equals
:: SCMFSA8B:def 4
SubFrom(a,b) ";" if=0(a,I,J);
func if>0(a,b,I,J) -> Program of SCM+FSA equals
:: SCMFSA8B:def 5
SubFrom(a,b) ";" if>0(a,I,J);
end;
registration
let a be Int-Location;
let I,J be MacroInstruction of SCM+FSA;
cluster if=0(a,I,J) -> halt-ending unique-halt;
cluster if>0(a,I,J) -> halt-ending unique-halt;
end;
registration
let a,b be Int-Location;
let I,J be really-closed MacroInstruction of SCM+FSA;
cluster if=0(a,b,I,J) -> really-closed;
cluster if>0(a,b,I,J) -> really-closed;
end;
registration
let a,b be Int-Location;
let I,J be MacroInstruction of SCM+FSA;
cluster if=0(a,b,I,J) -> halt-ending unique-halt;
cluster if>0(a,b,I,J) -> halt-ending unique-halt;
end;
registration
let I,J be parahalting really-closed MacroInstruction of SCM+FSA;
let a,b be read-write Int-Location;
cluster if=0(a,b,I,J) -> parahalting;
cluster if>0(a,b,I,J) -> parahalting;
end;
registration
let I,J be really-closed MacroInstruction of SCM+FSA;
let a,b be read-write Int-Location;
cluster if=0(a,b,I,J) -> really-closed;
cluster if>0(a,b,I,J) -> really-closed;
end;
theorem :: SCMFSA8B:32
for s being State of SCM+FSA, I being Program of SCM+FSA holds
DataPart Result(P+*I,Initialized s) = DataPart IExec(I,P,s);
theorem :: SCMFSA8B:33
for s being State of SCM+FSA, I being Program of SCM+FSA
holds Result(P+*I,Initialized s) = IExec(I,P,s);
theorem :: SCMFSA8B:34
for s1,s2 being State of SCM+FSA, i being Instruction of SCM+FSA
, a being Int-Location holds (for b being Int-Location st a <> b holds s1.b =
s2.b) & (for f being FinSeq-Location holds s1.f = s2.f) & i does not refer a &
IC s1 = IC s2 implies (for b being Int-Location st a <> b holds Exec(i,s1).b =
Exec(i,s2).b) & (for f being FinSeq-Location holds Exec(i,s1).f = Exec(i,s2).f)
& IC Exec(i,s1) = IC Exec(i,s2);
theorem :: SCMFSA8B:35
for s1,s2 being State of SCM+FSA, I being really-closed Program of SCM+FSA,
a being Int-Location
st I does not refer a &
(for b being Int-Location st a <> b holds s1.b = s2.b) &
(for f being FinSeq-Location holds s1.f = s2.f)
:::& I is_closed_on s1,P1
holds
for k being Nat holds
(for b being Int-Location st a <> b
holds Comput(P1+*I,(Initialize s1),k).b
= Comput(P2+*I, (Initialize s2),k).b) &
(for f being FinSeq-Location holds
Comput(P1+*I,(Initialize s1),k).f
= Comput(P2+*I, (Initialize s2),k).f) &
IC Comput(P1+*I, (Initialize s1),k)
= IC 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 :: SCMFSA8B:36
for s being State of SCM+FSA, I being really-closed Program of SCM+FSA, l
being Nat holds
:::I is_closed_on s,P &
I is_halting_on s,P
iff
:::I is_closed_on s +* Start-At(l,SCM+FSA),P+*I &
I is_halting_on s +* Start-At(l,SCM+FSA),P+*I;
theorem :: SCMFSA8B:37
for s1,s2 being State of SCM+FSA,
I being really-closed Program of SCM+FSA, a
being Int-Location st I does not refer a & (for b being Int-Location st a <> b
holds s1.b = s2.b) & (for f being FinSeq-Location holds s1.f = s2.f) &
:::& Iis_closed_on s1,P1 &
I is_halting_on s1,P1
holds
:::I is_closed_on s2,P2 &
I is_halting_on s2,P2;
theorem :: SCMFSA8B:38
for s1,s2 being State of SCM+FSA,
I being really-closed Program of SCM+FSA, a
being Int-Location holds (for d being read-write Int-Location st a <> d holds
s1.d = s2.d) & (for f being FinSeq-Location holds s1.f = s2.f) & I
does not refer a &
:::I is_closed_on Initialized s1,P1 &
I is_halting_on Initialized s1,P1
implies (for d being Int-Location st a <> d
holds IExec(I,P1,s1).d = IExec(I,P2,s2).d) &
(for f being FinSeq-Location holds IExec(I,P1,s1).f = IExec(I,P2,s2).f) & IC
IExec(I,P1,s1) = IC IExec(I,P2,s2);
theorem :: SCMFSA8B:39
for s being State of SCM+FSA,
I,J being parahalting really-closed MacroInstruction of SCM+FSA,
a,b being read-write Int-Location
st I does not refer a & J does not refer a
holds IC IExec(if=0(a,b,I,J),P,s) = (card I + card J + 5) & (s.a = s.b
implies ((for d being Int-Location st a <> d
holds IExec(if=0(a,b,I,J),P,s).d =
IExec(I,P,s).d) & for f being FinSeq-Location
holds IExec(if=0(a,b,I,J),P,s).f =
IExec(I,P,s).f)) & (s.a <> s.b implies
((for d being Int-Location st a <> d holds
IExec(if=0(a,b,I,J),P,s).d = IExec(J,P,s).d) &
for f being FinSeq-Location holds
IExec(if=0(a,b,I,J),P,s).f = IExec(J,P,s).f));
theorem :: SCMFSA8B:40
for s being State of SCM+FSA,
I,J being parahalting really-closed MacroInstruction of SCM+FSA
, a,b being read-write Int-Location st I does not refer a & J does not refer a
holds IC IExec(if>0(a,b,I,J),P,s) = (card I + card J + 5) & (s.a > s.b
implies (for d being Int-Location st a <> d
holds IExec(if>0(a,b,I,J),P,s).d =
IExec(I,P,s).d) & for f being FinSeq-Location
holds IExec(if>0(a,b,I,J),P,s).f =
IExec(I,P,s).f) & (s.a <= s.b implies
(for d being Int-Location st a <> d holds
IExec(if>0(a,b,I,J),P,s).d = IExec(J,P,s).d) &
for f being FinSeq-Location holds
IExec(if>0(a,b,I,J),P,s).f = IExec(J,P,s).f);
reserve s for State of SCM+FSA,
I for Program of SCM+FSA,
p for Instruction-Sequence of SCM+FSA;
:: theorem
:: s.intloc 0 = 1 implies (I is_closed_on s,p iff I is_closed_on
:: Initialized s,p)
:: proof
:: assume s.intloc 0 = 1;
:: then DataPart Initialized s = DataPart s by SCMFSA_M:19;
:: hence thesis by Th2;
:: end;
::$CT
theorem :: SCMFSA8B:42
for I being really-closed Program of SCM+FSA st s.intloc 0 = 1
holds I is_halting_on s,p iff I is_halting_on Initialized s,p;