:: Conditional branch macro instructions of SCM+FSA, Part II
:: by Noriko Asamoto
::
:: Received August 27, 1996
:: Copyright (c) 1996-2026 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, COMPOS_0, SCMFSA_M, SCMFSA6A, CARD_1;
requirements NUMERALS, REAL, SUBSET, ARITHM;
equalities FUNCOP_1, EXTPRO_1, SCMFSA6A, MEMSTR_0, SCMFSA_M;
expansions EXTPRO_1, SCMFSA_M;
theorems TARSKI, NAT_1, FUNCT_1, FUNCT_4, SCMFSA_2, MEMSTR_0, SCMFSA6A,
GRFUNC_1, SCMFSA6B, SCMFSA6C, SCMFSA7B, SCMFSA8A, XBOOLE_1, XREAL_1,
ORDINAL1, FUNCOP_1, PARTFUN1, AFINSQ_1, COMPOS_1, EXTPRO_1, PBOOLE,
AMISTD_1, COMPOS_0, SCMFSA_M, SCMFSA_X;
schemes NAT_1;
begin
set A = NAT;
set D = Data-Locations SCM+FSA;
set SA0 = Start-At(0,SCM+FSA);
reserve P,P1,P2 for Instruction-Sequence of SCM+FSA;
::$CT 4
theorem Th1:
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
proof
let s1,s2 be State of SCM+FSA;
let I be really-closed Program of SCM+FSA;
set S1 = Initialize s1, S2 = Initialize s2;
IC S1 = 0 by MEMSTR_0:47;
then
A1: IC S1 in dom I by AFINSQ_1:65;
A2: I c= P1+*I by FUNCT_4:25;
defpred P[Nat] means
IC Comput(P1+*I,S1,$1) = IC Comput(P2+*I,S2,$1) &
CurInstr(P1+*I,Comput(P1+*I,S1,$1))
= CurInstr(P2+*I,Comput(P2+*I,S2,$1)) &
DataPart Comput(P1+*I,S1,$1)
= DataPart Comput(P2+*I,S2,$1);
A3: IC SCM+FSA in dom Start-At(0,SCM+FSA) by MEMSTR_0:15;
A4: IC Comput(P1+*I,S1,0)
= IC Start-At(0,SCM+FSA) by A3,FUNCT_4:13
.= 0 by FUNCOP_1:72;
A5: IC Comput(P2+*I,S2,0)
= IC Start-At(0,SCM+FSA) by A3,FUNCT_4:13
.= 0 by FUNCOP_1:72;
assume DataPart s1 = DataPart s2;
then
A6: Comput(P1+*I,S1,0) = Comput(P2+*I,S2,0) by MEMSTR_0:80;
A7: now
let k be Nat;
A8: Comput(P2+*I,S2,k+1) = Following(P2+*I,Comput(P2+*I,S2,k)) by EXTPRO_1:3
.= Exec(CurInstr(P2+*I,Comput(P2+*I,S2,k)), Comput(P2+*I,S2,k));
assume
A9: P[k];
then
A10: for f being FinSeq-Location holds Comput(P1+*I,S1,k).f = Comput(
P2+*I,
S2, k).f by SCMFSA_M:2;
for a being Int-Location holds Comput(P1+*I,S1,k).a = Comput(
P2+*I,S2,k
) .a by A9,SCMFSA_M:2;
then
A11: Comput(P1+*I,S1,k) = Comput(P2+*I,S2,k)
by A9,A10,SCMFSA_2:61;
A12: IC Comput(P1+*I,S1,k+1) in dom I by A1,A2,AMISTD_1:21;
Comput(P1+*I,S1,k+1) = Following(P1+*I,
Comput(P1+*I,S1,k)) by EXTPRO_1:3
.= Exec(CurInstr(P1+*I,Comput(P1+*I,S1,k)),
Comput(P1+*I,S1,k));
then
A13: Comput(P1+*I,S1,k+1) = Comput(P2+*I,S2,k+1)
by A9,A11,A8;
A14: IC Comput(P1+*I,S1,k+1) = IC Comput(P2+*I,S2,k+1) by A13;
A15: (P1+*I)/.IC Comput(P1+*I,S1,k+1)
= (P1+*I).IC Comput(P1+*I,S1,k+1) by PBOOLE:143;
A16: (P2+*I)/.IC Comput(P2+*I,S2,k+1)
= (P2+*I).IC Comput(P2+*I,S2,k+1) by PBOOLE:143;
A17: I c= P1+*I by FUNCT_4:25;
A18: I c= P2+*I by FUNCT_4:25;
CurInstr(P1+*I,Comput(P1+*I,S1,k+1))
= I.IC Comput(P1+*I,S1,k+1) by A12,A15,A17,GRFUNC_1:2
.= CurInstr(P2+*I,Comput(P2+*I,S2,k+1))
by A14,A12,A16,A18,GRFUNC_1:2;
hence P[k+1] by A13;
end;
assume I is_halting_on s1,P1;
then P1+*I halts_on Initialize s1 by SCMFSA7B:def 7;
then consider m being Nat such that
A19: CurInstr(P1+*I,Comput(P1+*I,S1,m))
= halt SCM+FSA;
A20: (P1+*I)/.IC Comput(P1+*I,S1,0)
= (P1+*I).IC Comput(P1+*I,S1,0) by PBOOLE:143;
A21: (P2+*I)/.IC Comput(P2+*I,S2,0)
= (P2+*I).IC Comput(P2+*I,S2,0) by PBOOLE:143;
A22: 0 in dom I by AFINSQ_1:65;
then CurInstr(P1+*I,Comput(P1+*I,S1,0))
= I. 0 by A4,A20,FUNCT_4:13
.= CurInstr(P2+*I,Comput(P2+*I,S2,0))
by A5,A22,A21,FUNCT_4:13;
then
A23: P[0] by A6;
for k being Nat holds P[k] from NAT_1:sch 2(A23,A7);
then CurInstr(P2+*I,Comput(P2+*I,S2,m))
= halt SCM+FSA by A19;
then P2+*I halts_on Initialize s2 by EXTPRO_1:29;
hence thesis by SCMFSA7B:def 7;
end;
:: 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 Th2:
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)
proof
let s1 be 0-started State of SCM+FSA,
s2 be State of SCM+FSA;
let I be really-closed Program of SCM+FSA;
A1: Start-At(0,SCM+FSA) c= s1 by MEMSTR_0:29;
:: assume
:: A2: I is_closed_on s1,P1;
assume
A2: I c= P1;
let n be Nat;
A3: IC SCM+FSA in dom Start-At(0,SCM+FSA) by MEMSTR_0:15;
defpred P[Nat] means IC Comput(P1,s1,$1) + n = IC Comput(
P2,s2,$1) &
IncAddr(CurInstr(P1,Comput(P1,s1,$1)),n)
= CurInstr(P2,Comput(P2,s2,$1)) &
DataPart Comput(P1,s1,$1) = DataPart Comput(P2,s2,$1);
A4: IC Comput(P1,s1,0) = IC s1
.= IC Start-At(0,SCM+FSA) by A1,A3,GRFUNC_1:2
.= 0 by FUNCOP_1:72;
assume
A5: IC s2 = n;
A6: 0 in dom I by AFINSQ_1:65;
then
A7: 0 + n in dom Reloc(I,n) by COMPOS_1:46;
IC SCM+FSA in dom Start-At(0,SCM+FSA) by MEMSTR_0:15;
then
A8: P1.IC s1 = P1.IC Start-At(0,SCM+FSA) by A1,GRFUNC_1:2
.= P1. 0 by FUNCOP_1:72
.= I. 0 by A6,A2,GRFUNC_1:2;
assume DataPart s1 = DataPart s2;
then
A9: DataPart Comput(P1,s1,0) = DataPart s2
.= DataPart Comput(P2,s2,0);
assume
A10: Reloc(I,n) c= P2;
let i be Nat;
A11: (P2)/.IC s2 = P2.IC s2 by PBOOLE:143;
A12: CurInstr(P1,s1) = I.0 by A8,PBOOLE:143;
IncAddr(CurInstr(P1,Comput(P1,s1,0)),n)
= IncAddr(CurInstr(P1,s1),n)
.= Reloc(I,n).( 0 + n) by A12,A6,COMPOS_1:35
.= CurInstr(P2,s2) by A5,A7,A11,A10,GRFUNC_1:2
.= CurInstr(P2,Comput(P2,s2,0));
then
A13: P[0] by A5,A4,A9;
A14: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
A15: Comput(P1,s1,k+1) = Following(P1,Comput(P1,s1,k))
by EXTPRO_1:3
.= Exec(CurInstr(P1,Comput(P1,s1,k)),
Comput(P1,s1,k));
IC s1 = 0 by MEMSTR_0:def 11;
then
A16: IC s1 in dom I by AFINSQ_1:65;
A17: I c= P1+*I by FUNCT_4:25;
reconsider l = IC Comput(P1,s1,k+1) as Element of NAT;
reconsider
j = CurInstr(P1,Comput(P1,s1,k+1)) as Instruction of SCM+FSA;
A18: Comput(P2,s2,k+1) = Following(P2,Comput(P2,s2,k)) by EXTPRO_1:3
.= Exec(CurInstr(P2,Comput(P2,s2,k)),Comput(P2,s2,k));
A19: P1 = P1+*I by A2,FUNCT_4:98;
then
A20: IC Comput(P1,s1,k+1) in dom I by A16,A17,AMISTD_1:21;
assume
A21: P[k];
hence
A22: IC Comput(P1,s1,k+1) + n = IC Comput(P2,s2,k+1)
by A15,A18,SCMFSA6A:8;
then
A23: IC Comput(P2,s2,k+1) in dom Reloc(I,n) by A20,COMPOS_1:46;
A24: l in dom I by A19,A16,A17,AMISTD_1:21;
j = P1.IC Comput(P1,s1,k+1) by PBOOLE:143
.= I.l by A20,A2,GRFUNC_1:2;
hence IncAddr(CurInstr(P1,Comput(P1,s1,k+1)),n)
= Reloc(I,n).(l + n) by A24,COMPOS_1:35
.= P2.IC Comput(P2,s2,k+1) by A23,A22,A10,GRFUNC_1:2
.= CurInstr(P2,Comput(P2,s2,k+1)) by PBOOLE:143;
thus thesis by A21,A15,A18,SCMFSA6A:8;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A13,A14);
hence thesis;
end;
theorem Th3:
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
proof
let s be State of SCM+FSA;
let i be keeping_0 sequential Instruction of SCM+FSA;
let J be parahalting really-closed Program of SCM+FSA;
let a be Int-Location;
A1: IExec(Macro i,P,s) = Exec(i,Initialized s) by SCMFSA6C:5;
thus IExec(i ";" J,P,s).a
= IExec(J,P,IExec(Macro i,P,s)).a by SCMFSA6C:1
.= ( IExec(J,P,IExec(Macro i,P,s))).a
.= ( IExec(J,P,Exec(i,Initialized s))).a by A1
.= IExec(J,P,Exec(i,Initialized s)).a;
end;
theorem Th4:
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
proof
let s be State of SCM+FSA;
let i be keeping_0 sequential Instruction of SCM+FSA;
let J be parahalting really-closed Program of SCM+FSA;
let f be FinSeq-Location;
A1: IExec(Macro i,P,s) = Exec(i,Initialized s) by SCMFSA6C:5;
thus IExec(i ";" J,P,s).f
= IExec(J,P,IExec(Macro i,P,s)).f by SCMFSA6C:2
.= ( IExec(J,P,IExec(Macro i,P,s))).f
.= ( IExec(J,P,Exec(i,Initialized s))).f by A1
.= IExec(J,P,Exec(i,Initialized s)).f;
end;
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
a =0_goto (card J + 3)
";" J ";" Goto (card I + 1) ";" I ";" Stop SCM+FSA;
coherence;
func if>0(a,I,J) -> Program of SCM+FSA equals
a >0_goto (card J + 3)
";" J ";" Goto (card I + 1) ";" I ";" Stop SCM+FSA;
coherence;
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
Lm1: for a being Int-Location, I,J being MacroInstruction of SCM+FSA holds
1 in dom if=0(a,I,J) & 1 in dom if>0(a,I,J)
proof
let a be Int-Location;
let I,J be MacroInstruction of SCM+FSA;
set i = a =0_goto (card J + 3);
if=0(a,I,J) = i ";" J ";" Goto (card I + 1) ";" (I ";" Stop
SCM+FSA) by SCMFSA6A:25
.= i ";" J ";" (Goto (card I + 1) ";" (I ";" Stop SCM+FSA)) by SCMFSA6A:25
.= i ";" (J ";" (Goto (card I + 1) ";" (I ";" Stop SCM+FSA))) by
SCMFSA6A:29
.= Macro i ";" (J ";" (Goto (card I + 1) ";" (I ";" Stop SCM+FSA)
));
then
A1: dom Macro i c= dom if=0(a,I,J) by SCMFSA6A:17;
dom Macro i = { 0, 1} by COMPOS_1:61;
then 1 in dom Macro i by TARSKI:def 2;
hence 1 in dom if=0(a,I,J) by A1;
set i = a >0_goto (card J + 3);
if>0(a,I,J) = i ";" J ";" Goto (card I + 1) ";" (I ";" Stop
SCM+FSA) by SCMFSA6A:25
.= i ";" J ";" (Goto (card I + 1) ";" (I ";" Stop SCM+FSA)) by SCMFSA6A:25
.= i ";" (J ";" (Goto (card I + 1) ";" (I ";" Stop SCM+FSA))) by
SCMFSA6A:29
.= Macro i ";" (J ";" (Goto (card I + 1) ";" (I ";" Stop SCM+FSA)
));
then
A2: dom Macro i c= dom if>0(a,I,J) by SCMFSA6A:17;
dom Macro i = { 0, 1} by COMPOS_1:61;
then 1 in dom Macro i by TARSKI:def 2;
hence thesis by A2;
end;
Lm2: 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
proof
let a be Int-Location;
let I,J be MacroInstruction of SCM+FSA;
set i = a =0_goto (card J + 3);
A1: if=0(a,I,J) = i ";" J ";" Goto (card I + 1) ";" (I ";" Stop
SCM+FSA) by SCMFSA6A:25
.= i ";" J ";" (Goto (card I + 1) ";" (I ";" Stop SCM+FSA)) by SCMFSA6A:25
.= i ";" (J ";" (Goto (card I + 1) ";" (I ";" Stop SCM+FSA))) by
SCMFSA6A:29
.= Macro i ";" (J ";" (Goto (card I + 1) ";" (I ";" Stop SCM+FSA)
));
A2: dom Macro i = { 0, 1} by COMPOS_1:61;
then 0 in dom Macro i by TARSKI:def 2;
hence if=0(a,I,J). 0 = (Directed Macro i). 0 by A1,SCMFSA8A:14
.= i by SCMFSA7B:1;
1 in dom Macro i by A2,TARSKI:def 2;
hence if=0(a,I,J). 1 = (Directed Macro i). 1 by A1,SCMFSA8A:14
.= goto 2 by SCMFSA7B:2;
set i = a >0_goto (card J + 3);
A3: if>0(a,I,J) = i ";" J ";" Goto (card I + 1) ";" (I ";" Stop
SCM+FSA) by SCMFSA6A:25
.= i ";" J ";" (Goto (card I + 1) ";" (I ";" Stop SCM+FSA)) by SCMFSA6A:25
.= i ";" (J ";" (Goto (card I + 1) ";" (I ";" Stop SCM+FSA))) by
SCMFSA6A:29
.= Macro i ";" (J ";" (Goto (card I + 1) ";" (I ";" Stop SCM+FSA)
));
A4: dom Macro i = { 0, 1} by COMPOS_1:61;
then 0 in dom Macro i by TARSKI:def 2;
hence if>0(a,I,J). 0 = (Directed Macro i). 0 by A3,SCMFSA8A:14
.= i by SCMFSA7B:1;
1 in dom Macro i by A4,TARSKI:def 2;
hence if>0(a,I,J). 1 = (Directed Macro i). 1 by A3,SCMFSA8A:14
.= goto 2 by SCMFSA7B:2;
end;
theorem
for I,J being MacroInstruction of SCM+FSA, a being Int-Location holds
card if=0(a,I,J) = card I + card J + 4
proof
let I,J be MacroInstruction of SCM+FSA;
let a be Int-Location;
A1: card Stop SCM+FSA = 1 by COMPOS_1:4;
thus card if=0(a,I,J)
= card (Macro (a =0_goto (card J + 3)) ";" J ";" Goto (
card I + 1) ";" I) + 1 by A1,SCMFSA6A:21
.= card (Macro (a =0_goto (card J + 3)) ";" J ";" Goto (
card I + 1)) + card I + 1 by SCMFSA6A:21
.= card (Macro (a =0_goto (card J + 3)) ";" J) + card Goto
(card I + 1) + card I + 1 by SCMFSA6A:21
.= card (Macro (a =0_goto (card J + 3)) ";" J) + 1 + card I + 1
by SCMFSA8A:15
.= card Macro (a =0_goto (card J + 3)) + card J + 1 + card I + 1
by SCMFSA6A:21
.= 2 + card J + 1 + card I + 1 by COMPOS_1:56
.= card I + card J + 4;
end;
theorem
for I,J being MacroInstruction of SCM+FSA, a being Int-Location holds
card if>0(a,I,J) = card I + card J + 4
proof
let I,J be MacroInstruction of SCM+FSA;
let a be Int-Location;
A1: card Stop SCM+FSA = 1 by COMPOS_1:4;
thus card if>0(a,I,J)
= card (Macro (a >0_goto (card J + 3)) ";" J ";" Goto (
card I + 1) ";" I) + 1 by A1,SCMFSA6A:21
.= card (Macro (a >0_goto (card J + 3)) ";" J ";" Goto (
card I + 1)) + card I + 1 by SCMFSA6A:21
.= card (Macro (a >0_goto (card J + 3)) ";" J) + card Goto
(card I + 1) + card I + 1 by SCMFSA6A:21
.= card (Macro (a >0_goto (card J + 3)) ";" J) + 1 + card I + 1
by SCMFSA8A:15
.= card Macro (a >0_goto (card J + 3)) + card J + 1 + card I + 1
by SCMFSA6A:21
.= 2 + card J + 1 + card I + 1 by COMPOS_1:56
.= card I + card J + 4;
end;
theorem Th7:
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
proof
let s be State of SCM+FSA;
let I be really-closed MacroInstruction of SCM+FSA;
let J be MacroInstruction of SCM+FSA;
let a be read-write Int-Location;
set I1 = I ";" Stop SCM+FSA;
set s1 = Initialize s,
P1 = P +* I1;
set s3 = Initialize s,
P3 = P +* if=0(a,I,J);
set s4 = Comput(P+*if=0(a,I,J),s3,1);
set i = a =0_goto (card J + 3);
A1: not a in dom Start-At(0,SCM+FSA) by SCMFSA_2:102;
A2: 0 in dom if=0(a,I,J) by AFINSQ_1:65;
A3: P3.0 = if=0(a,I,J).0 by A2,FUNCT_4:13
.= i by Lm2;
IC SCM+FSA in dom Start-At(0,SCM+FSA) by MEMSTR_0:15;
then
A4: IC s3 = IC Start-At(0,SCM+FSA) by FUNCT_4:13
.= 0 by FUNCOP_1:72;
A5: if=0(a,I,J) c= P3 by FUNCT_4:25;
A6: if=0(a,I,J) = i ";" J ";" Goto (card I + 1) ";" I1 by SCMFSA6A:25;
card (i ";" J ";" Goto (card I + 1))
= card (Macro i ";" J) + card Goto (card I + 1) by SCMFSA6A:21
.= card (Macro i ";" J) + 1 by SCMFSA8A:15
.= card Macro i + card J + 1 by SCMFSA6A:21
.= card J + 2 + 1 by COMPOS_1:56
.= card J + (2 + 1);
then
A7: Reloc(I1,card J + 3) c= if=0(a,I,J) by A6,SCMFSA6A:38;
A8: Reloc(I1,card J+3) c= P3 by A7,A5,XBOOLE_1:1;
A9: Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3)
.= Exec(i,s3) by A4,A3,PBOOLE:143;
A10: for f being FinSeq-Location holds s1.f = s4.f by A9,SCMFSA_2:70;
for a being Int-Location holds s1.a = s4.a by A9,SCMFSA_2:70;
then
A11: DataPart s1 = DataPart s4 by A10,SCMFSA_M:2;
assume s.a = 0;
then s3.a = 0 by A1,FUNCT_4:11;
then
A12: IC Comput(P3,s3,1) = (card J + 3) by A9,SCMFSA_2:70;
assume
A13: I is_halting_on s,P;
I1 is_halting_on s,P by A13,SCMFSA8A:30;
then
A14: P1 halts_on s1 by SCMFSA7B:def 7;
A15: I1 c= P1 by FUNCT_4:25;
CurInstr(P3,
Comput(P3,s3,LifeSpan(P1,s1)+1))
= CurInstr(P3,
Comput(P3,s4,LifeSpan(P1,s1))) by EXTPRO_1:4
.= IncAddr(CurInstr(P1,
Comput(P1,s1,LifeSpan(P1,s1))),card J + 3) by A12,A11,Th2,A8,A15
.= IncAddr(halt SCM+FSA,(card J + 3)) by A14,EXTPRO_1:def 15
.= halt SCM+FSA by COMPOS_0:4;
then P3 halts_on s3 by EXTPRO_1:29;
hence thesis by SCMFSA7B:def 7;
end;
theorem Th8:
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)
proof
let s be State of SCM+FSA;
let I be really-closed MacroInstruction of SCM+FSA;
let J be MacroInstruction of SCM+FSA;
let a be read-write Int-Location;
set I1 = I ";" Stop SCM+FSA;
set s1 = Initialized s, P1 = P +* I1, P3 = P +* if=0(a,I,J);
A1: I1 c= P1 by FUNCT_4:25;
set s4 = Comput(P3,s1,1);
set i = a =0_goto (card J + 3);
A2: if=0(a,I,J) = i ";" J ";" Goto (card I + 1) ";" I1 by SCMFSA6A:25;
A3: 0 in dom if=0(a,I,J) by AFINSQ_1:65;
A4: P3. 0 = if=0(a,I,J). 0 by A3,FUNCT_4:13
.= i by Lm2;
A5: dom Initialize ((intloc 0) .--> 1) = {intloc 0,IC SCM+FSA} by SCMFSA_M:11;
a <> intloc 0 & a <> IC SCM+FSA by SCMFSA_2:56;
then
A6: not a in dom Initialize((intloc 0).-->1) by A5,TARSKI:def 2;
IC SCM+FSA in dom Initialize((intloc 0).-->1) by MEMSTR_0:48;
then
A7: IC s1 = IC Initialize((intloc 0).-->1) by FUNCT_4:13
.= 0 by MEMSTR_0:def 11;
A8: Comput(P3, s1,0 + 1) = Following(P3,Comput(P3,s1,0)) by EXTPRO_1:3
.= Following(P3,s1)
.= Exec(i,s1) by A7,A4,PBOOLE:143;
A9: if=0(a,I,J) c= P3 by FUNCT_4:25;
assume s.a = 0;
then s1.a = 0 by A6,FUNCT_4:11;
then
A10: IC Comput(P3,s1,1) = (card J + 3) by A8,SCMFSA_2:70;
A11: for f being FinSeq-Location holds s1.f = s4.f by A8,SCMFSA_2:70;
for a being Int-Location holds s1.a = s4.a by A8,SCMFSA_2:70;
then
A12: DataPart s1 = DataPart s4 by A11,SCMFSA_M:2;
card (i ";" J ";" Goto (card I + 1))
= card (Macro i ";" J) + card Goto (card I + 1) by SCMFSA6A:21
.= card (Macro i ";" J) + 1 by SCMFSA8A:15
.= card Macro i + card J + 1 by SCMFSA6A:21
.= card J + 2 + 1 by COMPOS_1:56
.= card J + (2 + 1);
then
A13: Reloc(I1,card J + 3) c= if=0(a,I,J) by A2,SCMFSA6A:38;
A14: Reloc(I1,card J + 3) c= P3 by A13,A9,XBOOLE_1:1;
assume
A15: I is_halting_on Initialized s,P;
then
A16: P1 halts_on s1 by SCMFSA8A:34;
A17: CurInstr(P3,Comput(P3,s1,LifeSpan(P1,s1)+1))
= CurInstr(P3,Comput(P3,s4,LifeSpan(P1,s1))) by EXTPRO_1:4
.= IncAddr(CurInstr(P1,Comput(P1,s1,LifeSpan(P1,s1))),(card J + 3))
by A10,A12,Th2,A14,A1
.= IncAddr(halt SCM+FSA,(card J + 3)) by A16,EXTPRO_1:def 15
.= halt SCM+FSA by COMPOS_0:4;
then
A18: P3 halts_on s1 by EXTPRO_1:29;
now
let l be Nat;
assume
A19: l < LifeSpan(P1,s1) + 1;
per cases;
suppose
l = 0;
hence CurInstr(P3,Comput(P3,s1,l)) <>
halt SCM+FSA by A7,A4,PBOOLE:143;
end;
suppose
l <> 0;
then consider n being Nat such that
A20: l = n + 1 by NAT_1:6;
assume
A21: CurInstr(P3,Comput(P3,s1,l)) = halt SCM+FSA;
reconsider n as Element of NAT by ORDINAL1:def 12;
A22: InsCode halt SCM+FSA = 0 by COMPOS_1:70;
InsCode CurInstr(P1,Comput(P1,s1,n))
= InsCode IncAddr(CurInstr(P1,Comput(P1,s1,n)),(card J + 3))
by COMPOS_0:def 9
.= InsCode CurInstr(P3,Comput(P3,s4,n))
by A10,A12,Th2,A14,A1
.= 0 by A20,A21,A22,EXTPRO_1:4;
then
A23: CurInstr(P1,Comput(P1,s1,n))
= halt SCM+FSA by SCMFSA_2:95;
n < LifeSpan(P1,s1) by A19,A20,XREAL_1:6;
hence contradiction by A16,A23,EXTPRO_1:def 15;
end;
end;
then for l be Nat st CurInstr(P3,
Comput(P3,s1,l)) = halt SCM+FSA
holds LifeSpan(P1,s1) + 1 <= l;
then
A24: LifeSpan(P3,s1) = LifeSpan(P1,s1) + 1 by A17,A18,EXTPRO_1:def 15;
A25: DataPart Result(P1,s1) = DataPart Comput(P1, s1
,LifeSpan(P1,s1)) by A15,EXTPRO_1:23,SCMFSA8A:34
.= DataPart Comput(P3, s4,LifeSpan(P1,s1)) by A10,A12,Th2,A1,A14
.= DataPart Comput(P3, s1,LifeSpan(P1,s1) + 1)
by EXTPRO_1:4
.= DataPart Result(P3,s1) by A18,A24,EXTPRO_1:23;
A26: now
let x be object;
A27: IExec(I1,P,s) = Result(P1,s1) by SCMFSA6B:def 1;
A29: IExec(if=0(a,I,J),P,s) = (Result(P3,s1)) by SCMFSA6B:def 1;
assume
A30: x in dom IExec(if=0(a,I,J),P,s);
per cases by A30,SCMFSA_M:1;
suppose
A31: x is Int-Location;
then x <> IC SCM+FSA by SCMFSA_2:56;
then
A32: not x in dom Start-At((card I+card J+3),SCM+FSA)
by TARSKI:def 1;
thus IExec(if=0(a,I,J),P,s).x = (Result(P3,s1)).x
by A29
.= (Result(P1,s1)).x by A25,A31,SCMFSA_M:2
.= IExec(I1,P,s).x by A27
.= (IExec(I1,P,s) +* Start-At((card I+card J+3),SCM+FSA)).x by A32,
FUNCT_4:11;
end;
suppose
A33: x is FinSeq-Location;
then x <> IC SCM+FSA by SCMFSA_2:57;
then
A34: not x in dom Start-At((card I+card J+3),SCM+FSA)
by TARSKI:def 1;
thus IExec(if=0(a,I,J),P,s).x
= (Result(P3,s1)).x by A29
.= (Result(P1,s1)).x by A25,A33,SCMFSA_M:2
.= IExec(I1,P,s).x by A27
.= (IExec(I1,P,s) +* Start-At((card I+card J+3),SCM+FSA)).x by A34,
FUNCT_4:11;
end;
suppose
A35: x = IC SCM+FSA;
then
A36: x in dom Start-At((card I+card J+3),SCM+FSA)by TARSKI:def 1;
A37: IC Result(P1,s1) = IExec(I1,P,s).IC SCM+FSA by A27
.= IC (IExec(I,P,s) +* Start-At( card I,SCM+FSA))
by A15,SCMFSA8A:36
.= card I by FUNCT_4:113;
thus IExec(if=0(a,I,J),P,s).x = (Result(P3,s1)).x by A29
.= Comput(P3, s1,LifeSpan(P1,s1) + 1).x by A18,A24,EXTPRO_1:23
.= IC Comput(P3, s4,LifeSpan(P1,s1)) by A35,EXTPRO_1:4
.= IC Comput(P1, s1,LifeSpan(P1,s1)) + (card
J + 3) by A10,A12,Th2,A14,A1
.= IC Result(P1,s1) + (card J + 3)
by A15,EXTPRO_1:23,SCMFSA8A:34
.= (Start-At((card I+(card J+3)),SCM+FSA)).IC SCM+FSA by A37,
FUNCOP_1:72
.= (IExec(I1,P,s) +* Start-At((card I+card J+3),SCM+FSA)).x
by A35,A36,FUNCT_4:13;
end;
end;
dom IExec(if=0(a,I,J),P,s) = the carrier of SCM+FSA by PARTFUN1:def 2
.= dom (IExec(I1,P,s) +* Start-At((card I+card J+3),SCM+FSA))
by PARTFUN1:def 2;
hence IExec(if=0(a,I,J),P,s) = IExec(I1,P,s) +* Start-At( (card I + card J
+ 3),SCM+FSA) by A26,FUNCT_1:2
.= IExec(I,P,s) +* Start-At( card I,SCM+FSA) +*
Start-At( (card I +
card J + 3),SCM+FSA) by A15,SCMFSA8A:36
.= IExec(I,P,s) +* Start-At((card I+card J+3),SCM+FSA)by FUNCT_4:114;
end;
Lm3:
for I,J being really-closed MacroInstruction of SCM+FSA
holds J ";" Goto (card I + 1) ";" I ";" Stop SCM+FSA
is really-closed
proof let I,J be really-closed MacroInstruction of SCM+FSA;
A1: J ";" Goto (card I + 1) ";" I ";" Stop SCM+FSA
= J ";" Goto (card I + 1) ";" (I ";" Stop SCM+FSA) by SCMFSA6A:25
.= J ";" (Goto (card I + 1) ";" (I ";" Stop SCM+FSA)) by SCMFSA6A:25
.= J ";" (Goto (card I + 1) ";" I ";" Stop SCM+FSA) by SCMFSA6A:25;
Goto (card I + 1) ";" I ";" Stop SCM+FSA is really-closed
by SCMFSA_X:28;
hence thesis by A1;
end;
registration
let I,J be really-closed MacroInstruction of SCM+FSA,
a be Int-Location;
cluster if=0(a,I,J) -> really-closed;
coherence
proof
A1: if=0(a,I,J)
= a =0_goto (card J+3) ";" J ";" Goto(card I + 1) ";" I ";" Stop SCM+FSA
.= a =0_goto (card J+3) ";" J ";" Goto(card I + 1) ";" (I ";" Stop SCM+FSA)
by SCMFSA6A:25
.= a =0_goto (card J+3) ";" J ";"
(Goto(card I + 1) ";" (I ";" Stop SCM+FSA))
by SCMFSA6A:25
.= a =0_goto (card J+3) ";" (J ";"
(Goto(card I + 1) ";" (I ";" Stop SCM+FSA)))
by SCMFSA6A:25
.= a =0_goto (card J+3) ";" (J ";"
Goto(card I + 1) ";" (I ";" Stop SCM+FSA))
by SCMFSA6A:25
.= a =0_goto (card J+3) ";" (J ";" Goto(card I + 1) ";" I ";" Stop SCM+FSA)
by SCMFSA6A:25;
A2: card(J ";" Goto(card I + 1) ";" I ";" Stop SCM+FSA)
= card(J ";" Goto(card I + 1) ";" I) + card Stop SCM+FSA by SCMFSA6A:21
.= card(J ";" Goto(card I + 1) ";" I) + 1 by COMPOS_1:4
.= card(J ";" Goto(card I + 1)) + card I + 1 by SCMFSA6A:21
.= card J + card Goto(card I + 1) + card I + 1 by SCMFSA6A:21
.= card J + 1 + card I + 1 by SCMFSA8A:15
.= card I + card J + 2;
0+1 <= card I by NAT_1:13;
then 1 + card J <= card I + card J by XREAL_1:7;
then
A3: 1 + card J + 2 <= card I + card J + 2 by XREAL_1:7;
J ";" Goto (card I + 1) ";" I ";" Stop SCM+FSA is really-closed by Lm3;
hence thesis by A3,SCMFSA_X:31,A1,A2;
end;
cluster if>0(a,I,J) -> really-closed;
coherence
proof
A4: if>0(a,I,J)
= a >0_goto (card J+3) ";" J ";" Goto(card I + 1) ";" I ";" Stop SCM+FSA
.= a >0_goto (card J+3) ";" J ";" Goto(card I + 1) ";" (I ";" Stop SCM+FSA)
by SCMFSA6A:25
.= a >0_goto (card J+3) ";" J ";"
(Goto(card I + 1) ";" (I ";" Stop SCM+FSA))
by SCMFSA6A:25
.= a >0_goto (card J+3) ";" (J ";"
(Goto(card I + 1) ";" (I ";" Stop SCM+FSA)))
by SCMFSA6A:25
.= a >0_goto (card J+3) ";" (J ";"
Goto(card I + 1) ";" (I ";" Stop SCM+FSA))
by SCMFSA6A:25
.= a >0_goto (card J+3) ";" (J ";" Goto(card I + 1) ";" I ";" Stop SCM+FSA)
by SCMFSA6A:25;
A5: card(J ";" Goto(card I + 1) ";" I ";" Stop SCM+FSA)
= card(J ";" Goto(card I + 1) ";" I) + card Stop SCM+FSA by SCMFSA6A:21
.= card(J ";" Goto(card I + 1) ";" I) + 1 by COMPOS_1:4
.= card(J ";" Goto(card I + 1)) + card I + 1 by SCMFSA6A:21
.= card J + card Goto(card I + 1) + card I + 1 by SCMFSA6A:21
.= card J + 1 + card I + 1 by SCMFSA8A:15
.= card I + card J + 2;
0+1 <= card I by NAT_1:13;
then 1 + card J <= card I + card J by XREAL_1:7;
then
A6: 1 + card J + 2 <= card I + card J + 2 by XREAL_1:7;
J ";" Goto(card I + 1) ";" I ";" Stop SCM+FSA is really-closed by Lm3;
hence thesis by A6,SCMFSA_X:32,A4,A5;
end;
end;
theorem Th9:
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
proof
let s be State of SCM+FSA;
let I,J be really-closed MacroInstruction of SCM+FSA;
let a be read-write Int-Location;
set I1 = I ";" Stop SCM+FSA;
reconsider JI2 = J ";" Goto (card I + 1) ";" I ";" Stop SCM+FSA
as really-closed Program of SCM+FSA by Lm3;
set s2 = Initialize s,
P2 = P +* JI2;
A1: JI2 c= P2 by FUNCT_4:25;
set s3 = Initialize s,
P3 = P +* if=0(a,I,J);
set s4 = Comput(P3,s3,1);
set s5 = Comput(P3,s3,2);
set i = a =0_goto (card J + 3);
IC SCM+FSA in dom Start-At(0,SCM+FSA) by MEMSTR_0:15;
then
A2: IC s3 = IC Start-At(0,SCM+FSA) by FUNCT_4:13
.= 0 by FUNCOP_1:72;
A3: if=0(a,I,J) c= P3 by FUNCT_4:25;
if=0(a,I,J) = i ";" J ";" Goto (card I + 1) ";" I1 by SCMFSA6A:25
.= i ";" J ";" (Goto (card I + 1) ";" I1) by SCMFSA6A:25
.= i ";" (J ";" (Goto (card I + 1) ";" I1)) by SCMFSA6A:29
.= i ";" (J ";" Goto (card I + 1) ";" I1) by SCMFSA6A:25
.= Macro i ";" JI2 by SCMFSA6A:25;
then Reloc(JI2,card Macro i) c= if=0(a,I,J) by SCMFSA6A:38;
then
A4: Reloc(JI2,2) c= if=0(a,I,J) by COMPOS_1:56;
A5: Reloc(JI2,2) c= P3 by A4,A3,XBOOLE_1:1;
A6: not a in dom Start-At(0,SCM+FSA) by SCMFSA_2:102;
A7: 0 in dom if=0(a,I,J) by AFINSQ_1:65;
A8: if=0(a,I,J) c= P3 by FUNCT_4:25;
A9: P3. 0 = if=0(a,I,J). 0 by A7,FUNCT_4:13
.= i by Lm2;
A10: 1 in dom if=0(a,I,J) by Lm1;
A11: Comput(P3, s3,0 + 1) = Following(P3,
Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3)
.= Exec(i,s3) by A2,A9,PBOOLE:143;
assume s.a <> 0;
then s3.a <> 0 by A6,FUNCT_4:11;
then
A12: IC Comput(P3,s3,1) = 0+1 by A2,A11,SCMFSA_2:70;
A13: P3. 1 = if=0(a,I,J). 1 by A10,A8,GRFUNC_1:2
.= goto 2 by Lm2;
A14: Comput(P3, s3,1 + 1) = Following(P3,s4) by EXTPRO_1:3
.= Exec(goto 2,s4) by A12,A13,PBOOLE:143;
A15: now
let f be FinSeq-Location;
thus s2.f = Comput(P3,s3,1).f by A11,SCMFSA_2:70
.= s5.f by A14,SCMFSA_2:69;
end;
now
let a be Int-Location;
thus s2.a = Comput(P3,s3,1).a by A11,SCMFSA_2:70
.= s5.a by A14,SCMFSA_2:69;
end;
then
A16: DataPart s2 = DataPart s5 by A15,SCMFSA_M:2;
assume
A17: J is_halting_on s,P;
A18: P2 halts_on s2 by A17,SCMFSA8A:38;
A19: IC s5 = 2 by A14,SCMFSA_2:69;
CurInstr(P3,
Comput(P3,s3,LifeSpan(P2,s2)+2))
= CurInstr(P3,Comput(P3,s5,LifeSpan(P2,s2))) by EXTPRO_1:4
.= IncAddr(CurInstr(P2,
Comput(P2,s2,LifeSpan(P2,s2))),2) by A19,A16,Th2,A5,A1
.= IncAddr(halt SCM+FSA,2) by A18,EXTPRO_1:def 15
.= halt SCM+FSA by COMPOS_0:4;
then P3 halts_on s3 by EXTPRO_1:29;
hence thesis by SCMFSA7B:def 7;
end;
theorem Th10:
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)
proof
let I,J be really-closed MacroInstruction of SCM+FSA;
let a be read-write Int-Location;
let s be State of SCM+FSA;
set I1 = I ";" Stop SCM+FSA;
reconsider JI2 = J ";" Goto (card I + 1) ";" I ";" Stop SCM+FSA
as really-closed Program of SCM+FSA by Lm3;
set s2 = Initialized s, P2 = P +* JI2;
A1: JI2 c= P2 by FUNCT_4:25;
set P3 = P +* if=0(a,I,J);
set s4 = Comput(P3, s2,1);
set s5 = Comput(P3, s2,2);
set i = a =0_goto (card J + 3);
0 in dom if=0(a,I,J) by AFINSQ_1:65;
then
A2: P3. 0 = if=0(a,I,J). 0 by FUNCT_4:13
.= i by Lm2;
A3: 1 in dom if=0(a,I,J) by Lm1;
A4: P3. 1 = if=0(a,I,J). 1 by A3,FUNCT_4:13
.= goto 2 by Lm2;
A5: dom Initialize ((intloc 0) .--> 1) = {intloc 0,IC SCM+FSA} by SCMFSA_M:11;
a <> intloc 0 & a <> IC SCM+FSA by SCMFSA_2:56;
then
A6: not a in dom Initialize((intloc 0).-->1) by A5,TARSKI:def 2;
IC SCM+FSA in dom Initialize((intloc 0).-->1) by MEMSTR_0:48;
then
A7: IC s2 = IC Initialize((intloc 0).-->1) by FUNCT_4:13
.= 0 by MEMSTR_0:def 11;
if=0(a,I,J) = i ";" J ";" Goto (card I + 1) ";" I1 by SCMFSA6A:25
.= i ";" J ";" (Goto (card I + 1) ";" I1) by SCMFSA6A:25
.= i ";" (J ";" (Goto (card I + 1) ";" I1)) by SCMFSA6A:29
.= i ";" (J ";" Goto (card I + 1) ";" I1) by SCMFSA6A:25
.= Macro i ";" JI2 by SCMFSA6A:25;
then Reloc(JI2,card Macro i) c= if=0(a,I,J) by SCMFSA6A:38;
then
A8: Reloc(JI2,2) c= if=0(a,I,J) by COMPOS_1:56;
if=0(a,I,J) c= P3 by FUNCT_4:25;
then
A9: Reloc(JI2,2) c= P3 by A8,XBOOLE_1:1;
A10: Comput(P3, s2,0 + 1) = Following(P3,
Comput(P3,s2,0)) by EXTPRO_1:3
.= Following(P3,s2)
.= Exec(i,s2) by A7,A2,PBOOLE:143;
assume s.a <> 0;
then s2.a <> 0 by A6,FUNCT_4:11;
then
A11: IC Comput(P3,s2,1) = 0+1 by A7,A10,SCMFSA_2:70;
A12: Comput(P3, s2,1 + 1) = Following(P3,s4) by EXTPRO_1:3
.= Exec(goto 2,s4) by A11,A4,PBOOLE:143;
then
A13: IC s5 = 2 by SCMFSA_2:69;
A14: now
let f be FinSeq-Location;
thus s2.f = Comput(P3,s2,1).f by A10,SCMFSA_2:70
.= s5.f by A12,SCMFSA_2:69;
end;
now
let a be Int-Location;
thus s2.a = Comput(P3,s2,1).a by A10,SCMFSA_2:70
.= s5.a by A12,SCMFSA_2:69;
end;
then
A15: DataPart s2 = DataPart s5 by A14,SCMFSA_M:2;
assume
A16: J is_halting_on Initialized s,P;
then
A17: P2 halts_on s2 by SCMFSA8A:39;
A18: CurInstr(P3,
Comput(P3,s2,LifeSpan(P2,s2)+2))
= CurInstr(P3,
Comput(P3,s5,LifeSpan(P2,s2))) by EXTPRO_1:4
.= IncAddr(CurInstr(P2,
Comput(P2,s2,LifeSpan(P2,s2))),2) by A9,A13,A15,Th2,A1
.= IncAddr(halt SCM+FSA,2) by A17,EXTPRO_1:def 15
.= halt SCM+FSA by COMPOS_0:4;
then
A19: P3 halts_on s2 by EXTPRO_1:29;
now
let l be Nat;
assume
A20: l < LifeSpan(P2,s2) + 2;
per cases;
suppose
l = 0;
hence CurInstr(P3,Comput(P3,s2,l)) <>
halt SCM+FSA by A7,A2,PBOOLE:143;
end;
suppose
l = 1;
hence CurInstr(P3,Comput(P3,s2,l)) <>
halt SCM+FSA by A11,A4,PBOOLE:143;
end;
suppose
A21: l <> 0 & l <> 1;
assume
A22: CurInstr(P3,Comput(P3,s2,l)) = halt SCM+FSA;
consider n being Nat such that
A23: l = n + 1 by A21,NAT_1:6;
n <> 0 by A21,A23;
then consider l2 being Nat such that
A24: n = l2 + 1 by NAT_1:6;
reconsider l2 as Element of NAT by ORDINAL1:def 12;
A25: InsCode halt SCM+FSA = 0 by COMPOS_1:70;
A26: Comput(P3,s2,l2+(1+1))
= Comput(P3,Comput(P3,s2,1+1),l2) by EXTPRO_1:4;
InsCode CurInstr(P2,Comput(
P2,s2,l2)) =
InsCode IncAddr(CurInstr(P2,
Comput(P2,s2,l2)),2) by COMPOS_0:def 9
.= 0 by A23,A24,A22,A26,A13,A15,Th2,A9,A1,A25;
then
A27: CurInstr(P2,Comput(P2
,s2,l2))
= halt SCM+FSA by SCMFSA_2:95;
n + 1 < LifeSpan(P2,s2) + 1 + 1 by A20,A23;
then n < LifeSpan(P2,s2) + 1 by XREAL_1:6;
then l2 < LifeSpan(P2,s2) by A24,XREAL_1:6;
hence contradiction by A17,A27,EXTPRO_1:def 15;
end;
end;
then for l be Nat st CurInstr(P3,
Comput(P3,s2,l)) = halt SCM+FSA
holds LifeSpan(P2,s2) + 2 <= l;
then
A28: LifeSpan(P3,s2) = LifeSpan(P2,s2) + 2 by A18,A19,EXTPRO_1:def 15;
A29: DataPart Result(P2,s2) = DataPart Comput(P2, s2
,LifeSpan(P2,s2)) by A16,EXTPRO_1:23,SCMFSA8A:39
.= DataPart Comput(P3, s5,LifeSpan(P2,s2)) by A13,A15,Th2,A9,A1
.= DataPart Comput(P3, s2,LifeSpan(P2,s2) + 2)
by EXTPRO_1:4
.= DataPart Result(P3,s2) by A19,A28,EXTPRO_1:23;
A30: now
let x be object;
A32: IExec(if=0(a,I,J),P,s) = (Result(P3,s2)) by SCMFSA6B:def 1;
A33: IExec(JI2,P,s) = Result(P2,s2) by SCMFSA6B:def 1;
assume
A34: x in dom IExec(if=0(a,I,J),P,s);
per cases by A34,SCMFSA_M:1;
suppose
A35: x is Int-Location;
then x <> IC SCM+FSA by SCMFSA_2:56;
then
A36: not x in dom Start-At((card I+card J+3),SCM+FSA)
by TARSKI:def 1;
thus IExec(if=0(a,I,J),P,s).x = (Result(P3,s2)).x
by A32
.= (Result(P2,s2)).x by A29,A35,SCMFSA_M:2
.= IExec(JI2,P,s).x by A33
.= (IExec(JI2,P,s) +* Start-At((card I+card J+3),SCM+FSA)).x
by A36,FUNCT_4:11;
end;
suppose
A37: x is FinSeq-Location;
then x <> IC SCM+FSA by SCMFSA_2:57;
then
A38: not x in dom Start-At((card I+card J+3),SCM+FSA)
by TARSKI:def 1;
thus IExec(if=0(a,I,J),P,s).x = (Result(P3,s2)).x by A32
.= (Result(P2,s2)).x by A29,A37,SCMFSA_M:2
.= IExec(JI2,P,s).x by A33
.= (IExec(JI2,P,s) +* Start-At((card I+card J+3),SCM+FSA)).x
by A38,FUNCT_4:11;
end;
suppose
A39: x = IC SCM+FSA;
then
A40: x in dom Start-At((card I+card J+3),SCM+FSA)by TARSKI:def 1;
A41: IC Result(P2,s2) = IC IExec(JI2,P,s) by A33
.= (card I + card J + 1) by A16,SCMFSA8A:40;
thus IExec(if=0(a,I,J),P,s).x = (Result(P3,s2)).x by A32
.= Comput(P3, s2,LifeSpan(P2,s2) + 2).x by A19,A28,EXTPRO_1:23
.= IC Comput(P3, s5,LifeSpan(P2,s2)) by A39,EXTPRO_1:4
.= IC Comput(P2, s2,LifeSpan(P2,s2)) + 2 by A13,A15,Th2,A9,A1
.= IC Result(P2,s2) + 2 by A16,EXTPRO_1:23,SCMFSA8A:39
.= (Start-At ( (card I + card J + 1) + 2,SCM+FSA)).IC SCM+FSA
by A41,FUNCOP_1:72
.= (IExec(JI2,P,s) +* Start-At((card I+card J+3),SCM+FSA)).x
by A39,A40,FUNCT_4:13;
end;
end;
dom IExec(if=0(a,I,J),P,s) = the carrier of SCM+FSA by PARTFUN1:def 2
.= dom (IExec(JI2,P,s) +* Start-At((card I+card J+3),SCM+FSA))
by PARTFUN1:def 2;
hence
IExec(if=0(a,I,J),P,s) = IExec(JI2,P,s) +* Start-At( (card I + card J
+ 3),SCM+FSA) by A30,FUNCT_1:2
.= IExec(J,P,s) +* Start-At( (card I + card J + 1),SCM+FSA)
+* Start-At(
(card I + card J + 3),SCM+FSA) by A16,SCMFSA8A:41
.= IExec(J,P,s) +* Start-At((card I+card J+3),SCM+FSA)by FUNCT_4:114;
end;
theorem Th11:
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))
proof
let s be State of SCM+FSA;
let I,J be parahalting really-closed MacroInstruction of SCM+FSA;
let a be read-write Int-Location;
A1: I is_halting_on Initialized s,P by SCMFSA7B:19;
for s being 0-started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
st if=0(a,I,J) c= P
holds P halts_on s
proof
let s be 0-started State of SCM+FSA;
Start-At(0,SCM+FSA) c= s by MEMSTR_0:29;
then
A2: s = Initialize s by FUNCT_4:98;
let Q be Instruction-Sequence of SCM+FSA
such that
A3: if=0(a,I,J) c= Q;
A4: if=0(a,I,J) c= Q by A3;
A5: I is_halting_on s,Q by SCMFSA7B:19;
A6: J is_halting_on s,Q by SCMFSA7B:19;
A7: Q +* if=0(a,I,J) = Q by A4,FUNCT_4:98;
per cases;
suppose
s.a = 0;
then if=0(a,I,J) is_halting_on s,Q by A5,Th7;
hence Q halts_on s by A2,A7,SCMFSA7B:def 7;
end;
suppose
s.a <> 0;
then if=0(a,I,J) is_halting_on s,Q by A6,Th9;
hence Q halts_on s by A2,A7,SCMFSA7B:def 7;
end;
end;
hence if=0(a,I,J) is parahalting by AMISTD_1:def 11;
thus 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)
by A1,Th8;
J is_halting_on Initialized s,P by SCMFSA7B:19;
hence thesis by Th10;
end;
theorem Th12:
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))
proof
let s be State of SCM+FSA;
let I,J be parahalting really-closed MacroInstruction of SCM+FSA;
let a be read-write Int-Location;
hereby
per cases;
suppose
s.a = 0;
then
IExec(if=0(a,I,J),P,s) = IExec(I,P,s) +* Start-At( (card I + card
J + 3),SCM+FSA) by Th11;
hence IC IExec(if=0(a,I,J),P,s) = (card I + card J + 3) by FUNCT_4:113;
end;
suppose
s.a <> 0;
then
IExec(if=0(a,I,J),P,s) = IExec(J,P,s) +* Start-At( (card I + card
J + 3),SCM+FSA) by Th11;
hence IC IExec(if=0(a,I,J),P,s) = (card I + card J + 3) by FUNCT_4:113;
end;
end;
hereby
assume s.a = 0;
then
A1: IExec(if=0(a,I,J),P,s) = IExec(I,P,s) +* Start-At( (card I + card J
+ 3),SCM+FSA) by Th11;
hereby
let d be Int-Location;
not d in dom Start-At((card I+card J+3),SCM+FSA)by SCMFSA_2:102;
hence IExec(if=0(a,I,J),P,s).d = IExec(I,P,s).d by A1,FUNCT_4:11;
end;
let f be FinSeq-Location;
not f in dom Start-At((card I+card J+3),SCM+FSA)by SCMFSA_2:103;
hence IExec(if=0(a,I,J),P,s).f = IExec(I,P,s).f by A1,FUNCT_4:11;
end;
assume s.a <> 0;
then
A2: IExec(if=0(a,I,J),P,s) = IExec(J,P,s) +* Start-At( (card I + card J +
3),SCM+FSA) by Th11;
hereby
let d be Int-Location;
not d in dom Start-At((card I+card J+3),SCM+FSA)by SCMFSA_2:102;
hence IExec(if=0(a,I,J),P,s).d = IExec(J,P,s).d by A2,FUNCT_4:11;
end;
let f be FinSeq-Location;
not f in dom Start-At((card I+card J+3),SCM+FSA)by SCMFSA_2:103;
hence thesis by A2,FUNCT_4:11;
end;
theorem Th13:
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
proof
let s be State of SCM+FSA;
let I,J be really-closed MacroInstruction of SCM+FSA;
let a be read-write Int-Location;
set I1 = I ";" Stop SCM+FSA;
set s1 = Initialize s,
P1 = P +* I1;
set s3 = Initialize s,
P3 = P +* if>0(a,I,J);
set s4 = Comput(P3, s3,1);
set i = a >0_goto (card J + 3);
A1: I1 c= P1 by FUNCT_4:25;
A2: not a in dom Start-At(0,SCM+FSA) by SCMFSA_2:102;
A3: 0 in dom if>0(a,I,J) by AFINSQ_1:65;
A4: P3. 0 = if>0(a,I,J). 0 by A3,FUNCT_4:13
.= i by Lm2;
IC SCM+FSA in dom Start-At(0,SCM+FSA) by MEMSTR_0:15;
then
A5: IC s3 = IC Start-At(0,SCM+FSA) by FUNCT_4:13
.= 0 by FUNCOP_1:72;
A6: if>0(a,I,J) c= P3 by FUNCT_4:25;
A7: if>0(a,I,J) = i ";" J ";" Goto (card I + 1) ";" I1 by SCMFSA6A:25;
card (i ";" J ";" Goto (card I + 1))
= card (Macro i ";" J) + card Goto (card I + 1) by SCMFSA6A:21
.= card (Macro i ";" J) + 1 by SCMFSA8A:15
.= card Macro i + card J + 1 by SCMFSA6A:21
.= card J + 2 + 1 by COMPOS_1:56
.= card J + (2 + 1);
then
A8: Reloc(I1,card J + 3) c= if>0(a,I,J) by A7,SCMFSA6A:38;
A9: Reloc(I1,card J + 3) c= P3 by A8,A6,XBOOLE_1:1;
A10: Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3)
.= Exec(i,s3) by A5,A4,PBOOLE:143;
A11: for f being FinSeq-Location holds s1.f = s4.f by A10,SCMFSA_2:71;
for a being Int-Location holds s1.a = s4.a by A10,SCMFSA_2:71;
then
A12: DataPart s1 = DataPart s4 by A11,SCMFSA_M:2;
assume s.a > 0;
then s3.a > 0 by A2,FUNCT_4:11;
then
A13: IC Comput(P3,s3,1) = (card J + 3) by A10,SCMFSA_2:71;
assume
A14: I is_halting_on s,P;
I1 is_halting_on s,P by A14,SCMFSA8A:30;
then
A15: P1 halts_on s1 by SCMFSA7B:def 7;
CurInstr(P3,
Comput(P3,s3,LifeSpan(P1,s1)+1))
= CurInstr(P3,
Comput(P3,s4,LifeSpan(P1,s1))) by EXTPRO_1:4
.= IncAddr(CurInstr(P1,
Comput(P1,s1,LifeSpan(P1,s1))),(card J + 3)) by A13,A12,Th2,A9,A1
.= IncAddr(halt SCM+FSA,(card J + 3)) by A15,EXTPRO_1:def 15
.= halt SCM+FSA by COMPOS_0:4;
then P3 halts_on s3 by EXTPRO_1:29;
hence thesis by SCMFSA7B:def 7;
end;
theorem Th14:
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)
proof
let I,J be really-closed MacroInstruction of SCM+FSA;
let a be read-write Int-Location;
let s be State of SCM+FSA;
set I1 = I ";" Stop SCM+FSA;
set s1 = Initialized s, P1 = P +* I1;
set P3 = P +* if>0(a,I,J);
set s4 = Comput(P3, s1,1);
set i = a >0_goto (card J + 3);
A1: I1 c= P1 by FUNCT_4:25;
A2: if>0(a,I,J) = i ";" J ";" Goto (card I + 1) ";" I1 by SCMFSA6A:25;
A3: 0 in dom if>0(a,I,J) by AFINSQ_1:65;
A4: P3. 0 = if>0(a,I,J). 0 by A3,FUNCT_4:13
.= i by Lm2;
A5: dom Initialize ((intloc 0) .--> 1) = {intloc 0,IC SCM+FSA} by SCMFSA_M:11;
a <> intloc 0 & a <> IC SCM+FSA by SCMFSA_2:56;
then
A6: not a in dom Initialize((intloc 0).-->1) by A5,TARSKI:def 2;
IC SCM+FSA in dom Initialize((intloc 0).-->1) by MEMSTR_0:48;
then
A7: IC s1 = IC Initialize((intloc 0).-->1) by FUNCT_4:13
.= 0 by MEMSTR_0:def 11;
A8: Comput(P3, s1,0 + 1) = Following(P3,
Comput(P3,s1,0)) by EXTPRO_1:3
.= Following(P3,s1)
.= Exec(i,s1) by A7,A4,PBOOLE:143;
A9: if>0(a,I,J) c= P3 by FUNCT_4:25;
assume s.a > 0;
then s1.a > 0 by A6,FUNCT_4:11;
then
A10: IC Comput(P3,s1,1) = (card J + 3) by A8,SCMFSA_2:71;
A11: for f being FinSeq-Location holds s1.f = s4.f by A8,SCMFSA_2:71;
for a being Int-Location holds s1.a = s4.a by A8,SCMFSA_2:71;
then
A12: DataPart s1 = DataPart s4 by A11,SCMFSA_M:2;
card (i ";" J ";" Goto (card I + 1))
= card (Macro i ";" J) + card Goto (card I + 1) by SCMFSA6A:21
.= card (Macro i ";" J) + 1 by SCMFSA8A:15
.= card Macro i + card J + 1 by SCMFSA6A:21
.= card J + 2 + 1 by COMPOS_1:56
.= card J + (2 + 1);
then
A13: Reloc(I1,card J + 3) c= if>0(a,I,J) by A2,SCMFSA6A:38;
A14: Reloc(I1,card J + 3) c= P3 by A13,A9,XBOOLE_1:1;
assume
A15: I is_halting_on Initialized s,P;
then
A16: P1 halts_on s1 by SCMFSA8A:34;
A17: CurInstr(P3,
Comput(P3,s1,LifeSpan(P1,s1)+1))
= CurInstr(P3,
Comput(P3,s4,LifeSpan(P1,s1)))
by EXTPRO_1:4
.= IncAddr(CurInstr(P1,
Comput(P1,s1,LifeSpan(P1,s1))),(card J + 3)) by A10,A12,Th2,A14,A1
.= IncAddr(halt SCM+FSA,(card J + 3)) by A16,EXTPRO_1:def 15
.= halt SCM+FSA by COMPOS_0:4;
then
A18: P3 halts_on s1 by EXTPRO_1:29;
now
let l be Nat;
assume
A19: l < LifeSpan(P1,s1) + 1;
per cases;
suppose
l = 0;
hence CurInstr(P3,Comput(P3,s1,l)) <>
halt SCM+FSA by A7,A4,PBOOLE:143;
end;
suppose
l <> 0;
then consider n being Nat such that
A20: l = n + 1 by NAT_1:6;
assume
A21: CurInstr(P3,Comput(P3,s1,l)) = halt SCM+FSA;
reconsider n as Element of NAT by ORDINAL1:def 12;
A22: InsCode halt SCM+FSA = 0 by COMPOS_1:70;
InsCode CurInstr(P1,Comput(P1,s1,n))
= InsCode IncAddr(CurInstr(P1,
Comput(P1,s1,n)),(card J + 3))
by COMPOS_0:def 9
.= InsCode CurInstr(P3,Comput(P3,s4,n)) by A10,A12,Th2,A14,A1
.= 0 by A20,A21,A22,EXTPRO_1:4;
then
A23: CurInstr(P1,Comput(P1,s1,n))
= halt SCM+FSA by SCMFSA_2:95;
n < LifeSpan(P1,s1) by A19,A20,XREAL_1:6;
hence contradiction by A16,A23,EXTPRO_1:def 15;
end;
end;
then for l be Nat st CurInstr(P3,Comput(P3,s1,l)) = halt SCM+FSA
holds LifeSpan(P1,s1) + 1 <= l;
then
A24: LifeSpan(P3,s1) = LifeSpan(P1,s1) + 1 by A17,A18,EXTPRO_1:def 15;
A25: DataPart Result(P1,s1) = DataPart Comput(P1, s1
,LifeSpan(P1,s1)) by A15,EXTPRO_1:23,SCMFSA8A:34
.= DataPart Comput(P3, s4,LifeSpan(P1,s1)) by A10,A12,Th2,A14,A1
.= DataPart Comput(P3, s1,LifeSpan(P1,s1) + 1)
by EXTPRO_1:4
.= DataPart Result(P3,s1) by A18,A24,EXTPRO_1:23;
A26: now
let x be object;
A28: IExec(if>0(a,I,J),P,s) = (Result(P3,s1)) by SCMFSA6B:def 1;
A29: IExec(I1,P,s) = Result(P1,s1) by SCMFSA6B:def 1;
assume
A30: x in dom IExec(if>0(a,I,J),P,s);
per cases by A30,SCMFSA_M:1;
suppose
A31: x is Int-Location;
then x <> IC SCM+FSA by SCMFSA_2:56;
then
A32: not x in dom Start-At((card I+card J+3),SCM+FSA)
by TARSKI:def 1;
thus IExec(if>0(a,I,J),P,s).x = (Result(P3,s1)).x by A28
.= (Result(P1,s1)).x by A25,A31,SCMFSA_M:2
.= IExec(I1,P,s).x by A29
.= (IExec(I1,P,s) +* Start-At((card I+card J+3),SCM+FSA)).x by A32,
FUNCT_4:11;
end;
suppose
A33: x is FinSeq-Location;
then x <> IC SCM+FSA by SCMFSA_2:57;
then
A34: not x in dom Start-At((card I+card J+3),SCM+FSA)
by TARSKI:def 1;
thus IExec(if>0(a,I,J),P,s).x = (Result(P3,s1)).x by A28
.= (Result(P1,s1)).x by A25,A33,SCMFSA_M:2
.= IExec(I1,P,s).x by A29
.= (IExec(I1,P,s) +* Start-At((card I+card J+3),SCM+FSA)).x by A34,
FUNCT_4:11;
end;
suppose
A35: x = IC SCM+FSA;
then
A36: x in dom Start-At((card I+card J+3),SCM+FSA)by TARSKI:def 1;
A37: IC Result(P1,s1) = IExec(I1,P,s).IC SCM+FSA by A29
.= IC (IExec(I,P,s) +* Start-At( card I,SCM+FSA)) by A15,SCMFSA8A:36
.= card I by FUNCT_4:113;
thus IExec(if>0(a,I,J),P,s).x = (Result(P3,s1)).x by A28
.= Comput(P3, s1,LifeSpan(P1,s1) + 1).x by A18,A24,EXTPRO_1:23
.= IC Comput(P3, s4,LifeSpan(P1,s1)) by A35,EXTPRO_1:4
.= IC Comput(P1, s1,LifeSpan(P1,s1)) + (card
J + 3) by A10,A12,Th2,A1,A14
.= IC Result(P1,s1) + (card J + 3)
by A15,EXTPRO_1:23,SCMFSA8A:34
.= (Start-At((card I+(card J+3)),SCM+FSA)).IC SCM+FSA by A37,
FUNCOP_1:72
.= (IExec(I1,P,s) +* Start-At((card I+card J+3),SCM+FSA)).x
by A35,A36,FUNCT_4:13;
end;
end;
dom IExec(if>0(a,I,J),P,s) = the carrier of SCM+FSA by PARTFUN1:def 2
.= dom (IExec(I1,P,s) +* Start-At((card I+card J+3),SCM+FSA))
by PARTFUN1:def 2;
hence IExec(if>0(a,I,J),P,s) = IExec(I1,P,s) +* Start-At( (card I + card J
+ 3),SCM+FSA) by A26,FUNCT_1:2
.= IExec(I,P,s) +* Start-At( card I,SCM+FSA) +*
Start-At( (card I +
card J + 3),SCM+FSA) by A15,SCMFSA8A:36
.= IExec(I,P,s) +* Start-At((card I+card J+3),SCM+FSA)by FUNCT_4:114;
end;
theorem Th15:
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
proof
let s be State of SCM+FSA;
let I,J be really-closed MacroInstruction of SCM+FSA;
let a be read-write Int-Location;
set I1 = I ";" Stop SCM+FSA;
reconsider JI2 = J ";" Goto (card I + 1) ";" I ";" Stop SCM+FSA
as really-closed Program of SCM+FSA by Lm3;
set s2 = Initialize s,
P2 = P +* JI2;
A1: JI2 c= P2 by FUNCT_4:25;
set s3 = Initialize s,
P3 = P +* if>0(a,I,J);
set s4 = Comput(P3, s3,1);
set s5 = Comput(P3,s3,2);
set i = a >0_goto (card J + 3);
IC SCM+FSA in dom Start-At(0,SCM+FSA) by MEMSTR_0:15;
then
A2: IC s3 = IC Start-At(0,SCM+FSA) by FUNCT_4:13
.= 0 by FUNCOP_1:72;
A3: if>0(a,I,J) c= P3 by FUNCT_4:25;
if>0(a,I,J) = i ";" J ";" Goto (card I + 1) ";" I1 by SCMFSA6A:25
.= i ";" J ";" (Goto (card I + 1) ";" I1) by SCMFSA6A:25
.= i ";" (J ";" (Goto (card I + 1) ";" I1)) by SCMFSA6A:29
.= i ";" (J ";" Goto (card I + 1) ";" I1) by SCMFSA6A:25
.= Macro i ";" JI2 by SCMFSA6A:25;
then
A4: Reloc(JI2,card Macro i) c= if>0(a,I,J) by SCMFSA6A:38;
card Macro i = 2 by COMPOS_1:56;
then
A5: Reloc(JI2,2) c= P3 by A3,A4,XBOOLE_1:1;
A6: not a in dom Start-At(0,SCM+FSA) by SCMFSA_2:102;
A7: 0 in dom if>0(a,I,J) by AFINSQ_1:65;
A8: P3. 0 = if>0(a,I,J). 0 by A7,FUNCT_4:13
.= i by Lm2;
A9: 1 in dom if>0(a,I,J) by Lm1;
A10: Comput(P3, s3,0 + 1) = Following(P3,
Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3)
.= Exec(i,s3) by A2,A8,PBOOLE:143;
assume s.a <= 0;
then s3.a <= 0 by A6,FUNCT_4:11;
then
A11: IC Comput(P3,s3,1) = 0+1 by A2,A10,SCMFSA_2:71;
A12: P3.1 = if>0(a,I,J). 1 by A9,FUNCT_4:13
.= goto 2 by Lm2;
A13: Comput(P3, s3,1 + 1) = Following(P3,s4) by EXTPRO_1:3
.= Exec(goto 2,s4) by A11,A12,PBOOLE:143;
A14: now
let f be FinSeq-Location;
thus s2.f = Comput(P3,s3,1).f by A10,SCMFSA_2:71
.= s5.f by A13,SCMFSA_2:69;
end;
now
let a be Int-Location;
thus s2.a = Comput(P3,s3,1).a by A10,SCMFSA_2:71
.= s5.a by A13,SCMFSA_2:69;
end;
then
A15: DataPart s2 = DataPart s5 by A14,SCMFSA_M:2;
assume
A16: J is_halting_on s,P;
A17: P2 halts_on s2 by A16,SCMFSA8A:38;
A18: IC s5 = 2 by A13,SCMFSA_2:69;
CurInstr(P3,
Comput(P3,s3,LifeSpan(P2,s2)+2))
= CurInstr(P3,
Comput(P3,s5,LifeSpan(P2,s2))) by EXTPRO_1:4
.= IncAddr(CurInstr(P2,
Comput(P2,s2,LifeSpan(P2,s2))),2) by A5,A18,A15,Th2,A1
.= IncAddr(halt SCM+FSA,2) by A17,EXTPRO_1:def 15
.= halt SCM+FSA by COMPOS_0:4;
then P3 halts_on s3 by EXTPRO_1:29;
hence thesis by SCMFSA7B:def 7;
end;
theorem Th16:
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)
proof
let I,J be really-closed MacroInstruction of SCM+FSA;
let a be read-write Int-Location;
let s be State of SCM+FSA;
set I1 = I ";" Stop SCM+FSA;
reconsider JI2 = J ";" Goto (card I + 1) ";" I ";" Stop SCM+FSA
as really-closed Program of SCM+FSA by Lm3;
set s2 = Initialized s, P2 = P +* JI2;
A1: JI2 c= P2 by FUNCT_4:25;
set P3 = P +* if>0(a,I,J);
set s4 = Comput(P3, s2,1);
set s5 = Comput(P3,s2,2);
set i = a >0_goto (card J + 3);
0 in dom if>0(a,I,J) by AFINSQ_1:65;
then
A2: P3. 0 = if>0(a,I,J). 0 by FUNCT_4:13
.= i by Lm2;
A3: 1 in dom if>0(a,I,J) by Lm1;
A4: P3. 1 = if>0(a,I,J). 1 by A3,FUNCT_4:13
.= goto 2 by Lm2;
A5: dom Initialize ((intloc 0) .--> 1) = {intloc 0,IC SCM+FSA} by SCMFSA_M:11;
a <> intloc 0 & a <> IC SCM+FSA by SCMFSA_2:56;
then
A6: not a in dom Initialize((intloc 0).-->1) by A5,TARSKI:def 2;
IC SCM+FSA in dom Initialize((intloc 0).-->1) by MEMSTR_0:48;
then
A7: IC s2 = IC Initialize((intloc 0).-->1) by FUNCT_4:13
.= 0 by MEMSTR_0:def 11;
if>0(a,I,J) = i ";" J ";" Goto (card I + 1) ";" I1 by SCMFSA6A:25
.= i ";" J ";" (Goto (card I + 1) ";" I1) by SCMFSA6A:25
.= i ";" (J ";" (Goto (card I + 1) ";" I1)) by SCMFSA6A:29
.= i ";" (J ";" Goto (card I + 1) ";" I1) by SCMFSA6A:25
.= Macro i ";" JI2 by SCMFSA6A:25;
then Reloc(JI2,card Macro i) c= if>0(a,I,J) by SCMFSA6A:38;
then
A8: Reloc(JI2,2) c= if>0(a,I,J) by COMPOS_1:56;
if>0(a,I,J) c= P3 by FUNCT_4:25;
then
A9: Reloc(JI2,2) c= P3 by A8,XBOOLE_1:1;
A10: Comput(P3, s2,0 + 1) =
Following(P3,Comput(P3,s2,0))
by EXTPRO_1:3
.= Following(P3,s2)
.= Exec(i,s2) by A7,A2,PBOOLE:143;
assume s.a <= 0;
then s2.a <= 0 by A6,FUNCT_4:11;
then
A11: IC Comput(P3,s2,1) = 0+1 by A7,A10,SCMFSA_2:71;
A12: Comput(P3, s2,1 + 1) = Following(P3,s4) by EXTPRO_1:3
.= Exec(goto 2,s4) by A11,A4,PBOOLE:143;
then
A13: IC s5 = 2 by SCMFSA_2:69;
A14: now
let f be FinSeq-Location;
thus s2.f = Comput(P3,s2,1).f by A10,SCMFSA_2:71
.= s5.f by A12,SCMFSA_2:69;
end;
now
let a be Int-Location;
thus s2.a = Comput(P3,s2,1).a by A10,SCMFSA_2:71
.= s5.a by A12,SCMFSA_2:69;
end;
then
A15: DataPart s2 = DataPart s5 by A14,SCMFSA_M:2;
assume
A16: J is_halting_on Initialized s,P;
then
A17: P2 halts_on s2 by SCMFSA8A:39;
A18: CurInstr(P3,
Comput(P3,s2,LifeSpan(P2,s2)+2))
= CurInstr(P3,
Comput(P3,s5,LifeSpan(P2,s2))) by EXTPRO_1:4
.= IncAddr(CurInstr(P2, Comput(P2,s2,LifeSpan(P2,s2))),2)
by A13,A15,Th2,A9,A1
.= IncAddr(halt SCM+FSA,2) by A17,EXTPRO_1:def 15
.= halt SCM+FSA by COMPOS_0:4;
then
A19: P3 halts_on s2 by EXTPRO_1:29;
now
let l be Nat;
assume
A20: l < LifeSpan(P2,s2) + 2;
per cases;
suppose
l = 0;
hence CurInstr(P3,Comput(P3,s2,l)) <>
halt SCM+FSA by A7,A2,PBOOLE:143;
end;
suppose
l = 1;
hence CurInstr(P3,Comput(P3,s2,l)) <>
halt SCM+FSA by A11,A4,PBOOLE:143;
end;
suppose
A21: l <> 0 & l <> 1;
assume
A22: CurInstr(P3,Comput(P3,
s2,l)) = halt SCM+FSA;
consider n being Nat such that
A23: l = n + 1 by A21,NAT_1:6;
n <> 0 by A21,A23;
then consider l2 being Nat such that
A24: n = l2 + 1 by NAT_1:6;
reconsider l2 as Element of NAT by ORDINAL1:def 12;
InsCode CurInstr(P2,Comput(P2,s2,l2))
= InsCode IncAddr(CurInstr(P2,
Comput(P2,s2,l2)),2) by COMPOS_0:def 9
.= InsCode CurInstr(P3,Comput(P3,s5,l2)) by A13,A15,Th2,A9,A1
.= InsCode CurInstr(P3,Comput(P3,s2,l2+(1+1))) by EXTPRO_1:4
.= 0 by A23,A24,A22,COMPOS_1:70;
then
A25: CurInstr(P2,Comput(P2,s2,l2)) = halt SCM+FSA by SCMFSA_2:95;
n + 1 < LifeSpan(P2,s2) + 1 + 1 by A20,A23;
then n < LifeSpan(P2,s2) + 1 by XREAL_1:6;
then l2 < LifeSpan(P2,s2) by A24,XREAL_1:6;
hence contradiction by A17,A25,EXTPRO_1:def 15;
end;
end;
then for l be Nat st CurInstr(P3,
Comput(P3,s2,l)) = halt SCM+FSA
holds LifeSpan(P2,s2) + 2 <= l;
then
A26: LifeSpan(P3,s2) = LifeSpan(P2,s2) + 2 by A18,A19,EXTPRO_1:def 15;
A27: DataPart Result(P2,s2) = DataPart Comput(P2, s2
,LifeSpan(P2,s2)) by A16,EXTPRO_1:23,SCMFSA8A:39
.= DataPart Comput(P3, s5,LifeSpan(P2,s2)) by A13,A15,Th2,A9,A1
.= DataPart Comput(P3, s2,LifeSpan(P2,s2) + 2)
by EXTPRO_1:4
.= DataPart Result(P3,s2) by A19,A26,EXTPRO_1:23;
A28: now
let x be object;
A30: IExec(if>0(a,I,J),P,s) = (Result(P3,s2)) by SCMFSA6B:def 1;
A31: IExec(JI2,P,s) = Result(P2,s2) by SCMFSA6B:def 1;
assume
A32: x in dom IExec(if>0(a,I,J),P,s);
per cases by A32,SCMFSA_M:1;
suppose
A33: x is Int-Location;
then x <> IC SCM+FSA by SCMFSA_2:56;
then
A34: not x in dom Start-At((card I+card J+3),SCM+FSA)
by TARSKI:def 1;
thus IExec(if>0(a,I,J),P,s).x = (Result(P3,s2)).x by A30
.= (Result(P2,s2)).x by A27,A33,SCMFSA_M:2
.= IExec(JI2,P,s).x by A31
.= (IExec(JI2,P,s) +* Start-At((card I+card J+3),SCM+FSA)).x
by A34,FUNCT_4:11;
end;
suppose
A35: x is FinSeq-Location;
then x <> IC SCM+FSA by SCMFSA_2:57;
then
A36: not x in dom Start-At((card I+card J+3),SCM+FSA)
by TARSKI:def 1;
thus IExec(if>0(a,I,J),P,s).x = (Result(P3,s2)).x by A30
.= (Result(P2,s2)).x by A27,A35,SCMFSA_M:2
.= IExec(JI2,P,s).x by A31
.= (IExec(JI2,P,s) +* Start-At((card I+card J+3),SCM+FSA)).x
by A36,FUNCT_4:11;
end;
suppose
A37: x = IC SCM+FSA;
then
A38: x in dom Start-At((card I+card J+3),SCM+FSA)by TARSKI:def 1;
A39: IC Result(P2,s2) = IC IExec(JI2,P,s)
by A31
.= (card I + card J + 1) by A16,SCMFSA8A:40;
thus IExec(if>0(a,I,J),P,s).x = (Result(P3,s2)).x by A30
.= Comput(P3, s2,LifeSpan(P2,s2) + 2).x by A19,A26,EXTPRO_1:23
.= IC Comput(P3, s5,LifeSpan(P2,s2)) by A37,EXTPRO_1:4
.= IC Comput(P2, s2,LifeSpan(P2,s2)) + 2 by A13,A15,Th2,A9,A1
.= IC Result(P2,s2) + 2 by A16,EXTPRO_1:23,SCMFSA8A:39
.= (Start-At ( (card I + card J + 1) + 2,SCM+FSA)).IC SCM+FSA
by A39,FUNCOP_1:72
.= (IExec(JI2,P,s) +* Start-At((card I+card J+3),SCM+FSA)).x
by A37,A38,FUNCT_4:13;
end;
end;
dom IExec(if>0(a,I,J),P,s) = the carrier of SCM+FSA by PARTFUN1:def 2
.= dom (IExec(JI2,P,s) +* Start-At((card I+card J+3),SCM+FSA))
by PARTFUN1:def 2;
hence
IExec(if>0(a,I,J),P,s)
= IExec(JI2,P,s) +* Start-At(card I + card J+ 3,SCM+FSA) by A28,FUNCT_1:2
.= IExec(J,P,s) +* Start-At(card I + card J + 1,SCM+FSA)
+* Start-At(card I + card J + 3,SCM+FSA) by A16,SCMFSA8A:41
.= IExec(J,P,s) +* Start-At(card I+card J+3,SCM+FSA)by FUNCT_4:114;
end;
theorem Th17:
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))
proof
let s be State of SCM+FSA;
let I,J be parahalting really-closed MacroInstruction of SCM+FSA;
let a be read-write Int-Location;
A1: I is_halting_on Initialized s,P by SCMFSA7B:19;
for s being 0-started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
st if>0(a,I,J) c= P
holds P halts_on s
proof
let s be 0-started State of SCM+FSA;
Start-At(0,SCM+FSA) c= s by MEMSTR_0:29;
then
A2: s = Initialize s by FUNCT_4:98;
let Q be Instruction-Sequence of SCM+FSA
such that
A3: if>0(a,I,J) c= Q;
A4: if>0(a,I,J) c= Q by A3;
A5: I is_halting_on s,Q by SCMFSA7B:19;
A6: J is_halting_on s,Q by SCMFSA7B:19;
A7: Q +* if>0(a,I,J) = Q by A4,FUNCT_4:98;
per cases;
suppose
s.a > 0;
then if>0(a,I,J) is_halting_on s,Q by A5,Th13;
hence Q halts_on s by A2,A7,SCMFSA7B:def 7;
end;
suppose
s.a <= 0;
then if>0(a,I,J) is_halting_on s,Q by A6,Th15;
hence Q halts_on s by A2,A7,SCMFSA7B:def 7;
end;
end;
hence if>0(a,I,J) is parahalting by AMISTD_1:def 11;
thus 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) by A1,Th14;
J is_halting_on Initialized s,P by SCMFSA7B:19;
hence thesis by Th16;
end;
theorem Th18:
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))
proof
let s be State of SCM+FSA;
let I,J be parahalting really-closed MacroInstruction of SCM+FSA;
let a be read-write Int-Location;
hereby
per cases;
suppose
s.a > 0;
then
IExec(if>0(a,I,J),P,s) = IExec(I,P,s) +* Start-At( (card I + card
J + 3),SCM+FSA) by Th17;
hence IC IExec(if>0(a,I,J),P,s) = (card I + card J + 3) by FUNCT_4:113;
end;
suppose
s.a <= 0;
then
IExec(if>0(a,I,J),P,s) = IExec(J,P,s) +* Start-At( (card I + card
J + 3),SCM+FSA) by Th17;
hence IC IExec(if>0(a,I,J),P,s) = (card I + card J + 3) by FUNCT_4:113;
end;
end;
hereby
assume s.a > 0;
then
A1: IExec(if>0(a,I,J),P,s) = IExec(I,P,s) +* Start-At( (card I + card J
+ 3),SCM+FSA) by Th17;
hereby
let d be Int-Location;
not d in dom Start-At((card I+card J+3),SCM+FSA)by SCMFSA_2:102;
hence IExec(if>0(a,I,J),P,s).d = IExec(I,P,s).d by A1,FUNCT_4:11;
end;
let f be FinSeq-Location;
not f in dom Start-At((card I+card J+3),SCM+FSA)by SCMFSA_2:103;
hence IExec(if>0(a,I,J),P,s).f = IExec(I,P,s).f by A1,FUNCT_4:11;
end;
assume s.a <= 0;
then
A2: IExec(if>0(a,I,J),P,s) = IExec(J,P,s) +* Start-At( (card I + card J +
3),SCM+FSA) by Th17;
hereby
let d be Int-Location;
not d in dom Start-At((card I+card J+3),SCM+FSA)by SCMFSA_2:102;
hence IExec(if>0(a,I,J),P,s).d = IExec(J,P,s).d by A2,FUNCT_4:11;
end;
let f be FinSeq-Location;
not f in dom Start-At((card I+card J+3),SCM+FSA)by SCMFSA_2:103;
hence thesis by A2,FUNCT_4:11;
end;
::$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;
correctness by Th11;
cluster if>0(a,I,J) -> parahalting;
correctness by Th17;
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
SubFrom(a,b) ";" if=0(a,I,J);
coherence;
func if>0(a,b,I,J) -> Program of SCM+FSA equals
SubFrom(a,b) ";" if>0(a,I,J);
coherence;
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;
coherence;
cluster if>0(a,I,J) -> halt-ending unique-halt;
coherence;
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;
coherence;
cluster if>0(a,b,I,J) -> really-closed;
coherence;
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;
coherence;
cluster if>0(a,b,I,J) -> halt-ending unique-halt;
coherence;
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;
correctness;
cluster if>0(a,b,I,J) -> parahalting;
correctness;
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;
correctness;
cluster if>0(a,b,I,J) -> really-closed;
correctness;
end;
theorem
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)
by SCMFSA6B:def 1;
theorem Th20:
for s being State of SCM+FSA, I being Program of SCM+FSA
holds Result(P+*I,Initialized s) = IExec(I,P,s)
by SCMFSA6B:def 1;
theorem Th21:
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)
proof
let s1,s2 be State of SCM+FSA;
let i be Instruction of SCM+FSA;
let a be Int-Location;
defpred S[State of SCM+FSA,State of SCM+FSA] means (for b being Int-Location
st a <> b holds $1.b = $2.b) & for f being FinSeq-Location holds $1.f = $2.f;
assume
A1: S[s1,s2];
assume
A2: i does not refer a;
A3: InsCode i <= 12 by SCMFSA_2:16;
A4: now
let b be Int-Location;
assume
A5: a <> b;
InsCode i = 0 or ... or InsCode i = 12 by A3;
then per cases;
suppose
InsCode i = 0;
then
A6: i = halt SCM+FSA by SCMFSA_2:95;
hence Exec(i,s1).b = s1.b by EXTPRO_1:def 3
.= s2.b by A1,A5
.= Exec(i,s2).b by A6,EXTPRO_1:def 3;
end;
suppose
InsCode i = 1;
then consider da, db being Int-Location such that
A7: i = da := db by SCMFSA_2:30;
A8: a <> db by A2,A7,SCMFSA7B:def 1;
hereby
per cases;
suppose
A9: b = da;
hence Exec(i,s1).b = s1.db by A7,SCMFSA_2:63
.= s2.db by A1,A8
.= Exec(i,s2).b by A7,A9,SCMFSA_2:63;
end;
suppose
A10: b <> da;
hence Exec(i,s1).b = s1.b by A7,SCMFSA_2:63
.= s2.b by A1,A5
.= Exec(i,s2).b by A7,A10,SCMFSA_2:63;
end;
end;
end;
suppose
InsCode i = 2;
then consider da, db being Int-Location such that
A11: i = AddTo(da,db) by SCMFSA_2:31;
A12: a <> db by A2,A11,SCMFSA7B:def 1;
hereby
per cases;
suppose
A13: b = da;
hence Exec(i,s1).b = s1.b + s1.db by A11,SCMFSA_2:64
.= s2.b + s1.db by A1,A5
.= s2.b + s2.db by A1,A12
.= Exec(i,s2).b by A11,A13,SCMFSA_2:64;
end;
suppose
A14: b <> da;
hence Exec(i,s1).b = s1.b by A11,SCMFSA_2:64
.= s2.b by A1,A5
.= Exec(i,s2).b by A11,A14,SCMFSA_2:64;
end;
end;
end;
suppose
InsCode i = 3;
then consider da, db being Int-Location such that
A15: i = SubFrom(da, db) by SCMFSA_2:32;
A16: a <> db by A2,A15,SCMFSA7B:def 1;
hereby
per cases;
suppose
A17: b = da;
hence Exec(i,s1).b = s1.b - s1.db by A15,SCMFSA_2:65
.= s2.b - s1.db by A1,A5
.= s2.b - s2.db by A1,A16
.= Exec(i,s2).b by A15,A17,SCMFSA_2:65;
end;
suppose
A18: b <> da;
hence Exec(i,s1).b = s1.b by A15,SCMFSA_2:65
.= s2.b by A1,A5
.= Exec(i,s2).b by A15,A18,SCMFSA_2:65;
end;
end;
end;
suppose
InsCode i = 4;
then consider da, db being Int-Location such that
A19: i = MultBy(da,db) by SCMFSA_2:33;
A20: a <> db by A2,A19,SCMFSA7B:def 1;
hereby
per cases;
suppose
A21: b = da;
hence Exec(i,s1).b = s1.b * s1.db by A19,SCMFSA_2:66
.= s2.b * s1.db by A1,A5
.= s2.b * s2.db by A1,A20
.= Exec(i,s2).b by A19,A21,SCMFSA_2:66;
end;
suppose
A22: b <> da;
hence Exec(i,s1).b = s1.b by A19,SCMFSA_2:66
.= s2.b by A1,A5
.= Exec(i,s2).b by A19,A22,SCMFSA_2:66;
end;
end;
end;
suppose
InsCode i = 5;
then consider da, db being Int-Location such that
A23: i = Divide(da, db) by SCMFSA_2:34;
A24: a <> db by A2,A23,SCMFSA7B:def 1;
A25: a <> da by A2,A23,SCMFSA7B:def 1;
hereby
per cases;
suppose
A26: b = db;
hence Exec(i,s1).b = s1.da mod s1.db by A23,SCMFSA_2:67
.= s2.da mod s1.db by A1,A25
.= s2.da mod s2.db by A1,A24
.= Exec(i,s2).b by A23,A26,SCMFSA_2:67;
end;
suppose
A27: b = da & b <> db;
hence Exec(i,s1).b = s1.da div s1.db by A23,SCMFSA_2:67
.= s1.da div s2.db by A1,A24
.= s2.da div s2.db by A1,A25
.= Exec(i,s2).b by A23,A27,SCMFSA_2:67;
end;
suppose
A28: b <> da & b <> db;
hence Exec(i,s1).b = s1.b by A23,SCMFSA_2:67
.= s2.b by A1,A5
.= Exec(i,s2).b by A23,A28,SCMFSA_2:67;
end;
end;
end;
suppose
InsCode i = 6;
then
A29: ex loc being Nat st i = goto loc by SCMFSA_2:35;
hence Exec(i,s1).b = s1.b by SCMFSA_2:69
.= s2.b by A1,A5
.= Exec(i,s2).b by A29,SCMFSA_2:69;
end;
suppose
InsCode i = 7;
then
A30: ex loc being Nat, da being Int-Location
st i = da =0_goto loc by SCMFSA_2:36;
hence Exec(i,s1).b = s1.b by SCMFSA_2:70
.= s2.b by A1,A5
.= Exec(i,s2).b by A30,SCMFSA_2:70;
end;
suppose
InsCode i = 8;
then
A31: ex loc being Nat, da being Int-Location
st i = da >0_goto loc by SCMFSA_2:37;
hence Exec(i,s1).b = s1.b by SCMFSA_2:71
.= s2.b by A1,A5
.= Exec(i,s2).b by A31,SCMFSA_2:71;
end;
suppose
InsCode i = 9;
then consider
db, da being Int-Location, g being FinSeq-Location such that
A32: i = da := (g,db) by SCMFSA_2:38;
A33: a <> db by A2,A32,SCMFSA7B:def 1;
hereby
per cases;
suppose
A34: b = da;
then consider m2 being Nat such that
A35: m2 = |.s2.db.| and
A36: Exec(da:=(g,db), s2).b = (s2.g)/.m2 by SCMFSA_2:72;
consider m1 being Nat such that
A37: m1 = |.s1.db.| and
A38: Exec(da:=(g,db), s1).b = (s1.g)/.m1 by A34,SCMFSA_2:72;
m1 = m2 by A1,A33,A37,A35;
hence Exec(i,s1).b = Exec(i,s2).b by A1,A32,A38,A36;
end;
suppose
A39: b <> da;
hence Exec(i,s1).b = s1.b by A32,SCMFSA_2:72
.= s2.b by A1,A5
.= Exec(i,s2).b by A32,A39,SCMFSA_2:72;
end;
end;
end;
suppose
InsCode i = 10;
then
A40: ex db, da being Int-Location, g being FinSeq-Location st i = (g,db
):= da by SCMFSA_2:39;
hence Exec(i,s1).b = s1.b by SCMFSA_2:73
.= s2.b by A1,A5
.= Exec(i,s2).b by A40,SCMFSA_2:73;
end;
suppose
InsCode i = 11;
then consider da being Int-Location, g being FinSeq-Location such that
A41: i = da :=len g by SCMFSA_2:40;
hereby
per cases;
suppose
A42: b = da;
hence Exec(i,s1).b = len (s1.g) by A41,SCMFSA_2:74
.= len (s2.g) by A1
.= Exec(i,s2).b by A41,A42,SCMFSA_2:74;
end;
suppose
A43: b <> da;
hence Exec(i,s1).b = s1.b by A41,SCMFSA_2:74
.= s2.b by A1,A5
.= Exec(i,s2).b by A41,A43,SCMFSA_2:74;
end;
end;
end;
suppose
InsCode i = 12;
then
A44: ex da being Int-Location, g being FinSeq-Location st i = g
:=<0,...,0>da by SCMFSA_2:41;
hence Exec(i,s1).b = s1.b by SCMFSA_2:75
.= s2.b by A1,A5
.= Exec(i,s2).b by A44,SCMFSA_2:75;
end;
end;
assume
A45: IC s1 = IC s2;
now
let f be FinSeq-Location;
InsCode i = 0 or ... or InsCode i = 12 by A3;
then per cases;
suppose
InsCode i = 0;
then
A46: i = halt SCM+FSA by SCMFSA_2:95;
hence Exec(i,s1).f = s1.f by EXTPRO_1:def 3
.= s2.f by A1
.= Exec(i,s2).f by A46,EXTPRO_1:def 3;
end;
suppose
InsCode i = 1;
then
A47: ex da, db being Int-Location st i = da := db by SCMFSA_2:30;
hence Exec(i,s1).f = s1.f by SCMFSA_2:63
.= s2.f by A1
.= Exec(i,s2).f by A47,SCMFSA_2:63;
end;
suppose
InsCode i = 2;
then
A48: ex da, db being Int-Location st i = AddTo(da,db) by SCMFSA_2:31;
hence Exec(i,s1).f = s1.f by SCMFSA_2:64
.= s2.f by A1
.= Exec(i,s2).f by A48,SCMFSA_2:64;
end;
suppose
InsCode i = 3;
then
A49: ex da, db being Int-Location st i = SubFrom(da, db) by SCMFSA_2:32;
hence Exec(i,s1).f = s1.f by SCMFSA_2:65
.= s2.f by A1
.= Exec(i,s2).f by A49,SCMFSA_2:65;
end;
suppose
InsCode i = 4;
then
A50: ex da, db being Int-Location st i = MultBy(da,db) by SCMFSA_2:33;
hence Exec(i,s1).f = s1.f by SCMFSA_2:66
.= s2.f by A1
.= Exec(i,s2).f by A50,SCMFSA_2:66;
end;
suppose
InsCode i = 5;
then
A51: ex da, db being Int-Location st i = Divide(da, db) by SCMFSA_2:34;
hence Exec(i,s1).f = s1.f by SCMFSA_2:67
.= s2.f by A1
.= Exec(i,s2).f by A51,SCMFSA_2:67;
end;
suppose
InsCode i = 6;
then
A52: ex loc being Nat st i = goto loc by SCMFSA_2:35;
hence Exec(i,s1).f = s1.f by SCMFSA_2:69
.= s2.f by A1
.= Exec(i,s2).f by A52,SCMFSA_2:69;
end;
suppose
InsCode i = 7;
then
A53: ex loc being Nat, da being Int-Location
st i = da=0_goto loc by SCMFSA_2:36;
hence Exec(i,s1).f = s1.f by SCMFSA_2:70
.= s2.f by A1
.= Exec(i,s2).f by A53,SCMFSA_2:70;
end;
suppose
InsCode i = 8;
then
A54: ex loc being Nat, da being Int-Location
st i = da>0_goto loc by SCMFSA_2:37;
hence Exec(i,s1).f = s1.f by SCMFSA_2:71
.= s2.f by A1
.= Exec(i,s2).f by A54,SCMFSA_2:71;
end;
suppose
InsCode i = 9;
then
A55: ex db, da being Int-Location, g being FinSeq-Location st i = da :=
(g,db) by SCMFSA_2:38;
hence Exec(i,s1).f = s1.f by SCMFSA_2:72
.= s2.f by A1
.= Exec(i,s2).f by A55,SCMFSA_2:72;
end;
suppose
InsCode i = 10;
then consider
db, da being Int-Location, g being FinSeq-Location such that
A56: i = (g,db):=da by SCMFSA_2:39;
A57: a <> db by A2,A56,SCMFSA7B:def 1;
A58: a <> da by A2,A56,SCMFSA7B:def 1;
hereby
per cases;
suppose
A59: f = g;
A60: s1.da = s2.da by A1,A58;
consider m2 being Nat such that
A61: m2 = |.s2.db.| and
A62: Exec((g,db):=da,s2).g = s2.g+*(m2,s2.da) by SCMFSA_2:73;
consider m1 being Nat such that
A63: m1 = |.s1.db.| and
A64: Exec((g,db):=da,s1).g = s1.g+*(m1,s1.da) by SCMFSA_2:73;
m1 = m2 by A1,A57,A63,A61;
hence Exec(i,s1).f = Exec(i,s2).f by A1,A56,A59,A64,A62,A60;
end;
suppose
A65: f <> g;
hence Exec(i,s1).f = s1.f by A56,SCMFSA_2:73
.= s2.f by A1
.= Exec(i,s2).f by A56,A65,SCMFSA_2:73;
end;
end;
end;
suppose
InsCode i = 11;
then
A66: ex da being Int-Location, g being FinSeq-Location st i = da :=len
g by SCMFSA_2:40;
hence Exec(i,s1).f = s1.f by SCMFSA_2:74
.= s2.f by A1
.= Exec(i,s2).f by A66,SCMFSA_2:74;
end;
suppose
InsCode i = 12;
then consider da being Int-Location, g being FinSeq-Location such that
A67: i = g:=<0,...,0>da by SCMFSA_2:41;
A68: a <> da by A2,A67,SCMFSA7B:def 1;
hereby
per cases;
suppose
A69: f = g;
A70: ex m2 being Nat st m2 = |.s2.da.| & Exec(g
:=<0,...,0>da, s2).g = m2 |-> 0 by SCMFSA_2:75;
ex m1 being Nat st m1 = |.s1.da.| & Exec(g
:=<0,...,0>da, s1).g = m1 |-> 0 by SCMFSA_2:75;
hence Exec(i,s1).f = Exec(i,s2).f by A1,A67,A68,A69,A70;
end;
suppose
A71: f <> g;
hence Exec(i,s1).f = s1.f by A67,SCMFSA_2:75
.= s2.f by A1
.= Exec(i,s2).f by A67,A71,SCMFSA_2:75;
end;
end;
end;
end;
hence S[Exec(i,s1),Exec(i,s2)] by A4;
now
InsCode i = 0 or ... or InsCode i = 12 by A3;
then per cases;
suppose
InsCode i = 0;
then
A72: i = halt SCM+FSA by SCMFSA_2:95;
hence Exec(i,s1).IC SCM+FSA = IC s1 by EXTPRO_1:def 3
.= Exec(i,s2).IC SCM+FSA by A45,A72,EXTPRO_1:def 3;
end;
suppose
InsCode i = 1;
then
A73: ex da, db being Int-Location st i = da := db by SCMFSA_2:30;
hence Exec(i,s1).IC SCM+FSA = IC s1 + 1 by SCMFSA_2:63
.= Exec(i,s2).IC SCM+FSA by A45,A73,SCMFSA_2:63;
end;
suppose
InsCode i = 2;
then
A74: ex da, db being Int-Location st i = AddTo(da,db) by SCMFSA_2:31;
hence Exec(i,s1).IC SCM+FSA = IC s1 + 1 by SCMFSA_2:64
.= Exec(i,s2).IC SCM+FSA by A45,A74,SCMFSA_2:64;
end;
suppose
InsCode i = 3;
then
A75: ex da, db being Int-Location st i = SubFrom(da, db) by SCMFSA_2:32;
hence Exec(i,s1).IC SCM+FSA = IC s1 + 1 by SCMFSA_2:65
.= Exec(i,s2).IC SCM+FSA by A45,A75,SCMFSA_2:65;
end;
suppose
InsCode i = 4;
then
A76: ex da, db being Int-Location st i = MultBy(da,db) by SCMFSA_2:33;
hence Exec(i,s1).IC SCM+FSA = IC s1 + 1 by SCMFSA_2:66
.= Exec(i,s2).IC SCM+FSA by A45,A76,SCMFSA_2:66;
end;
suppose
InsCode i = 5;
then
A77: ex da, db being Int-Location st i = Divide(da, db) by SCMFSA_2:34;
hence Exec(i,s1).IC SCM+FSA = IC s1 + 1 by SCMFSA_2:67
.= Exec(i,s2).IC SCM+FSA by A45,A77,SCMFSA_2:67;
end;
suppose
InsCode i = 6;
then consider loc being Nat such that
A78: i = goto loc by SCMFSA_2:35;
thus Exec(i,s1).IC SCM+FSA = loc by A78,SCMFSA_2:69
.= Exec(i,s2).IC SCM+FSA by A78,SCMFSA_2:69;
end;
suppose
InsCode i = 7;
then consider loc being Nat, da being
Int-Location such that
A79: i = da =0_goto loc by SCMFSA_2:36;
a <> da by A2,A79,SCMFSA7B:def 1;
then
A80: s1.da = s2.da by A1;
hereby
per cases;
suppose
A81: s1.da = 0;
hence Exec(i,s1).IC SCM+FSA = loc by A79,SCMFSA_2:70
.= Exec(i,s2).IC SCM+FSA by A79,A80,A81,SCMFSA_2:70;
end;
suppose
A82: s1.da <> 0;
hence Exec(i,s1).IC SCM+FSA = IC s1 + 1 by A79,SCMFSA_2:70
.= Exec(i,s2).IC SCM+FSA by A45,A79,A80,A82,SCMFSA_2:70;
end;
end;
end;
suppose
InsCode i = 8;
then consider loc being Nat, da being
Int-Location such that
A83: i = da>0_goto loc by SCMFSA_2:37;
a <> da by A2,A83,SCMFSA7B:def 1;
then
A84: s1.da = s2.da by A1;
hereby
per cases;
suppose
A85: s1.da > 0;
hence Exec(i,s1).IC SCM+FSA = loc by A83,SCMFSA_2:71
.= Exec(i,s2).IC SCM+FSA by A83,A84,A85,SCMFSA_2:71;
end;
suppose
A86: s1.da <= 0;
hence Exec(i,s1).IC SCM+FSA = IC s1 + 1 by A83,SCMFSA_2:71
.= Exec(i,s2).IC SCM+FSA by A45,A83,A84,A86,SCMFSA_2:71;
end;
end;
end;
suppose
InsCode i = 9;
then
A87: ex db, da being Int-Location, g being FinSeq-Location st i = da
:= (g,db) by SCMFSA_2:38;
hence Exec(i,s1).IC SCM+FSA = IC s1 + 1 by SCMFSA_2:72
.= Exec(i,s2).IC SCM+FSA by A45,A87,SCMFSA_2:72;
end;
suppose
InsCode i = 10;
then
A88: ex db, da being Int-Location, g being FinSeq-Location st i = (g,
db):=da by SCMFSA_2:39;
hence Exec(i,s1).IC SCM+FSA = IC s1 + 1 by SCMFSA_2:73
.= Exec(i,s2).IC SCM+FSA by A45,A88,SCMFSA_2:73;
end;
suppose
InsCode i = 11;
then
A89: ex da being Int-Location, g being FinSeq-Location st i = da :=len
g by SCMFSA_2:40;
hence Exec(i,s1).IC SCM+FSA = IC s1 + 1 by SCMFSA_2:74
.= Exec(i,s2).IC SCM+FSA by A45,A89,SCMFSA_2:74;
end;
suppose
InsCode i = 12;
then
A90: ex da being Int-Location, g being FinSeq-Location st i = g
:=<0,...,0>da by SCMFSA_2:41;
hence Exec(i,s1).IC SCM+FSA = IC s1 + 1 by SCMFSA_2:75
.= Exec(i,s2).IC SCM+FSA by A45,A90,SCMFSA_2:75;
end;
end;
hence thesis;
end;
theorem Th22:
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))
proof
let s1,s2 be State of SCM+FSA;
let I be really-closed Program of SCM+FSA;
let a be Int-Location;
assume
A1: I does not refer a;
set S2 = Initialize s2,
Q2 = P2 +* I;
set S1 = Initialize s1,
Q1 = P1 +* I;
A2: I c= Q1 by FUNCT_4:25;
A3: I c= Q2 by FUNCT_4:25;
defpred S[State of SCM+FSA,State of SCM+FSA] means (for b being Int-Location
st a <> b holds $1.b = $2.b) & for f being FinSeq-Location holds $1.f = $2.f;
assume that
A4: for b being Int-Location st a <> b holds s1.b = s2.b and
A5: for f being FinSeq-Location holds s1.f = s2.f;
A6: IC SCM+FSA in dom Start-At(0,SCM+FSA) by MEMSTR_0:15;
A7: now
let f be FinSeq-Location;
A8: not f in dom Start-At(0,SCM+FSA) by SCMFSA_2:103;
hence S1.f = s1.f by FUNCT_4:11
.= s2.f by A5
.= S2.f by A8,FUNCT_4:11;
end;
defpred P[Nat] means S[ Comput(Q1,S1,$1), Comput(Q2,S2,$1)] &
IC Comput(Q1,S1,$1) = IC Comput(Q2,S2,$1) &
CurInstr(Q1,Comput(Q1,S1,$1)) = CurInstr(Q2,Comput(Q2,S2,$1));
A9: IC Comput(Q1,S1,0) = IC S1
.= IC Start-At(0,SCM+FSA) by A6,FUNCT_4:13
.= IC S2 by A6,FUNCT_4:13
.= IC Comput(Q2,S2,0);
A10: now
let b be Int-Location;
assume
A11: a <> b;
A12: not b in dom Start-At(0,SCM+FSA) by SCMFSA_2:102;
hence S1.b = s1.b by FUNCT_4:11
.= s2.b by A4,A11
.= S2.b by A12,FUNCT_4:11;
end;
IC S1 = 0 by MEMSTR_0:def 11;
then
A13: IC S1 in dom I by AFINSQ_1:65;
then
A14: IC Comput(Q1,S1,0) in dom I;
A15: for k being Nat holds P[k] implies P[k + 1]
proof
let k be Nat;
A16: Comput(Q1,S1,k+1) = Following(Q1,Comput(Q1,S1,k)) by EXTPRO_1:3
.= Exec(CurInstr(Q1,Comput(Q1,S1,k)),
Comput(Q1,S1,k));
A17: IC Comput(Q1,S1,k) in dom I by A2,A13,AMISTD_1:21;
A18: Comput(Q2,S2,k+1) = Following(Q2,Comput(Q2,S2,k)) by EXTPRO_1:3
.= Exec(CurInstr(Q2,Comput(Q2,S2,k)),
Comput(Q2,S2,k));
A19: Q1/.IC Comput(Q1,S1,k)
= Q1.IC Comput(Q1,S1,k) by PBOOLE:143;
CurInstr(Q1,Comput(Q1,S1,k))
= I.IC Comput(Q1,S1,k) by A17,A19,A2,GRFUNC_1:2;
then CurInstr(Q1,Comput(Q1,S1,k)) in rng I by A17,FUNCT_1:def 3;
then
A20: CurInstr(Q1,Comput(Q1,S1,k)) does not refer a
by A1,SCMFSA7B:def 2;
assume
A21: P[k];
hence S[ Comput(Q1,S1,k+1), Comput(Q2,S2,k+1)]
by A16,A18,A20,Th21;
thus
A22: IC Comput(Q1,S1,k+1) = IC Comput(Q2,S2,k+1) by A21,A16,A18,A20,Th21;
A23: IC Comput(Q1,S1,k+1) in dom I by A2,A13,AMISTD_1:21;
A24: Q1/.IC Comput(Q1,S1,k+1)
= Q1.IC Comput(Q1,S1,k+1) by PBOOLE:143;
A25: Q2/.IC Comput(Q2,S2,k+1)
= Q2.IC Comput(Q2,S2,k+1) by PBOOLE:143;
thus CurInstr(Q1,Comput(Q1,S1,k+1))
= I.IC Comput(Q1,S1,k+1) by A23,A24,A2,GRFUNC_1:2
.= CurInstr(Q2,Comput(Q2,S2,k+1))
by A22,A23,A25,A3,GRFUNC_1:2;
end;
CurInstr(Q1,Comput(Q1,S1,0))
= Q1.IC Comput(Q1,S1,0) by PBOOLE:143
.= I.IC Comput(Q1,S1,0) by A14,A2,GRFUNC_1:2
.= Q2.IC Comput(Q2,S2,0) by A9,A14,A3,GRFUNC_1:2
.= CurInstr(Q2,Comput(Q2,S2,0)) by PBOOLE:143;
then
A26: P[0] by A10,A7,A9;
for k being Nat holds P[k] from NAT_1:sch 2(A26,A15);
hence thesis;
end;
theorem
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
proof
let s be State of SCM+FSA;
let I be really-closed Program of SCM+FSA;
let l be Nat;
DataPart s = DataPart(s +* Start-At(l,SCM+FSA)) by MEMSTR_0:79;
hence thesis by Th1;
end;
theorem Th24:
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
proof
let s1,s2 be State of SCM+FSA;
let I be really-closed Program of SCM+FSA;
let a be Int-Location;
assume
A1: I does not refer a;
set S2 = Initialize s2,
Q2 = P2 +* I;
set S1 = Initialize s1,
Q1 = P1 +* I;
assume
A2: for b being Int-Location st a <> b holds s1.b = s2.b;
assume
A3: for f being FinSeq-Location holds s1.f = s2.f;
assume that
A4: I is_halting_on s1,P1;
Q1 halts_on S1 by A4,SCMFSA7B:def 7;
then consider n being Nat such that
A5: CurInstr(Q1,Comput(Q1,S1,n)) = halt SCM+FSA;
CurInstr(Q2,Comput(Q2,S2,n)) = halt SCM+FSA by A1,A5,Th22,A3,A2;
then Q2 halts_on S2 by EXTPRO_1:29;
hence thesis by SCMFSA7B:def 7;
end;
theorem Th25:
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)
proof
let s1,s2 be State of SCM+FSA;
let I be really-closed Program of SCM+FSA;
let a be Int-Location;
assume that
A1: for d being read-write Int-Location st a <> d holds s1.d = s2.d and
A2: for f being FinSeq-Location holds s1.f = s2.f;
A3: now
let d be Int-Location;
assume
A4: a <> d;
per cases;
suppose
A5: d = intloc 0;
hence (Initialized s1).d = 1 by SCMFSA_M:9
.= (Initialized s2).d by A5,SCMFSA_M:9;
end;
suppose
d <> intloc 0;
then
A6: d is read-write;
hence (Initialized s1).d = s1.d by SCMFSA_M:37
.= s2.d by A1,A4,A6
.= (Initialized s2).d by A6,SCMFSA_M:37;
end;
end;
set S1 = Initialized s1, Q1 = P1 +* I;
set S2 = Initialized s2, Q2 = P2 +* I;
assume
A7: I does not refer a;
A8: S2 = Initialize Initialized s2 by MEMSTR_0:44;
assume that
A9: I is_halting_on Initialized s1,P1;
A10: now
let f be FinSeq-Location;
thus (Initialized s1).f = s1.f by SCMFSA_M:37
.= s2.f by A2
.= (Initialized s2).f by SCMFSA_M:37;
end;
then I is_halting_on Initialized s2,P2 by A7,A9,A3,Th24;
then
A11: Q2 halts_on S2 by A8,SCMFSA7B:def 7;
A12: S1 = Initialize Initialized s1 by MEMSTR_0:44;
then
A13: Q1 halts_on S1 by A9,SCMFSA7B:def 7;
now
let l be Nat;
assume l < LifeSpan(Q1,S1);
then CurInstr(Q1,Comput(Q1,S1,l))
<> halt SCM+FSA by A13,EXTPRO_1:def 15;
hence CurInstr(Q2,Comput(Q2,S2,l)) <>
halt SCM+FSA by A7,A3,A10,A12,A8,Th22;
end;
then
A14: for l be Nat st CurInstr(Q2,Comput(Q2,S2,l)) = halt SCM+FSA
holds LifeSpan(Q1,S1) <= l;
CurInstr (Q2,Comput(Q2,S2,LifeSpan(Q1,S1)))
= CurInstr(Q1,Comput(Q1,S1,LifeSpan(Q1,S1))) by A7,A3,A10,A12,A8,Th22
.= halt SCM+FSA by A13,EXTPRO_1:def 15;
then
A15: LifeSpan(Q1,S1) = LifeSpan(Q2,S2) by A11,A14,EXTPRO_1:def 15;
then
A16: Result(Q2,S2) = Comput(Q2,S2,LifeSpan(Q1,S1)) by A11,EXTPRO_1:23;
A17: Result(Q1,S1) = Comput(Q1,S1,LifeSpan(Q1,S1)) by A13,EXTPRO_1:23;
A18: Result(P1+*I,Initialized s1) = IExec(I,P1,s1) by Th20;
A19: Result(P2+*I,Initialized s2) = IExec(I,P2,s2) by Th20;
thus for d being Int-Location st a <> d
holds IExec(I,P1,s1).d = IExec(I,P2,s2).d
by A19,A18,A7,A3,A10,A12,A8,A16,A17,Th22;
thus for f being FinSeq-Location holds IExec(I,P1,s1).f= IExec(I,P2,s2).f
by A19,A18,A7,A3,A10,A12,A8,A16,A17,Th22;
thus IC IExec(I,P1,s1) = IC Result(Q1,S1) by SCMFSA6B:def 1
.= IC Comput(Q1,S1,LifeSpan(Q1,S1)) by A13,EXTPRO_1:23
.= IC Comput(Q2,S2,LifeSpan(Q2,S2)) by A7,A3,A10,A12,A8,A15,Th22
.= IC Result(Q2,S2) by A11,EXTPRO_1:23
.= IC IExec(I,P2,s2) by SCMFSA6B:def 1;
end;
theorem
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))
proof
let s be State of SCM+FSA;
let I,J be parahalting really-closed MacroInstruction of SCM+FSA;
let a,b be read-write Int-Location;
assume that
A1: I does not refer a and
A2: J does not refer a;
reconsider JJ = if=0(a,I,J) as parahalting Program of SCM+FSA;
reconsider II = Macro SubFrom(a,b) as keeping_0 parahalting Program of
SCM+FSA;
set i = SubFrom(a,b);
set s1 = Exec(i,Initialized s);
A3: now
let c be read-write Int-Location;
assume a <> c;
hence s1.c = (Initialized s).c by SCMFSA_2:65
.= s.c by SCMFSA_M:37;
end;
IExec(if=0(a,b,I,J),P,s) = IncIC(IExec(JJ,P,IExec(II,P,s)),card II)
by SCMFSA6B:20;
hence IC IExec(if=0(a,b,I,J),P,s) = IC IExec(JJ,P,IExec(II,P,s)) + card II
by FUNCT_4:113
.= (card I + card J + 3) + card II by Th12
.= (card I + card J + 3) + 2 by COMPOS_1:56
.= (card I + card J + 5);
A4: now
let f be FinSeq-Location;
thus s1.f = (Initialized s).f by SCMFSA_2:65
.= s.f by SCMFSA_M:37;
end;
hereby
assume
A5: s.a = s.b;
A6: I is_halting_on Initialized s,P by SCMFSA7B:19;
A7: Exec(i,Initialized s).a = (Initialized s).a - (Initialized s).b
by SCMFSA_2:65
.= s.a - (Initialized s).b by SCMFSA_M:37
.= s.a - s.b by SCMFSA_M:37
.= 0 by A5;
hereby
let d be Int-Location;
assume
A8: a <> d;
thus IExec(if=0(a,b,I,J),P,s).d
= IExec(JJ,P,Exec(i,Initialized s)).d by Th3
.= IExec(I,P,Exec(i,Initialized s)).d by A7,Th12
.= IExec(I,P,s).d by A1,A3,A4,A6,A8,Th25;
end;
let f be FinSeq-Location;
thus IExec(if=0(a,b,I,J),P,s).f
= IExec(JJ,P,Exec(i,Initialized s)).f by Th4
.= IExec(I,P,Exec(i,Initialized s)).f by A7,Th12
.= IExec(I,P,s).f by A1,A3,A4,A6,Th25;
end;
A9: Exec(i,Initialized s).a = (Initialized s).a - (Initialized s).b by
SCMFSA_2:65
.= s.a - (Initialized s).b by SCMFSA_M:37
.= s.a - s.b by SCMFSA_M:37;
A10: J is_halting_on Initialized s,P by SCMFSA7B:19;
assume s.a <> s.b;
then
A11: s.a + (- s.b) <> s.b + (- s.b);
hereby
let d be Int-Location;
assume
A12: a <> d;
thus IExec(if=0(a,b,I,J),P,s).d
= IExec(JJ,P,Exec(i,Initialized s)).d by Th3
.= IExec(J,P,Exec(i,Initialized s)).d by A9,A11,Th12
.= IExec(J,P,s).d by A2,A3,A4,A10,A12,Th25;
end;
let f be FinSeq-Location;
thus IExec(if=0(a,b,I,J),P,s).f = IExec(JJ,P,Exec(i,Initialized s)).f by Th4
.= IExec(J,P,Exec(i,Initialized s)).f by A9,A11,Th12
.= IExec(J,P,s).f by A2,A3,A4,A10,Th25;
end;
theorem
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)
proof
let s be State of SCM+FSA;
let I,J be parahalting really-closed MacroInstruction of SCM+FSA;
let a,b be read-write Int-Location;
assume that
A1: I does not refer a and
A2: J does not refer a;
reconsider JJ = if>0(a,I,J) as parahalting Program of SCM+FSA;
reconsider II = Macro SubFrom(a,b) as keeping_0 parahalting Program of
SCM+FSA;
set i = SubFrom(a,b);
set s1 = Exec(i,Initialized s);
A3: now
let c be read-write Int-Location;
assume a <> c;
hence s1.c = (Initialized s).c by SCMFSA_2:65
.= s.c by SCMFSA_M:37;
end;
IExec(if>0(a,b,I,J),P,s) = IncIC(IExec(JJ,P,IExec(II,P,s)),card II)
by SCMFSA6B:20;
hence IC IExec(if>0(a,b,I,J),P,s)
= IC IExec(JJ,P,IExec(II,P,s)) + card II by FUNCT_4:113
.= (card I + card J + 3) + card II by Th18
.= (card I + card J + 3) + 2 by COMPOS_1:56
.= (card I + card J + 5);
A4: now
let f be FinSeq-Location;
thus s1.f = (Initialized s).f by SCMFSA_2:65
.= s.f by SCMFSA_M:37;
end;
hereby
A5: Exec(i,Initialized s).a = (Initialized s).a - (Initialized s).b
by SCMFSA_2:65
.= s.a - (Initialized s).b by SCMFSA_M:37
.= s.a - s.b by SCMFSA_M:37;
assume s.a > s.b;
then
A6: Exec(i,Initialized s).a > 0 by A5,XREAL_1:50;
A7: I is_halting_on Initialized s,P by SCMFSA7B:19;
hereby
let d be Int-Location;
assume
A8: a <> d;
thus IExec(if>0(a,b,I,J),P,s).d
= IExec(JJ,P,Exec(i,Initialized s)).d by Th3
.= IExec(I,P,Exec(i,Initialized s)).d by A6,Th18
.= IExec(I,P,s).d by A1,A3,A4,A7,A8,Th25;
end;
let f be FinSeq-Location;
thus IExec(if>0(a,b,I,J),P,s).f
= IExec(JJ,P,Exec(i,Initialized s)).f by Th4
.= IExec(I,P,Exec(i,Initialized s)).f by A6,Th18
.= IExec(I,P,s).f by A1,A3,A4,A7,Th25;
end;
A9: Exec(i,Initialized s).a = (Initialized s).a - (Initialized s).b by
SCMFSA_2:65
.= s.a - (Initialized s).b by SCMFSA_M:37
.= s.a - s.b by SCMFSA_M:37;
A10: J is_halting_on Initialized s,P by SCMFSA7B:19;
assume s.a <= s.b;
then
A11: Exec(i,Initialized s).a <= 0 by A9,XREAL_1:47;
hereby
let d be Int-Location;
assume
A12: a <> d;
thus IExec(if>0(a,b,I,J),P,s).d
= IExec(JJ,P,Exec(i,Initialized s)).d by Th3
.= IExec(J,P,Exec(i,Initialized s)).d by A11,Th18
.= IExec(J,P,s).d by A2,A3,A4,A10,A12,Th25;
end;
let f be FinSeq-Location;
thus IExec(if>0(a,b,I,J),P,s).f
= IExec(JJ,P,Exec(i,Initialized s)).f by Th4
.= IExec(J,P,Exec(i,Initialized s)).f by A11,Th18
.= IExec(J,P,s).f by A2,A3,A4,A10,Th25;
end;
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
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
proof let I be really-closed Program of SCM+FSA;
assume s.intloc 0 = 1;
then DataPart Initialized s = DataPart s by SCMFSA_M:19;
hence thesis by Th1;
end;