:: Conditional branch macro instructions of SCM+FSA, Part I (preliminary)
:: 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, SUBSET_1, SCMFSA_2, XBOOLE_0, FSM_1, RELAT_1, AMI_1,
GRAPHSP, XXREAL_0, CIRCUIT2, ARYTM_3, CARD_1, FUNCT_1, SCMFSA6B,
MSUALG_1, FUNCT_4, SCMFSA6A, FUNCOP_1, TARSKI, AMISTD_2, EXTPRO_1, AMI_3,
SCMFSA7B, VALUED_1, CAT_1, NAT_1, SCMFSA8A, PARTFUN1, RELOC, SCMFSA6C,
AFINSQ_1, COMPOS_1, SCMPDS_4, TURING_1, ARYTM_1, SCMFSA_7, AMISTD_1;
notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0,
NAT_1, FUNCOP_1, RELAT_1, FUNCT_1, PARTFUN1, AFINSQ_1, FUNCT_4, FUNCT_7,
NAT_D, FINSEQ_1, VALUED_1, PBOOLE, STRUCT_0, MEMSTR_0, COMPOS_0,
COMPOS_1, EXTPRO_1, AMISTD_1, AMISTD_2, SCMFSA_2, SCMFSA10, SCMFSA_7,
SCMFSA6A, SCMFSA6B, SCMFSA6C, SCMFSA7B, XXREAL_0, SCMFSA_M;
constructors DOMAIN_1, XXREAL_0, SCMFSA_7, SCMFSA6A, SF_MASTR, SCMFSA6B,
SCMFSA6C, SCMFSA7B, AMISTD_2, RELSET_1, PRE_POLY, SCMFSA10, AMISTD_1,
PBOOLE, AMISTD_5, MEMSTR_0, SCMFSA_M, FUNCT_7, NAT_D;
registrations FUNCOP_1, XXREAL_0, MEMBERED, SCMFSA_2, SCMFSA6A, AFINSQ_1,
SCMFSA7B, SCMFSA10, AMISTD_2, COMPOS_1, EXTPRO_1, FUNCT_4, ORDINAL1,
STRUCT_0, MEMSTR_0, AMI_3, COMPOS_0, SCMFSA_M, XCMPLX_0, NAT_1, FUNCT_7,
AMISTD_1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions SCMFSA7B;
equalities COMPOS_1, EXTPRO_1, SCMFSA6A, MEMSTR_0, SCMFSA_M, ORDINAL1;
expansions COMPOS_1;
theorems TARSKI, NAT_1, FUNCT_1, FUNCT_4, MEMSTR_0, RELAT_1, SCMFSA_2,
SCMFSA_4, SCMFSA6A, GRFUNC_1, SCMFSA6B, SCMFSA7B, XBOOLE_0, XREAL_1,
XXREAL_0, VALUED_1, AFINSQ_1, PARTFUN1, COMPOS_1, EXTPRO_1, PBOOLE,
COMPOS_0, SCMFSA_M, CARD_1, FUNCT_7, AMISTD_1, SCMFSA10;
schemes NAT_1;
begin
reserve m for Nat;
reserve P for Instruction-Sequence of SCM+FSA;
set A = NAT;
set D = Data-Locations SCM+FSA;
set SA0 = Start-At(0,SCM+FSA);
set T = intloc 0 .--> 1;
::$CT 7
theorem Th1:
for i being Instruction of SCM+FSA, a being Int-Location, n
being Element of NAT holds i does not destroy a implies IncAddr(i,n)
does not destroy a
proof
let i be Instruction of SCM+FSA;
let a be Int-Location;
let n be Element of NAT;
assume
A1: i does not destroy a;
InsCode i = 0 or ... or InsCode i = 12 by SCMFSA_2:16;
then per cases;
suppose
InsCode i = 0;
then i = halt SCM+FSA by SCMFSA_2:95;
then IncAddr(i,n) = halt SCM+FSA by COMPOS_0:4;
hence thesis by SCMFSA7B:5;
end;
suppose
InsCode i = 1;
then ex da, db being Int-Location st i = da := db by SCMFSA_2:30;
hence thesis by A1,COMPOS_0:4;
end;
suppose
InsCode i = 2;
then ex da, db being Int-Location st i = AddTo(da,db) by SCMFSA_2:31;
hence thesis by A1,COMPOS_0:4;
end;
suppose
InsCode i = 3;
then ex da, db being Int-Location st i = SubFrom(da, db) by SCMFSA_2:32;
hence thesis by A1,COMPOS_0:4;
end;
suppose
InsCode i = 4;
then ex da, db being Int-Location st i = MultBy(da,db) by SCMFSA_2:33;
hence thesis by A1,COMPOS_0:4;
end;
suppose
InsCode i = 5;
then ex da, db being Int-Location st i = Divide(da, db) by SCMFSA_2:34;
hence thesis by A1,COMPOS_0:4;
end;
suppose
InsCode i = 6;
then consider loc being Nat such that
A2: i = goto loc by SCMFSA_2:35;
IncAddr(i,n) = goto (loc + n) by A2,SCMFSA_4:1;
hence thesis by SCMFSA7B:11;
end;
suppose
InsCode i = 7;
then consider
loc being Nat, da being Int-Location
such that
A3: i = da =0_goto loc by SCMFSA_2:36;
IncAddr(i,n) = da =0_goto (loc + n) by A3,SCMFSA_4:2;
hence thesis by SCMFSA7B:12;
end;
suppose
InsCode i = 8;
then consider
loc being Nat, da being Int-Location
such that
A4: i = da >0_goto loc by SCMFSA_2:37;
IncAddr(i,n) = da >0_goto (loc + n) by A4,SCMFSA_4:3;
hence thesis by SCMFSA7B:13;
end;
suppose
InsCode i = 9;
then
ex db, da being Int-Location, g being FinSeq-Location st i = da := (g,
db) by SCMFSA_2:38;
hence thesis by A1,COMPOS_0:4;
end;
suppose
InsCode i = 10;
then ex db, da being Int-Location, g being FinSeq-Location st i = (g,db):=
da by SCMFSA_2:39;
hence thesis by A1,COMPOS_0:4;
end;
suppose
InsCode i = 11;
then
ex da being Int-Location, g being FinSeq-Location st i = da :=len g by
SCMFSA_2:40;
hence thesis by A1,COMPOS_0:4;
end;
suppose
InsCode i = 12;
then
ex da being Int-Location, g being FinSeq-Location st i = g :=<0,...,0>
da by SCMFSA_2:41;
hence thesis by A1,COMPOS_0:4;
end;
end;
theorem Th2:
for P being preProgram of SCM+FSA, n being Element of NAT, a
being Int-Location st P does not destroy a
holds Reloc(P,n) does not destroy a
proof
let I be preProgram of SCM+FSA;
let n be Element of NAT;
let a be Int-Location;
A1: dom IncAddr(I,n) = dom I by COMPOS_1:def 21;
A2: dom Shift(IncAddr(I,n),n) = { m+n where m is Nat: m in dom IncAddr(I,n) }
by VALUED_1:def 12;
assume
A3: I does not destroy a;
now
let i be Instruction of SCM+FSA;
assume i in rng Reloc(I,n);
then consider x being object such that
A4: x in dom Shift(IncAddr(I,n),n) and
A5: i = Shift(IncAddr(I,n),n).x by FUNCT_1:def 3;
consider m being Nat such that
A6: x = m + n and
A7: m in dom IncAddr(I,n) by A2,A4;
A8: I. m in rng I by A1,A7,FUNCT_1:def 3;
rng I c= the InstructionsF of SCM+FSA by RELAT_1:def 19;
then reconsider ii = I. m as Instruction of SCM+FSA by A8;
A9: ii does not destroy a by A3,A8,SCMFSA7B:def 4;
i = IncAddr(I,n). m by A5,A6,A7,VALUED_1:def 12
.= IncAddr(I/.m,n) by A1,A7,COMPOS_1:def 21
.= IncAddr(ii,n) by A1,A7,PARTFUN1:def 6;
hence i does not destroy a by A9,Th1;
end;
hence thesis by SCMFSA7B:def 4;
end;
theorem Th3:
for P being good preProgram of SCM+FSA, n being Element of NAT
holds Reloc(P,n) is good
proof
let I be good preProgram of SCM+FSA;
let n be Element of NAT;
I does not destroy intloc 0 by SCMFSA7B:def 5;
then Reloc(I,n) does not destroy intloc 0 by Th2;
hence thesis by SCMFSA7B:def 5;
end;
theorem Th4:
for I,J being preProgram of SCM+FSA, a being Int-Location holds
I does not destroy a & J does not destroy a implies I +* J does not destroy a
proof
let I,J be preProgram of SCM+FSA;
let a be Int-Location;
assume
A1: I does not destroy a;
assume
A2: J does not destroy a;
now
let i be Instruction of SCM+FSA;
A3: rng (I +* J) c= rng I \/ rng J by FUNCT_4:17;
assume
A4: i in rng (I +* J);
per cases by A4,A3,XBOOLE_0:def 3;
suppose
i in rng I;
hence i does not destroy a by A1,SCMFSA7B:def 4;
end;
suppose
i in rng J;
hence i does not destroy a by A2,SCMFSA7B:def 4;
end;
end;
hence thesis by SCMFSA7B:def 4;
end;
theorem Th5:
for I,J being good preProgram of SCM+FSA holds I +* J is good
proof
let I,J be good preProgram of SCM+FSA;
I does not destroy intloc 0 & J does not destroy intloc 0 by SCMFSA7B:def 5;
then I +* J does not destroy intloc 0 by Th4;
hence thesis by SCMFSA7B:def 5;
end;
theorem Th6:
for I being preProgram of SCM+FSA, a being Int-Location
st I does not destroy a
holds Directed I does not destroy a
proof
let I be preProgram of SCM+FSA;
let a be Int-Location;
assume
A1: I does not destroy a;
now
let i be Instruction of SCM+FSA;
A2: dom Directed I = dom I by FUNCT_4:99;
assume i in rng Directed I;
then consider x being object such that
A3: x in dom Directed I and
A4: i = (Directed I).x by FUNCT_1:def 3;
per cases;
suppose
I.x <> halt SCM+FSA;
then i = I.x by A4,FUNCT_4:105;
then i in rng I by A3,A2,FUNCT_1:def 3;
hence i does not destroy a by A1,SCMFSA7B:def 4;
end;
suppose
I.x = halt SCM+FSA;
then i = goto card I by A3,A4,A2,FUNCT_4:106;
hence i does not destroy a by SCMFSA7B:11;
end;
end;
hence thesis by SCMFSA7B:def 4;
end;
registration
let I be good Program of SCM+FSA;
cluster Directed I -> good;
correctness
proof
I does not destroy intloc 0 by SCMFSA7B:def 5;
then Directed I does not destroy intloc 0 by Th6;
hence thesis by SCMFSA7B:def 5;
end;
end;
registration
let I be Program of SCM+FSA;
cluster Directed I -> initial;
correctness;
end;
registration
let I,J be good Program of SCM+FSA;
cluster I ";" J -> good;
coherence
proof
A1: Reloc(J,card I) is good by Th3;
I ";" J
= CutLastLoc stop Directed I +* Reloc(J,card stop I -' 1) by SCMFSA6A:37
.= Directed I +* Reloc(J,card I) by COMPOS_1:71;
hence thesis by A1,Th5;
end;
end;
Lm1: for l being Nat holds dom (Load goto
l) = { 0} & 0 in dom ( Load goto l) & ( Load goto
l). 0 = goto l & card ( Load goto l) = 1 & not halt SCM+FSA in
rng ( Load goto l)
proof
let l be Nat;
thus dom ( Load goto l) = { 0} by AFINSQ_1:def 4,CARD_1:49;
hence 0 in dom ( Load goto l) by TARSKI:def 1;
thus ( Load goto l). 0 = goto l;
thus card ( Load goto l) = card <% goto l %>
.= 1 by AFINSQ_1:34;
now
A1: rng ( Load goto l) = {goto l} by AFINSQ_1:33;
assume halt SCM+FSA in rng Load goto l;
hence contradiction by A1,TARSKI:def 1;
end;
hence thesis;
end;
definition
let l be Nat;
func Goto l -> Program of SCM+FSA equals
Load goto l;
coherence;
end;
registration
let l be Element of NAT;
cluster Goto l -> halt-free good;
coherence
proof
set I = Load goto l;
not halt SCM+FSA in rng I by Lm1;
hence Goto l is halt-free;
now
let x be Instruction of SCM+FSA;
A1: rng Load goto l = {goto l} by AFINSQ_1:33;
assume x in rng Load goto l;
then x = goto l by A1,TARSKI:def 1;
hence x does not destroy intloc 0 by SCMFSA7B:11;
end;
then I does not destroy intloc 0 by SCMFSA7B:def 4;
hence thesis by SCMFSA7B:def 5;
end;
end;
registration
cluster halt-free good for Program of SCM+FSA;
existence
proof
take Goto 0;
thus thesis;
end;
end;
definition
let s be State of SCM+FSA;
let P be Instruction-Sequence of SCM+FSA;
let I be initial Program of SCM+FSA;
pred I is_pseudo-closed_on s,P means
ex k being Nat st
IC Comput(P +* I, Initialize s,k) = card I &
for n being Nat st n < k
holds IC Comput(P +* I,Initialize s,n) in dom I;
end;
definition
::$CD
let s be State of SCM+FSA,
P be Instruction-Sequence of SCM+FSA,
I be initial Program of SCM+FSA such that
A1: I is_pseudo-closed_on s,P;
func pseudo-LifeSpan(s,P,I) -> Nat means
:Def3:
IC Comput(P +* I,Initialize s,it) = card I &
for n being Nat
st not IC Comput(P +* I, Initialize s,n) in dom I
holds it <= n;
existence
proof
consider k being Nat such that
A2: IC Comput(P+*I, Initialize s,k)
= card I &
for n being Nat st n < k holds
IC Comput(P+*I, Initialize s,n) in dom I by A1;
take k;
thus thesis by A2;
end;
uniqueness
proof
reconsider II = I as initial preProgram of SCM+FSA;
let k1,k2 be Nat such that
A3: IC Comput(P+*I, Initialize s,k1)
= card I and
A4: ( for n being Nat st
not IC Comput(P+*I,Initialize s,n) in dom I holds
k1 <= n)&
IC Comput(P+*I, Initialize s,k2)
= card I and
A5: for n being Nat st
not IC Comput(P+*I,Initialize s,n) in dom I holds
k2 <= n;
A6: now
assume k2 < k1;
then card II in dom II by A4;
hence contradiction;
end;
now
assume k1 < k2;
then card II in dom II by A3,A5;
hence contradiction;
end;
hence thesis by A6,XXREAL_0:1;
end;
end;
theorem Th7:
for I,J being Program of SCM+FSA, x being set holds x in dom I
implies (I ";" J).x = (Directed I).x
proof
let I,J be Program of SCM+FSA;
let x be set;
assume x in dom I;
then
A1: x in dom Directed I by FUNCT_4:99;
Directed I c= I ";" J by SCMFSA6A:16;
hence thesis by A1,GRFUNC_1:2;
end;
theorem
for l being Nat holds card Goto l = 1 by Lm1;
theorem
for P being preProgram of SCM+FSA, x being set st x in dom P holds (P.
x = halt SCM+FSA implies (Directed P).x = goto card P) & (P.x <> halt
SCM+FSA implies (Directed P).x = P.x) by FUNCT_4:105,106;
theorem Th10:
for s being State of SCM+FSA,
P being Instruction-Sequence of SCM+FSA,
I being initial Program of
SCM+FSA st I is_pseudo-closed_on s,P
holds for n being Nat st n < pseudo-LifeSpan(s,P,I)
holds IC ( Comput(P+* I,
Initialize s,n)) in dom I &
CurInstr(P+*I,Comput(P+*I,
Initialize s,n)) <>
halt SCM+FSA
proof
let s be State of SCM+FSA;
let P be Instruction-Sequence of SCM+FSA;
let I be initial Program of SCM+FSA;
set k = pseudo-LifeSpan(s,P,I);
assume
A1: I is_pseudo-closed_on s,P;
then
A2: IC Comput(P+*I, Initialize s,k) = card I by Def3;
hereby
let n be Nat;
assume
A3: n < k;
hence
A4: IC Comput(P+*I, Initialize s,n) in dom I by A1,Def3;
assume
CurInstr (P+*I,Comput(P+*I, Initialize s,n)) = halt SCM+FSA;
then
IC Comput(P+*I, Initialize s,k) = IC Comput(P+*I, Initialize s,n)
by A3,EXTPRO_1:5;
hence contradiction by A2,A4;
end;
end;
theorem Th11:
for s being State of SCM+FSA,
P being Instruction-Sequence of SCM+FSA,
I,J being Program of SCM+FSA st I
is_pseudo-closed_on s,P for k being Nat st
k <= pseudo-LifeSpan(s,P,I)
holds Comput(P+*I, Initialize s,k)
= Comput(P+*(I ";" J), Initialize s,k)
proof
let s be State of SCM+FSA;
let P be Instruction-Sequence of SCM+FSA;
let I,J be Program of SCM+FSA;
set s1 = Initialize s;
set s2 = Initialize s;
defpred P[Nat] means $1 <= pseudo-LifeSpan(s,P,I) implies
Comput(P+*I,s1,$1) = Comput(P+*(I ";" J),s2,$1);
A1: dom(P+*I) = NAT by PARTFUN1:def 2;
A2: dom(P+*(I ";" J)) = NAT by PARTFUN1:def 2;
assume
A3: I is_pseudo-closed_on s,P;
A4: now
let k be Nat;
assume
A5: P[k];
thus P[k+1]
proof
A6: Comput(P+*(I ";" J),s2,k+1) = Following(P+*(I ";" J),
Comput(P+*(I ";" J),s2,k)) by EXTPRO_1:3
.= Exec(CurInstr(P+*(I ";" J),Comput(P+*(I ";" J),s2,k)),
Comput(P+*(I ";" J),s2,k));
A7: Comput(P+*I,s1,k+1) = Following(P+*I,
Comput(P+*I,s1,k)) by EXTPRO_1:3
.= Exec(CurInstr(P+*I,Comput(P+*I,s1,k)),
Comput(P+*I,s1,k));
A8: dom I c= dom (I ";" J) by SCMFSA6A:17;
A9: k + 0 < k + 1 by XREAL_1:6;
assume
A10: k + 1 <= pseudo-LifeSpan(s,P,I);
then
A11: k < pseudo-LifeSpan(s,P,I) by A9,XXREAL_0:2;
then
A12: IC Comput(P+*I,s1,k) in dom I by A3,Th10;
A13: I c= P+*I by FUNCT_4:25;
A14: I ";" J c= P+*(I ";" J) by FUNCT_4:25;
A15: CurInstr(P+*I,Comput(P+*I,s1,k))
= (P+*I).IC Comput(P+*I,s1,k) by A1,PARTFUN1:def 6
.= I.IC Comput(P+*I,s1,k) by A12,A13,GRFUNC_1:2;
then I.IC Comput(P+*I,s1,k) <> halt SCM+FSA by A3,A11,Th10;
then
CurInstr(P+*I,Comput(P+*I,s1,k))
= (I ";" J).IC Comput(P+*I,s1,k) by A12,A15,SCMFSA6A:15
.= (P+*(I ";" J)).IC Comput(P+*I,s1,k)
by A12,A8,A14,GRFUNC_1:2
.= (P+*(I ";" J)).IC Comput(P+*(I ";" J),s2,k)
by A5,A10,A9,XXREAL_0:2
.= CurInstr(P+*(I ";" J),Comput(P+*(I ";" J),s2,k))
by A2,PARTFUN1:def 6;
hence thesis by A5,A10,A9,A7,A6,XXREAL_0:2;
end;
end;
A16: P[0];
thus for k being Nat holds P[k] from NAT_1:sch 2(A16,A4);
end;
::$CT 2
theorem Th12:
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA,
I being really-closed Program of SCM+FSA st I is_halting_on s,P
for k being Nat st k <= LifeSpan(P+*I,Initialize s)
holds Comput(P+*I, (Initialize s),k)
= Comput(P+*Directed I, (Initialize s),k) &
CurInstr(P+*Directed I,
Comput(P+*Directed I, (Initialize s),k))
<> halt SCM+FSA
proof
let s be State of SCM+FSA;
let P be Instruction-Sequence of SCM+FSA;
let I be really-closed Program of SCM+FSA;
assume that
A1: I is_halting_on s,P;
A2: dom(P+*Directed I) = NAT by PARTFUN1:def 2;
A3: dom(P+*I) = NAT by PARTFUN1:def 2;
set s2 = Initialize s;
set s1 = Initialize s;
defpred P[Nat] means $1 <= LifeSpan(P+*I,s1)
implies Comput(P+*I,s1,$1) = Comput(P+*Directed I,s2,$1) &
CurInstr(P+*Directed I,Comput(P+*Directed I,s2,$1)) <> halt SCM+FSA;
IC s1 = 0 by MEMSTR_0:47;
then
A4: IC s1 in dom I by AFINSQ_1:65;
A5: I c= P+*I by FUNCT_4:25;
A6: now
let k be Element of NAT;
dom Directed I = dom I by FUNCT_4:99;
then
A7: IC Comput(P+*I,s1,k) in dom Directed I by AMISTD_1:21,A4,A5;
A8: (P+*Directed I)/.IC Comput(P+*Directed I,s2,k)
= (P+*Directed I).IC Comput(P+*Directed I,s2,k) by A2,PARTFUN1:def 6;
A9: Directed I c= P+*Directed I by FUNCT_4:25;
assume
Comput(P+*I,s1,k) = Comput(P+*Directed I,s2,k);
then CurInstr(P+*Directed I,Comput(P+*Directed I,s2,k))
= (P+*Directed I).IC Comput(P+*I,s1,k) by A8
.= (Directed I).IC Comput(P+*I,s1,k) by A7,A9,GRFUNC_1:2;
then
A10: CurInstr(P+*Directed I,Comput(P+*Directed I,s2,k)) in rng Directed I
by A7,FUNCT_1:def 3;
assume
CurInstr(P+*Directed I,Comput(P+*Directed I,s2,k)) = halt SCM+FSA;
hence contradiction by A10,SCMFSA6A:1;
end;
now
A11: P+*I halts_on s1 by A1,SCMFSA7B:def 7;
A12: dom I c= dom Directed I by FUNCT_4:99;
let k be Nat;
assume
A13: k <= LifeSpan(P+*I,s1) implies
Comput(P+*I,s1,k) = Comput(P+*Directed I,s2,k);
A14: Comput(P+*Directed I,s2,k+1) = Following(P+*Directed I,
Comput(P+*Directed I,s2,k)) by EXTPRO_1:3
.= Exec(CurInstr(P+*Directed I,Comput(P+*Directed I,s2,k)),
Comput(P+*Directed I,s2,k));
A15: IC Comput(P+*I,s1,k) in dom I by AMISTD_1:21,A4,A5;
A16: I c=P+*I by FUNCT_4:25;
A17: CurInstr(P+*I,Comput(P+*I,s1,k))
= (P+*I).IC Comput(P+*I,s1,k) by A3,PARTFUN1:def 6
.= I.IC Comput(P+*I,s1,k) by A15,A16,GRFUNC_1:2;
A18: k + 0 < k + 1 by XREAL_1:6;
A19: (P+*Directed I)/.IC Comput(P+*Directed I,s2,k)
= (P+*Directed I).IC Comput(P+*Directed I,s2,k) by A2,PARTFUN1:def 6;
A20: Directed I c= P+*Directed I by FUNCT_4:25;
assume
A21: k + 1 <= LifeSpan(P+*I,s1);
then k < LifeSpan(P+*I,s1) by A18,XXREAL_0:2;
then I.IC Comput(P+*I,s1,k) <> halt SCM+FSA by A17,A11,EXTPRO_1:def 15;
then
A22: CurInstr(P+*I,Comput(P+*I,s1,k))
= (Directed I).IC Comput(P+*I,s1,k) by A17,FUNCT_4:105
.= (P+*Directed I).IC Comput(P+*I,s1,k) by A15,A12,A20,GRFUNC_1:2
.= CurInstr(P+*Directed I,Comput(P+*Directed I,s2,k))
by A13,A21,A18,A19,XXREAL_0:2;
Comput(P+*I,s1,k+1) = Following(P+*I,Comput(P+*I,s1,k)) by EXTPRO_1:3
.= Exec(CurInstr(P+*I,Comput(P+*I,s1,k)),
Comput(P+*I,s1,k));
hence Comput(P+*I,s1,k+1) = Comput(P+*Directed I,s2,k+1)
by A13,A21,A18,A22,A14,XXREAL_0:2;
hence CurInstr(P+*Directed I,Comput(P+*Directed I,s2,k+1)) <>
halt SCM+FSA
by A6;
end;
then
A23: for k being Nat st P[k] holds P[k + 1];
now
assume 0 <= LifeSpan(P+*I,s1);
thus Comput(P+*I,s1,0) = Comput(P+*Directed I,s2,0);
hence CurInstr(P+*Directed I,Comput(P+*Directed I,s2,0)) <>
halt SCM+FSA by A6;
end;
then
A24: P[0];
thus for k being Nat holds P[k] from NAT_1:sch 2(A24,A23);
end;
theorem Th13:
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA,
I being really-closed Program of SCM+FSA st I is_halting_on s,P
holds
IC Comput(P+*Directed I, Initialize s,
(LifeSpan(P+*I,Initialize s) + 1)) = card I &
DataPart Comput(P+*I, Initialize s,
(LifeSpan(P+*I,Initialize s))) =
DataPart Comput(P+*Directed I, Initialize s,
(LifeSpan(P+*I,Initialize s) + 1))
proof
let s be State of SCM+FSA;
let P be Instruction-Sequence of SCM+FSA;
let I be really-closed Program of SCM+FSA;
set s1 = Initialize s;
set s2 = Initialize s;
set m1 = LifeSpan(P+*I,s1);
A1: dom(P+*I) = NAT by PARTFUN1:def 2;
A2: dom(P+*Directed I) = NAT by PARTFUN1:def 2;
assume that
A3: I is_halting_on s,P;
A4: P+*I halts_on s1 by A3,SCMFSA7B:def 7;
:: wzmocnienie is_halting_on
set l1 = IC Comput(P+*I, s1,m1);
IC s1 = 0 by MEMSTR_0:47;
then
A5: IC s1 in dom I by AFINSQ_1:65;
A6: I c= P+*I by FUNCT_4:25;
A7: l1 in dom I by A5,A6,AMISTD_1:21;
A8: Comput(P+*I, (Initialize s),m1)
= Comput(P+*Directed I, (Initialize s),m1) by A3,Th12;
then IC Comput(P+*Directed I, s2,m1) in dom I by A7;
then
A9: IC Comput(P+*Directed I, s2,m1) in dom Directed I by FUNCT_4:99;
I c= P+*I by FUNCT_4:25;
then
A10: I.l1 = (P+*I).IC Comput(P+*I,s1,m1) by A7,GRFUNC_1:2
.= CurInstr(P+*I,Comput(P+*I,s1,m1)) by A1,PARTFUN1:def 6
.= halt SCM+FSA by A4,EXTPRO_1:def 15;
l1 = IC Comput(P+*Directed I, s2,m1) by A8;
then
A11: (P+*Directed I).l1 = (Directed I).l1 by A9,FUNCT_4:13
.= goto card I by A7,A10,FUNCT_4:106;
A12: CurInstr(P+*Directed I,Comput(P+*Directed I,s2,m1))
= (P+*Directed I).IC Comput(P+*Directed I,s2,m1) by A2,PARTFUN1:def 6
.= goto card I by A11,A8;
A13: Comput(P+*Directed I, s2,m1 + 1) = Following(P+*Directed I,
Comput(P+*Directed I,s2,m1)) by EXTPRO_1:3
.= Exec(goto card I, Comput(P+*Directed I, s2,m1)) by A12;
hence IC Comput(P+*Directed I, s2,m1 + 1) = card I by SCMFSA_2:69;
A14: ( for a being Int-Location holds Comput(P+*Directed I, s2,m1 + 1).a =
Comput(P+*Directed I, s2, m1).a)& for f being FinSeq-Location holds Comput(
P+*Directed I, s2,m1
+ 1).f = Comput(P+*Directed I, s2,m1).f by A13,SCMFSA_2:69;
DataPart Comput(P+*I, s1,m1) = DataPart Comput(P+*Directed I,
s2,m1) by A8;
hence thesis by A14,SCMFSA_M:2;
end;
Lm2: for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA,
I being really-closed Program of SCM+FSA st I is_halting_on s,P
holds Directed I is_pseudo-closed_on s,P &
pseudo-LifeSpan(s,P,Directed I) = LifeSpan(P+*I,Initialize s) + 1
proof
let s be State of SCM+FSA;
let P be Instruction-Sequence of SCM+FSA;
let I be really-closed Program of SCM+FSA;
set s1 = Initialize s;
set s2 = Initialize s;
set m1 = LifeSpan(P+*I,s1);
IC s2 = 0 by MEMSTR_0:47;
then
A1: IC s2 in dom I by AFINSQ_1:65;
A2: I c= P+*I by FUNCT_4:25;
assume that
A3: I is_halting_on s,P;
A4: dom I = dom Directed I by FUNCT_4:99;
A5: now
let n be Nat;
assume n < m1 + 1;
then n <= m1 by NAT_1:13;
then Comput(P+*I, s1,n) = Comput(P+*Directed I, s2,n) by A3,Th12;
then IC Comput(P+*I, s1,n) = IC Comput(P+*Directed I, s2,n);
hence IC Comput(P+*Directed I, s2,n) in dom Directed I
by A4,AMISTD_1:21,A1,A2;
end;
card I = card Directed I by SCMFSA6A:36;
then
A6: IC Comput(P+*Directed I, s2,m1 + 1) = card Directed I by A3,Th13;
hence
A7: Directed I is_pseudo-closed_on s,P by A5;
for n be Nat st
not IC Comput(P+*Directed I, s2,n) in dom Directed I
holds m1 + 1 <= n by A5;
hence thesis by A6,A7,Def3;
end;
theorem
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA,
I being really-closed Program of SCM+FSA st I is_halting_on s,P
holds Directed I is_pseudo-closed_on s,P by Lm2;
theorem
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA,
I being really-closed Program of SCM+FSA st I is_halting_on s,P
holds pseudo-LifeSpan(s,P,Directed I) =
LifeSpan(P +* I,Initialize s) + 1 by Lm2;
theorem
for I,J being Program of SCM+FSA holds Directed I ";" J = I ";" J;
theorem Th17:
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA,
I being really-closed Program of SCM+FSA,
J being Program of SCM+FSA st I is_halting_on s,P holds
(for k being Nat st k <= LifeSpan(P+*I,Initialize s)
holds IC Comput(P+*Directed I, Initialize s,k)
= IC Comput(P+*(I ";" J), Initialize s,k) &
CurInstr(P+*Directed I,
Comput(P+*Directed I, Initialize s,k))
= CurInstr(P+*(I ";" J),
Comput(P+*(I ";" J), Initialize s,k))) &
DataPart Comput(P+*Directed I, Initialize s,
(LifeSpan(P+*I,Initialize s) + 1)) =
DataPart Comput(P+*(I ";" J), Initialize s,
(LifeSpan(P+*I,Initialize s) + 1)) &
IC Comput(P+*Directed I, Initialize s,
(LifeSpan(P+*I,Initialize s) + 1))
= IC Comput(P+*(I ";" J), Initialize s,
(LifeSpan(P+*I,Initialize s) + 1))
proof
let s be State of SCM+FSA;
let P be Instruction-Sequence of SCM+FSA;
let I be really-closed Program of SCM+FSA;
let J be Program of SCM+FSA;
A1: dom(P+*Directed I) = NAT by PARTFUN1:def 2;
A2: dom(P+*(I ";" J)) = NAT by PARTFUN1:def 2;
set s2 = Initialize s;
A3: Directed I ";" J = I ";" J;
set s1 = Initialize s;
assume
A4: I is_halting_on s,P;
then
A5: LifeSpan(P+*I,s1) + 1 = pseudo-LifeSpan(s,P,Directed I)
by Lm2;
A6: Directed I is_pseudo-closed_on s,P by A4,Lm2;
hereby
let k be Nat;
assume k <= LifeSpan(P+*I,s1);
then
A7: k < pseudo-LifeSpan(s,P,Directed I) by A5,NAT_1:13;
then
A8: IC Comput(P+*Directed I, Initialize s,k)
in dom Directed I by A6,Def3;
( Comput(P+*Directed I,Initialize s,k))
= Comput(P+*(I ";" J), s2,k) by A3,A4,Lm2,A7,Th11;
hence
A9: IC ( Comput(P+*Directed I,Initialize s,k))
= IC Comput(P+*(I ";" J), s2,k);
A10: Directed I c= I ";" J by SCMFSA6A:16;
then
A11: dom Directed I c= dom (I ";" J) by GRFUNC_1:2;
thus CurInstr(P +* Directed I, Comput(P+*Directed I,
Initialize s,k))
= (P+*Directed I). IC Comput(P+*Directed I,
Initialize s,k) by A1,PARTFUN1:def 6
.= (Directed I). IC Comput(P+*Directed I,
Initialize s,k) by A8,FUNCT_4:13
.= (I ";" J).IC Comput(P+*Directed I,
Initialize s,k) by A8,A10,GRFUNC_1:2
.= (P+*(I ";" J)).IC Comput(P+*(I ";" J), s2,k)
by A9,A11,A8,FUNCT_4:13
.= CurInstr(P+*(I ";" J),Comput(P+*(I ";" J),s2,k))
by A2,PARTFUN1:def 6;
end;
Comput(P+*Directed I, Initialize s,LifeSpan(P+*I,s1) + 1 )
= Comput(P+*(I ";" J), s2,LifeSpan(P+*I,s1) + 1) by A4,A3,A5,Lm2,Th11;
hence thesis;
end;
theorem Th18:
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA,
I being really-closed Program of SCM+FSA,
J being Program of SCM+FSA st I is_halting_on Initialized s,P
holds (for k being Nat
st k <= LifeSpan(P+*I,s +* Initialize((intloc 0).-->1))
holds IC Comput(P+*Directed I, s +* Initialize((intloc 0).-->1),k)
= IC Comput(P+*(I ";" J),s +* Initialize((intloc 0).-->1),k) &
CurInstr(P+*Directed I,Comput(P+*Directed I,
s +* Initialize((intloc 0).-->1),k))
= CurInstr(P+*(I ";" J),
Comput(P+*(I ";" J),
s +* Initialize((intloc 0).-->1),k)))
&
DataPart Comput(P+*Directed I,
s +* Initialize((intloc 0).-->1),
LifeSpan(P+*I,s +* Initialize((intloc 0).-->1)) + 1)
= DataPart Comput(P+*(I ";" J),
s +* Initialize((intloc 0).-->1),
LifeSpan(P+*I,s +* Initialize((intloc 0).-->1)) + 1)
&
IC Comput(P+*Directed I,
s +* Initialize((intloc 0).-->1),
LifeSpan(P+*I,s +* Initialize((intloc 0).-->1)) + 1)
= IC Comput(P+*(I ";" J),
s +* Initialize((intloc 0).-->1),
LifeSpan(P+*I,s +* Initialize((intloc 0).-->1)) + 1)
proof
let s be State of SCM+FSA;
let P be Instruction-Sequence of SCM+FSA;
let I be really-closed Program of SCM+FSA;
let J be Program of SCM+FSA;
A1: dom(P +* (I ";" J)) = NAT by PARTFUN1:def 2;
A2: dom(P +* Directed I) = NAT by PARTFUN1:def 2;
set s2 =s +* Initialize((intloc 0).-->1);
A3: s +* Initialize((intloc 0).-->1)
= Initialize Initialized s &
s2 = Initialize Initialized s by MEMSTR_0:44;
A4: Directed I ";" J = I ";" J;
set s1 = s +* Initialize((intloc 0).-->1);
assume
A5: I is_halting_on Initialized s,P;
s1 = Initialize Initialized s by MEMSTR_0:44;
then
A6: LifeSpan(P+*I,s1) + 1 = pseudo-LifeSpan(
Initialized s,P,Directed I) by A5,Lm2;
A7: Directed I is_pseudo-closed_on Initialized s,P by A5,Lm2;
hereby
let k be Nat;
assume k <= LifeSpan(P+*I,s1);
then
A8: k < pseudo-LifeSpan(Initialized s,P,Directed I) by A6,NAT_1:13;
then
Comput(P+*Directed I, s +* Initialize((intloc 0).-->1),k) =
Comput(P+*(I ";" J), s2,k) by A3,A4,A5,Lm2,Th11;
hence
A9: IC Comput(P+*Directed I, s +* Initialize((intloc 0).-->1),k) = IC
Comput(P+*(I ";" J), s2,k);
s +* Initialize((intloc 0).-->1)
= Initialize Initialized s by MEMSTR_0:44;
then
A10: IC Comput(P+*Directed I, s +* Initialize((intloc 0).-->1),k)
in dom Directed I by A7,A8,Def3;
A11: Directed I c= I ";" J by SCMFSA6A:16;
then
A12: dom Directed I c= dom (I ";" J) by GRFUNC_1:2;
thus CurInstr(P+*Directed I,
Comput(P+*Directed I, (s +* Initialize((intloc 0).-->1)),k))
= (P+*Directed I). IC Comput(P+*Directed I,
(s +* Initialize((intloc 0).-->1)),k) by A2,PARTFUN1:def 6
.= (Directed I).IC Comput(P+*Directed I,
s +* Initialize((intloc 0).-->1),k) by A10,FUNCT_4:13
.= (I ";" J).IC Comput(P+*Directed I,
s +* Initialize((intloc 0).-->1),k) by A10,A11,GRFUNC_1:2
.= (P+*(I ";" J)).IC Comput(P+*(I ";" J), s2,k) by A9,A12,A10,FUNCT_4:13
.= CurInstr(P+*(I ";" J),Comput(P+*(I ";" J),s2,k))
by A1,PARTFUN1:def 6;
end;
Comput(P+*Directed I, s +* Initialize((intloc 0).-->1),
LifeSpan(P+*I,s1) + 1)
= Comput(P+*(I ";" J), s2,LifeSpan(P+*I,s1) + 1)
by A5,A3,A4,A6,Lm2,Th11;
hence thesis;
end;
theorem Th19:
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA,
I being really-closed Program of SCM+FSA st I is_halting_on Initialized s,P
holds for k being Nat
st k <= LifeSpan(P+*I,s +* Initialize((intloc 0).-->1)) holds
Comput(P+*I,s +* Initialize((intloc 0).-->1),k)
= Comput(P+*Directed I, s +* Initialize((intloc 0).-->1),k)
&
CurInstr(P+*Directed I,
Comput(P+*Directed I,s +* Initialize((intloc 0).-->1),k))
<> halt SCM+FSA
proof
let s be State of SCM+FSA;
let P be Instruction-Sequence of SCM+FSA;
let I be really-closed Program of SCM+FSA;
set s1 = s +* Initialize((intloc 0).-->1);
set s2 = s +* Initialize((intloc 0).-->1);
A1: dom(P+*Directed I) = NAT by PARTFUN1:def 2;
A2: dom(P+*I) = NAT by PARTFUN1:def 2;
A3: Directed I c= P+*Directed I by FUNCT_4:25;
defpred P[Nat] means $1 <= LifeSpan(P+*I,s1) implies
Comput(P+*I,s1,$1) = Comput(P+*Directed I,s2,$1) &
CurInstr(P+*Directed I,Comput(P+*Directed I,s2,$1)) <> halt SCM+FSA;
A4: s1 = Initialize Initialized s by MEMSTR_0:44;
IC s1 = 0 by A4,MEMSTR_0:47;
then
A5: IC s1 in dom I by AFINSQ_1:65;
A6: I c= P+*I by FUNCT_4:25;
A7: now
let k be Nat;
dom Directed I = dom I by FUNCT_4:99;
then
A8: IC Comput(P+*I,s1,k) in dom Directed I by A5,A6,AMISTD_1:21;
A9: (P+*Directed I)/.IC Comput(P+*Directed I,s2,k)
= (P+*Directed I).IC Comput(P+*Directed I,s2,k) by A1,PARTFUN1:def 6;
assume
Comput(P+*I,s1,k) = Comput(P+*Directed I,s2,k);
then CurInstr(P+*Directed I,Comput(P+*Directed I,s2,k))
= (P+*Directed I).IC Comput(P+*I,s1,k) by A9
.= (Directed I).IC Comput(P+*I,s1,k) by A8,A3,GRFUNC_1:2;
then
A10: CurInstr(P+*Directed I,Comput(P+*Directed I,s2
,k)) in rng Directed I
by A8,FUNCT_1:def 3;
assume
CurInstr(P+*Directed I,Comput(P+*Directed I,s2
,k)) = halt SCM+FSA;
hence contradiction by A10,SCMFSA6A:1;
end;
assume
A11: I is_halting_on Initialized s,P;
now
A12: P+*I halts_on s1 by A11,A4,SCMFSA7B:def 7;
A13: dom I c= dom Directed I by FUNCT_4:99;
let k be Nat;
assume
A14: k <= LifeSpan(P+*I,s1) implies
Comput(P+*I,s1,k) = Comput(P+*Directed I,s2,k);
A15: Comput(P+*Directed I,s2,k+1) =
Following(P+*Directed I,Comput(P+*Directed I,s2,k)
)
by EXTPRO_1:3
.= Exec(CurInstr(P+*Directed I,Comput(
P+*Directed I,s2,k)),
Comput(P+*Directed I,s2,k));
A16: IC Comput(P+*I,s1,k) in dom I by A5,A6,AMISTD_1:21;
A17: I c= P+* I by FUNCT_4:25;
A18: CurInstr(P+*I,Comput(P+*I,s1,k))
= (P+*I).IC Comput(P+*I,s1,k) by A2,PARTFUN1:def 6
.= I.IC Comput(P+*I,s1,k) by A16,A17,GRFUNC_1:2;
A19: k + 0 < k + 1 by XREAL_1:6;
assume
A20: k + 1 <= LifeSpan(P+*I,s1);
then k < LifeSpan(P+*I,s1) by A19,XXREAL_0:2;
then I.IC Comput(P+*I,s1,k) <> halt SCM+FSA by A18,A12,EXTPRO_1:def 15;
then
A21: CurInstr(P+*I,Comput(P+*I,
s1,k))
= (Directed I).IC Comput(P+*I,s1,k) by A18,FUNCT_4:105
.= (P+*Directed I).IC Comput(P+*I,s1,k) by A3,A16,A13,GRFUNC_1:2
.= (P+*Directed I).IC Comput(P+*Directed I,s2,k)
by A14,A20,A19,XXREAL_0:2
.= CurInstr(P+*Directed I,Comput(P+*Directed I,s2,k))
by A1,PARTFUN1:def 6;
Comput(P+*I,s1,k+1) =
Following(P+*I,Comput(P+*I,s1,k)
)
by EXTPRO_1:3
.= Exec(CurInstr(P+*I,Comput(
P+*I,s1,k)),
Comput(P+*I,s1,k));
hence Comput(P+*I,s1,k+1) = Comput(P+*Directed I,s2,k+1)
by A14,A20,A19,A21,A15,XXREAL_0:2;
hence CurInstr(P+*Directed I,Comput(P+*Directed I,s2,k+1)) <>
halt SCM+FSA
by A7;
end;
then
A22: for k being Nat st P[k] holds P[k + 1];
now
assume 0 <= LifeSpan(P+*I,s1);
thus Comput(P+*I,s1,0) = Comput(P+*Directed I,s2,0);
hence CurInstr(P+*Directed I,Comput(P+*Directed I,s2,0))
<> halt SCM+FSA by A7;
end;
then
A23: P[0];
thus for k being Nat holds P[k] from NAT_1:sch 2(A23,A22);
end;
theorem Th20:
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA,
I being really-closed Program of SCM+FSA st I is_halting_on Initialized s,P
holds IC Comput(P+*Directed I,
(s +* Initialize((intloc 0).-->1)),
(LifeSpan(P+*I,s +* Initialize((intloc 0).-->1)) + 1)) =
card I & DataPart Comput(P+*I, s +* Initialize((intloc 0).-->1),
LifeSpan(P+*I,s +* Initialize((intloc 0).-->1)))
= DataPart Comput(P+*Directed I, s +* Initialize((intloc 0).-->1),
(LifeSpan(P+*I,s +* Initialize((intloc 0).-->1)) + 1))
proof
let s be State of SCM+FSA;
let P be Instruction-Sequence of SCM+FSA;
let I be really-closed Program of SCM+FSA;
set s1 = s +* Initialize((intloc 0).-->1);
set s2 = s +* Initialize((intloc 0).-->1);
set m1 = LifeSpan(P+*I,s1);
A1: dom(P+*I) = NAT by PARTFUN1:def 2;
A2: dom(P+*Directed I) = NAT by PARTFUN1:def 2;
set l1 = IC Comput(P+*I, s1,m1);
A3: I c= P+*I by FUNCT_4:25;
A4: s1 = Initialize Initialized s by MEMSTR_0:44;
then IC s1 = 0 by MEMSTR_0:47;
then IC s1 in dom I by AFINSQ_1:65;
then
A5: l1 in dom I by A3,AMISTD_1:21;
assume
A6: I is_halting_on Initialized s,P;
then
A7: Comput(P+*I, s1,m1) = Comput(P+*Directed I, s2,m1) by Th19;
then IC Comput(P+*Directed I, s2,m1) in dom I by A5;
then
A8: IC Comput(P+*Directed I, s2,m1) in dom Directed I by FUNCT_4:99;
A9: P+*I halts_on s1 by A6,A4,SCMFSA7B:def 7;
A10: I c= P+*I by FUNCT_4:25;
A11: I.l1 = (P+*I).l1 by A5,A10,GRFUNC_1:2
.= CurInstr(P+*I,Comput(P+*I,s1,m1))
by A1,PARTFUN1:def 6
.= halt SCM+FSA by A9,EXTPRO_1:def 15;
l1 = IC Comput(P+*Directed I, s2,m1) by A7;
then
A12: (P+*Directed I).l1 = (Directed I).l1 by A8,FUNCT_4:13
.= goto card I by A5,A11,FUNCT_4:106;
A13: (P+*Directed I)/.IC Comput(P+*Directed I,s2,
m1)
= (P+*Directed I).IC Comput(P+*Directed I,s2,m1) by A2,PARTFUN1:def 6;
A14: Comput(P+*Directed I, s2,m1 + 1) =
Following(P+*Directed I,Comput(P+*Directed I,s2,m1)) by EXTPRO_1:3
.= Exec(goto card I, Comput(P+*Directed I, s2,m1))
by A12,A13,A7;
hence IC Comput(P+*Directed I, s2,m1 + 1) = card I by SCMFSA_2:69;
A15: ( for a being Int-Location holds Comput(P+*Directed I, s2,m1 + 1).a =
Comput(P+*Directed I, s2, m1).a)& for f being FinSeq-Location holds Comput(
P+*Directed I, s2,m1
+ 1).f = Comput(P+*Directed I, s2,m1).f by A14,SCMFSA_2:69;
DataPart Comput(P+*I, s1,m1) = DataPart Comput(P+*Directed I,
s2,m1) by A7;
hence thesis by A15,SCMFSA_M:2;
end;
Lm3: for I being really-closed Program of SCM+FSA
for P being Instruction-Sequence of SCM+FSA,s being State of SCM+FSA
st I is_halting_on s,P
holds IC Comput(P +* (I ";" Stop SCM+FSA),
Initialize s,
LifeSpan(P+*I,Initialize s) + 1) = card I &
DataPart Comput(P+*I, Initialize s,
LifeSpan(P+*I,Initialize s)) =
DataPart Comput(P +* (I ";" Stop SCM+FSA),
Initialize s,
LifeSpan(P+*I,Initialize s) + 1) &
P +* (I ";" Stop SCM+FSA) halts_on
Initialize s &
LifeSpan(P +* (I ";" Stop SCM+FSA),
Initialize s) =
LifeSpan(P+*I,Initialize s) + 1 &
I ";" Stop SCM+FSA is_halting_on s,P
proof
let I be really-closed Program of SCM+FSA;
let P be Instruction-Sequence of SCM+FSA;
let s be State of SCM+FSA;
card Stop SCM+FSA = 1 by COMPOS_1:4;
then card (I ";" Stop SCM+FSA) = card I + 1 by SCMFSA6A:21;
then card I < card (I ";" Stop SCM+FSA) by NAT_1:13;
then
A1: card I in dom (I ";" Stop SCM+FSA) by AFINSQ_1:66;
A2: 0 in dom Stop SCM+FSA by COMPOS_1:3;
(0 + card I) in {m + card I where m is Nat: m in dom Stop SCM+FSA}
by A2;
then
A3: (0 + card I) in dom Reloc(Stop SCM+FSA,card I ) by COMPOS_1:33;
set s2 = Initialize s;
set s1 = Initialize s;
A4: 0 in dom Stop SCM+FSA by COMPOS_1:3;
A5: (Stop SCM+FSA).0 = halt SCM+FSA;
assume
A6: I is_halting_on s,P;
then
A7: IC Comput(P+*Directed I, Initialize s,
(LifeSpan(P+*I,s1)
+ 1)) = IC Comput(P +* (I ";" Stop SCM+FSA), s2,LifeSpan(P+*I,s1) + 1) by
Th17;
A8: (P +* (I ";" Stop SCM+FSA)). card I = (I ";" Stop SCM+FSA).card I
by A1,FUNCT_4:13
.= Reloc(Stop SCM+FSA,card I). (0 + card I) by A3,SCMFSA6A:40
.= IncAddr(halt SCM+FSA,card I) by A5,A4,COMPOS_1:35
.= halt SCM+FSA by COMPOS_0:4;
DataPart Comput(P+*Directed I, Initialize s,
LifeSpan(P+*I,
s1) + 1) = DataPart Comput(P +* (I ";" Stop SCM+FSA), s2,LifeSpan(P+*I,s1)
+1) by A6,Th17;
hence IC Comput(P +* (I ";" Stop SCM+FSA),s2,LifeSpan(P+*I,s1) + 1)
= card I &
DataPart Comput(P+*I, s1,LifeSpan(P+*I,s1))
= DataPart Comput(P +* (I ";" Stop SCM+FSA), s2,LifeSpan(P+*I,s1) + 1)
by A6,A7,Th13;
dom(P +* (I ";" Stop SCM+FSA)) = NAT by PARTFUN1:def 2;
then
A9: (P +* (I ";" Stop SCM+FSA))/.
IC Comput(P +* (I ";" Stop SCM+FSA),s2,LifeSpan(P+*I,s1)+1)
= (P +* (I ";" Stop SCM+FSA)).IC Comput(P +* (I ";" Stop SCM+FSA),s2,
LifeSpan(P+*I,s1)+1) by PARTFUN1:def 6;
A10: CurInstr(P +* (I ";" Stop SCM+FSA),
Comput(P +* (I ";" Stop SCM+FSA),s2,LifeSpan(P+*I,s1)+1))
= halt SCM+FSA by A8,A6,A7,Th13,A9;
hence
A11: P +* (I ";" Stop SCM+FSA) halts_on s2 by EXTPRO_1:29;
now
let k be Nat;
assume k < LifeSpan(P+*I,s1) + 1;
then
A12: k <= LifeSpan(P+*I,s1) by NAT_1:13;
then CurInstr(P+*Directed I,
Comput(P+*Directed I,
Initialize s,k)) <> halt SCM+FSA by A6,Th12;
hence CurInstr(P +* (I ";" Stop SCM+FSA),
Comput(P +* (I ";" Stop SCM+FSA),s2,k)) <> halt SCM+FSA by A6,A12,Th17;
end;
then for k be Nat st
CurInstr(P +* (I ";" Stop SCM+FSA),Comput(P +* (I ";" Stop SCM+FSA),s2,k))
= halt SCM+FSA
holds LifeSpan(P+*I,s1) + 1 <= k;
hence LifeSpan(P +* (I ";" Stop SCM+FSA),s2) = LifeSpan(P+*I,s1) + 1 by A10
,A11,EXTPRO_1:def 15;
thus thesis by A11,SCMFSA7B:def 7;
end;
theorem
for I being really-closed Program of SCM+FSA
for P being Instruction-Sequence of SCM+FSA,
s being State of SCM+FSA st I is_halting_on s,P
holds I ";" Stop SCM+FSA is_halting_on s,P by Lm3;
theorem
for l being Nat holds 0 in dom Goto
l & (Goto l). 0 = goto l by Lm1;
Lm4: for I being really-closed Program of SCM+FSA, s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
st I is_halting_on Initialized s,P
holds IC Comput(P +* (I ";" Stop SCM+FSA),
(s +* Initialize((intloc 0).-->1)),
(LifeSpan(P+*I,s +* Initialize((intloc 0).-->1)) + 1)) =
card I &
DataPart Comput(P+*I, s +* Initialize((intloc 0).-->1),LifeSpan(P+*I,
s +* Initialize((intloc 0).-->1)))
= DataPart Comput(P +* (I ";" Stop SCM+FSA),
(s +* Initialize((intloc 0).-->1))
, (LifeSpan(P+*I,s +* Initialize((intloc 0).-->1)) + 1)) &
P+* (I ";" Stop SCM+FSA)
halts_on s +* Initialize((intloc 0).-->1) &
LifeSpan(P+*(I ";" Stop SCM+FSA),s +* Initialize((intloc 0).-->1))
= LifeSpan(P+*I,s +* Initialize((intloc 0).-->1)) + 1
proof
let I be really-closed Program of SCM+FSA;
let s be State of SCM+FSA;
let P be Instruction-Sequence of SCM+FSA;
card Stop SCM+FSA = 1 by COMPOS_1:4;
then card (I ";" Stop SCM+FSA) = card I + 1 by SCMFSA6A:21;
then card I < card (I ";" Stop SCM+FSA) by NAT_1:13;
then
A1: card I in dom (I ";" Stop SCM+FSA) by AFINSQ_1:66;
A2: 0 in dom Stop SCM+FSA by COMPOS_1:3;
(0 + card I) in {m + card I where m is Nat: m in dom Stop SCM+FSA}
by A2;
then
A3: (0 + card I) in dom Reloc(Stop SCM+FSA,card I ) by COMPOS_1:33;
set s2 = s +* Initialize((intloc 0).-->1);
set s1 = s +* Initialize((intloc 0).-->1);
assume
A4: I is_halting_on Initialized s,P;
then
A5: IC Comput(P+*Directed I,
s +* Initialize((intloc 0).-->1),LifeSpan(P+*I,s1) + 1) = IC
Comput(P +* (I ";" Stop SCM+FSA), s2,LifeSpan(P+*I,s1) + 1) by Th18;
A6: 0 in dom Stop SCM+FSA by COMPOS_1:3;
A7: (Stop SCM+FSA).0 = halt SCM+FSA;
A8: (P +* (I ";" Stop SCM+FSA)). card I
= (I ";" Stop SCM+FSA). card I by A1,FUNCT_4:13
.= Reloc(Stop SCM+FSA,card I). (0 + card I) by A3,SCMFSA6A:40
.= IncAddr(halt SCM+FSA,card I) by A7,A6,COMPOS_1:35
.= halt SCM+FSA by COMPOS_0:4;
DataPart Comput(P+*Directed I,
s +* Initialize((intloc 0).-->1),LifeSpan(P+*I,s1) + 1) =
DataPart Comput(P +* (I ";" Stop SCM+FSA), s2,LifeSpan(P+*I,s1) + 1) by A4
,Th18;
hence IC Comput(P +* (I ";" Stop SCM+FSA),s2,LifeSpan(P+*I,s1) + 1) = card
I & DataPart
Comput(P+*I, s1,LifeSpan(P+*I,s1)) = DataPart Comput(
P +* (I ";" Stop SCM+FSA), s2
,LifeSpan(P+*I,s1) + 1) by A4,A5,Th20;
dom(P +* (I ";" Stop SCM+FSA)) = NAT by PARTFUN1:def 2;
then
A9: (P +* (I ";" Stop SCM+FSA))/.
IC Comput(P +* (I ";" Stop SCM+FSA),s2,LifeSpan(P+*I,s1)+1)
= (P +* (I ";" Stop SCM+FSA)).
IC Comput(P +* (I ";" Stop SCM+FSA),s2,LifeSpan(P+*I,s1)+1)
by PARTFUN1:def 6;
A10: CurInstr(P +* (I ";" Stop SCM+FSA),
Comput(P +* (I ";" Stop SCM+FSA),s2,LifeSpan(P+*I,s1)+1))
= halt SCM+FSA by A8,A4,A5,Th20,A9;
hence
A11: P +* (I ";" Stop SCM+FSA) halts_on s2 by EXTPRO_1:29;
now
let k be Nat;
assume k < LifeSpan(P+*I,s1) + 1;
then
A12: k <= LifeSpan(P+*I,s1) by NAT_1:13;
then CurInstr(P+*Directed I,
Comput(P+*Directed I, s +* Initialize((intloc 0).-->1),k)) <> halt
SCM+FSA by A4,Th19;
hence CurInstr(P +* (I ";" Stop SCM+FSA),
Comput(P +* (I ";" Stop SCM+FSA),s2,k)) <>
halt SCM+FSA by A4,A12,Th18;
end;
then for k be Nat st
CurInstr(P +* (I ";" Stop SCM+FSA),
Comput(P +* (I ";" Stop SCM+FSA),s2,k)) = halt SCM+FSA
holds LifeSpan(P+*I,s1) + 1 <= k;
hence thesis by A10,A11,EXTPRO_1:def 15;
end;
theorem
for I being really-closed Program of SCM+FSA, s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
st I is_halting_on Initialized s,P
holds IC Comput(P +* (I ";" Stop SCM+FSA),
(s +* Initialize((intloc 0).-->1)),
(LifeSpan(P+*I,s +* Initialize((intloc 0).-->1)) + 1)) = card I by Lm4;
theorem
for I being really-closed Program of SCM+FSA, s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
st I is_halting_on Initialized s,P
holds DataPart Comput(P+*I, (s +* Initialize((intloc 0).-->1)),
LifeSpan(P+*I,s
+* Initialize((intloc 0).-->1))) = DataPart
Comput(P +* (I ";" Stop SCM+FSA), (s +*
Initialize((intloc 0).-->1)),
(LifeSpan(P+*I,s +* Initialize((intloc 0).-->1)) + 1)) by Lm4;
theorem
for I being really-closed Program of SCM+FSA, s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
st I is_halting_on Initialized s,P
holds P+*(I ";" Stop SCM+FSA) halts_on s +* Initialize((intloc 0).-->1)
by Lm4;
theorem
for I being really-closed Program of SCM+FSA, s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
st I is_halting_on Initialized s,P
holds LifeSpan(P+*(I ";" Stop SCM+FSA),
s +* Initialize((intloc 0).-->1)) = LifeSpan(P+*I,
s +* Initialize((intloc 0).-->1)) + 1 by Lm4;
theorem
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA,
I being really-closed Program of SCM+FSA st
I is_halting_on Initialized s,P
holds IExec(I ";" Stop SCM+FSA,P,s) = IExec(I,P,s) +* Start-At(card I,SCM+FSA)
proof
let s be State of SCM+FSA;
let P be Instruction-Sequence of SCM+FSA;
let I be really-closed Program of SCM+FSA;
set s1 = Initialized s;
assume
A1: I is_halting_on Initialized s,P;
s1 = Initialize Initialized s by MEMSTR_0:44;
then
A2: P+*I halts_on s1 by A1,SCMFSA7B:def 7;
P +* (I ";" Stop SCM+FSA) halts_on s1 &
LifeSpan(P +* (I ";" Stop SCM+FSA),s1) = LifeSpan(P+*I,s1) + 1 by A1,Lm4;
then
A3: Result(P +* (I ";" Stop SCM+FSA),s1) =
Comput(P +* (I ";" Stop SCM+FSA), s1,LifeSpan(
P+*I,s1) + 1) by EXTPRO_1:23;
then DataPart Result(P +* (I ";" Stop SCM+FSA),s1) = DataPart Comput(P+*I,
s1,LifeSpan(P+*I,s1))
by A1,Lm4;
then
A4: DataPart Result(P +* (I ";" Stop SCM+FSA),s1) = DataPart Result(P+*I,s1)
by A2,EXTPRO_1:23
.= DataPart(Result(P+*I,s1) +* Start-At(card I,SCM+FSA)) by MEMSTR_0:79;
IC Result(P +* (I ";" Stop SCM+FSA),s1) = card I by A1,A3,Lm4
.= IC (Result(P+*I,s1) +* Start-At(card I,SCM+FSA)) by FUNCT_4:113;
then
A5: Result(P +* (I ";" Stop SCM+FSA),s1)
= (Result(P+*I,s1) +* Start-At(card I,SCM+FSA))
by A4,MEMSTR_0:78;
A6: Result(P +* (I ";" Stop SCM+FSA),s1) = Result(P+*I,s1) +*
Start-At(card I,SCM+FSA) by A5;
thus IExec(I ";" Stop SCM+FSA,P,s)
= Result(P +* (I ";" Stop SCM+FSA),s1) by SCMFSA6B:def 1
.= Result(P+*I,s1) +* (Start-At(card I,SCM+FSA)) by A6
.= Result(P+*I,s1) +* (Start-At(card I,SCM+FSA))
.= Result(P+*I,s1) +* Start-At(card I,SCM+FSA)
.= IExec(I,P,s) +* Start-At(card I,SCM+FSA) by SCMFSA6B:def 1;
end;
Lm5: for I being really-closed Program of SCM+FSA,
J being Program of SCM+FSA,
s being State of SCM+FSA st I is_halting_on s,P holds
IC Comput(P +* (I ";" Goto (card J + 1) ";" J ";" Stop SCM+FSA),
Initialize s, LifeSpan(P+*I,Initialize s) + 2)
= card I + card J + 1
&
DataPart Comput(P+*I,(Initialize s),
LifeSpan(P+*I,Initialize s))
= DataPart Comput(P +* (I ";" Goto (card J + 1) ";" J ";" Stop SCM+FSA),
Initialize s,
LifeSpan(P+*I,Initialize s) + 2) &
(for k being Nat st
k < LifeSpan(P+*I,Initialize s) + 2
holds CurInstr(P +* (I ";" Goto (card J + 1) ";" J ";" Stop SCM+FSA),
Comput(P +* (I ";" Goto (card J + 1) ";" J ";" Stop SCM+FSA),
Initialize s,k))
<> halt SCM+FSA) &
(for k being Nat st
k <= LifeSpan(P+*I,Initialize s)
holds IC Comput(P +* (I ";" Goto (card J + 1) ";" J ";" Stop SCM+FSA),
Initialize s,k)
= IC Comput(P+*I, (Initialize s),k)) &
IC Comput(P +* (I ";" Goto (card J + 1) ";" J ";" Stop SCM+FSA),
Initialize s,
(LifeSpan(P+*I,Initialize s) + 1)) = card I &
P +* (I ";" Goto (card J + 1) ";" J ";" Stop SCM+FSA)
halts_on
Initialize s
&
LifeSpan(P +* (I ";" Goto (card J + 1) ";" J ";" Stop SCM+FSA),
Initialize s)
= LifeSpan(P+*I,Initialize s) + 2
proof
let I be really-closed Program of SCM+FSA;
let J be Program of SCM+FSA;
let s be State of SCM+FSA;
A1: card (Goto (card J + 1) ";" J) = card Goto (card J + 1) +
card J by SCMFSA6A:21
.= 1 + card J by Lm1;
A2: card (Goto (card J + 1) ";" J) = card Goto (card J + 1) +
card J by SCMFSA6A:21
.= card J + 1 by Lm1;
A3: (card I + card J + 1) = ((card J + 1) + card I);
A4: 0 in dom Stop SCM+FSA by COMPOS_1:3;
set J2 = Goto (card J + 1) ";" (J ";" Stop SCM+FSA);
set s2 = Initialize s;
set P2 = P +* (I ";" Goto (card J + 1) ";" J ";" Stop SCM+FSA);
set s1 = Initialize s;
assume
A5: I is_halting_on s,P;
dom Reloc(Stop SCM+FSA,card J + 1)
= {m + (card J + 1) where m is Nat: m in dom Stop SCM+FSA} by COMPOS_1:33;
then
A6: (0 + (card J + 1)) in dom Reloc(Stop SCM+FSA,card J + 1) by A4;
A7: dom Goto (card J + 1) c= dom (Goto (card J + 1) ";" J) by SCMFSA6A:17;
A8: 0 in dom Goto (card J + 1) by Lm1;
A9: J2. 0 = (Goto (card J + 1) ";" J ";" Stop SCM+FSA).
0 by SCMFSA6A:25
.= (Directed (Goto (card J + 1) ";" J)). 0 by A8,A7,Th7
.= (Goto (card J + 1) ";" Directed J). 0 by SCMFSA6A:24
.= (Directed Goto (card J + 1)). 0 by A8,Th7
.= (Goto (card J + 1)). 0 by SCMFSA6A:22
.= goto (card J + 1);
A10: I ";" Goto (card J + 1) ";" J ";" Stop SCM+FSA = I ";" Goto
(card J + 1) ";" (J ";" Stop SCM+FSA) by SCMFSA6A:25
.= I ";" J2 by SCMFSA6A:25;
then
A11: DataPart Comput(P +* Directed I,
Initialize s, LifeSpan(P+*I,s1) + 1)
= DataPart Comput(P2, s2, LifeSpan(P+*I,s1) + 1) by A5,Th17;
A12: card J2 = card Goto (card J + 1) + card (J ";" Stop SCM+FSA) by
SCMFSA6A:21
.= 1 + card (J ";" Stop SCM+FSA) by Lm1;
then
A13: 0 + 1 <= card J2 by NAT_1:11;
A14: card (I ";" J2) = card I + card J2 by SCMFSA6A:21;
then card I + 0 < card (I ";" J2) by A13,XREAL_1:6;
then
A15: card I in dom (I ";" J2) by AFINSQ_1:66;
A16: card Stop SCM+FSA = 1 by COMPOS_1:4;
card (I ";" J2) = card I + card (Goto (card J + 1) ";" J ";"
Stop SCM+FSA) by A14,SCMFSA6A:25
.= card I + (card J + 1 + 1) by A2,A16,SCMFSA6A:21
.= card I + card J + 1 + 1;
then card I + card J + 1 < card (I ";" J2) by NAT_1:13;
then
A17: (card I + card J + 1) in dom (I ";" J2) by AFINSQ_1:66;
A18: 0 in dom J2 by A13,AFINSQ_1:66;
then (0 + card I) in {m + card I where m is Nat: m in dom J2};
then
A19: 0 + card I in dom Reloc(J2,card I) by COMPOS_1:33;
A20: card Stop SCM+FSA = 1 by COMPOS_1:4;
A21: (Stop SCM+FSA).0 = halt SCM+FSA;
card J2 = 1 + (card J + card Stop SCM+FSA) by A12,SCMFSA6A:21
.= card J + (1 + card Stop SCM+FSA);
then card J + 1 < card J2 by A20,XREAL_1:6;
then
A22: (card J + 1) in dom J2 by AFINSQ_1:66;
A23: J2. (card J + 1) = (Goto (card J + 1) ";" J ";" Stop
SCM+FSA). (card J + 1) by SCMFSA6A:25
.= Reloc(Stop SCM+FSA,card J + 1). (0 + (card J + 1)) by A1,A6,SCMFSA6A:40
.= IncAddr(halt SCM+FSA,card J + 1) by A4,A21,COMPOS_1:35
.= halt SCM+FSA by COMPOS_0:4;
dom Reloc(J2,card I) = {m + card I where m is Nat: m in dom J2}
by COMPOS_1:33;
then
A24: (card I + card J + 1) in dom Reloc(J2,card I )
by A22,A3;
A25: IC Comput(P+*Directed I, Initialize s,
(LifeSpan(P+*I,s1)+ 1))
= IC Comput(P2, s2,LifeSpan(P+*I,s1) + 1) by A5,A10,Th17;
A26: CurInstr(P2,Comput(P2,s2,LifeSpan(P+*I,s1)+1))
= P2.IC Comput(P2,s2,LifeSpan(P+*I,s1)+1) by PBOOLE:143
.= P2.IC Comput(P+*Directed I, Initialize s,
(LifeSpan(P+*I,s1) + 1)) by A5,A10,Th17
.= P2. card I by A5,Th13
.= (I ";" J2). card I by A10,A15,FUNCT_4:13
.= Reloc(J2,card I). (0 + card I) by A19,SCMFSA6A:40
.= IncAddr(goto (card J + 1),card I) by A18,A9,COMPOS_1:35
.= goto ( (card J + 1) + card I) by SCMFSA_4:1
.= goto (card I + card J + 1);
A27: now
let f be FinSeq-Location;
thus Comput(P2, s2,LifeSpan(P+*I,s1) + (1 + 1)).f
= Comput(P2, s2,LifeSpan(P+*I,s1) + 1 + 1).f
.= (Following(P2,
Comput(P2, s2,LifeSpan(P+*I,s1) + 1))).f
by EXTPRO_1:3
.= Comput(P2, s2,LifeSpan(P+*I,s1) + 1).f by A26,SCMFSA_2:69;
end;
thus IC Comput(P2, s2,LifeSpan(P+*I,s1) + 2) = IC
Comput(P2, s2,LifeSpan(P+*I,s1) + 1 + 1)
.= IC Following(P2,
Comput(P2, s2,LifeSpan(P+*I,s1) + 1)) by EXTPRO_1:3
.= (card I + card J + 1) by A26,SCMFSA_2:69;
then
A28: CurInstr(P2,Comput(P2,s2,LifeSpan(P+*I,s1)+2))
= P2. (card I + card J + 1) by PBOOLE:143
.= (I ";" J2). (card I + card J + 1) by A10,A17,FUNCT_4:13
.= Reloc(J2,card I). ((card J + 1) + card I) by A24,SCMFSA6A:40
.= IncAddr(halt SCM+FSA,card I) by A22,A23,COMPOS_1:35
.= halt SCM+FSA by COMPOS_0:4;
now
let a be Int-Location;
thus Comput(P2, s2,LifeSpan(P+*I,s1) + (1 + 1)).a
= Comput(
P2, s2,LifeSpan(P+*I,s1) + 1 + 1).a
.= (Following(P2,
Comput(P2, s2,LifeSpan(P+*I,s1) + 1))).a by EXTPRO_1:3
.= Comput(P2, s2,LifeSpan(P+*I,s1) + 1).a by A26,SCMFSA_2:69;
end;
then DataPart Comput(P2, s2,LifeSpan(P+*I,s1) + 1) =
DataPart Comput(
P2, s2,
LifeSpan(P+*I,s1) + 2) by A27,SCMFSA_M:2;
hence DataPart Comput(P+*I,s1,LifeSpan(P+*I,s1)) =
DataPart Comput(P2, s2, LifeSpan(P+*I,s1) + 2) by A5,A11,Th13;
thus
A29: now
let k be Nat;
assume
A30: k < LifeSpan(P+*I,s1) + 2;
per cases;
suppose
A31: k <= LifeSpan(P+*I,s1);
then CurInstr(P +* Directed I,
Comput(P+* Directed I, Initialize s,k))
<> halt SCM+FSA by A5,Th12;
hence CurInstr(P2,Comput(P2,s2,k)) <>
halt SCM+FSA by A5,A10,A31,Th17;
end;
suppose
A32: LifeSpan(P+*I,s1) < k;
k < LifeSpan(P+*I,s1) + 1 + 1 by A30;
then
A33: k <= LifeSpan(P+*I,s1) + 1 by NAT_1:13;
LifeSpan(P+*I,s1) + 1 <= k by A32,NAT_1:13;
hence CurInstr(P2,Comput(P2,s2,k)) <> halt SCM+FSA by A26,A33,XXREAL_0:1;
end;
end;
hereby
let k be Nat;
assume
A34: k <= LifeSpan(P+*I,s1);
then
Comput(P+*I, s1,k) = Comput(P +* Directed I,
Initialize s,k) by A5,Th12;
then
IC Comput(P+*I, s1,k) = IC Comput(P +* Directed I,
Initialize s,k);
hence IC Comput(P2, s2,k) = IC Comput(P+*I, s1,k) by A5,A10,A34,Th17;
end;
thus IC Comput(P2, s2,LifeSpan(P+*I,s1) + 1) = card I by A5,A25,Th13;
thus
A35: P2 halts_on s2 by A28,EXTPRO_1:29;
for k be Nat st
CurInstr(P2,Comput(P2,s2,k)) = halt SCM+FSA
holds LifeSpan(P+*I,s1) + 2 <= k by A29;
hence thesis by A28,A35,EXTPRO_1:def 15;
end;
theorem
for I being really-closed Program of SCM+FSA,
J being Program of SCM+FSA,s being State of SCM+FSA
st I is_halting_on s,P
holds
I ";" Goto (card J + 1) ";" J ";" Stop SCM+FSA is_halting_on s,P
proof
let I be really-closed Program of SCM+FSA;
let J be Program of SCM+FSA;
let s be State of SCM+FSA;
set IJ2 = I ";" Goto (card J + 1) ";" J ";" Stop SCM+FSA;
set s2 = Initialize s;
set P2 = P +* IJ2;
assume I is_halting_on s,P;
then P2 halts_on s2 by Lm5;
hence thesis by SCMFSA7B:def 7;
end;
theorem
for I being really-closed Program of SCM+FSA,
J being Program of SCM+FSA,
s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
st I is_halting_on s,P
holds
P+*(I ";" Goto (card J + 1) ";" J ";" Stop SCM+FSA)
halts_on Initialize s
by Lm5;
Lm6: for I being really-closed Program of SCM+FSA,
J being Program of SCM+FSA,
s being State of SCM+FSA st
I is_halting_on Initialized s,P
holds IC Comput(P +* (I ";" Goto (card J + 1) ";" J ";" Stop SCM+FSA),
s +* Initialize((intloc 0).-->1),
LifeSpan(P+*I,s +* Initialize((intloc 0).-->1)) + 2)
= (card I + card J + 1) &
DataPart
Comput(P+*I, (s +* Initialize((intloc 0).-->1)),
LifeSpan(P +* I,s +* Initialize((intloc 0).-->1)))
= DataPart
Comput(P +* (I ";" Goto (card J + 1) ";" J ";" Stop SCM+FSA),
s +* Initialize((intloc 0).-->1),
LifeSpan(P+*I,s +* Initialize((intloc 0).-->1)) + 2) & (
for k being Nat st k
< LifeSpan(P+*I,s +* Initialize((intloc 0).-->1)) + 2
holds CurInstr(P +* (I ";" Goto (card J + 1) ";" J ";" Stop SCM+FSA),
Comput(P +* (I ";" Goto (card J + 1) ";" J ";" Stop SCM+FSA),
s +* Initialize((intloc 0).-->1),k)) <> halt SCM+FSA) &
(for k being Nat
st k <= LifeSpan(P +* I,s +* Initialize((intloc 0).-->1))
holds IC Comput(P +* (I ";" Goto (card J + 1) ";" J ";" Stop SCM+FSA),
s +* Initialize((intloc 0).-->1),k)
= IC Comput(P+*I, (s +* Initialize((intloc 0).-->1)),k)) &
IC Comput(P +* (I ";" Goto (card J + 1) ";" J ";" Stop SCM+FSA),
s +* Initialize((intloc 0).-->1),
LifeSpan(P+*I,s +* Initialize((intloc 0).-->1)) + 1)
= card I &
P +* (I ";" Goto (card J + 1) ";" J ";" Stop SCM+FSA)
halts_on s +* Initialize((intloc 0).-->1)
& LifeSpan(P +* (I ";" Goto (card J + 1) ";" J ";" Stop SCM+FSA),
s +* Initialize((intloc 0).-->1))
= LifeSpan(P+*I,s +* Initialize((intloc 0).-->1)) + 2
proof
let I be really-closed Program of SCM+FSA;
let J be Program of SCM+FSA;
let s be State of SCM+FSA;
A1: card (Goto (card J + 1) ";" J) = card Goto (card J + 1) +
card J by SCMFSA6A:21
.= 1 + card J by Lm1;
A2: card (Goto (card J + 1) ";" J) = card Goto (card J + 1) +
card J by SCMFSA6A:21
.= card J + 1 by Lm1;
A3: (card I + card J + 1) = ((card J + 1) + card I);
A4: 0 in dom Stop SCM+FSA by COMPOS_1:3;
set J2 = Goto (card J + 1) ";" (J ";" Stop SCM+FSA);
set s2 = s +* Initialize((intloc 0).-->1);
set P2 = P +* (I ";" Goto (card J + 1) ";" J ";" Stop SCM+FSA);
set s1 = s +* Initialize((intloc 0).-->1);
assume
A5: I is_halting_on Initialized s,P;
dom Reloc(Stop SCM+FSA,card J + 1) = {m + (card J + 1) where m is Nat:
m in dom Stop SCM+FSA} by COMPOS_1:33;
then
A6: (0 + (card J + 1)) in dom Reloc(Stop SCM+FSA,
card J + 1) by A4;
A7: dom Goto (card J + 1) c= dom (Goto (card J + 1) ";" J) by SCMFSA6A:17;
A8: 0 in dom Goto (card J + 1) by Lm1;
A9: J2. 0 = (Goto (card J + 1) ";" J ";" Stop SCM+FSA).
0 by SCMFSA6A:25
.= (Directed (Goto (card J + 1) ";" J)). 0 by A8,A7,Th7
.= (Goto (card J + 1) ";" Directed J). 0 by SCMFSA6A:24
.= (Directed Goto (card J + 1)). 0 by A8,Th7
.= (Goto (card J + 1)). 0 by SCMFSA6A:22
.= goto (card J + 1);
A10: I ";" Goto (card J + 1) ";" J ";" Stop SCM+FSA = I ";" Goto
(card J + 1) ";" (J ";" Stop SCM+FSA) by SCMFSA6A:25
.= I ";" J2 by SCMFSA6A:25;
then
A11: DataPart Comput(P+*Directed I, (s +*
Initialize((intloc 0).-->1)),LifeSpan(P+*I,s1) + 1) =
DataPart Comput(P2, s2,LifeSpan(P+*I,s1) + 1) by A5,Th18;
A12: card J2 = card Goto (card J + 1) + card (J ";" Stop SCM+FSA) by
SCMFSA6A:21
.= 1 + card (J ";" Stop SCM+FSA) by Lm1;
then
A13: 0 + 1 <= card J2 by NAT_1:11;
A14: card (I ";" J2) = card I + card J2 by SCMFSA6A:21;
then card I + 0 < card (I ";" J2) by A13,XREAL_1:6;
then
A15: card I in dom (I ";" J2) by AFINSQ_1:66;
A16: card Stop SCM+FSA = 1 by COMPOS_1:4;
card (I ";" J2) = card I + card (Goto (card J + 1) ";" J ";"
Stop SCM+FSA) by A14,SCMFSA6A:25
.= card I + (card J + 1 + 1) by A2,A16,SCMFSA6A:21
.= card I + card J + 1 + 1;
then card I + card J + 1 < card (I ";" J2) by NAT_1:13;
then
A17: (card I + card J + 1) in dom (I ";" J2) by AFINSQ_1:66;
A18: 0 in dom J2 by A13,AFINSQ_1:66;
then (0 + card I) in {m + card I where m is Nat: m in dom J2};
then
A19: (0 + card I) in dom Reloc(J2,card I) by COMPOS_1:33;
A20: card Stop SCM+FSA = 1 by COMPOS_1:4;
A21: (Stop SCM+FSA).0 = halt SCM+FSA;
card J2 = 1 + (card J + card Stop SCM+FSA) by A12,SCMFSA6A:21
.= card J + (1 + card Stop SCM+FSA);
then card J + 1 < card J2 by A20,XREAL_1:6;
then
A22: card J + 1 in dom J2 by AFINSQ_1:66;
A23: P2/.IC Comput(P2,s2,LifeSpan(P+*I,s1)+1)
= P2.IC Comput(P2,s2,LifeSpan(P+*I,s1)+1) by PBOOLE:143;
A24: J2. (card J + 1) = (Goto (card J + 1) ";" J ";" Stop
SCM+FSA). (card J + 1) by SCMFSA6A:25
.= Reloc(Stop SCM+FSA,card J + 1). (0 + (card J + 1)) by A1,A6,SCMFSA6A:40
.= IncAddr(halt SCM+FSA,card J + 1) by A4,A21,COMPOS_1:35
.= halt SCM+FSA by COMPOS_0:4;
dom Reloc(J2,card I) = {m + card I where m is Nat: m in dom J2}
by COMPOS_1:33;
then
A25: (card I + card J + 1) in dom Reloc(J2,card I )
by A22,A3;
A26: IC Comput(P+*Directed I, s +* Initialize((intloc 0).-->1),
LifeSpan(P+*I,s1) + 1) = IC
Comput(P2, s2,LifeSpan(P+*I,s1) + 1) by A5,A10,Th18;
then
A27: CurInstr(P2,Comput(P2,s2,LifeSpan(P+*I,s1)+1))
= P2. card I by A5,Th20,A23
.= (I ";" J2). card I by A10,A15,FUNCT_4:13
.= Reloc(J2,card I). (0 + card I) by A19,SCMFSA6A:40
.= IncAddr(goto (card J + 1),card I) by A18,A9,COMPOS_1:35
.= goto ( (card J + 1) + card I) by SCMFSA_4:1
.= goto (card I + card J + 1);
A28: now
let f be FinSeq-Location;
thus Comput(P2, s2,LifeSpan(P+*I,s1) + (1 + 1)).f
= Comput(
P2, s2,LifeSpan(P+*I,
s1) + 1 + 1).f
.= (Following(P2,
Comput(P2, s2,LifeSpan(P+*I,s1) + 1))).f by EXTPRO_1:3
.= Comput(P2, s2,LifeSpan(P+*I,s1) + 1).f by A27,SCMFSA_2:69;
end;
thus IC Comput(P2, s2,LifeSpan(P+*I,s1) + 2)
= IC Comput(P2, s2,LifeSpan(P+*I,s1) + 1 + 1)
.= IC Following(P2,Comput(P2, s2,LifeSpan(P+*I,s1) + 1)) by EXTPRO_1:3
.= (card I + card J + 1) by A27,SCMFSA_2:69;
then
A29: CurInstr(P2,Comput(P2,s2,LifeSpan(P+*I,s1)+2))
= P2. (card I + card J+ 1) by PBOOLE:143
.= (I ";" J2). (card I + card J + 1)
by A10,A17,FUNCT_4:13
.= Reloc(J2,card I). ((card J + 1) + card I) by A25,SCMFSA6A:40
.= IncAddr(halt SCM+FSA,card I) by A22,A24,COMPOS_1:35
.= halt SCM+FSA by COMPOS_0:4;
now
let a be Int-Location;
thus Comput(P2, s2,LifeSpan(P+*I,s1) + (1 + 1)).a
= Comput(P2, s2,LifeSpan(P+*I,s1) + 1 + 1).a
.= (Following(P2,Comput(P2, s2,LifeSpan(P+*I,s1) + 1))).a by EXTPRO_1:3
.= Comput(P2, s2,LifeSpan(P+*I,s1) + 1).a by A27,SCMFSA_2:69;
end;
then DataPart Comput(P2, s2,LifeSpan(P+*I,s1) + 1) =
DataPart Comput(
P2, s2,
LifeSpan(P+*I,s1) + 2) by A28,SCMFSA_M:2;
hence DataPart Comput(P+*I,s1,LifeSpan(P+*I,s1)) =
DataPart Comput(P2, s2,
LifeSpan(P+*I,s1) + 2) by A5,A11,Th20;
thus
A30: now
let k be Nat;
assume
A31: k < LifeSpan(P+*I,s1) + 2;
per cases;
suppose
A32: k <= LifeSpan(P+*I,s1);
then CurInstr(P +* Directed I,
Comput(P+*Directed I, s +* Initialize((intloc 0).-->1),k))
<> halt
SCM+FSA by A5,Th19;
hence CurInstr(P2,Comput(P2,s2,k)) <>
halt SCM+FSA by A5,A10,A32,Th18;
end;
suppose
A33: LifeSpan(P+*I,s1) < k;
k < LifeSpan(P+*I,s1) + 1 + 1 by A31;
then
A34: k <= LifeSpan(P+*I,s1) + 1 by NAT_1:13;
LifeSpan(P+*I,s1) + 1 <= k by A33,NAT_1:13;
hence CurInstr(P2,Comput(P2,s2,k)) <> halt SCM+FSA by A27,A34,XXREAL_0:1;
end;
end;
hereby
let k be Nat;
assume
A35: k <= LifeSpan(P+*I,s1);
then
Comput(P+*I, s1,k) = Comput(P +* Directed I,
(s +* Initialize((intloc 0).-->1))
,k) by A5,Th19;
then
IC Comput(P+*I, s1,k) = IC Comput(P +* Directed I,
(s +* Initialize((intloc 0).-->1))
,k);
hence IC Comput(P2, s2,k) = IC Comput(P+*I, s1,k)
by A5,A10,A35,Th18;
end;
thus IC Comput(P2, s2,LifeSpan(P+*I,s1) + 1) = card I by A5,A26,Th20;
thus
A36: P2 halts_on s2 by A29,EXTPRO_1:29;
for k be Nat
st CurInstr(P2,Comput(P2,s2,k))
= halt SCM+FSA
holds LifeSpan(P+*I,s1) + 2 <= k by A30;
hence thesis by A29,A36,EXTPRO_1:def 15;
end;
theorem
for I being really-closed Program of SCM+FSA,
J being Program of SCM+FSA, s being State of SCM+FSA
st I is_halting_on Initialized s,P
holds P +* (I ";" Goto (card J + 1) ";" J ";" Stop SCM+FSA)
halts_on s +* Initialize((intloc 0).-->1) by Lm6;
theorem
for I being really-closed Program of SCM+FSA,
J being Program of SCM+FSA, s being State of SCM+FSA
st I is_halting_on Initialized s,P
holds IC IExec(I ";"
Goto (card J + 1) ";" J ";" Stop SCM+FSA,P,s) = (card I + card J + 1)
proof
let I be really-closed Program of SCM+FSA;
let J be Program of SCM+FSA;
let s be State of SCM+FSA;
set s2 = Initialized s;
set P2 = P +* (I ";" Goto (card J + 1) ";" J ";" Stop SCM+FSA);
assume
A1: I is_halting_on Initialized s,P;
then P2 halts_on s2 & LifeSpan(P2,s2)
= LifeSpan(P+*I,s2) + 2 by Lm6;
then
IC Result(P2,s2) =
IC Comput(P2, s2,LifeSpan(P+*I,s2) +2) by EXTPRO_1:23
.= card I + card J + 1 by A1,Lm6;
hence thesis by SCMFSA6B:def 1;
end;
theorem
for I being really-closed Program of SCM+FSA,
J being Program of SCM+FSA, s being State of SCM+FSA st
I is_halting_on Initialized s,P
holds IExec(I ";" Goto(card J + 1) ";" J ";" Stop SCM+FSA,P,s)
= IExec(I,P,s) +* Start-At(card I + card J + 1,SCM+FSA)
proof
let I be really-closed Program of SCM+FSA;
let J be Program of SCM+FSA;
let s be State of SCM+FSA;
set s1 = Initialized s;
set P2 = P +* (I ";" Goto (card J + 1) ";" J ";" Stop SCM+FSA);
assume that
A1: I is_halting_on Initialized s,P;
s1 = Initialize Initialized s by MEMSTR_0:44;
then
A2: P+*I halts_on s1 by A1,SCMFSA7B:def 7;
P2 halts_on s1 & LifeSpan(P2,s1) = LifeSpan(P+*I,s1) + 2 by A1,Lm6;
then
A3: Result(P2,s1) = Comput(P2, s1,LifeSpan(
P+*I,s1) + 2) by EXTPRO_1:23;
then DataPart Result(P2,s1) = DataPart Comput(P+*I,s1,LifeSpan(P+*I,s1))
by A1,Lm6;
then
A4: DataPart Result(P2,s1) = DataPart Result(P+*I,s1)
by A2,EXTPRO_1:23
.= DataPart(Result(P+*I,s1) +* Start-At((card I+card J +1),SCM+FSA))
by MEMSTR_0:79;
IC Result(P2,s1) = (card I + card J + 1) by A1,A3,Lm6
.= IC (Result(P+*I,s1) +* Start-At((card I+card J +1),SCM+FSA))
by FUNCT_4:113;
then
A5: Result(P2,s1) = (Result(P+*I,s1) +* Start-At((card I+card J +1),SCM+FSA))
by A4,MEMSTR_0:78;
A6: Result(P2,s1) = Result(P+*I,s1) +*
Start-At((card I + card J + 1
),SCM+FSA) by A5;
thus IExec(I ";" Goto (card J + 1) ";" J ";" Stop SCM+FSA,P,s)
= Result(P2,s1) by SCMFSA6B:def 1
.= Result(P+*I,s1) +* (Start-At((card I+card J +1),SCM+FSA))
by A6
.= Result(P+*I,s1) +* (Start-At((card I+card J +1),SCM+FSA))
.= Result(P+*I,s1) +* Start-At((card I+card J +1),SCM+FSA)
.= IExec(I,P,s) +* Start-At((card I+card J +1),SCM+FSA)
by SCMFSA6B:def 1;
end;
theorem
for I being Program of SCM+FSA, a being Int-Location,
k being Nat, i being Instruction of SCM+FSA
st I does not destroy a & i does not destroy a
holds I +*(k,i) does not destroy a
proof
let I be Program of SCM+FSA, a be Int-Location,
k be Nat, i be Instruction of SCM+FSA such that
A1: I does not destroy a and
A2: i does not destroy a;
let j be Instruction of SCM+FSA such that
A3: j in rng(I +*(k,i));
rng(I+*(k,i)) c= rng I \/ {i} by FUNCT_7:100;
then j in rng I \/ {i} by A3;
then per cases by XBOOLE_0:def 3;
suppose j in rng I;
hence thesis by A1,SCMFSA7B:def 4;
end;
suppose j in {i};
hence j does not destroy a by A2,TARSKI:def 1;
end;
end;
registration let I,J be good preProgram of SCM+FSA;
cluster I +* J -> good;
coherence
proof
I does not destroy intloc 0 & J does not destroy intloc 0
by SCMFSA7B:def 5;
hence I +* J does not destroy intloc 0 by Th4;
end;
end;
theorem
for I being MacroInstruction of SCM+FSA, k being Nat
holds Goto k ";" I = Macro(goto k) ';' I
proof let I be MacroInstruction of SCM+FSA, k being Nat;
rng Goto k = {goto k} by AFINSQ_1:33;
then not halt SCM+FSA in rng Goto k by TARSKI:def 1;
then Directed Goto k = Goto k by FUNCT_4:103;
hence Goto k ";" I = Macro(goto k) ';' I;
end;
theorem
for i,j being Nat holds IncAddr(Goto i,j) = <%goto(i+j)%>
proof let i,j be Nat;
A1: dom<%goto(i+j)%> = Segm 1 by AFINSQ_1:33
.= dom Goto i by AFINSQ_1:33;
for m being Nat st m in dom Goto i
holds <%goto(i+j)%>.m = IncAddr((Goto i)/.m,j)
proof let m be Nat;
assume
A2: m in dom Goto i;
then m in {0} by CARD_1:49,AFINSQ_1:33;
then
A3: m = 0 by TARSKI:def 1;
A4: (Goto i)/.m = (Goto i).m by A2,PARTFUN1:def 6
.= goto i by A3;
thus <%goto(i+j)%>.m
= goto(i+j) by A3
.= IncAddr((Goto i)/.m,j) by A4,SCMFSA10:41;
end;
hence IncAddr(Goto i,j) = <%goto(i+j)%> by A1,COMPOS_1:def 21;
end;
theorem
for I,J being NAT-defined (the InstructionsF of SCM+FSA)-valued Function
st I c= J
for a be Int-Location st J does not destroy a
holds I does not destroy a
proof let I,J be NAT-defined (the InstructionsF of SCM+FSA)-valued Function
such that
A1: I c= J;
let a be Int-Location such that
A2: J does not destroy a;
let i be Instruction of SCM+FSA such that
A3: i in rng I;
rng I c= rng J by A1,RELAT_1:11;
then i in rng J by A3;
hence i does not destroy a by A2,SCMFSA7B:def 4;
end;