Copyright (c) 1997 Association of Mizar Users
environ
vocabulary AMI_1, SCMFSA_2, BOOLE, SCMFSA8A, SCMFSA6A, CAT_1, FUNCT_4, AMI_3,
FUNCT_1, RELAT_1, CARD_1, AMI_5, UNIALG_2, SCMFSA7B, SCM_1, FUNCT_7,
RELOC, ARYTM_1, SCMFSA6C, SCMFSA6B, SF_MASTR, SCMFSA_4, FUNCOP_1,
SCMFSA8B, AMI_2, SCMFSA8C, CARD_3;
notation TARSKI, XBOOLE_0, ENUMSET1, XCMPLX_0, XREAL_0, NAT_1, CQC_LANG,
RELAT_1, FUNCT_1, FUNCT_4, FUNCT_7, CARD_1, STRUCT_0, AMI_1, AMI_3,
AMI_5, SCMFSA_2, SCMFSA_4, SCMFSA_5, SCM_1, SF_MASTR, SCMFSA6A, SCMFSA6B,
SCMFSA6C, SCMFSA7B, SCMFSA8A, SCMFSA8B, BINARITH;
constructors ENUMSET1, AMI_5, SCM_1, SCMFSA_5, SCMFSA6A, SF_MASTR, SCMFSA6B,
SCMFSA6C, SCMFSA8A, SCMFSA8B, BINARITH, MEMBERED;
clusters FUNCT_1, PRELAMB, AMI_1, SCMFSA_2, SCMFSA_4, SCMFSA6A, SF_MASTR,
SCMFSA6B, SCMFSA6C, SCMFSA7B, SCMFSA8A, INT_1, CQC_LANG, NAT_1, FRAENKEL,
XREAL_0, MEMBERED;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
theorems FUNCT_4, SCMFSA_4, SCMFSA6A, AXIOMS, SCMFSA8B, AMI_1, SCMFSA6C,
AMI_5, SCMFSA7B, SCMFSA8A, SCMFSA_7, SF_MASTR, NAT_1, SCMFSA6B, GRFUNC_1,
SCMFSA_2, SCMFSA_5, FUNCT_1, FUNCT_7, REAL_1, AMI_3, TARSKI, GOBOARD9,
REAL_2, CQC_THE1, SCM_1, ENUMSET1, CQC_LANG, RELAT_1, PRE_CIRC, SCMFSA_3,
BINARITH, INT_1, SQUARE_1, XBOOLE_0, XBOOLE_1, XCMPLX_1;
schemes NAT_1;
begin :: Preliminaries
reserve m for Nat;
set A = the Instruction-Locations of SCM+FSA;
set D = Int-Locations \/ FinSeq-Locations;
definition
cluster pseudo-paraclosed Macro-Instruction;
existence
proof
consider K being pseudo-paraclosed Macro-Instruction;
take K;
thus thesis;
end;
end;
canceled;
theorem Th2: ::T4425 ** n.t
for s being State of SCM+FSA,P being initial FinPartState of SCM+FSA
st P is_pseudo-closed_on s
for k being Nat st
(for n being Nat st n <= k holds
IC (Computation (s +* (P +* Start-At insloc 0))).n in dom P)
holds k < pseudo-LifeSpan(s,P)
proof
let s be State of SCM+FSA;
let P be initial FinPartState of SCM+FSA;
assume A1: P is_pseudo-closed_on s;
let k be Nat;
assume A2: for n being Nat st n <= k holds
IC (Computation (s +* (P +* Start-At insloc 0))).n in dom P;
IC (Computation (s +* (P +* Start-At insloc 0))).pseudo-LifeSpan(s,P) =
insloc card ProgramPart P by A1,SCMFSA8A:def 5;
then not IC (Computation (s +* (P +* Start-At insloc 0))).pseudo-LifeSpan(s
,P) in
dom ProgramPart P by SCMFSA6A:15;
then A3: not IC (Computation (s +* (P +* Start-At insloc 0))).pseudo-LifeSpan(s
,P)
in
dom P by AMI_5:73;
assume pseudo-LifeSpan(s,P) <= k;
hence contradiction by A2,A3;
end;
canceled 3;
theorem Th6: ::T210837
for f be Function, x be set st x in dom f holds
f +* (x .--> f.x) = f
proof
let f be Function;
let x be set;
assume x in dom f;
hence f +* (x .--> f.x) = f +*(x,f.x) by FUNCT_7:def 3
.= f by FUNCT_7:37;
end;
theorem Th7: ::TMP12
for l being Instruction-Location of SCM+FSA holds
l + 0 = l
proof
let l be Instruction-Location of SCM+FSA;
consider m being Nat such that
A1: l = insloc m & l + 0 = insloc (m + 0) by SCMFSA_4:def 1;
thus l + 0 = l by A1;
end;
theorem Th8: ::TMP19
for i being Instruction of SCM+FSA holds
IncAddr(i,0) = i
proof
let i be Instruction of SCM+FSA;
A1: InsCode i <= 11 + 1 by SCMFSA_2:35;
A2: InsCode i <= 10+1 implies InsCode i <= 10 or InsCode i = 11 by NAT_1:26;
A3: InsCode i <= 9+1 implies InsCode i <= 8+1 or InsCode i = 10 by NAT_1:26;
A4: InsCode i <= 8+1 implies InsCode i <= 7+1 or InsCode i = 9 by NAT_1:26;
per cases by A1,A2,A3,A4,CQC_THE1:9,NAT_1:26;
suppose InsCode i = 0;
then i = halt SCM+FSA by SCMFSA_2:122;
hence IncAddr(i,0) = i by SCMFSA_4:8;
suppose InsCode i = 1;
then ex a,b being Int-Location st i = a:=b by SCMFSA_2:54;
hence IncAddr(i,0) = i by SCMFSA_4:9;
suppose InsCode i = 2;
then ex a,b being Int-Location st i = AddTo(a,b) by SCMFSA_2:55;
hence IncAddr(i,0) = i by SCMFSA_4:10;
suppose InsCode i = 3;
then ex a,b being Int-Location st i = SubFrom(a,b) by SCMFSA_2:56;
hence IncAddr(i,0) = i by SCMFSA_4:11;
suppose InsCode i = 4;
then ex a,b being Int-Location st i = MultBy(a,b) by SCMFSA_2:57;
hence IncAddr(i,0) = i by SCMFSA_4:12;
suppose InsCode i = 5;
then ex a,b being Int-Location st i = Divide(a,b) by SCMFSA_2:58;
hence IncAddr(i,0) = i by SCMFSA_4:13;
suppose InsCode i = 6;
then consider l being Instruction-Location of SCM+FSA
such that A5: i = goto l by SCMFSA_2:59;
thus IncAddr(i,0) = goto (l + 0) by A5,SCMFSA_4:14
.= i by A5,Th7;
suppose InsCode i = 7;
then consider l being Instruction-Location of SCM+FSA,a being Int-Location
such that A6: i = a =0_goto l by SCMFSA_2:60;
thus IncAddr(i,0) = a =0_goto (l + 0) by A6,SCMFSA_4:15
.= i by A6,Th7;
suppose InsCode i = 8;
then consider l being Instruction-Location of SCM+FSA,a being Int-Location
such that A7: i = a >0_goto l by SCMFSA_2:61;
thus IncAddr(i,0) = a >0_goto (l + 0) by A7,SCMFSA_4:16
.= i by A7,Th7;
suppose InsCode i = 9;
then ex a,b being Int-Location,f being FinSeq-Location
st i = b:=(f,a) by SCMFSA_2:62;
hence IncAddr(i,0) = i by SCMFSA_4:17;
suppose InsCode i = 10;
then ex a,b being Int-Location,f being FinSeq-Location
st i = (f,a):=b by SCMFSA_2:63;
hence IncAddr(i,0) = i by SCMFSA_4:18;
suppose InsCode i = 11;
then ex a being Int-Location,f being FinSeq-Location
st i = a:=len f by SCMFSA_2:64;
hence IncAddr(i,0) = i by SCMFSA_4:19;
suppose InsCode i = 12;
then ex a being Int-Location,f being FinSeq-Location
st i = f:=<0,...,0>a by SCMFSA_2:65;
hence IncAddr(i,0) = i by SCMFSA_4:20;
end;
theorem Th9: ::TMP13
for P being programmed FinPartState of SCM+FSA holds
ProgramPart Relocated(P,0) = P
proof
let P be programmed FinPartState of SCM+FSA;
now let x be set;
hereby assume A1: x in dom P;
dom P c= the Instruction-Locations of SCM+FSA by AMI_3:def 13;
then consider n being Nat such that A2: x = insloc n by A1,SCMFSA_2:21;
thus x in {insloc m:insloc m in dom P} by A1,A2;
end;
assume x in {insloc m:insloc m in dom P};
then consider m being Nat such that A3: x = insloc m & insloc m in dom P;
thus x in dom P by A3;
end;
then A4: dom P = {insloc m:insloc m in dom P} by TARSKI:2;
A5: dom ProgramPart P = dom P by AMI_5:72;
now let x be set;
A6: dom ProgramPart Relocated(P,0) = {insloc (m + 0):insloc m in dom P}
by A5,SCMFSA_5:3;
hereby assume x in dom ProgramPart Relocated(P,0);
then consider n be Nat such that
A7: x = insloc (n + 0) & insloc n in dom P by A6;
thus x in {insloc m:insloc m in dom P} by A7;
end;
assume x in {insloc m:insloc m in dom P};
then consider m being Nat such that A8: x = insloc m & insloc m in dom P;
x = insloc (m + 0) & insloc m in dom P by A8;
hence x in dom ProgramPart Relocated(P,0) by A6;
end;
then A9: dom ProgramPart Relocated(P,0) = {insloc m:insloc m in dom P} by
TARSKI:2;
now let x be set;
assume x in {insloc m:insloc m in dom P};
then consider n being Nat such that
A10: x = insloc n and
A11: insloc n in dom P;
A12: insloc n in dom ProgramPart P by A11,AMI_5:72;
dom Shift(ProgramPart P,0) =
{insloc (m + 0):insloc m in
dom ProgramPart P} by SCMFSA_4:def 7;
then A13: insloc (n + 0) in dom Shift(ProgramPart P,0) by A5,A11;
then A14: pi(Shift(ProgramPart P,0),insloc (n + 0))
= Shift(ProgramPart P,0).insloc (n + 0) by AMI_5:def 5
.= Shift(ProgramPart P,0).(insloc n + 0) by SCMFSA_4:def 1
.= (ProgramPart P).insloc n by A12,SCMFSA_4:30
.= P.insloc n by AMI_5:72;
then consider i being Instruction of SCM+FSA such that A15: i = P.insloc
n;
thus (ProgramPart Relocated(P,0)).x
= IncAddr(Shift(ProgramPart P,0),0).insloc (n + 0) by A10,SCMFSA_5:2
.= IncAddr(i,0) by A13,A14,A15,SCMFSA_4:def 6
.= P.x by A10,A15,Th8;
end;
hence ProgramPart Relocated(P,0) = P by A4,A9,FUNCT_1:9;
end;
theorem Th10: ::TMP15'
for P,Q being FinPartState of SCM+FSA st P c= Q holds
ProgramPart P c= ProgramPart Q
proof
let P,Q be FinPartState of SCM+FSA;
assume A1: P c= Q;
then A2: dom P c= dom Q by GRFUNC_1:8;
A3: ProgramPart P = P | A & ProgramPart Q = Q | A by AMI_5:def 6;
then A4: dom ProgramPart P = dom P /\ A & dom ProgramPart Q = dom Q /\ A
by RELAT_1:90;
then A5: dom ProgramPart P c= dom ProgramPart Q by A2,XBOOLE_1:26;
now let x be set;
assume A6: x in dom ProgramPart P;
then A7: x in dom P by A4,XBOOLE_0:def 3;
thus (ProgramPart P).x = P.x by A3,A6,FUNCT_1:68
.= Q.x by A1,A7,GRFUNC_1:8
.= (ProgramPart Q).x by A3,A5,A6,FUNCT_1:68;
end;
hence ProgramPart P c= ProgramPart Q by A5,GRFUNC_1:8;
end;
theorem Th11: ::TMP18
for P,Q being programmed FinPartState of SCM+FSA, k being Nat st P c= Q holds
Shift(P,k) c= Shift(Q,k)
proof
let P,Q be programmed FinPartState of SCM+FSA;
let k be Nat;
assume A1: P c= Q;
then A2: dom P c= dom Q by GRFUNC_1:8;
A3: dom Shift(P,k) = {insloc (m + k):insloc m in dom P} by SCMFSA_4:def 7;
A4: dom Shift(Q,k) = {insloc (m + k):insloc m in dom Q} by SCMFSA_4:def 7;
now let x be set;
assume x in dom Shift(P,k);
then consider m1 being Nat such that
A5: x = insloc (m1 + k) & insloc m1 in dom P by A3;
thus x in dom Shift(Q,k) by A2,A4,A5;
end;
then A6: dom Shift(P,k) c= dom Shift(Q,k) by TARSKI:def 3;
now let x be set;
assume x in dom Shift(P,k);
then consider m1 being Nat such that
A7: x = insloc (m1 + k) & insloc m1 in dom P by A3;
thus Shift(P,k).x
= Shift(P,k).(insloc m1 + k) by A7,SCMFSA_4:def 1
.= P.insloc m1 by A7,SCMFSA_4:30
.= Q.insloc m1 by A1,A7,GRFUNC_1:8
.= Shift(Q,k).(insloc m1 + k) by A2,A7,SCMFSA_4:30
.= Shift(Q,k).x by A7,SCMFSA_4:def 1;
end;
hence Shift(P,k) c= Shift(Q,k) by A6,GRFUNC_1:8;
end;
theorem Th12: ::TMP15
for P,Q being FinPartState of SCM+FSA, k being Nat st P c= Q holds
ProgramPart Relocated(P,k) c= ProgramPart Relocated(Q,k)
proof
let P,Q be FinPartState of SCM+FSA;
let k be Nat;
assume A1: P c= Q;
set rP = Relocated(P,k);
set rQ = Relocated(Q,k);
A2: dom ProgramPart rP = {insloc (m + k):insloc m in dom ProgramPart P}
by SCMFSA_5:3;
A3: ProgramPart rP = IncAddr(Shift(ProgramPart P,k),k) by SCMFSA_5:2;
A4: ProgramPart rQ = IncAddr(Shift(ProgramPart Q,k),k) by SCMFSA_5:2;
A5: ProgramPart P c= ProgramPart Q by A1,Th10;
then A6: Shift(ProgramPart P,k) c= Shift(ProgramPart Q,k) by Th11;
then A7: dom Shift(ProgramPart P,k) c= dom Shift(ProgramPart Q,k) by GRFUNC_1:8
;
A8: dom ProgramPart P c= dom ProgramPart Q by A5,GRFUNC_1:8;
now let x be set;
assume x in dom ProgramPart rP;
then x in dom Shift(ProgramPart P,k) by A3,SCMFSA_4:def 6;
then x in dom Shift(ProgramPart Q,k) by A7;
hence x in dom ProgramPart rQ by A4,SCMFSA_4:def 6;
end;
then A9: dom ProgramPart rP c= dom ProgramPart rQ by TARSKI:def 3;
A10: dom Shift(ProgramPart P,k) = {insloc (m + k):insloc m in
dom ProgramPart P}
by SCMFSA_4:def 7;
A11: dom Shift(ProgramPart Q,k) = {insloc (m + k):insloc m in
dom ProgramPart Q}
by SCMFSA_4:def 7;
now let x be set;
assume x in dom ProgramPart rP;
then consider m1 being Nat such that
A12: x = insloc (m1 + k) & insloc m1 in dom ProgramPart P by A2;
A13: insloc (m1 + k) in dom Shift(ProgramPart P,k) &
insloc (m1 + k) in dom Shift(ProgramPart Q,k) by A8,A10,A11,A12;
then A14: pi(Shift(ProgramPart P,k),insloc (m1 + k))
= Shift(ProgramPart P,k).insloc (m1 + k) by AMI_5:def 5
.= Shift(ProgramPart Q,k).insloc (m1 + k) by A6,A13,GRFUNC_1:8
.= pi(Shift(ProgramPart Q,k),insloc (m1 + k)) by A13,AMI_5:def 5;
thus (ProgramPart rP).x
= IncAddr(Shift(ProgramPart P,k),k).insloc (m1 + k) by A12,SCMFSA_5:2
.= IncAddr(pi(Shift(ProgramPart Q,k),insloc (m1 + k)),k) by A13,A14,
SCMFSA_4:def 6
.= IncAddr(Shift(ProgramPart Q,k),k).insloc (m1 + k) by A13,SCMFSA_4:def
6
.= (ProgramPart rQ).x by A12,SCMFSA_5:2;
end;
hence ProgramPart rP c= ProgramPart rQ by A9,GRFUNC_1:8;
end;
theorem Th13: ::TMP16
for I,J being Macro-Instruction, k being Nat st
card I <= k & k < card I + card J holds
for i being Instruction of SCM+FSA st i = J.insloc (k -' card I) holds
(I ';' J).insloc k = IncAddr(i,card I)
proof
let I,J be Macro-Instruction;
let k be Nat;
assume A1: card I <= k;
assume k < card I + card J;
then A2: k + 0 < card J + card I;
let i be Instruction of SCM+FSA;
assume A3: i = J.insloc (k -' card I);
A4: I ';' J = Directed I +* ProgramPart Relocated(J,card I) by SCMFSA6A:def 4;
k -' card I = k - card I by A1,SCMFSA_7:3;
then A5: k -' card I < card J - 0 by A2,REAL_2:168;
ProgramPart J = J by AMI_5:72;
then A6: insloc (k -' card I) in dom ProgramPart J by A5,SCMFSA6A:15;
A7: k -' card I + card I = k - card I + card I by A1,SCMFSA_7:3
.= k by XCMPLX_1:27;
then A8: insloc (k -' card I) + card I = insloc k by SCMFSA_4:def 1;
insloc k in {insloc (m + card I):insloc m in
dom ProgramPart J} by A6,A7;
then A9: insloc k in dom ProgramPart Relocated(J, card I) by SCMFSA_5:3;
hence (I ';' J).insloc k
= (ProgramPart Relocated(J,card I)).insloc k by A4,FUNCT_4:14
.= Relocated(J,card I).insloc k by A9,SCMFSA8A:49
.= IncAddr(i,card I) by A3,A6,A8,SCMFSA_5:7;
end;
theorem Th14: ::T22246 ---???
for s being State of SCM+FSA st s.intloc 0 = 1 & IC s = insloc 0 holds
Initialize s = s
proof
let s be State of SCM+FSA;
assume A1: s.intloc 0 = 1;
assume IC s = insloc 0;
then A2: s.IC SCM+FSA = insloc 0 by AMI_1:def 15;
A3: intloc 0 in dom s & IC SCM+FSA in dom s by AMI_5:25,SCMFSA_2:66;
thus Initialize s
= s +* (intloc 0 .--> 1) +* Start-At insloc 0 by SCMFSA6C:def 3
.= s +* Start-At insloc 0 by A1,A3,Th6
.= s +* (IC SCM+FSA .--> insloc 0) by AMI_3:def 12
.= s by A2,A3,Th6;
end;
theorem Th15: ::T200922
for s being State of SCM+FSA holds
Initialize Initialize s = Initialize s
proof
let s be State of SCM+FSA;
(Initialize s).intloc 0 = 1 & IC Initialize s = insloc 0 by SCMFSA6C:3;
hence Initialize Initialize s = Initialize s by Th14;
end;
theorem Th16: ::TMP6
for s being State of SCM+FSA, I being Macro-Instruction holds
s +* (Initialized I +* Start-At insloc 0) =
Initialize s +* (I +* Start-At insloc 0)
proof
let s be State of SCM+FSA;
let I be Macro-Instruction;
Start-At insloc 0 c= Initialized I by SCMFSA6B:4;
hence s +* (Initialized I +* Start-At insloc 0)
= s +* Initialized I by AMI_5:10
.= Initialize s +* (I +* Start-At insloc 0) by SCMFSA8A:13;
end;
theorem Th17: ::T200938
for s being State of SCM+FSA, I being Macro-Instruction holds
IExec(I,s) = IExec(I,Initialize s)
proof
let s be State of SCM+FSA;
let I be Macro-Instruction;
dom s = D \/ {IC SCM+FSA} \/ A by SCMFSA6A:34;
then A1: A c= dom s by XBOOLE_1:7;
dom Initialize s = D \/ {IC SCM+FSA} \/ A by SCMFSA6A:34;
then A2: A c= dom Initialize s by XBOOLE_1:7;
for x be set st x in A holds s.x = (Initialize s).x by SCMFSA6C:3;
then A3: s | A = (Initialize s) | A by A1,A2,SCMFSA6A:9;
thus IExec(I,s) = Result (s +* Initialized I) +* s | A by SCMFSA6B:def 1
.= Result (Initialize s +* Initialized I) +* s | A by SCMFSA8A:8
.= IExec(I,Initialize s) by A3,SCMFSA6B:def 1;
end;
theorem Th18: ::T26401 --- ???
for s being State of SCM+FSA, I being Macro-Instruction
st s.intloc 0 = 1 holds
s +* (I +* Start-At insloc 0) = s +* Initialized I
proof
let s be State of SCM+FSA;
let I be Macro-Instruction;
assume A1: s.intloc 0 = 1;
intloc 0 in dom s by SCMFSA_2:66;
then A2: s = s +* (intloc 0 .--> 1) by A1,Th6;
thus s +* Initialized I
= Initialize s +* (I +* Start-At insloc 0) by SCMFSA8A:13
.= Initialize s +* I +* Start-At insloc 0 by FUNCT_4:15
.= Initialize s +* Start-At insloc 0 +* I by SCMFSA6B:14
.= s +* Start-At insloc 0 +* Start-At insloc 0 +* I by A2,SCMFSA6C:def 3
.= s +* (Start-At insloc 0 +* Start-At insloc 0) +* I by FUNCT_4:15
.= s +* I +* Start-At insloc 0 by SCMFSA6B:14
.= s +* (I +* Start-At insloc 0) by FUNCT_4:15;
end;
theorem Th19: ::T24634 --- ???
for I being Macro-Instruction holds
I +* Start-At insloc 0 c= Initialized I
proof
let I be Macro-Instruction;
I c= Initialized I & Start-At insloc 0 c= Initialized I
by SCMFSA6A:26,SCMFSA6B:4;
hence I +* Start-At insloc 0 c= Initialized I by SCMFSA6A:6;
end;
theorem Th20: ::TMP10
for l being Instruction-Location of SCM+FSA, I being Macro-Instruction holds
l in dom I iff l in dom Initialized I
proof
let l be Instruction-Location of SCM+FSA;
let I be Macro-Instruction;
A1: (Initialized I) | the Instruction-Locations of SCM+FSA = I by SCMFSA6A:33;
A2: dom ((Initialized I) | the Instruction-Locations of SCM+FSA) c=
dom Initialized I by FUNCT_1:76;
A3: dom ((Initialized I) | the Instruction-Locations of SCM+FSA) =
dom Initialized I /\ the Instruction-Locations of SCM+FSA by RELAT_1:90;
thus l in dom I implies l in dom Initialized I by A1,A2;
assume l in dom Initialized I;
hence l in dom I by A1,A3,XBOOLE_0:def 3;
end;
theorem
for s being State of SCM+FSA, I being Macro-Instruction holds
Initialized I is_closed_on s iff I is_closed_on Initialize s
proof
let s be State of SCM+FSA;
let I be Macro-Instruction;
hereby assume A1: Initialized I is_closed_on s;
now let k be Nat;
IC (Computation (s +* (Initialized I +* Start-At insloc 0))).k in
dom Initialized I by A1,SCMFSA7B:def 7;
then IC (Computation (Initialize s +* (I +* Start-At insloc 0))).k in
dom Initialized I by Th16;
hence IC (Computation (Initialize s +* (I +* Start-At insloc 0))).k
in
dom I by Th20;
end;
hence I is_closed_on Initialize s by SCMFSA7B:def 7;
end;
assume A2: I is_closed_on Initialize s;
now let k be Nat;
IC (Computation (Initialize s +* (I +* Start-At insloc 0))).k in
dom I by A2,SCMFSA7B:def 7;
then IC (Computation (Initialize s +* (I +* Start-At insloc 0))).k in
dom Initialized I by Th20;
hence IC (Computation (s +* (Initialized I +* Start-At insloc 0))).k in
dom Initialized I by Th16;
end;
hence Initialized I is_closed_on s by SCMFSA7B:def 7;
end;
theorem Th22: ::TMP5
for s being State of SCM+FSA, I being Macro-Instruction holds
Initialized I is_halting_on s iff I is_halting_on Initialize s
proof
let s be State of SCM+FSA;
let I be Macro-Instruction;
hereby assume Initialized I is_halting_on s;
then s +* (Initialized I +* Start-At insloc 0) is halting
by SCMFSA7B:def 8;
then Initialize s +* (I +* Start-At insloc 0) is halting by Th16;
hence I is_halting_on Initialize s by SCMFSA7B:def 8;
end;
assume I is_halting_on Initialize s;
then Initialize s +* (I +* Start-At insloc 0) is halting
by SCMFSA7B:def 8;
then s +* (Initialized I +* Start-At insloc 0) is halting by Th16;
hence Initialized I is_halting_on s by SCMFSA7B:def 8;
end;
theorem
for I being Macro-Instruction holds
(for s being State of SCM+FSA holds I is_halting_on Initialize s) implies
Initialized I is halting
proof
let I be Macro-Instruction;
assume A1: for s being State of SCM+FSA holds I is_halting_on Initialize s;
now let s be State of SCM+FSA;
assume A2: Initialized I c= s;
I is_halting_on Initialize s by A1;
then Initialize s +* (I +* Start-At insloc 0) is halting
by SCMFSA7B:def 8;
then s +* Initialized I is halting by SCMFSA8A:13;
hence s is halting by A2,AMI_5:10;
end;
hence Initialized I is halting by AMI_1:def 26;
end;
theorem Th24: ::TMP3'
for I being Macro-Instruction holds
(for s being State of SCM+FSA holds Initialized I is_halting_on s) implies
Initialized I is halting
proof
let I be Macro-Instruction;
assume A1: for s being State of SCM+FSA holds Initialized I is_halting_on s;
now let s be State of SCM+FSA;
assume A2: Initialized I c= s;
Initialized I is_halting_on s by A1;
then A3: s +* (Initialized I +* Start-At insloc 0) is halting by SCMFSA7B:
def 8;
Start-At insloc 0 c= Initialized I by SCMFSA6B:4;
then s +* (Initialized I +* Start-At insloc 0)
= s +* Initialized I by AMI_5:10;
hence s is halting by A2,A3,AMI_5:10;
end;
hence Initialized I is halting by AMI_1:def 26;
end;
theorem Th25: ::TMP9
for I being Macro-Instruction holds
ProgramPart Initialized I = I
proof
let I be Macro-Instruction;
thus ProgramPart Initialized I
= (Initialized I) | the Instruction-Locations of SCM+FSA by AMI_5:def 6
.= I by SCMFSA6A:33;
end;
theorem Th26: ::T18750
for s being State of SCM+FSA, I being Macro-Instruction,
l being Instruction-Location of SCM+FSA, x being set holds
x in dom I implies I.x = (s +* (I +* Start-At l)).x
proof
let s be State of SCM+FSA;
let I be Macro-Instruction;
let l be Instruction-Location of SCM+FSA;
let x be set;
assume A1: x in dom I;
dom I c= the Instruction-Locations of SCM+FSA by AMI_3:def 13;
then reconsider y = x as Instruction-Location of SCM+FSA by A1;
A2: not y in dom Start-At l by SCMFSA6B:11;
x in dom (I +* Start-At l) by A1,FUNCT_4:13;
hence (s +* (I +* Start-At l)).x = (I +* Start-At l).x by FUNCT_4:14
.= I.x by A2,FUNCT_4:12;
end;
theorem Th27: ::T22246' ---???
for s being State of SCM+FSA st s.intloc 0 = 1 holds
(Initialize s) | (Int-Locations \/ FinSeq-Locations) =
s | (Int-Locations \/ FinSeq-Locations)
proof
let s be State of SCM+FSA;
assume A1: s.intloc 0 = 1;
A2: intloc 0 in dom s & IC SCM+FSA in dom s by AMI_5:25,SCMFSA_2:66;
Initialize s
= s +* (intloc 0 .--> 1) +* Start-At insloc 0 by SCMFSA6C:def 3
.= s +* Start-At insloc 0 by A1,A2,Th6;
hence thesis by SCMFSA8A:10;
end;
theorem Th28: ::T210615
for s being State of SCM+FSA, I being Macro-Instruction,
a being Int-Location, l being Instruction-Location of SCM+FSA holds
(s +* (I +* Start-At l)).a = s.a
proof
let s be State of SCM+FSA;
let I be Macro-Instruction;
let a be Int-Location;
let l be Instruction-Location of SCM+FSA;
a in dom s & not a in dom (I +* Start-At l) by SCMFSA6B:12,SCMFSA_2:66;
hence (s +* (I +* Start-At l)).a = s.a by FUNCT_4:12;
end;
theorem
for I being programmed FinPartState of SCM+FSA,
l being Instruction-Location of SCM+FSA holds
IC SCM+FSA in dom (I +* Start-At l)
proof
let I be programmed FinPartState of SCM+FSA;
let l be Instruction-Location of SCM+FSA;
dom Start-At l = {IC SCM+FSA} by AMI_3:34;
then IC SCM+FSA in dom Start-At l by TARSKI:def 1;
hence IC SCM+FSA in dom (I +* Start-At l) by FUNCT_4:13;
end;
theorem
for I being programmed FinPartState of SCM+FSA,
l being Instruction-Location of SCM+FSA holds
(I +* Start-At l).IC SCM+FSA = l
proof
let I be programmed FinPartState of SCM+FSA;
let l be Instruction-Location of SCM+FSA;
dom Start-At l = {IC SCM+FSA} by AMI_3:34;
then A1: IC SCM+FSA in dom Start-At l by TARSKI:def 1;
Start-At l = IC SCM+FSA .--> l by AMI_3:def 12;
then (Start-At l).IC SCM+FSA = l by CQC_LANG:6;
hence (I +* Start-At l).IC SCM+FSA = l by A1,FUNCT_4:14;
end;
theorem Th31: ::T4633 -- ??
for s being State of SCM+FSA, P being FinPartState of SCM+FSA,
l being Instruction-Location of SCM+FSA holds
IC (s +* (P +* Start-At l)) = l
proof
let s be State of SCM+FSA;
let I be FinPartState of SCM+FSA;
let l be Instruction-Location of SCM+FSA;
thus IC (s +* (I +* Start-At l))
= IC (s +* I +* Start-At l) by FUNCT_4:15
.= l by AMI_5:79;
end;
theorem Th32: ::T30408
for s being State of SCM+FSA, i being Instruction of SCM+FSA st
InsCode i in {0,6,7,8} holds
Exec(i,s) | (Int-Locations \/ FinSeq-Locations) =
s | (Int-Locations \/ FinSeq-Locations)
proof
let s be State of SCM+FSA;
let i be Instruction of SCM+FSA;
assume A1: InsCode i in {0,6,7,8};
now
let a be Int-Location;
let f be FinSeq-Location;
per cases by A1,ENUMSET1:18;
suppose InsCode i = 0;
then i = halt SCM+FSA by SCMFSA_2:122;
hence Exec(i,s).a = s.a & Exec(i,s).f = s.f by AMI_1:def 8;
suppose InsCode i = 6;
then consider lb being Instruction-Location of SCM+FSA such that
A2: i = goto lb by SCMFSA_2:59;
thus Exec(i,s).a = s.a & Exec(i,s).f = s.f by A2,SCMFSA_2:95;
suppose InsCode i = 7;
then consider lb being Instruction-Location of SCM+FSA, b being
Int-Location
such that
A3: i = b=0_goto lb by SCMFSA_2:60;
thus Exec(i,s).a = s.a & Exec(i,s).f = s.f by A3,SCMFSA_2:96;
suppose InsCode i = 8;
then consider lb being Instruction-Location of SCM+FSA, b being
Int-Location
such that
A4: i = b>0_goto lb by SCMFSA_2:61;
thus Exec(i,s).a = s.a & Exec(i,s).f = s.f by A4,SCMFSA_2:97;
end;
hence thesis by SCMFSA6A:38;
end;
theorem Th33: ::T271245 --- ???
for s1,s2 being State of SCM+FSA st
s1.intloc 0 = s2.intloc 0 &
((for a being read-write Int-Location holds s1.a = s2.a) &
for f being FinSeq-Location holds s1.f = s2.f) holds
s1 | (Int-Locations \/ FinSeq-Locations) =
s2 | (Int-Locations \/ FinSeq-Locations)
proof
let s1,s2 be State of SCM+FSA;
assume A1: s1.intloc 0 = s2.intloc 0;
assume A2: for a being read-write Int-Location holds s1.a = s2.a;
assume A3: for f being FinSeq-Location holds s1.f = s2.f;
A4: dom (s1 | D) = dom s1 /\ D by RELAT_1:90
.= (Int-Locations \/ FinSeq-Locations \/ {IC SCM+FSA} \/
the Instruction-Locations of SCM+FSA) /\ D by SCMFSA6A:34
.= dom s2 /\ D by SCMFSA6A:34
.= dom (s2 | D) by RELAT_1:90;
now let x be set;
assume A5: x in dom (s1 | D);
then A6: x in dom s1 /\ D by RELAT_1:90;
then A7: x in dom s1 & x in D by XBOOLE_0:def 3;
per cases by A7,SCMFSA6A:35;
suppose A8: x is Int-Location;
hereby per cases;
suppose A9: x is read-write Int-Location;
thus (s1 | D).x = s1.x by A5,FUNCT_1:70
.= s2.x by A2,A9
.= (s2 | D).x by A4,A5,FUNCT_1:70;
suppose A10: not x is read-write Int-Location;
reconsider a = x as Int-Location by A8;
a = intloc 0 by A10,SF_MASTR:def 5;
hence (s1 | D).x = s2.a by A1,A5,FUNCT_1:70
.= (s2 | D).x by A4,A5,FUNCT_1:70;
end;
suppose A11: x is FinSeq-Location;
thus (s1 | D).x = s1.x by A5,FUNCT_1:70
.= s2.x by A3,A11
.= (s2 | D).x by A4,A5,FUNCT_1:70;
suppose A12: x = IC SCM+FSA;
assume not (s1 | D).x = (s2 | D).x;
thus contradiction by A6,A12,SCMFSA6A:37,XBOOLE_0:def 3;
suppose A13: x is Instruction-Location of SCM+FSA;
assume not (s1 | D).x = (s2 | D).x;
thus contradiction by A7,A13,SCMFSA6A:37;
end;
then s1 | D c= s2 | D by A4,GRFUNC_1:8;
hence s1 | D = s2 | D by A4,GRFUNC_1:9;
end;
theorem
for s being State of SCM+FSA,P being programmed FinPartState of SCM+FSA
holds
(s +* P) | (Int-Locations \/ FinSeq-Locations) =
s | (Int-Locations \/ FinSeq-Locations)
proof
let s be State of SCM+FSA;
let P be programmed FinPartState of SCM+FSA;
A1: dom P c= A by AMI_3:def 13;
A misses D by SCMFSA_2:13,14,XBOOLE_1:70;
then dom P misses D by A1,XBOOLE_1:63;
hence thesis by AMI_5:7;
end;
theorem Th35: ::T1643 --- ??
for s,ss being State of SCM+FSA holds
(s +* ss | the Instruction-Locations of SCM+FSA) |
(Int-Locations \/ FinSeq-Locations) =
s | (Int-Locations \/ FinSeq-Locations)
proof
let s,ss be State of SCM+FSA;
dom (ss | A) = dom ss /\ A by RELAT_1:90
.= (Int-Locations \/ FinSeq-Locations \/ {IC SCM+FSA} \/ A) /\
A by SCMFSA6A:34
.= A by XBOOLE_1:21;
then dom (ss | A) misses D by SCMFSA_2:13,14,XBOOLE_1:70;
hence thesis by AMI_5:7;
end;
theorem Th36: ::T27643 --- ???
for s being State of SCM+FSA holds
(Initialize s) | the Instruction-Locations of SCM+FSA =
s | the Instruction-Locations of SCM+FSA
proof
let s be State of SCM+FSA;
A1: Initialize s
= s +* (intloc 0 .--> 1) +* Start-At insloc 0 by SCMFSA6C:def 3
.= s +* ((intloc 0 .--> 1) +* Start-At insloc 0) by FUNCT_4:15;
now let x be set;
assume A2: x in A;
then A3: not x in dom Start-At insloc 0 by SCMFSA6B:11;
x <> intloc 0 & dom (intloc 0 .--> 1) = {intloc 0}
by A2,CQC_LANG:5,SCMFSA_2:84;
then not x in dom (intloc 0 .--> 1) by TARSKI:def 1;
hence not x in dom (intloc 0 .--> 1) \/ dom Start-At insloc 0
by A3,XBOOLE_0:def 2;
end;
then dom (intloc 0 .--> 1) \/ dom Start-At insloc 0 misses A by XBOOLE_0:3;
then dom ((intloc 0 .--> 1) +* Start-At insloc 0) misses A by FUNCT_4:def 1
;
hence thesis by A1,SCMFSA8A:2;
end;
theorem Th37: ::T26530 --- ???
for s,ss being State of SCM+FSA, I being Macro-Instruction holds
(ss +* (s | (the Instruction-Locations of SCM+FSA))) |
(Int-Locations \/ FinSeq-Locations) =
ss | (Int-Locations \/ FinSeq-Locations)
proof
let s,ss be State of SCM+FSA;
let I be Macro-Instruction;
dom (s | A) = A & A misses D by SCMFSA8A:3,SCMFSA_2:13,14,XBOOLE_1:70
;
hence thesis by SCMFSA8A:2;
end;
theorem Th38: ::T27500 ue
for s being State of SCM+FSA holds
IExec(SCM+FSA-Stop,s) = Initialize s +* Start-At insloc 0
proof
let s be State of SCM+FSA;
set s1 = Initialize s +* (SCM+FSA-Stop +* Start-At insloc 0);
A1: s +* Initialized SCM+FSA-Stop = s1 by SCMFSA8A:13;
then Initialized SCM+FSA-Stop c= s1 by FUNCT_4:26;
then IC s1 = insloc 0 by SCMFSA6B:34;
then CurInstr s1 = s1.insloc 0 by AMI_1:def 17
.= SCM+FSA-Stop.insloc 0 by Th26,SCMFSA8A:16;
then A2: CurInstr s1 = halt SCM+FSA & s1 = (Computation s1).0
by AMI_1:def 19,SCMFSA8A:16;
then A3: s1 is halting by AMI_1:def 20;
A4: IExec(SCM+FSA-Stop,s) = Result (s +* Initialized SCM+FSA-Stop) +* s | A
by SCMFSA6B:def 1;
then A5: IExec(SCM+FSA-Stop,s) = s1 +* s | A by A1,A2,A3,AMI_1:def 22;
then A6: IExec(SCM+FSA-Stop,s) | D = s1 | D by Th37
.= (Initialize s) | D by SCMFSA8A:11;
hereby
A7: dom IExec(SCM+FSA-Stop,s) = the carrier of SCM+FSA by AMI_3:36
.= dom (Initialize s +* Start-At insloc 0) by AMI_3:36;
A8: dom Start-At insloc 0 = {IC SCM+FSA} by AMI_3:34;
now let x be set;
assume A9: x in dom IExec(SCM+FSA-Stop,s);
per cases by A9,SCMFSA6A:35;
suppose A10: x is Int-Location;
then A11: IExec(SCM+FSA-Stop,s).x = (Initialize s).x by A6,SCMFSA6A:38;
x <> IC SCM+FSA by A10,SCMFSA_2:81;
then not x in dom Start-At insloc 0 by A8,TARSKI:def 1;
hence IExec(SCM+FSA-Stop,s).x
= (Initialize s +* Start-At insloc 0).x by A11,FUNCT_4:12;
suppose A12: x is FinSeq-Location;
then A13: IExec(SCM+FSA-Stop,s).x = (Initialize s).x by A6,SCMFSA6A:38;
x <> IC SCM+FSA by A12,SCMFSA_2:82;
then not x in dom Start-At insloc 0 by A8,TARSKI:def 1;
hence IExec(SCM+FSA-Stop,s).x
= (Initialize s +* Start-At insloc 0).x by A13,FUNCT_4:12;
suppose A14: x = IC SCM+FSA;
then x in {IC SCM+FSA} by TARSKI:def 1;
then A15: x in dom Start-At insloc 0 by AMI_3:34;
not x in A by A14,AMI_1:48;
then not x in dom s /\ A by XBOOLE_0:def 3;
then x in dom s1 & not x in dom (s | A) by A14,RELAT_1:90,SCMFSA8B:1;
hence IExec(SCM+FSA-Stop,s).x
= s1.IC SCM+FSA by A5,A14,FUNCT_4:12
.= (Initialize s +* SCM+FSA-Stop +* Start-At insloc 0).IC SCM+FSA
by FUNCT_4:15
.= (Start-At insloc 0).IC SCM+FSA by A14,A15,FUNCT_4:14
.= (Initialize s +* Start-At insloc 0).x by A14,A15,FUNCT_4:14;
suppose A16: x is Instruction-Location of SCM+FSA;
IExec(SCM+FSA-Stop,s) | A = s | A by A4,SCMFSA6A:40
.= (Initialize s) | A by Th36;
then A17: IExec(SCM+FSA-Stop,s).x = (Initialize s).x by A16,SCMFSA6A:36;
x <> IC SCM+FSA by A16,AMI_1:48;
then not x in dom Start-At insloc 0 by A8,TARSKI:def 1;
hence IExec(SCM+FSA-Stop,s).x = (Initialize s +* Start-At insloc 0).x
by A17,FUNCT_4:12;
end;
hence thesis by A7,FUNCT_1:9;
end;
end;
theorem Th39: ::T9x
for s being State of SCM+FSA,I being Macro-Instruction
st I is_closed_on s holds insloc 0 in dom I
proof
let s be State of SCM+FSA;
let I be Macro-Instruction;
assume A1: I is_closed_on s;
consider n being Nat such that
A2: insloc n = IC (Computation (s +* (I +* Start-At insloc 0))).0
by SCMFSA_2:21;
A3: insloc n in dom I by A1,A2,SCMFSA7B:def 7;
per cases by NAT_1:19;
suppose n = 0;
hence insloc 0 in dom I by A1,A2,SCMFSA7B:def 7;
suppose 0 < n;
hence insloc 0 in dom I by A3,SCMFSA_4:def 4;
end;
theorem
for s being State of SCM+FSA,I being paraclosed Macro-Instruction holds
insloc 0 in dom I
proof
let s be State of SCM+FSA;
let I be paraclosed Macro-Instruction;
I is_closed_on s by SCMFSA7B:24;
hence insloc 0 in dom I by Th39;
end;
theorem Th41: ::Tm1(@BBB8)
for i being Instruction of SCM+FSA holds
rng Macro i = {i,halt SCM+FSA}
proof
let i be Instruction of SCM+FSA;
A1: Macro i = (insloc 0,insloc 1) --> (i,halt SCM+FSA) by SCMFSA6A:def 2;
insloc 0 <> insloc 1 by SCMFSA_2:18;
hence rng Macro i = {i,halt SCM+FSA} by A1,FUNCT_4:67;
end;
theorem Th42: ::T0x
for s1,s2 being State of SCM+FSA,I being Macro-Instruction st
I is_closed_on s1 & I +* Start-At insloc 0 c= s1
for n being Nat st ProgramPart Relocated(I,n) c= s2 &
IC s2 = insloc n &
s1 | (Int-Locations \/ FinSeq-Locations) =
s2 | (Int-Locations \/ FinSeq-Locations)
for i being Nat holds
IC (Computation s1).i + n = IC (Computation s2).i &
IncAddr(CurInstr ((Computation s1).i),n) = CurInstr ((Computation s2).i) &
(Computation s1).i | (Int-Locations \/ FinSeq-Locations)
= (Computation s2).i | (Int-Locations \/ FinSeq-Locations)
proof
let s1,s2 be State of SCM+FSA;
let J be Macro-Instruction;
assume A1: J is_closed_on s1;
assume
A2: J +* Start-At insloc 0 c= s1;
set JAt = J +* Start-At insloc 0;
let n be Nat; assume that
A3: ProgramPart Relocated(J,n) c= s2 and
A4: IC s2 = insloc n and
A5: s1 | (Int-Locations \/ FinSeq-Locations)
= s2 | (Int-Locations \/ FinSeq-Locations);
set C1 = Computation s1;
set C2 = Computation s2;
let i be Nat;
defpred P[Nat] means
IC C1.$1 + n = IC C2.$1 &
IncAddr(CurInstr (C1.$1),n) = CurInstr (C2.$1) &
C1.$1 | (Int-Locations \/ FinSeq-Locations)
= C2.$1 | (Int-Locations \/ FinSeq-Locations);
A6: ProgramPart Relocated(J,n)
= Relocated(J,n) | the Instruction-Locations of SCM+FSA by AMI_5:def 6;
A7: P[0]
proof
A8: IC SCM+FSA in dom JAt by SF_MASTR:65;
insloc 0 in dom J by A1,Th39;
then insloc 0 + n in dom Relocated(J,n) by SCMFSA_5:4;
then insloc 0 + n in dom ProgramPart Relocated(J,n) by AMI_5:73;
then A9: insloc (0 + n) in dom ProgramPart Relocated(J,n) by SCMFSA_4:def 1;
IC C1.0 = IC s1 by AMI_1:def 19
.= s1.IC SCM+FSA by AMI_1:def 15
.= (JAt).IC SCM+FSA by A2,A8,GRFUNC_1:8
.= insloc 0 by SF_MASTR:66;
hence IC C1.0 + n = insloc (0 + n) by SCMFSA_4:def 1
.= IC C2.0 by A4,AMI_1:def 19;
dom J misses dom Start-At insloc 0 by SF_MASTR:64;
then A10: J c= JAt by FUNCT_4:33;
then A11: dom J c= dom JAt by GRFUNC_1:8;
A12: insloc 0 in dom J by A1,Th39;
A13: s1.IC s1 = s1.(s1.IC SCM+FSA) by AMI_1:def 15
.= s1.((JAt).IC SCM+FSA) by A2,A8,GRFUNC_1:8
.= s1.insloc 0 by SF_MASTR:66
.= (JAt).insloc 0 by A2,A11,A12,GRFUNC_1:8
.= J.insloc 0 by A10,A12,GRFUNC_1:8;
ProgramPart J = J by AMI_5:72;
then A14: insloc 0 in dom ProgramPart J by A1,Th39;
thus IncAddr(CurInstr (C1.0),n)
= IncAddr(CurInstr s1,n) by AMI_1:def 19
.= IncAddr(s1.IC s1,n) by AMI_1:def 17
.= Relocated(J,n).(insloc 0 + n) by A13,A14,SCMFSA_5:7
.= Relocated(J,n).insloc (0 + n) by SCMFSA_4:def 1
.= (ProgramPart Relocated(J,n)).insloc n by A6,FUNCT_1:72
.= s2.IC s2 by A3,A4,A9,GRFUNC_1:8
.= CurInstr s2 by AMI_1:def 17
.= CurInstr (C2.0) by AMI_1:def 19;
thus C1.0 | (Int-Locations \/ FinSeq-Locations)
= s2 | (Int-Locations \/ FinSeq-Locations) by A5,AMI_1:def 19
.= C2.0 | (Int-Locations \/ FinSeq-Locations) by AMI_1:def 19;
end;
A15: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume A16: P[k];
A17: C1.(k + 1) = Following C1.k by AMI_1:def 19
.= Exec(CurInstr C1.k,C1.k) by AMI_1:def 18;
A18: C2.(k + 1) = Following C2.k by AMI_1:def 19
.= Exec(CurInstr C2.k,C2.k) by AMI_1:def 18;
hence A19: IC C1.(k + 1) + n
= IC C2.(k + 1) by A16,A17,SCMFSA6A:41;
reconsider j = CurInstr C1.(k + 1) as Instruction of SCM+FSA;
reconsider l = IC C1.(k + 1) as Instruction-Location of SCM+FSA;
dom J misses dom Start-At insloc 0 by SF_MASTR:64;
then A20: J c= JAt by FUNCT_4:33;
then A21: dom J c= dom JAt by GRFUNC_1:8;
s1 +* (J +* Start-At insloc 0) = s1 by A2,AMI_5:10;
then A22: IC C1.(k + 1) in dom J by A1,SCMFSA7B:def 7;
ProgramPart J = J | the Instruction-Locations of SCM+FSA
by AMI_5:def 6;
then dom ProgramPart J = dom J /\ the Instruction-Locations of SCM+FSA
by FUNCT_1:68;
then A23: l in dom ProgramPart J by A22,XBOOLE_0:def 3;
A24: j = C1.(k + 1).IC C1.(k + 1) by AMI_1:def 17
.= s1.IC C1.(k + 1) by AMI_1:54
.= (JAt).IC C1.(k + 1) by A2,A21,A22,GRFUNC_1:8
.= J.l by A20,A22,GRFUNC_1:8;
IC C2.(k + 1) in dom Relocated(J,n) by A19,A22,SCMFSA_5:4;
then IC C2.(k + 1) in
dom Relocated(J,n) /\ the Instruction-Locations of SCM+FSA
by XBOOLE_0:def 3;
then A25: IC C2.(k + 1) in dom ProgramPart Relocated(J,n) by A6,FUNCT_1:68;
thus IncAddr(CurInstr C1.(k + 1),n)
= Relocated(J,n).(l + n) by A23,A24,SCMFSA_5:7
.= (ProgramPart Relocated(J,n)).(IC C2.(k + 1)) by A6,A19,FUNCT_1:72
.= s2.IC C2.(k + 1) by A3,A25,GRFUNC_1:8
.= C2.(k + 1).IC C2.(k + 1) by AMI_1:54
.= CurInstr C2.(k + 1) by AMI_1:def 17;
thus C1.(k + 1) | (Int-Locations \/ FinSeq-Locations)
= C2.(k + 1) | (Int-Locations \/
FinSeq-Locations) by A16,A17,A18,SCMFSA6A:41;
end;
for k being Nat holds P[k] from Ind(A7,A15);
hence thesis;
end;
theorem Th43: ::T24441
for s1,s2 being State of SCM+FSA,I being Macro-Instruction st
I is_closed_on s1 &
I +* Start-At insloc 0 c= s1 & I +* Start-At insloc 0 c= s2 &
s1 | (Int-Locations \/ FinSeq-Locations) =
s2 | (Int-Locations \/ FinSeq-Locations)
for i being Nat holds
IC (Computation s1).i = IC (Computation s2).i &
CurInstr (Computation s1).i = CurInstr (Computation s2).i &
(Computation s1).i | (Int-Locations \/ FinSeq-Locations) =
(Computation s2).i | (Int-Locations \/ FinSeq-Locations)
proof
let s1,s2 be State of SCM+FSA;
let J be Macro-Instruction;
assume A1: J is_closed_on s1 &
J +* Start-At insloc 0 c= s1 & J +* Start-At insloc 0 c= s2 &
s1 | (Int-Locations \/ FinSeq-Locations) =
s2 | (Int-Locations \/ FinSeq-Locations);
let i be Nat;
A2: IC (Computation s1).i + 0 = IC (Computation s1).i by Th7;
A3: s2 = s2 +* (J +* Start-At insloc 0) by A1,AMI_5:10
.= s2 +* J +* Start-At insloc 0 by FUNCT_4:15
.= s2 +* Start-At insloc 0 +* J by SCMFSA6B:14;
ProgramPart Relocated(J,0) = J by Th9;
then A4: ProgramPart Relocated(J,0) c= s2 by A3,FUNCT_4:26;
A5: IncAddr(CurInstr (Computation s1).i,0) = CurInstr (Computation s1).i
by Th8;
IC s2 = IC (s2 +* (J +* Start-At insloc 0)) by A1,AMI_5:10
.= IC (s2 +* J +* Start-At insloc 0) by FUNCT_4:15
.= insloc 0 by AMI_5:79;
hence IC (Computation s1).i = IC (Computation s2).i &
CurInstr (Computation s1).i = CurInstr (Computation s2).i &
(Computation s1).i | (Int-Locations \/ FinSeq-Locations)
= (Computation s2).i | (Int-Locations \/ FinSeq-Locations)
by A1,A2,A4,A5,Th42;
end;
theorem Th44: ::T24441'
for s1,s2 being State of SCM+FSA,I being Macro-Instruction st
I is_closed_on s1 & I is_halting_on s1 &
I +* Start-At insloc 0 c= s1 & I +* Start-At insloc 0 c= s2 &
s1 | (Int-Locations \/ FinSeq-Locations) =
s2 | (Int-Locations \/ FinSeq-Locations) holds
LifeSpan s1 = LifeSpan s2
proof
let s1,s2 be State of SCM+FSA;
let J be Macro-Instruction;
assume A1: J is_closed_on s1 & J is_halting_on s1 &
J +* Start-At insloc 0 c= s1 & J +* Start-At insloc 0 c= s2 &
s1 | (Int-Locations \/ FinSeq-Locations) =
s2 | (Int-Locations \/ FinSeq-Locations);
then s1 = s1 +* (J +* Start-At insloc 0) by AMI_5:10;
then A2: s1 is halting by A1,SCMFSA7B:def 8;
then CurInstr (Computation s1).(LifeSpan s1) = halt SCM+FSA &
for k being Nat st CurInstr (Computation s1).k = halt SCM+FSA holds
LifeSpan s1 <= k by SCM_1:def 2;
then A3: CurInstr (Computation s2).(LifeSpan s1) = halt SCM+FSA by A1,Th43;
then A4: s2 is halting by AMI_1:def 20;
now let k be Nat;
assume CurInstr (Computation s2).k = halt SCM+FSA;
then CurInstr (Computation s1).k = halt SCM+FSA by A1,Th43;
hence LifeSpan s1 <= k by A2,SCM_1:def 2;
end;
hence LifeSpan s1 = LifeSpan s2 by A3,A4,SCM_1:def 2;
end;
theorem Th45: ::T27835
for s1,s2 being State of SCM+FSA,I being Macro-Instruction st
s1.intloc 0 = 1 & I is_closed_on s1 & I is_halting_on s1 &
((for a being read-write Int-Location holds s1.a = s2.a) &
for f being FinSeq-Location holds s1.f = s2.f) holds
IExec(I,s1) | (Int-Locations \/ FinSeq-Locations) =
IExec(I,s2) | (Int-Locations \/ FinSeq-Locations)
proof
let s1,s2 be State of SCM+FSA;
let I be Macro-Instruction;
set s11 = s1 +* Initialized I;
set s21 = s2 +* Initialized I;
assume A1: s1.intloc 0 = 1;
assume A2: I is_closed_on s1 & I is_halting_on s1;
assume A3: for a being read-write Int-Location holds s1.a = s2.a;
assume A4: for f being FinSeq-Location holds s1.f = s2.f;
A5: Initialized I c= s11 & Initialized I c= s21 by FUNCT_4:26;
A6: s11 = s1 +* (I +* Start-At insloc 0) by A1,Th18;
then s11 | D = s1 | D by SCMFSA8A:11;
then A7: I is_closed_on s11 & I is_halting_on s11 by A2,SCMFSA8B:8;
A8: now let a be read-write Int-Location;
A9: a in dom s1 & a in dom s2 & not a in dom Initialized I
by SCMFSA6A:48,SCMFSA_2:66;
hence s11.a = s1.a by FUNCT_4:12
.= s2.a by A3
.= s21.a by A9,FUNCT_4:12;
end;
A10: now let f be FinSeq-Location;
A11: f in dom s1 & f in dom s2 & not f in dom Initialized I
by SCMFSA6A:49,SCMFSA_2:67;
hence s11.f = s1.f by FUNCT_4:12
.= s2.f by A4
.= s21.f by A11,FUNCT_4:12;
end;
A12: intloc 0 in dom Initialized I by SCMFSA6A:45;
then s11.intloc 0 = (Initialized I).intloc 0 by FUNCT_4:14
.= s21.intloc 0 by A12,FUNCT_4:14;
then A13: s11 | D = s21 | D by A8,A10,Th33;
I +* Start-At insloc 0 c= Initialized I by Th19;
then A14: I +* Start-At insloc 0 c= s11 & I +* Start-At insloc 0 c= s21
by A5,XBOOLE_1:1;
then A15: LifeSpan s11 = LifeSpan s21 by A7,A13,Th44;
A16: s11 is halting by A2,A6,SCMFSA7B:def 8;
then CurInstr (Computation s11).(LifeSpan s11) = halt SCM+FSA &
for k being Nat st CurInstr (Computation s11).k = halt SCM+FSA holds
LifeSpan s11 <= k by SCM_1:def 2;
then CurInstr (Computation s21).(LifeSpan s11) = halt SCM+FSA
by A7,A13,A14,Th43;
then A17: s21 is halting by AMI_1:def 20;
thus IExec(I,s1) | (Int-Locations \/ FinSeq-Locations)
= (Result s11) | D by SCMFSA8B:35
.= (Computation s11).(LifeSpan s11) | D by A16,SCMFSA6B:16
.= (Computation s21).(LifeSpan s11) | D by A7,A13,A14,Th43
.= (Result s21) | D by A15,A17,SCMFSA6B:16
.= IExec(I,s2) | (Int-Locations \/ FinSeq-Locations) by SCMFSA8B:35;
end;
theorem Th46: ::T27835'
for s1,s2 being State of SCM+FSA,I being Macro-Instruction st
s1.intloc 0 = 1 & I is_closed_on s1 & I is_halting_on s1 &
s1 | (Int-Locations \/ FinSeq-Locations) =
s2 | (Int-Locations \/ FinSeq-Locations) holds
IExec(I,s1) | (Int-Locations \/ FinSeq-Locations) =
IExec(I,s2) | (Int-Locations \/ FinSeq-Locations)
proof
let s1,s2 be State of SCM+FSA;
let I be Macro-Instruction;
set s11 = s1 +* Initialized I;
set s21 = s2 +* Initialized I;
assume A1: s1.intloc 0 = 1 & I is_closed_on s1 & I is_halting_on s1 &
s1 | (Int-Locations \/ FinSeq-Locations) =
s2 | (Int-Locations \/ FinSeq-Locations);
A2: Initialized I c= s11 & Initialized I c= s21 by FUNCT_4:26;
s2.intloc 0 = 1 by A1,SCMFSA6A:38;
then A3: s11 = s1 +* (I +* Start-At insloc 0) &
s21 = s2 +* (I +* Start-At insloc 0) by A1,Th18;
then A4: s11 | D = s1 | D by SCMFSA8A:11;
then A5: I is_closed_on s11 & I is_halting_on s11 by A1,SCMFSA8B:8;
A6: s11 | D = s21 | D by A1,A3,A4,SCMFSA8A:11;
I +* Start-At insloc 0 c= Initialized I by Th19;
then A7: I +* Start-At insloc 0 c= s11 & I +* Start-At insloc 0 c= s21
by A2,XBOOLE_1:1;
then A8: LifeSpan s11 = LifeSpan s21 by A5,A6,Th44;
A9: s11 is halting by A1,A3,SCMFSA7B:def 8;
then CurInstr (Computation s11).(LifeSpan s11) = halt SCM+FSA &
for k being Nat st CurInstr (Computation s11).k = halt SCM+FSA holds
LifeSpan s11 <= k by SCM_1:def 2;
then CurInstr (Computation s21).(LifeSpan s11) = halt SCM+FSA
by A5,A6,A7,Th43;
then A10: s21 is halting by AMI_1:def 20;
thus IExec(I,s1) | (Int-Locations \/ FinSeq-Locations)
= (Result s11) | D by SCMFSA8B:35
.= (Computation s11).(LifeSpan s11) | D by A9,SCMFSA6B:16
.= (Computation s21).(LifeSpan s11) | D by A5,A6,A7,Th43
.= (Result s21) | D by A8,A10,SCMFSA6B:16
.= IExec(I,s2) | (Int-Locations \/ FinSeq-Locations) by SCMFSA8B:35;
end;
definition
let I be Macro-Instruction;
cluster Initialized I -> initial;
correctness
proof
now let m,n be Nat;
assume insloc n in dom Initialized I;
then A1: insloc n in dom I by Th20;
I c= Initialized I by SCMFSA6A:26;
then A2: dom I c= dom Initialized I by GRFUNC_1:8;
assume m < n;
then insloc m in dom I by A1,SCMFSA_4:def 4;
hence insloc m in dom Initialized I by A2;
end;
hence thesis by SCMFSA_4:def 4;
end;
end;
Lm1:
now
let s be State of SCM+FSA;
let I be Macro-Instruction;
A1: ProgramPart Initialized I = I by Th25;
hereby assume A2: Initialized I is_pseudo-closed_on s;
set k = pseudo-LifeSpan(s,Initialized I);
IC (Computation (s +* (Initialized I +* Start-At insloc 0))).k =
insloc card ProgramPart Initialized I &
for n being Nat st n < k holds
IC (Computation (s +* (Initialized I +* Start-At insloc 0))).n in
dom Initialized I by A2,SCMFSA8A:def 5;
then IC (Computation (Initialize s +* (I +* Start-At insloc 0))).k =
insloc card ProgramPart Initialized I by Th16;
then A3: IC (Computation (Initialize s +* (I +* Start-At insloc 0))).k =
insloc card ProgramPart I by A1,AMI_5:72;
A4: now let n be Nat;
assume n < k;
then IC (Computation (s +* (Initialized I +* Start-At insloc 0))).n
in
dom Initialized I by A2,SCMFSA8A:def 5;
then IC (Computation (Initialize s +* (I +* Start-At insloc 0))).n in
dom Initialized I by Th16;
hence IC (Computation (Initialize s +* (I +* Start-At insloc 0))).n
in
dom I by Th20;
end;
then A5: for n be Nat st
not IC (Computation (Initialize s +* (I +* Start-At insloc 0)))
.n in dom I holds k <= n;
thus I is_pseudo-closed_on Initialize s by A3,A4,SCMFSA8A:def 3;
hence pseudo-LifeSpan(s,Initialized I) = pseudo-LifeSpan(Initialize s,I)
by A3,A5,SCMFSA8A:def 5;
end;
assume A6: I is_pseudo-closed_on Initialize s;
set k = pseudo-LifeSpan(Initialize s,I);
IC (Computation (Initialize s +* (I +* Start-At insloc 0))).k =
insloc card ProgramPart I &
for n being Nat st n < k holds
IC (Computation (Initialize s +* (I +* Start-At insloc 0))).n in
dom I by A6,SCMFSA8A:def 5;
then IC (Computation (s +* (Initialized I +* Start-At insloc 0))).k =
insloc card ProgramPart I by Th16;
then A7: IC (Computation (s +* (Initialized I +* Start-At insloc 0))).k =
insloc card ProgramPart Initialized I by A1,AMI_5:72;
A8: now let n be Nat;
assume n < k;
then IC (Computation (Initialize s +* (I +* Start-At insloc 0))).n in
dom I by A6,SCMFSA8A:def 5;
then IC (Computation (s +* (Initialized I +* Start-At insloc 0))).n in
dom I by Th16;
hence IC (Computation (s +* (Initialized I +* Start-At insloc 0))).n in
dom Initialized I by Th20;
end;
then A9: for n be Nat st not IC (Computation (s +* (Initialized I +*
Start-At insloc 0))).n in dom Initialized I holds k <= n;
thus Initialized I is_pseudo-closed_on s by A7,A8,SCMFSA8A:def 3;
hence pseudo-LifeSpan(s,Initialized I) = pseudo-LifeSpan(Initialize s,I)
by A7,A9,SCMFSA8A:def 5;
end;
theorem ::TMP8
for s being State of SCM+FSA, I being Macro-Instruction holds
Initialized I is_pseudo-closed_on s iff I is_pseudo-closed_on Initialize s
by Lm1;
theorem
for s being State of SCM+FSA, I being Macro-Instruction
st I is_pseudo-closed_on Initialize s holds
pseudo-LifeSpan(s,Initialized I) = pseudo-LifeSpan(Initialize s,I)
by Lm1;
theorem
for s being State of SCM+FSA, I being Macro-Instruction
st Initialized I is_pseudo-closed_on s holds
pseudo-LifeSpan(s,Initialized I) = pseudo-LifeSpan(Initialize s,I)
by Lm1;
theorem Th50: ::TMP14
for s being State of SCM+FSA, I being initial FinPartState of SCM+FSA
st I is_pseudo-closed_on s holds
I is_pseudo-closed_on s +* (I +* Start-At insloc 0) &
pseudo-LifeSpan(s,I) = pseudo-LifeSpan(s +* (I +* Start-At insloc 0),I)
proof
let s be State of SCM+FSA;
let I be initial FinPartState of SCM+FSA;
assume A1: I is_pseudo-closed_on s;
set s2 = s +* (I +* Start-At insloc 0) +* (I +* Start-At insloc 0);
A2: s +* (I +* Start-At insloc 0) +* (I +* Start-At insloc 0)
= s +* ((I +* Start-At insloc 0) +* (I +* Start-At insloc 0)) by FUNCT_4:15
.= s +* (I +* Start-At insloc 0);
then A3: IC (Computation s2).pseudo-LifeSpan(s,I) = insloc card ProgramPart I &
for n being Nat st not IC (Computation s2).n in dom I
holds pseudo-LifeSpan(s,I) <= n by A1,SCMFSA8A:def 5;
IC (Computation s2).pseudo-LifeSpan(s,I) = insloc card ProgramPart I &
for n being Nat st n < pseudo-LifeSpan(s,I) holds
IC (Computation s2).n in dom I by A1,A2,SCMFSA8A:def 5;
hence I is_pseudo-closed_on s +* (I +* Start-At insloc 0) by SCMFSA8A:def 3
;
hence pseudo-LifeSpan(s,I) =
pseudo-LifeSpan(s +* (I +* Start-At insloc 0),I) by A3,SCMFSA8A:def 5;
end;
theorem Th51: ::P'115'
for s1,s2 being State of SCM+FSA, I being Macro-Instruction
st I +* Start-At insloc 0 c= s1 & I is_pseudo-closed_on s1
for n being Nat st ProgramPart Relocated(I,n) c= s2 &
IC s2 = insloc n &
s1 | (Int-Locations \/ FinSeq-Locations)
= s2 | (Int-Locations \/ FinSeq-Locations) holds
((for i being Nat st i < pseudo-LifeSpan(s1,I) holds
IncAddr(CurInstr (Computation s1).i,n) = CurInstr (Computation s2).i) &
for i being Nat st i <= pseudo-LifeSpan(s1,I) holds
IC (Computation s1).i + n = IC (Computation s2).i &
(Computation s1).i | (Int-Locations \/ FinSeq-Locations)
= (Computation s2).i | (Int-Locations \/ FinSeq-Locations))
proof
let s1,s2 be State of SCM+FSA;
let I be Macro-Instruction;
assume A1: I +* Start-At insloc 0 c= s1;
assume A2: I is_pseudo-closed_on s1;
let n be Nat;
assume A3: ProgramPart Relocated(I,n) c= s2;
assume A4: IC s2 = insloc n;
assume A5: s1 | (Int-Locations \/ FinSeq-Locations)
= s2 | (Int-Locations \/ FinSeq-Locations);
set C1 = Computation s1;
set C2 = Computation s2;
thus A6: now let i be Nat;
assume A7: i < pseudo-LifeSpan(s1,I);
defpred P[Nat] means
$1 < pseudo-LifeSpan(s1,I) implies
IC C1.$1 + n = IC C2.$1 &
IncAddr(CurInstr (C1.$1),n) = CurInstr (C2.$1) &
C1.$1 | (Int-Locations \/ FinSeq-Locations)
= C2.$1 | (Int-Locations \/ FinSeq-Locations);
A8: ProgramPart Relocated(I,n)
= Relocated(I,n) | the Instruction-Locations of SCM+FSA by AMI_5:def 6;
A9: P[0]
proof
assume A10: 0 < pseudo-LifeSpan(s1,I);
A11: IC SCM+FSA in dom (I +* Start-At insloc 0) by SF_MASTR:65;
IC C1.0 = IC s1 by AMI_1:def 19
.= s1.IC SCM+FSA by AMI_1:def 15
.= (I +* Start-At insloc 0).IC SCM+FSA by A1,A11,GRFUNC_1:8
.= insloc 0 by SF_MASTR:66;
hence IC C1.0 + n = insloc (0 + n) by SCMFSA_4:def 1
.= IC C2.0 by A4,AMI_1:def 19;
A12: I c= I +* Start-At insloc 0 by SCMFSA8A:9;
then A13: dom I c= dom (I +* Start-At insloc 0) by GRFUNC_1:8;
IC (Computation (s1 +* (I +* Start-At insloc 0))).0
= IC (s1 +* (I +* Start-At insloc 0)) by AMI_1:def 19
.= IC (s1 +* I +* Start-At insloc 0) by FUNCT_4:15
.= insloc 0 by AMI_5:79;
then A14: insloc 0 in dom I by A2,A10,SCMFSA8A:def 5;
A15: IC SCM+FSA in dom (I +* Start-At insloc 0) by SF_MASTR:65;
A16: s1.IC s1 = s1.(s1.IC SCM+FSA) by AMI_1:def 15
.= s1.((I +* Start-At insloc 0).IC SCM+FSA) by A1,A15,GRFUNC_1:8
.= s1.insloc 0 by SF_MASTR:66
.= (I +* Start-At insloc 0).insloc 0 by A1,A13,A14,GRFUNC_1:8
.= I.insloc 0 by A12,A14,GRFUNC_1:8;
insloc 0 + n in dom Relocated(I,n) by A14,SCMFSA_5:4;
then insloc 0 + n in dom ProgramPart Relocated(I,n) by AMI_5:73;
then A17: insloc (0 + n) in dom ProgramPart Relocated(I,n) by SCMFSA_4:def 1;
A18: insloc 0 in dom ProgramPart I by A14,AMI_5:72;
thus IncAddr(CurInstr (C1.0),n)
= IncAddr(CurInstr s1,n) by AMI_1:def 19
.= IncAddr(s1.IC s1,n) by AMI_1:def 17
.= Relocated(I,n).(insloc 0 + n) by A16,A18,SCMFSA_5:7
.= Relocated(I,n).insloc (0 + n) by SCMFSA_4:def 1
.= (ProgramPart Relocated(I,n)).insloc n by A8,FUNCT_1:72
.= s2.IC s2 by A3,A4,A17,GRFUNC_1:8
.= CurInstr s2 by AMI_1:def 17
.= CurInstr (C2.0) by AMI_1:def 19;
thus C1.0 | (Int-Locations \/ FinSeq-Locations)
= s2 | (Int-Locations \/ FinSeq-Locations) by A5,AMI_1:def 19
.= C2.0 | (Int-Locations \/ FinSeq-Locations) by AMI_1:def 19;
end;
A19: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume A20: P[k];
assume A21: k + 1 < pseudo-LifeSpan(s1,I);
A22: k + 0 < k + 1 by REAL_1:53;
A23: C1.(k + 1) = Following C1.k by AMI_1:def 19
.= Exec(CurInstr C1.k,C1.k) by AMI_1:def 18;
A24: C2.(k + 1) = Following C2.k by AMI_1:def 19
.= Exec(CurInstr C2.k,C2.k) by AMI_1:def 18;
hence
A25: IC C1.(k + 1) + n
= IC C2.(k + 1) by A20,A21,A22,A23,AXIOMS:22,SCMFSA6A:41;
reconsider j = CurInstr C1.(k + 1) as Instruction of SCM+FSA;
reconsider l = IC C1.(k + 1) as Instruction-Location of SCM+FSA;
A26: I c= I +* Start-At insloc 0 by SCMFSA8A:9;
then A27: dom I c= dom (I +* Start-At insloc 0) by GRFUNC_1:8;
s1 +* (I +* Start-At insloc 0) = s1 by A1,AMI_5:10;
then A28: IC C1.(k + 1) in dom I by A2,A21,SCMFSA8A:def 5;
ProgramPart I = I | the Instruction-Locations of SCM+FSA
by AMI_5:def 6;
then dom ProgramPart I = dom I /\ the Instruction-Locations of SCM+FSA
by FUNCT_1:68;
then A29: l in dom ProgramPart I by A28,XBOOLE_0:def 3;
A30: j = C1.(k + 1).IC C1.(k + 1) by AMI_1:def 17
.= s1.IC C1.(k + 1) by AMI_1:54
.= (I +* Start-At insloc 0).IC C1.(k + 1) by A1,A27,A28,GRFUNC_1:8
.= I.l by A26,A28,GRFUNC_1:8;
IC C2.(k + 1) in dom Relocated(I,n) by A25,A28,SCMFSA_5:4;
then IC C2.(k + 1) in
dom Relocated(I,n) /\ the Instruction-Locations of SCM+FSA
by XBOOLE_0:def 3;
then A31: IC C2.(k + 1) in dom ProgramPart Relocated(I,n) by A8,FUNCT_1:68;
thus IncAddr(CurInstr C1.(k + 1),n)
= Relocated(I,n).(l + n) by A29,A30,SCMFSA_5:7
.= (ProgramPart Relocated(I,n)).(IC C2.(k + 1)) by A8,A25,FUNCT_1:72
.= s2.IC C2.(k + 1) by A3,A31,GRFUNC_1:8
.= C2.(k + 1).IC C2.(k + 1) by AMI_1:54
.= CurInstr C2.(k + 1) by AMI_1:def 17;
thus C1.(k + 1) | (Int-Locations \/ FinSeq-Locations)
= C2.(k + 1) | (Int-Locations \/ FinSeq-Locations) by A20,A21,A22,A23,
A24,AXIOMS:22,SCMFSA6A:41;
end;
for k being Nat holds P[k] from Ind(A9,A19);
hence IncAddr(CurInstr ((Computation s1).i),n) =
CurInstr ((Computation s2).i) by A7;
end;
let i be Nat;
assume A32: i <= pseudo-LifeSpan(s1,I);
defpred P[Nat] means
$1 <= pseudo-LifeSpan(s1,I) implies
IC C1.$1 + n = IC C2.$1 &
C1.$1 | (Int-Locations \/ FinSeq-Locations)
= C2.$1 | (Int-Locations \/ FinSeq-Locations);
A33: P[0]
proof
assume 0 <= pseudo-LifeSpan(s1,I);
A34: IC SCM+FSA in dom (I +* Start-At insloc 0) by SF_MASTR:65;
IC C1.0 = IC s1 by AMI_1:def 19
.= s1.IC SCM+FSA by AMI_1:def 15
.= (I +* Start-At insloc 0).IC SCM+FSA by A1,A34,GRFUNC_1:8
.= insloc 0 by SF_MASTR:66;
hence IC C1.0 + n = insloc (0 + n) by SCMFSA_4:def 1
.= IC C2.0 by A4,AMI_1:def 19;
thus C1.0 | (Int-Locations \/ FinSeq-Locations)
= s2 | (Int-Locations \/ FinSeq-Locations) by A5,AMI_1:def 19
.= C2.0 | (Int-Locations \/ FinSeq-Locations) by AMI_1:def 19;
end;
A35: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume A36: P[k];
assume A37: k + 1 <= pseudo-LifeSpan(s1,I);
then A38: k + 1 <= pseudo-LifeSpan(s1,I) + 1 by NAT_1:37;
A39: k < pseudo-LifeSpan(s1,I) by A37,NAT_1:38;
set i = CurInstr C1.k;
A40: C1.(k + 1) = Following C1.k by AMI_1:def 19
.= Exec(CurInstr C1.k,C1.k) by AMI_1:def 18;
A41: C2.(k + 1) = Following C2.k by AMI_1:def 19
.= Exec(CurInstr C2.k,C2.k) by AMI_1:def 18;
thus IC C1.(k + 1) + n
= IC Exec(IncAddr(i,n),C2.k) by A36,A38,A40,REAL_1:53,SCMFSA6A:41
.= IC C2.(k + 1) by A6,A39,A41;
thus C1.(k + 1) | (Int-Locations \/ FinSeq-Locations)
= Exec(IncAddr(i,n),C2.k) | (Int-Locations \/ FinSeq-Locations)
by A36,A38,A40,REAL_1:53,SCMFSA6A:41
.= C2.(k + 1) | (Int-Locations \/ FinSeq-Locations) by A6,A39,A41;
end;
for k being Nat holds P[k] from Ind(A33,A35);
hence thesis by A32;
end;
theorem Th52: ::TMP11
for s1,s2 being State of SCM+FSA, I being Macro-Instruction st
s1 | (Int-Locations \/ FinSeq-Locations) =
s2 | (Int-Locations \/ FinSeq-Locations) holds
I is_pseudo-closed_on s1 implies I is_pseudo-closed_on s2
proof
let s1,s2 be State of SCM+FSA;
let I be Macro-Instruction;
set C1 = Computation (s1 +* (I +* Start-At insloc 0));
set C2 = Computation (s2 +* (I +* Start-At insloc 0));
assume s1 | D = s2 | D;
then A1: (s1 +* (I +* Start-At insloc 0)) | D = s2 | D by SCMFSA8A:11
.= (s2 +* (I +* Start-At insloc 0)) | D by SCMFSA8A:11;
assume A2: I is_pseudo-closed_on s1;
then A3: IC C1.pseudo-LifeSpan(s1,I) = insloc card ProgramPart I &
for n being Nat st n < pseudo-LifeSpan(s1,I) holds
IC C1.n in dom I by SCMFSA8A:def 5;
A4: I is_pseudo-closed_on s1 +* (I +* Start-At insloc 0) by A2,Th50;
A5: I +* Start-At insloc 0 c= s1 +* (I +* Start-At insloc 0) by FUNCT_4:26;
A6: I +* Start-At insloc 0 c= s2 +* (I +* Start-At insloc 0) by FUNCT_4:26;
I c= I +* Start-At insloc 0 by SCMFSA8A:9;
then I c= s2 +* (I +* Start-At insloc 0) by A6,XBOOLE_1:1;
then A7: ProgramPart Relocated(I,0) c= s2 +* (I +* Start-At insloc 0) by Th9;
A8: IC (s2 +* (I +* Start-At insloc 0))
= IC (s2 +* I +* Start-At insloc 0) by FUNCT_4:15
.= insloc 0 by AMI_5:79;
A9: IC C2.pseudo-LifeSpan(s1,I)
= IC C2.pseudo-LifeSpan(s1 +* (I +* Start-At insloc 0),I) by A2,Th50
.= IC C1.pseudo-LifeSpan(s1 +* (I +* Start-At insloc 0),I) + 0
by A1,A4,A5,A7,A8,Th51
.= IC C1.pseudo-LifeSpan(s1,I) + 0 by A2,Th50
.= IC C1.pseudo-LifeSpan(s1,I) by Th7;
now let k be Nat;
assume A10: k < pseudo-LifeSpan(s1,I);
then k <= pseudo-LifeSpan(s1 +* (I +* Start-At insloc 0),I) by A2,Th50;
then IC C2.k = IC C1.k + 0 by A1,A4,A5,A7,A8,Th51
.= IC C1.k by Th7;
hence IC C2.k in dom I by A2,A10,SCMFSA8A:def 5;
end;
hence I is_pseudo-closed_on s2 by A3,A9,SCMFSA8A:def 3;
end;
theorem Th53: ::T1702
for s being State of SCM+FSA, I being Macro-Instruction
st s.intloc 0 = 1 holds
I is_pseudo-closed_on s iff I is_pseudo-closed_on Initialize s
proof
let s be State of SCM+FSA;
let I be Macro-Instruction;
assume s.intloc 0 = 1;
then s | D = (Initialize s) | D by Th27;
hence I is_pseudo-closed_on s iff I is_pseudo-closed_on Initialize s
by Th52;
end;
Lm2:
for l being Instruction-Location of SCM+FSA holds
goto l <> halt SCM+FSA
proof
let l be Instruction-Location of SCM+FSA;
thus thesis by SCMFSA_2:47,124;
end;
Lm3:
for a being Int-Location, l being Instruction-Location of SCM+FSA holds
a =0_goto l <> halt SCM+FSA
proof
let a be Int-Location;
let l be Instruction-Location of SCM+FSA;
thus thesis by SCMFSA_2:48,124;
end;
Lm4:
for a being Int-Location, l being Instruction-Location of SCM+FSA holds
a >0_goto l <> halt SCM+FSA
proof
let a be Int-Location;
let l be Instruction-Location of SCM+FSA;
thus thesis by SCMFSA_2:49,124;
end;
Lm5:
for I,J being Macro-Instruction holds
ProgramPart Relocated(J,card I) c= I ';' J
proof
let I,J be Macro-Instruction;
I ';' J = Directed I +* ProgramPart Relocated(J,card I) by SCMFSA6A:def 4;
hence thesis by FUNCT_4:26;
end;
theorem Th54: ::TD2' ** n.t
for a being Int-Location, I,J being Macro-Instruction holds
insloc 0 in dom if=0(a,I,J) &
insloc 1 in dom if=0(a,I,J) &
insloc 0 in dom if>0(a,I,J) &
insloc 1 in dom if>0(a,I,J)
proof
let a be Int-Location;
let I,J be Macro-Instruction;
set i = a =0_goto insloc (card J + 3);
if=0(a,I,J)
= i ';' J ';' Goto insloc (card I + 1) ';' I ';' SCM+FSA-Stop
by SCMFSA8B:def 1
.= i ';' J ';' Goto insloc (card I + 1) ';' (I ';' SCM+FSA-Stop)
by SCMFSA6A:62
.= i ';' J ';' (Goto insloc (card I + 1) ';' (I ';' SCM+FSA-Stop))
by SCMFSA6A:62
.= i ';' (J ';' (Goto insloc (card I + 1) ';' (I ';' SCM+FSA-Stop)))
by SCMFSA6A:66
.= Macro i ';' (J ';' (Goto insloc (card I + 1) ';' (I ';' SCM+FSA-Stop)))
by SCMFSA6A:def 5;
then A1: dom Macro i c= dom if=0(a,I,J) by SCMFSA6A:56;
dom Macro i = {insloc 0, insloc 1} by SCMFSA7B:4;
then insloc 0 in dom Macro i & insloc 1 in dom Macro i by TARSKI:def 2;
hence insloc 0 in dom if=0(a,I,J) & insloc 1 in dom if=0(a,I,J) by A1;
set i = a >0_goto insloc (card J + 3);
if>0(a,I,J)
= i ';' J ';' Goto insloc (card I + 1) ';' I ';' SCM+FSA-Stop
by SCMFSA8B:def 2
.= i ';' J ';' Goto insloc (card I + 1) ';' (I ';' SCM+FSA-Stop)
by SCMFSA6A:62
.= i ';' J ';' (Goto insloc (card I + 1) ';' (I ';' SCM+FSA-Stop))
by SCMFSA6A:62
.= i ';' (J ';' (Goto insloc (card I + 1) ';' (I ';' SCM+FSA-Stop)))
by SCMFSA6A:66
.= Macro i ';' (J ';' (Goto insloc (card I + 1) ';' (I ';' SCM+FSA-Stop)))
by SCMFSA6A:def 5;
then A2: dom Macro i c= dom if>0(a,I,J) by SCMFSA6A:56;
dom Macro i = {insloc 0, insloc 1} by SCMFSA7B:4;
then insloc 0 in dom Macro i & insloc 1 in dom Macro i by TARSKI:def 2;
hence insloc 0 in dom if>0(a,I,J) & insloc 1 in dom if>0(a,I,J) by A2;
end;
theorem Th55: ::TD2 ** n.t
for a being Int-Location, I,J being Macro-Instruction holds
if=0(a,I,J).insloc 0 = a =0_goto insloc (card J + 3) &
if=0(a,I,J).insloc 1 = goto insloc 2 &
if>0(a,I,J).insloc 0 = a >0_goto insloc (card J + 3) &
if>0(a,I,J).insloc 1 = goto insloc 2
proof
let a be Int-Location;
let I,J be Macro-Instruction;
set i = a =0_goto insloc (card J + 3);
A1: i <> halt SCM+FSA by Lm3;
A2: if=0(a,I,J)
= i ';' J ';' Goto insloc (card I + 1) ';' I ';' SCM+FSA-Stop
by SCMFSA8B:def 1
.= i ';' J ';' Goto insloc (card I + 1) ';' (I ';' SCM+FSA-Stop)
by SCMFSA6A:62
.= i ';' J ';' (Goto insloc (card I + 1) ';' (I ';' SCM+FSA-Stop))
by SCMFSA6A:62
.= i ';' (J ';' (Goto insloc (card I + 1) ';' (I ';' SCM+FSA-Stop)))
by SCMFSA6A:66
.= Macro i ';' (J ';' (Goto insloc (card I + 1) ';' (I ';' SCM+FSA-Stop)))
by SCMFSA6A:def 5;
dom Macro i = {insloc 0, insloc 1} by SCMFSA7B:4;
then A3: insloc 0 in dom Macro i & insloc 1 in dom Macro i by TARSKI:def 2;
hence if=0(a,I,J).insloc 0 = (Directed Macro i).insloc 0 by A2,SCMFSA8A:28
.= i by A1,SCMFSA7B:7;
thus if=0(a,I,J).insloc 1 = (Directed Macro i).insloc 1 by A2,A3,SCMFSA8A:28
.= goto insloc 2 by SCMFSA7B:8;
set i = a >0_goto insloc (card J + 3);
A4: i <> halt SCM+FSA by Lm4;
A5: if>0(a,I,J)
= i ';' J ';' Goto insloc (card I + 1) ';' I ';' SCM+FSA-Stop
by SCMFSA8B:def 2
.= i ';' J ';' Goto insloc (card I + 1) ';' (I ';' SCM+FSA-Stop)
by SCMFSA6A:62
.= i ';' J ';' (Goto insloc (card I + 1) ';' (I ';' SCM+FSA-Stop))
by SCMFSA6A:62
.= i ';' (J ';' (Goto insloc (card I + 1) ';' (I ';' SCM+FSA-Stop)))
by SCMFSA6A:66
.= Macro i ';' (J ';' (Goto insloc (card I + 1) ';' (I ';' SCM+FSA-Stop)))
by SCMFSA6A:def 5;
dom Macro i = {insloc 0, insloc 1} by SCMFSA7B:4;
then A6: insloc 0 in dom Macro i & insloc 1 in dom Macro i by TARSKI:def 2;
hence if>0(a,I,J).insloc 0 = (Directed Macro i).insloc 0 by A5,SCMFSA8A:28
.= i by A4,SCMFSA7B:7;
thus if>0(a,I,J).insloc 1 = (Directed Macro i).insloc 1 by A5,A6,SCMFSA8A:28
.= goto insloc 2 by SCMFSA7B:8;
end;
theorem Th56: ::T6327 ** n.t
for a being Int-Location, I,J being Macro-Instruction, n being Nat st
n < card I + card J + 3 holds insloc n in dom if=0(a,I,J) &
if=0(a,I,J).insloc n <> halt SCM+FSA
proof
let a be Int-Location;
let I,J be Macro-Instruction;
let n be Nat;
assume A1: n < card I + card J + 3;
A2: if=0(a,I,J) = a =0_goto insloc (card J + 3) ';' J ';'
Goto insloc (card I + 1) ';' I ';' SCM+FSA-Stop by SCMFSA8B:def 1;
set J1 = a =0_goto insloc (card J + 3) ';' J ';'
Goto insloc (card I + 1) ';' I;
card J1
= card (Macro (a =0_goto insloc (card J + 3)) ';' J ';'
Goto insloc (card I + 1) ';' I) by SCMFSA6A:def 5
.= card (Macro (a =0_goto insloc (card J + 3)) ';' J ';'
Goto insloc (card I + 1)) + card I by SCMFSA6A:61
.= card (Macro (a =0_goto insloc (card J + 3)) ';' J) +
card Goto insloc (card I + 1) + card I by SCMFSA6A:61
.= card (Macro (a =0_goto insloc (card J + 3)) ';' J) + 1 + card I
by SCMFSA8A:29
.= card Macro (a =0_goto insloc (card J + 3)) + card J + 1 + card I
by SCMFSA6A:61
.= 2 + card J + 1 + card I by SCMFSA7B:6
.= card J + (2 + 1) + card I by XCMPLX_1:1
.= card I + card J + 3 by XCMPLX_1:1;
then insloc n in dom J1 by A1,SCMFSA6A:15;
then A3: insloc n in dom Directed J1 by SCMFSA6A:14;
Directed J1 c= if=0(a,I,J) by A2,SCMFSA6A:55;
then A4: dom Directed J1 c= dom if=0(a,I,J) &
if=0(a,I,J).insloc n = (Directed J1).insloc n by A3,GRFUNC_1:8;
hence insloc n in dom if=0(a,I,J) by A3;
(Directed J1).insloc n in rng Directed J1 by A3,FUNCT_1:def 5;
hence if=0(a,I,J).insloc n <> halt SCM+FSA by A4,SCMFSA7B:def 6;
end;
theorem Th57: ::T6327' ** n.t
for a being Int-Location, I,J being Macro-Instruction, n being Nat st
n < card I + card J + 3 holds insloc n in dom if>0(a,I,J) &
if>0(a,I,J).insloc n <> halt SCM+FSA
proof
let a be Int-Location;
let I,J be Macro-Instruction;
let n be Nat;
assume A1: n < card I + card J + 3;
A2: if>0(a,I,J) = a >0_goto insloc (card J + 3) ';' J ';'
Goto insloc (card I + 1) ';' I ';' SCM+FSA-Stop by SCMFSA8B:def 2;
set J1 = a >0_goto insloc (card J + 3) ';' J ';'
Goto insloc (card I + 1) ';' I;
card J1
= card (Macro (a >0_goto insloc (card J + 3)) ';' J ';'
Goto insloc (card I + 1) ';' I) by SCMFSA6A:def 5
.= card (Macro (a >0_goto insloc (card J + 3)) ';' J ';'
Goto insloc (card I + 1)) + card I by SCMFSA6A:61
.= card (Macro (a >0_goto insloc (card J + 3)) ';' J) +
card Goto insloc (card I + 1) + card I by SCMFSA6A:61
.= card (Macro (a >0_goto insloc (card J + 3)) ';' J) + 1 + card I
by SCMFSA8A:29
.= card Macro (a >0_goto insloc (card J + 3)) + card J + 1 + card I
by SCMFSA6A:61
.= 2 + card J + 1 + card I by SCMFSA7B:6
.= card J + (2 + 1) + card I by XCMPLX_1:1
.= card I + card J + 3 by XCMPLX_1:1;
then insloc n in dom J1 by A1,SCMFSA6A:15;
then A3: insloc n in dom Directed J1 by SCMFSA6A:14;
Directed J1 c= if>0(a,I,J) by A2,SCMFSA6A:55;
then A4: dom Directed J1 c= dom if>0(a,I,J) &
if>0(a,I,J).insloc n = (Directed J1).insloc n by A3,GRFUNC_1:8;
hence insloc n in dom if>0(a,I,J) by A3;
(Directed J1).insloc n in rng Directed J1 by A3,FUNCT_1:def 5;
hence if>0(a,I,J).insloc n <> halt SCM+FSA by A4,SCMFSA7B:def 6;
end;
theorem Th58: ::T29502
for s being State of SCM+FSA, I being Macro-Instruction st
Directed I is_pseudo-closed_on s holds
I ';' SCM+FSA-Stop is_closed_on s &
I ';' SCM+FSA-Stop is_halting_on s &
LifeSpan (s +* (I ';' SCM+FSA-Stop +* Start-At insloc 0)) =
pseudo-LifeSpan(s,Directed I) &
(for n being Nat st n < pseudo-LifeSpan(s,Directed I) holds
IC (Computation (s +* (I +* Start-At insloc 0))).n =
IC (Computation (s +* (I ';' SCM+FSA-Stop +* Start-At insloc 0))).n) &
for n being Nat st n <= pseudo-LifeSpan(s,Directed I) holds
(Computation (s +* (I +* Start-At insloc 0))).n | D =
(Computation (s +* (I ';' SCM+FSA-Stop +* Start-At insloc 0))).n | D
proof
let s be State of SCM+FSA;
let I be Macro-Instruction;
set I0 = Directed I;
set I1 = I ';' SCM+FSA-Stop;
set s00 = s +* (I0 +* Start-At insloc 0);
set s10 = s +* (I1 +* Start-At insloc 0);
assume A1: I0 is_pseudo-closed_on s;
set k = pseudo-LifeSpan(s00,I0);
A2: I0 c= I1 by SCMFSA6A:55;
then A3: dom I0 c= dom I1 by GRFUNC_1:8;
card I1 = card I + 1 by SCMFSA6A:61,SCMFSA8A:17;
then card I < card I1 by NAT_1:38;
then A4: insloc card I in dom I1 by SCMFSA6A:15;
A5: card I < card I + card SCM+FSA-Stop by NAT_1:38,SCMFSA8A:17;
halt SCM+FSA = SCM+FSA-Stop.insloc (card I -' card I)
by GOBOARD9:1,SCMFSA8A:16;
then I1.insloc card I = IncAddr(halt SCM+FSA,card I) by A5,Th13
.= halt SCM+FSA by SCMFSA_4:8;
then A6: s10.insloc card I = halt SCM+FSA by A4,Th26;
A7: I0 +* Start-At insloc 0 c= s00 by FUNCT_4:26;
A8: s00 +* (I0 +* Start-At insloc 0)
= s +* ((I0 +* Start-At insloc 0) +* (I0 +* Start-At insloc 0))
by FUNCT_4:15
.= s00;
A9: I0 is_pseudo-closed_on s00 by A1,Th50;
A10: k = pseudo-LifeSpan(s,I0) by A1,Th50;
I1 c= I1 +* Start-At insloc 0 & I1 +* Start-At insloc 0 c= s10
by FUNCT_4:26,SCMFSA8A:9;
then ProgramPart Relocated(I0,0) c= I1 & I1 c= s10 by A2,Th9,XBOOLE_1:1;
then A11: ProgramPart Relocated(I0,0) c= s10 by XBOOLE_1:1;
s10 = s +* I1 +* Start-At insloc 0 by FUNCT_4:15;
then A12: IC s10 = insloc 0 by AMI_5:79;
A13: s00 | D = s | D by SCMFSA8A:11
.= s10 | D by SCMFSA8A:11;
A14: now let n be Nat;
assume A15: n < pseudo-LifeSpan(s00,I0);
then IncAddr(CurInstr (Computation s00).n,0) = CurInstr (Computation s10
).n
by A7,A9,A11,A12,A13,Th51;
hence CurInstr (Computation s00).n = CurInstr (Computation s10).n
by Th8;
thus IC (Computation s00).n in dom I0 by A8,A9,A15,SCMFSA8A:31;
thus CurInstr (Computation s00).n <> halt SCM+FSA by A8,A9,A15,SCMFSA8A:
31;
end;
A16: now let n be Nat;
assume A17: n <= pseudo-LifeSpan(s00,I0);
then IC (Computation s00).n + 0 = IC (Computation s10).n
by A7,A9,A11,A12,A13,Th51;
hence IC (Computation s00).n = IC (Computation s10).n by Th7;
thus (Computation s00).n | D = (Computation s10).n | D
by A7,A9,A11,A12,A13,A17,Th51;
end;
defpred P[Nat] means
k <= $1 implies IC (Computation s10).$1 = insloc card I &
CurInstr (Computation s10).$1 = halt SCM+FSA;
A18: P[0]
proof
assume k <= 0;
then k = 0 by NAT_1:19;
hence
A19: IC (Computation s10).0 = IC (Computation s00).k by A16
.= insloc card ProgramPart I0 by A1,A10,SCMFSA8A:def 5
.= insloc card I0 by AMI_5:72
.= insloc card I by SCMFSA8A:34;
thus CurInstr (Computation s10).0
= (Computation s10).0.IC (Computation s10).0 by AMI_1:def 17
.= halt SCM+FSA by A6,A19,AMI_1:def 19;
end;
A20: for n being Nat st P[n] holds P[n + 1]
proof
let n be Nat;
assume A21: P[n];
assume A22: k <= n + 1;
thus
A23: now per cases by A22,NAT_1:26;
suppose k = n + 1;
hence IC (Computation s10).(n + 1) = IC (Computation s00).k by A16
.= insloc card ProgramPart I0 by A1,A10,SCMFSA8A:def 5
.= insloc card I0 by AMI_5:72
.= insloc card I by SCMFSA8A:34;
suppose A24: k <= n;
(Computation s10).(n + 1) = Following (Computation s10).n by AMI_1:def
19
.= Exec(CurInstr (Computation s10).n,(Computation s10).n)
by AMI_1:def 18;
hence IC (Computation s10).(n + 1) = insloc card I by A21,A24,AMI_1:def
8;
end;
thus CurInstr (Computation s10).(n + 1)
= (Computation s10).(n + 1).IC (Computation s10).(n + 1)
by AMI_1:def 17
.= halt SCM+FSA by A6,A23,AMI_1:54;
end;
A25: for n being Nat holds P[n] from Ind(A18,A20);
now let n be Nat;
per cases;
suppose A26: n < k;
then IC (Computation s00).n = IC (Computation s10).n by A16;
then IC (Computation s10).n in dom I0 by A1,A10,A26,SCMFSA8A:def 5;
hence IC (Computation s10).n in dom I1 by A3;
suppose k <= n;
hence IC (Computation s10).n in dom I1 by A4,A25;
end;
hence I1 is_closed_on s by SCMFSA7B:def 7;
P[k] by A25;
then A27: s10 is halting by AMI_1:def 20;
hence I1 is_halting_on s by SCMFSA7B:def 8;
A28: CurInstr (Computation s10).k = halt SCM+FSA by A25;
now let n be Nat;
assume A29: CurInstr (Computation s10).n = halt SCM+FSA;
assume A30: k > n;
reconsider l = IC (Computation s00).n as Instruction-Location of SCM+FSA;
A31: l in dom I0 by A1,A10,A30,SCMFSA8A:def 5;
CurInstr (Computation s10).n = CurInstr (Computation s00).n by A14,A30
.= (Computation s00).n.l by AMI_1:def 17
.= s00.l by AMI_1:54
.= I0.l by A31,Th26;
then halt SCM+FSA in rng I0 by A29,A31,FUNCT_1:def 5;
hence contradiction by SCMFSA7B:def 6;
end;
then A32: LifeSpan s10 = k by A27,A28,SCM_1:def 2;
IC (Computation s10).k = insloc card I by A25;
then A33: IC (Computation s00).LifeSpan s10 = insloc card I by A16,A32;
A34: card ProgramPart I0 = card I0 by AMI_5:72
.= card I by SCMFSA8A:34;
for n be Nat st not IC (Computation s00).n in dom I0 holds
LifeSpan s10 <= n by A14,A32;
hence LifeSpan s10 = pseudo-LifeSpan(s,I0) by A1,A33,A34,SCMFSA8A:def 5;
set s1 = s +* (I +* Start-At insloc 0);
defpred P[Nat] means
$1 < pseudo-LifeSpan(s,I0) implies
IC (Computation s1).$1 in dom I &
IC (Computation s1).$1 = IC (Computation s10).$1 &
(Computation s1).$1 | D = (Computation s10).$1 | D;
A35: P[0]
proof
assume 0 < pseudo-LifeSpan(s,I0);
then IC (Computation (s +* (I0 +* Start-At insloc 0))).0 in dom I0
by A1,SCMFSA8A:31;
then IC (s +* (I0 +* Start-At insloc 0)) in dom I0 by AMI_1:def 19;
then A36: insloc 0 in dom I0 by Th31;
A37: IC (Computation s1).0 = IC s1 by AMI_1:def 19
.= IC (s +* I +* Start-At insloc 0) by FUNCT_4:15
.= insloc 0 by AMI_5:79;
hence IC (Computation s1).0 in dom I by A36,SCMFSA6A:14;
thus IC (Computation s1).0 = IC (Computation s10).0 by A12,A37,AMI_1:def
19;
thus (Computation s1).0 | D = s1 | D by AMI_1:def 19
.= s | D by SCMFSA8A:11
.= s10 | D by SCMFSA8A:11
.= (Computation s10).0 | D by AMI_1:def 19;
end;
A38: for n being Nat st P[n] holds P[n + 1]
proof
let n be Nat;
set l = IC (Computation s1).n;
set l0 = IC (Computation s10).n;
assume A39: P[n];
assume A40: n + 1 < pseudo-LifeSpan(s,I0);
A41: pseudo-LifeSpan(s,I0) = k by A1,Th50;
n < k by A10,A40,NAT_1:37;
then A42: IC (Computation s00).(n + 1) = IC (Computation s10).(n + 1) &
(Computation s00).n | D = (Computation s10).n | D &
l in dom I &
l = l0 &
(Computation s1).n | D = (Computation s10).n | D by A16,A39,A40,A41;
A43: l0 in dom I0 by A39,A40,NAT_1:37,SCMFSA6A:14;
A44: now assume A45: I.l = halt SCM+FSA;
A46: l0 in dom I & dom I = dom I0 by A39,A40,NAT_1:37,SCMFSA6A:14;
n < k by A10,A40,NAT_1:37;
then IC (Computation s00).n = IC (Computation s10).n by A16;
then A47: CurInstr (Computation s00).n = (Computation s00).n.l0 by AMI_1:
def 17
.= s00.l0 by AMI_1:54
.= I0.l by A39,A40,A46,Th26,NAT_1:37
.= goto insloc card I by A39,A40,A45,NAT_1:37,SCMFSA8A:30;
A48: IC (Computation s00).(n + 1)
= IC Following (Computation s00).n by AMI_1:def 19
.= IC Exec(goto insloc card I,(Computation s00).n) by A47,AMI_1:def 18
.= Exec(goto insloc card I,(Computation s00).n).IC SCM+FSA
by AMI_1:def 15
.= insloc card I by SCMFSA_2:95
.= insloc card I0 by SCMFSA8A:34;
IC (Computation s00).(n + 1) in dom I0 by A1,A40,SCMFSA8A:31;
hence contradiction by A48,SCMFSA6A:15;
end;
A49: CurInstr (Computation s1).n = (Computation s1).n.l by AMI_1:def 17
.= s1.l by AMI_1:54
.= I.l by A39,A40,Th26,NAT_1:37
.= I0.l0 by A39,A40,A44,NAT_1:37,SCMFSA8A:30
.= I1.l0 by A2,A43,GRFUNC_1:8
.= s10.l0 by A3,A43,Th26
.= (Computation s10).n.l0 by AMI_1:54
.= CurInstr (Computation s10).n by AMI_1:def 17;
A50: (Computation s1).(n + 1) = Following (Computation s1).n by AMI_1:def 19
.= Exec(CurInstr (Computation s1).n,(Computation s1).n) by AMI_1:def 18;
A51: (Computation s10).(n + 1) = Following (Computation s10).n by AMI_1:def
19
.= Exec(CurInstr (Computation s1).n,(Computation s10).n)
by A49,AMI_1:def 18;
(for a being Int-Location holds
(Computation s1).n.a = (Computation s10).n.a) &
for f being FinSeq-Location holds
(Computation s1).n.f = (Computation s10).n.f
by A39,A40,NAT_1:37,SCMFSA6A:38;
then (Computation s1).n,(Computation s10).n equal_outside A
by A39,A40,NAT_1:37,SCMFSA6A:28;
then A52: (Computation s1).(n + 1),(Computation s10).(n + 1) equal_outside A
by A50,A51,SCMFSA6A:32;
dom I0 = dom I & IC (Computation s00).(n + 1) in dom I0
by A1,A40,SCMFSA6A:14,SCMFSA8A:31;
hence IC (Computation s1).(n + 1) in dom I by A42,A52,SCMFSA6A:29;
thus IC (Computation s1).(n + 1) = IC (Computation s10).(n + 1)
by A52,SCMFSA6A:29;
(for a being Int-Location holds
(Computation s1).(n + 1).a = (Computation s10).(n + 1).a) &
for f being FinSeq-Location holds
(Computation s1).(n + 1).f = (Computation s10).(n + 1).f
by A52,SCMFSA6A:30,31;
hence (Computation s1).(n + 1) | D = (Computation s10).(n + 1) | D
by SCMFSA6A:38;
end;
A53: for n being Nat holds P[n] from Ind(A35,A38);
hence for n be Nat st n < pseudo-LifeSpan(s,I0) holds
IC (Computation s1).n = IC (Computation s10).n;
let n be Nat;
assume A54: n <= pseudo-LifeSpan(s,Directed I);
per cases by A54,REAL_1:def 5;
suppose n < pseudo-LifeSpan(s,I0);
hence (Computation s1).n | D = (Computation s10).n | D by A53;
suppose A55: n = pseudo-LifeSpan(s,I0);
hereby per cases by NAT_1:22;
suppose A56: n = 0;
hence (Computation s1).n | D = s1 | D by AMI_1:def 19
.= s | D by SCMFSA8A:11
.= s10 | D by SCMFSA8A:11
.= (Computation s10).n | D by A56,AMI_1:def 19;
suppose ex m st n = m + 1;
then consider m being Nat such that A57: n = m + 1;
A58: (Computation s1).n = Following (Computation s1).m by A57,AMI_1:def 19
.= Exec(CurInstr (Computation s1).m,(Computation s1).m) by AMI_1:def 18;
A59: (Computation s10).n = Following (Computation s10).m by A57,AMI_1:def 19
.= Exec(CurInstr (Computation s10).m,(Computation s10).m) by AMI_1:def 18;
set i = CurInstr (Computation s1).m;
set l = IC (Computation s1).m;
set l0 = IC (Computation s10).m;
A60: m + 0 < pseudo-LifeSpan(s,I0) by A55,A57,REAL_1:53;
then A61: (Computation s1).m | D = (Computation s10).m | D & l in dom I & l =
l0
by A53;
then A62: l0 in dom I0 by SCMFSA6A:14;
A63: i = (Computation s1).m.l by AMI_1:def 17
.= s1.l by AMI_1:54
.= I.l by A61,Th26;
I0 c= I1 by SCMFSA6A:55;
then A64: I0.l0 = I1.l0 by A62,GRFUNC_1:8
.= s10.l0 by A3,A62,Th26
.= (Computation s10).m.l0 by AMI_1:54
.= CurInstr (Computation s10).m by AMI_1:def 17;
hereby per cases;
suppose A65: i = halt SCM+FSA;
then CurInstr (Computation s10).m = goto insloc card I
by A61,A63,A64,SCMFSA8A:30;
then InsCode CurInstr (Computation s10).m = 6 by SCMFSA_2:47;
then A66: InsCode CurInstr (Computation s10).m in {0,6,7,8} by ENUMSET1:19;
thus (Computation s1).n | D
= (Computation s1).m | D by A58,A65,AMI_1:def 8
.= (Computation s10).m | D by A53,A60
.= (Computation s10).n | D by A59,A66,Th32;
suppose i <> halt SCM+FSA;
then CurInstr (Computation s10).m = i by A61,A63,A64,SCMFSA8A:30;
hence (Computation s1).n | D = (Computation s10).n | D
by A58,A59,A61,SCMFSA6C:5;
end;
end;
end;
theorem Th59: ::T29502'
for s being State of SCM+FSA, I being Macro-Instruction st
Directed I is_pseudo-closed_on s holds
(Result (s +* (I ';' SCM+FSA-Stop +* Start-At insloc 0))) | D =
(Computation (s +* (I +* Start-At insloc 0))).
pseudo-LifeSpan(s,Directed I) | D
proof
let s be State of SCM+FSA;
let I be Macro-Instruction;
set I0 = Directed I;
set I1 = I ';' SCM+FSA-Stop;
set s2 = s +* (I +* Start-At insloc 0);
set s10 = s +* (I1 +* Start-At insloc 0);
set k = pseudo-LifeSpan(s,I0);
assume I0 is_pseudo-closed_on s;
then A1: I1 is_halting_on s & LifeSpan s10 = k &
(Computation s2).k | D = (Computation s10).k | D by Th58;
then s10 is halting by SCMFSA7B:def 8;
hence (Result s10) | D = (Computation s2).k | D by A1,SCMFSA6B:16;
end;
theorem
for s being State of SCM+FSA, I being Macro-Instruction st
s.intloc 0 = 1 & Directed I is_pseudo-closed_on s holds
IExec(I ';' SCM+FSA-Stop,s) | D =
(Computation (s +* (I +* Start-At insloc 0))).
pseudo-LifeSpan(s,Directed I) | D
proof
let s be State of SCM+FSA;
let I be Macro-Instruction;
set I0 = Directed I;
set I1 = I ';' SCM+FSA-Stop;
set s2 = s +* (I +* Start-At insloc 0);
set s10 = s +* (I1 +* Start-At insloc 0);
set k = pseudo-LifeSpan(s,I0);
assume A1: s.intloc 0 = 1;
assume A2: I0 is_pseudo-closed_on s;
thus IExec(I1,s) | D
= (Result (s +* Initialized I1) +* s | A) | D by SCMFSA6B:def 1
.= (Result (s +* Initialized I1)) | D by Th35
.= (Result s10) | D by A1,Th18
.= (Computation s2).k | D by A2,Th59;
end;
theorem Th61: ::TMP20 ** n.t
for I,J being Macro-Instruction,a being Int-Location holds
if=0(a,I,J).insloc (card I + card J + 3) = halt SCM+FSA
proof
let I,J be Macro-Instruction;
let a be Int-Location;
A1: if=0(a,I,J) = a =0_goto insloc (card J + 3) ';' J ';'
Goto insloc (card I + 1) ';' I ';' SCM+FSA-Stop by SCMFSA8B:def 1;
set II =
a =0_goto insloc (card J + 3) ';' J ';' Goto insloc (card I + 1) ';' I;
A2: card II = card (Macro (a =0_goto insloc (card J + 3)) ';' J ';'
Goto insloc (card I + 1) ';' I) by SCMFSA6A:def 5
.= card (Macro (a =0_goto insloc (card J + 3)) ';' J ';'
Goto insloc (card I + 1)) + card I by SCMFSA6A:61
.= card (Macro (a =0_goto insloc (card J + 3)) ';' J) +
card Goto insloc (card I + 1) + card I by SCMFSA6A:61
.= card (Macro (a =0_goto insloc (card J + 3)) ';' J) + 1 + card I
by SCMFSA8A:29
.= card Macro (a =0_goto insloc (card J + 3)) + card J + 1 + card I
by SCMFSA6A:61
.= 2 + card J + 1 + card I by SCMFSA7B:6
.= card J + (2 + 1) + card I by XCMPLX_1:1
.= card I + card J + 3 by XCMPLX_1:1;
then A3: card I + card J + 3 < card II + card SCM+FSA-Stop by NAT_1:38,SCMFSA8A
:17;
card I + card J + 3 -' card II = 0 by A2,GOBOARD9:1;
hence if=0(a,I,J).insloc (card I + card J + 3)
= IncAddr(halt SCM+FSA,card II) by A1,A2,A3,Th13,SCMFSA8A:16
.= halt SCM+FSA by SCMFSA_4:8;
end;
theorem Th62: ::TMP20' ** n.t
for I,J being Macro-Instruction,a being Int-Location holds
if>0(a,I,J).insloc (card I + card J + 3) = halt SCM+FSA
proof
let I,J be Macro-Instruction;
let a be Int-Location;
A1: if>0(a,I,J) = a >0_goto insloc (card J + 3) ';' J ';'
Goto insloc (card I + 1) ';' I ';' SCM+FSA-Stop by SCMFSA8B:def 2;
set II =
a >0_goto insloc (card J + 3) ';' J ';' Goto insloc (card I + 1) ';' I;
A2: card II = card (Macro (a >0_goto insloc (card J + 3)) ';' J ';'
Goto insloc (card I + 1) ';' I) by SCMFSA6A:def 5
.= card (Macro (a >0_goto insloc (card J + 3)) ';' J ';'
Goto insloc (card I + 1)) + card I by SCMFSA6A:61
.= card (Macro (a >0_goto insloc (card J + 3)) ';' J) +
card Goto insloc (card I + 1) + card I by SCMFSA6A:61
.= card (Macro (a >0_goto insloc (card J + 3)) ';' J) + 1 + card I
by SCMFSA8A:29
.= card Macro (a >0_goto insloc (card J + 3)) + card J + 1 + card I
by SCMFSA6A:61
.= 2 + card J + 1 + card I by SCMFSA7B:6
.= card J + (2 + 1) + card I by XCMPLX_1:1
.= card I + card J + 3 by XCMPLX_1:1;
then A3: card I + card J + 3 < card II + card SCM+FSA-Stop by NAT_1:38,SCMFSA8A
:17;
card I + card J + 3 -' card II = 0 by A2,GOBOARD9:1;
hence if>0(a,I,J).insloc (card I + card J + 3)
= IncAddr(halt SCM+FSA,card II) by A1,A2,A3,Th13,SCMFSA8A:16
.= halt SCM+FSA by SCMFSA_4:8;
end;
theorem Th63: ::TMP21 ** n.t
for I,J being Macro-Instruction,a being Int-Location holds
if=0(a,I,J).insloc (card J + 2) = goto insloc (card I + card J + 3)
proof
let I,J be Macro-Instruction;
let a be Int-Location;
set JJ = a =0_goto insloc (card J + 3) ';' J;
set J3 = a =0_goto insloc (card J + 3) ';' J ';' Goto insloc (card I + 1);
A1: if=0(a,I,J) = a =0_goto insloc (card J + 3) ';' J ';'
Goto insloc (card I + 1) ';' I ';' SCM+FSA-Stop by SCMFSA8B:def 1;
A2: card JJ
= card (Macro (a =0_goto insloc (card J + 3)) ';' J) by SCMFSA6A:def 5
.= card Macro (a =0_goto insloc (card J + 3)) + card J by SCMFSA6A:61
.= 2 + card J by SCMFSA7B:6;
card Goto insloc (card I + 1) = 1 by SCMFSA8A:29;
then A3: card J3 = card J + 2 + 1 by A2,SCMFSA6A:61
.= card J + (2 + 1) by XCMPLX_1:1;
card J + 2 -' card JJ = 0 by A2,GOBOARD9:1;
then A4: goto insloc (card I + 1) =
(Goto insloc (card I + 1)).insloc (card J + 2 -' card JJ)
by SCMFSA8A:47;
card Goto insloc (card I + 1) = 1 by SCMFSA8A:29;
then card J + 2 < card JJ + card Goto insloc (card I + 1) by A2,NAT_1:38;
then A5: J3.insloc (card J + 2)
= IncAddr(goto insloc (card I + 1),card JJ) by A2,A4,Th13
.= goto (insloc (card I + 1) + (card J + 2)) by A2,SCMFSA_4:14
.= goto insloc (card I + 1 + (card J + 2)) by SCMFSA_4:def 1
.= goto insloc (card I + 1 + card J + 2) by XCMPLX_1:1
.= goto insloc (card I + (card J + 1) + 2) by XCMPLX_1:1
.= goto insloc (card I + (card J + 1 + 2)) by XCMPLX_1:1
.= goto insloc (card I + (card J + (1 + 2))) by XCMPLX_1:1
.= goto insloc (card I + card J + (1 + 2)) by XCMPLX_1:1;
A6: 6 <> 0 & InsCode goto insloc (card I + card J + 3) = 6 &
InsCode halt SCM+FSA = 0 by SCMFSA_2:47,124;
card J3 = card J + 2 + 1 by A3,XCMPLX_1:1;
then card J + 2 < card J3 by NAT_1:38;
then A7: insloc (card J + 2) in dom J3 by SCMFSA6A:15;
then (J3 ';' (I ';' SCM+FSA-Stop)).insloc (card J + 2)
= (Directed J3).insloc (card J + 2) by SCMFSA8A:28
.= goto insloc (card I + card J + 3) by A5,A6,A7,SCMFSA8A:30;
hence if=0(a,I,J).insloc (card J + 2)
= goto insloc (card I + card J + 3) by A1,SCMFSA6A:62;
end;
theorem Th64: ::TMP21' ** n.t
for I,J being Macro-Instruction,a being Int-Location holds
if>0(a,I,J).insloc (card J + 2) = goto insloc (card I + card J + 3)
proof
let I,J be Macro-Instruction;
let a be Int-Location;
set JJ = a >0_goto insloc (card J + 3) ';' J;
set J3 = a >0_goto insloc (card J + 3) ';' J ';' Goto insloc (card I + 1);
A1: if>0(a,I,J) = a >0_goto insloc (card J + 3) ';' J ';'
Goto insloc (card I + 1) ';' I ';' SCM+FSA-Stop by SCMFSA8B:def 2;
A2: card JJ
= card (Macro (a >0_goto insloc (card J + 3)) ';' J) by SCMFSA6A:def 5
.= card Macro (a >0_goto insloc (card J + 3)) + card J by SCMFSA6A:61
.= 2 + card J by SCMFSA7B:6;
card Goto insloc (card I + 1) = 1 by SCMFSA8A:29;
then A3: card J3 = card J + 2 + 1 by A2,SCMFSA6A:61
.= card J + (2 + 1) by XCMPLX_1:1;
card J + 2 -' card JJ = 0 by A2,GOBOARD9:1;
then A4: goto insloc (card I + 1) =
(Goto insloc (card I + 1)).insloc (card J + 2 -' card JJ)
by SCMFSA8A:47;
card Goto insloc (card I + 1) = 1 by SCMFSA8A:29;
then card J + 2 < card JJ + card Goto insloc (card I + 1) by A2,NAT_1:38;
then A5: J3.insloc (card J + 2)
= IncAddr(goto insloc (card I + 1),card JJ) by A2,A4,Th13
.= goto (insloc (card I + 1) + (card J + 2)) by A2,SCMFSA_4:14
.= goto insloc (card I + 1 + (card J + 2)) by SCMFSA_4:def 1
.= goto insloc (card I + 1 + card J + 2) by XCMPLX_1:1
.= goto insloc (card I + (card J + 1) + 2) by XCMPLX_1:1
.= goto insloc (card I + (card J + 1 + 2)) by XCMPLX_1:1
.= goto insloc (card I + (card J + (1 + 2))) by XCMPLX_1:1
.= goto insloc (card I + card J + (1 + 2)) by XCMPLX_1:1;
A6: 6 <> 0 & InsCode goto insloc (card I + card J + 3) = 6 &
InsCode halt SCM+FSA = 0 by SCMFSA_2:47,124;
card J3 = card J + 2 + 1 by A3,XCMPLX_1:1;
then card J + 2 < card J3 by NAT_1:38;
then A7: insloc (card J + 2) in dom J3 by SCMFSA6A:15;
then (J3 ';' (I ';' SCM+FSA-Stop)).insloc (card J + 2)
= (Directed J3).insloc (card J + 2) by SCMFSA8A:28
.= goto insloc (card I + card J + 3) by A5,A6,A7,SCMFSA8A:30;
hence if>0(a,I,J).insloc (card J + 2)
= goto insloc (card I + card J + 3) by A1,SCMFSA6A:62;
end;
theorem Th65: ::T31139 ** n.t
for J being Macro-Instruction,a being Int-Location holds
if=0(a,Goto insloc 2,J).insloc (card J + 3) = goto insloc (card J + 5)
proof
let J be Macro-Instruction;
let a be Int-Location;
set JJ = a =0_goto insloc (card J + 3) ';' J;
set J3 = a =0_goto insloc (card J + 3) ';' J ';' Goto insloc 2;
set J4 =
a =0_goto insloc (card J + 3) ';' J ';' Goto insloc 2 ';' Goto insloc 2;
card Goto insloc 2 = 1 by SCMFSA8A:29;
then A1: if=0(a,Goto insloc 2,J) = (a =0_goto insloc (card J + 3) ';' J ';'
Goto insloc (1 + 1) ';' Goto insloc 2) ';' SCM+FSA-Stop
by SCMFSA8B:def 1;
A2: card Goto insloc 2 = 1 by SCMFSA8A:29;
card JJ
= card (Macro (a =0_goto insloc (card J + 3)) ';' J) by SCMFSA6A:def 5
.= card Macro (a =0_goto insloc (card J + 3)) + card J by SCMFSA6A:61
.= 2 + card J by SCMFSA7B:6;
then A3: card J3 = card J + 2 + 1 by A2,SCMFSA6A:61
.= card J + (2 + 1) by XCMPLX_1:1;
then A4: card J4 = card J + 3 + 1 by A2,SCMFSA6A:61
.= card J + (3 + 1) by XCMPLX_1:1;
card J + 3 -' card J3 = 0 by A3,GOBOARD9:1;
then A5: goto insloc 2 = (Goto insloc 2).insloc (card J + 3 -' card J3)
by SCMFSA8A:47;
card Goto insloc 2 = 1 by SCMFSA8A:29;
then card J + 3 < card J3 + card Goto insloc 2 by A3,NAT_1:38;
then A6: J4.insloc (card J + 3)
= IncAddr(goto insloc 2,card J3) by A3,A5,Th13
.= goto (insloc 2 + (card J + 3)) by A3,SCMFSA_4:14
.= goto insloc (2 + (card J + 3)) by SCMFSA_4:def 1
.= goto insloc (card J + (2 + 3)) by XCMPLX_1:1;
A7: 6 <> 0 & InsCode goto insloc (card J + 5) = 6 &
InsCode halt SCM+FSA = 0 by SCMFSA_2:47,124;
card J4 = card J + 3 + 1 by A4,XCMPLX_1:1;
then card J + 3 < card J4 by NAT_1:38;
then A8: insloc (card J + 3) in dom J4 by SCMFSA6A:15;
then (J4 ';' SCM+FSA-Stop).insloc (card J + 3)
= (Directed J4).insloc (card J + 3) by SCMFSA8A:28
.= goto insloc (card J + 5) by A6,A7,A8,SCMFSA8A:30;
hence if=0(a,Goto insloc 2,J).insloc (card J + 3)
= goto insloc (card J + 5) by A1;
end;
theorem Th66: ::TMP71
for s being State of SCM+FSA, I,J being Macro-Instruction,
a being read-write Int-Location
st s.a = 0 & Directed I is_pseudo-closed_on s holds
if=0(a,I,J) is_halting_on s & if=0(a,I,J) is_closed_on s &
LifeSpan (s +* (if=0(a,I,J) +* Start-At insloc 0)) =
LifeSpan (s +* (I ';' SCM+FSA-Stop +* Start-At insloc 0)) + 1
proof
let s be State of SCM+FSA;
let I,J be Macro-Instruction;
let a be read-write Int-Location;
set I0 = Directed I;
set I1 = I ';' SCM+FSA-Stop;
set s00 = s +* (I0 +* Start-At insloc 0);
set s3 = s +* (if=0(a,I,J) +* Start-At insloc 0);
set s4 = (Computation s3).1;
set C3 = Computation s3;
set i = a =0_goto insloc (card J + 3);
assume A1: s.a = 0;
assume A2: I0 is_pseudo-closed_on s;
A3: if=0(a,I,J) = a =0_goto insloc (card J + 3) ';' J ';'
Goto insloc (card I + 1) ';' I ';' SCM+FSA-Stop by SCMFSA8B:def 1;
A4: I0 +* Start-At insloc 0 c= s00 by FUNCT_4:26;
s | D = s00 | D by SCMFSA8A:11;
then A5: I0 is_pseudo-closed_on s00 by A2,Th52;
A6: insloc 0 in dom if=0(a,I,J) by Th54;
if=0(a,I,J) c= if=0(a,I,J) +* Start-At insloc 0 by SCMFSA8A:9;
then A7: dom if=0(a,I,J) c= dom (if=0(a,I,J) +* Start-At insloc 0)
by GRFUNC_1:8;
A8: IC SCM+FSA in dom (if=0(a,I,J) +* Start-At insloc 0) by SF_MASTR:65;
A9: now thus IC s3 = s3.IC SCM+FSA by AMI_1:def 15
.= (if=0(a,I,J) +* Start-At insloc 0).IC SCM+FSA by A8,FUNCT_4:14
.= insloc 0 by SF_MASTR:66;
end;
now thus s3.insloc 0
= (if=0(a,I,J) +* Start-At insloc 0).insloc 0 by A6,A7,FUNCT_4:14
.= if=0(a,I,J).insloc 0 by A6,SCMFSA6B:7
.= i by Th55;
end;
then A10: CurInstr s3 = i by A9,AMI_1:def 17;
A11: now thus (Computation s3).(0 + 1)
= Following (Computation s3).0 by AMI_1:def 19
.= Following s3 by AMI_1:def 19
.= Exec(i,s3) by A10,AMI_1:def 18;
end;
A12: now thus card (i ';' J ';' Goto insloc (card I + 1))
= card (Macro i ';' J ';' Goto insloc (card I + 1)) by SCMFSA6A:def 5
.= card (Macro i ';' J) + card Goto insloc (card I + 1) by SCMFSA6A:61
.= card (Macro i ';' J) + 1 by SCMFSA8A:29
.= card Macro i + card J + 1 by SCMFSA6A:61
.= card J + 2 + 1 by SCMFSA7B:6
.= card J + (2 + 1) by XCMPLX_1:1;
end;
not a in dom (if=0(a,I,J) +* Start-At insloc 0) & a in dom s
by SCMFSA6B:12,SCMFSA_2:66;
then A13: s3.a = 0 by A1,FUNCT_4:12;
A14: if=0(a,I,J) +* Start-At insloc 0 c= s3 by FUNCT_4:26;
if=0(a,I,J) c= if=0(a,I,J) +* Start-At insloc 0 by SCMFSA8A:9;
then A15: if=0(a,I,J) c= s3 by A14,XBOOLE_1:1;
if=0(a,I,J) = i ';' J ';' Goto insloc (card I + 1) ';' I1
by A3,SCMFSA6A:62;
then ProgramPart Relocated(I1,card J + 3) c= if=0(a,I,J) by A12,Lm5;
then ProgramPart Relocated(I1,card J + 3) c= s3 by A15,XBOOLE_1:1;
then ProgramPart ProgramPart Relocated(I1,card J + 3) c= s4 by AMI_5:64;
then A16: ProgramPart Relocated(I1,card J + 3) c= s4 by AMI_5:72;
I0 c= I1 by SCMFSA6A:55;
then ProgramPart Relocated(I0,card J + 3) c= ProgramPart Relocated(I1,card
J + 3)
by Th12;
then A17: ProgramPart Relocated(I0,card J + 3) c= s4 by A16,XBOOLE_1:1;
A18: now thus IC C3.1 = C3.1.IC SCM+FSA by AMI_1:def 15
.= insloc (card J + 3) by A11,A13,SCMFSA_2:96;
end;
s00,s3 equal_outside A by SCMFSA8A:14;
then A19: s00 | D = s3 | D by SCMFSA6A:39;
A20: now let a be Int-Location;
thus s00.a = s3.a by A19,SCMFSA6A:38
.= s4.a by A11,SCMFSA_2:96;
end;
now let f be FinSeq-Location;
thus s00.f = s3.f by A19,SCMFSA6A:38
.= s4.f by A11,SCMFSA_2:96;
end;
then A21: s00 | D = s4 | D by A20,SCMFSA6A:38;
if=0(a,I,J) +* Start-At insloc 0 c= s3 by FUNCT_4:26;
then A22: if=0(a,I,J) c= s3 by SCMFSA6B:5;
now thus card if=0(a,I,J) = card I + card J + (3 + 1) by SCMFSA8B:14
.= card I + card J + 3 + 1 by XCMPLX_1:1;
end;
then card I + card J + 3 < card if=0(a,I,J) by NAT_1:38;
then A23: insloc (card I + card J + 3) in dom if=0(a,I,J) by SCMFSA6A:15;
A24: now thus IC (Computation s3).(pseudo-LifeSpan(s00,I0) + 1)
= IC (Computation s4).pseudo-LifeSpan(s00,I0) by AMI_1:51
.= IC (Computation s00).pseudo-LifeSpan(s00,I0) + (card J + 3)
by A4,A5,A17,A18,A21,Th51
.= IC (Computation s00).pseudo-LifeSpan(s,I0) + (card J + 3) by A2,Th50
.= insloc card ProgramPart I0 + (card J + 3) by A2,SCMFSA8A:def 5
.= insloc card I0 + (card J + 3) by AMI_5:72
.= insloc card I + (card J + 3) by SCMFSA8A:34
.= insloc (card I + (card J + 3)) by SCMFSA_4:def 1
.= insloc (card I + card J + 3) by XCMPLX_1:1;
end;
then A25: CurInstr (Computation s3).(pseudo-LifeSpan(s00,I0) + 1)
= (Computation s3).(pseudo-LifeSpan(s00,I0) + 1).
insloc (card I + card J + 3) by AMI_1:def 17
.= s3.insloc (card I + card J + 3) by AMI_1:54
.= if=0(a,I,J).insloc (card I + card J + 3) by A22,A23,GRFUNC_1:8
.= halt SCM+FSA by Th61;
then A26: s3 is halting by AMI_1:def 20;
hence if=0(a,I,J) is_halting_on s by SCMFSA7B:def 8;
now let k be Nat;
per cases by NAT_1:19;
suppose k = 0;
then (Computation s3).k = s3 by AMI_1:def 19;
then IC (Computation s3).k = insloc 0 by Th31;
hence IC (Computation s3).k in dom if=0(a,I,J) by Th54;
suppose A27: 0 < k & k < pseudo-LifeSpan(s00,I0) + 1;
then 0 + 1 <= k by INT_1:20;
then consider k1 being Nat such that A28: 1 + k1 = k by NAT_1:28;
A29: k1 < pseudo-LifeSpan(s00,I0) by A27,A28,AXIOMS:24;
then A30: k1 < pseudo-LifeSpan(s,I0) by A2,Th50;
A31: IC (Computation s3).k = IC (Computation s4).k1 by A28,AMI_1:51
.= IC (Computation s00).k1 + (card J + 3) by A4,A5,A17,A18,A21,A29,Th51;
consider n being Nat such that
A32: IC (Computation s00).k1 = insloc n by SCMFSA_2:21;
insloc n in dom I0 by A2,A30,A32,SCMFSA8A:31;
then n < card I0 by SCMFSA6A:15;
then n + (card J + 3) < card I0 + (card J + 3) by REAL_1:53;
then n + (card J + 3) < card I + (card J + 3) by SCMFSA8A:34;
then A33: n + (card J + 3) < card I + card J + 3 by XCMPLX_1:1;
card if=0(a,I,J) = card I + card J + (3 + 1) by SCMFSA8B:14
.= card I + card J + 3 + 1 by XCMPLX_1:1;
then card I + card J + 3 < card if=0(a,I,J) by REAL_1:69;
then n + (card J + 3) < card if=0(a,I,J) by A33,AXIOMS:22;
then insloc (n + (card J + 3)) in dom if=0(a,I,J) by SCMFSA6A:15;
hence IC (Computation s3).k in
dom if=0(a,I,J) by A31,A32,SCMFSA_4:def 1;
suppose 0 < k & pseudo-LifeSpan(s00,I0) + 1 <= k;
hence IC (Computation s3).k in dom if=0(a,I,J) by A23,A24,A25,AMI_1:52;
end;
hence if=0(a,I,J) is_closed_on s by SCMFSA7B:def 7;
now let k be Nat;
assume A34: CurInstr (Computation s3).k = halt SCM+FSA;
assume not pseudo-LifeSpan(s00,I0) + 1 <= k;
then A35: k <= pseudo-LifeSpan(s00,I0) by NAT_1:38;
A36: IC s3 = insloc 0 by Th31;
A37: insloc 0 in dom if=0(a,I,J) by Th54;
A38: InsCode halt SCM+FSA = 0 & InsCode (a =0_goto insloc (card J + 3)) = 7
by SCMFSA_2:48,124;
CurInstr (Computation s3).0 = CurInstr s3 by AMI_1:def 19
.= s3.insloc 0 by A36,AMI_1:def 17
.= if=0(a,I,J).insloc 0 by A37,Th26
.= a =0_goto insloc (card J + 3) by Th55;
then consider k1 being Nat such that A39: k1 + 1 = k by A34,A38,NAT_1:22;
k1 < k by A39,REAL_1:69;
then A40: k1 < pseudo-LifeSpan(s00,I0) by A35,AXIOMS:22;
A41: IC (Computation s3).k = IC (Computation s4).k1 by A39,AMI_1:51
.= IC (Computation s00).k1 + (card J + 3) by A4,A5,A17,A18,A21,A40,Th51;
consider n being Nat such that
A42: IC (Computation s00).k1 = insloc n by SCMFSA_2:21;
k1 < pseudo-LifeSpan(s,I0) by A2,A40,Th50;
then insloc n in dom I0 by A2,A42,SCMFSA8A:31;
then n < card I0 by SCMFSA6A:15;
then n + (card J + 3) < card I0 + (card J + 3) by REAL_1:53;
then n + (card J + 3) < card I + (card J + 3) by SCMFSA8A:34;
then A43: n + (card J + 3) < card I + card J + 3 by XCMPLX_1:1;
card if=0(a,I,J) = card I + card J + (3 + 1) by SCMFSA8B:14
.= card I + card J + 3 + 1 by XCMPLX_1:1;
then card I + card J + 3 < card if=0(a,I,J) by REAL_1:69;
then n + (card J + 3) < card if=0(a,I,J) by A43,AXIOMS:22;
then insloc (n + (card J + 3)) in dom if=0(a,I,J) by SCMFSA6A:15;
then A44: IC (Computation s3).k in dom if=0(a,I,J) by A41,A42,SCMFSA_4:def 1;
set J1 = a =0_goto insloc (card J + 3) ';' J ';'
Goto insloc (card I + 1) ';' I;
card J1
= card (Macro (a =0_goto insloc (card J + 3)) ';' J ';'
Goto insloc (card I + 1) ';' I) by SCMFSA6A:def 5
.= card (Macro (a =0_goto insloc (card J + 3)) ';' J ';'
Goto insloc (card I + 1)) + card I by SCMFSA6A:61
.= card (Macro (a =0_goto insloc (card J + 3)) ';' J) +
card Goto insloc (card I + 1) + card I by SCMFSA6A:61
.= card (Macro (a =0_goto insloc (card J + 3)) ';' J) + 1 + card I
by SCMFSA8A:29
.= card Macro (a =0_goto insloc (card J + 3)) + card J + 1 + card I
by SCMFSA6A:61
.= 2 + card J + 1 + card I by SCMFSA7B:6
.= card J + (2 + 1) + card I by XCMPLX_1:1
.= card I + card J + 3 by XCMPLX_1:1;
then insloc (n + (card J + 3)) in dom J1 by A43,SCMFSA6A:15;
then IC (Computation s3).k in dom J1 by A41,A42,SCMFSA_4:def 1;
then A45: IC (Computation s3).k in dom Directed J1 by SCMFSA6A:14;
Directed J1 c= if=0(a,I,J) by A3,SCMFSA6A:55;
then A46: if=0(a,I,J).IC (Computation s3).k = (Directed J1).IC (Computation
s3).k
by A45,GRFUNC_1:8;
A47: (Directed J1).IC (Computation s3).k in rng Directed J1 by A45,FUNCT_1:def
5;
CurInstr (Computation s3).k
= (Computation s3).k.IC (Computation s3).k by AMI_1:def 17
.= s3.IC (Computation s3).k by AMI_1:54
.= if=0(a,I,J).IC (Computation s3).k by A44,Th26;
hence contradiction by A34,A46,A47,SCMFSA7B:def 6;
end;
then A48: LifeSpan s3 = pseudo-LifeSpan(s00,I0) + 1 by A25,A26,SCM_1:def 2;
pseudo-LifeSpan(s,I0) = LifeSpan (s +* (I1 +* Start-At insloc 0))
by A2,Th58;
hence LifeSpan s3 = LifeSpan (s +* (I1 +* Start-At insloc 0)) + 1
by A2,A48,Th50;
end;
theorem
for s being State of SCM+FSA, I,J being Macro-Instruction,
a being read-write Int-Location
st s.intloc 0 = 1 & s.a = 0 & Directed I is_pseudo-closed_on s holds
IExec(if=0(a,I,J),s) | (Int-Locations \/ FinSeq-Locations) =
IExec(I ';' SCM+FSA-Stop,s) | (Int-Locations \/ FinSeq-Locations)
proof
let ss be State of SCM+FSA;
let I,J be Macro-Instruction;
let a be read-write Int-Location;
set I0 = Directed I;
set s = Initialize ss;
set I1 = I ';' SCM+FSA-Stop;
set s00 = s +* (I0 +* Start-At insloc 0);
set s3 = s +* (if=0(a,I,J) +* Start-At insloc 0);
set s4 = (Computation s3).1;
set C3 = Computation s3;
set i = a =0_goto insloc (card J + 3);
assume A1: ss.intloc 0 = 1;
assume ss.a = 0;
then A2: s.a = 0 by SCMFSA6C:3;
assume I0 is_pseudo-closed_on ss;
then A3: I0 is_pseudo-closed_on s by A1,Th53;
A4: if=0(a,I,J) = a =0_goto insloc (card J + 3) ';' J ';'
Goto insloc (card I + 1) ';' I ';' SCM+FSA-Stop by SCMFSA8B:def 1;
A5: I0 +* Start-At insloc 0 c= s00 by FUNCT_4:26;
s | D = s00 | D by SCMFSA8A:11;
then A6: I0 is_pseudo-closed_on s00 by A3,Th52;
A7: insloc 0 in dom if=0(a,I,J) by Th54;
if=0(a,I,J) c= if=0(a,I,J) +* Start-At insloc 0 by SCMFSA8A:9;
then A8: dom if=0(a,I,J) c= dom (if=0(a,I,J) +* Start-At insloc 0)
by GRFUNC_1:8;
A9: IC SCM+FSA in dom (if=0(a,I,J) +* Start-At insloc 0) by SF_MASTR:65;
A10: now thus IC s3 = s3.IC SCM+FSA by AMI_1:def 15
.= (if=0(a,I,J) +* Start-At insloc 0).IC SCM+FSA by A9,FUNCT_4:14
.= insloc 0 by SF_MASTR:66;
end;
now thus s3.insloc 0
= (if=0(a,I,J) +* Start-At insloc 0).insloc 0 by A7,A8,FUNCT_4:14
.= if=0(a,I,J).insloc 0 by A7,SCMFSA6B:7
.= i by Th55;
end;
then A11: CurInstr s3 = i by A10,AMI_1:def 17;
A12: now thus (Computation s3).(0 + 1)
= Following (Computation s3).0 by AMI_1:def 19
.= Following s3 by AMI_1:def 19
.= Exec(i,s3) by A11,AMI_1:def 18;
end;
A13: now thus card (i ';' J ';' Goto insloc (card I + 1))
= card (Macro i ';' J ';' Goto insloc (card I + 1)) by SCMFSA6A:def 5
.= card (Macro i ';' J) + card Goto insloc (card I + 1) by SCMFSA6A:61
.= card (Macro i ';' J) + 1 by SCMFSA8A:29
.= card Macro i + card J + 1 by SCMFSA6A:61
.= card J + 2 + 1 by SCMFSA7B:6
.= card J + (2 + 1) by XCMPLX_1:1;
end;
not a in dom (if=0(a,I,J) +* Start-At insloc 0) & a in dom s
by SCMFSA6B:12,SCMFSA_2:66;
then A14: s3.a = 0 by A2,FUNCT_4:12;
A15: if=0(a,I,J) +* Start-At insloc 0 c= s3 by FUNCT_4:26;
if=0(a,I,J) c= if=0(a,I,J) +* Start-At insloc 0 by SCMFSA8A:9;
then A16: if=0(a,I,J) c= s3 by A15,XBOOLE_1:1;
if=0(a,I,J) = i ';' J ';' Goto insloc (card I + 1) ';' I1
by A4,SCMFSA6A:62;
then ProgramPart Relocated(I1,card J + 3) c= if=0(a,I,J) by A13,Lm5;
then ProgramPart Relocated(I1,card J + 3) c= s3 by A16,XBOOLE_1:1;
then ProgramPart ProgramPart Relocated(I1,card J + 3) c= s4 by AMI_5:64;
then A17: ProgramPart Relocated(I1,card J + 3) c= s4 by AMI_5:72;
I0 c= I1 by SCMFSA6A:55;
then ProgramPart Relocated(I0,card J + 3) c= ProgramPart Relocated(I1,card
J + 3)
by Th12;
then A18: ProgramPart Relocated(I0,card J + 3) c= s4 by A17,XBOOLE_1:1;
A19: now thus IC C3.1 = C3.1.IC SCM+FSA by AMI_1:def 15
.= insloc (card J + 3) by A12,A14,SCMFSA_2:96;
end;
s00,s3 equal_outside A by SCMFSA8A:14;
then A20: s00 | D = s3 | D by SCMFSA6A:39;
A21: now let a be Int-Location;
thus s00.a = s3.a by A20,SCMFSA6A:38
.= s4.a by A12,SCMFSA_2:96;
end;
now let f be FinSeq-Location;
thus s00.f = s3.f by A20,SCMFSA6A:38
.= s4.f by A12,SCMFSA_2:96;
end;
then A22: s00 | D = s4 | D by A21,SCMFSA6A:38;
if=0(a,I,J) +* Start-At insloc 0 c= s3 by FUNCT_4:26;
then A23: if=0(a,I,J) c= s3 by SCMFSA6B:5;
now thus card if=0(a,I,J) = card I + card J + (3 + 1) by SCMFSA8B:14
.= card I + card J + 3 + 1 by XCMPLX_1:1;
end;
then card I + card J + 3 < card if=0(a,I,J) by NAT_1:38;
then A24: insloc (card I + card J + 3) in dom if=0(a,I,J) by SCMFSA6A:15;
now thus IC (Computation s3).(pseudo-LifeSpan(s00,I0) + 1)
= IC (Computation s4).pseudo-LifeSpan(s00,I0) by AMI_1:51
.= IC (Computation s00).pseudo-LifeSpan(s00,I0) + (card J + 3)
by A5,A6,A18,A19,A22,Th51
.= IC (Computation s00).pseudo-LifeSpan(s,I0) + (card J + 3) by A3,Th50
.= insloc card ProgramPart I0 + (card J + 3) by A3,SCMFSA8A:def 5
.= insloc card I0 + (card J + 3) by AMI_5:72
.= insloc card I + (card J + 3) by SCMFSA8A:34
.= insloc (card I + (card J + 3)) by SCMFSA_4:def 1
.= insloc (card I + card J + 3) by XCMPLX_1:1;
end;
then A25: CurInstr (Computation s3).(pseudo-LifeSpan(s00,I0) + 1)
= (Computation s3).(pseudo-LifeSpan(s00,I0) + 1).
insloc (card I + card J + 3) by AMI_1:def 17
.= s3.insloc (card I + card J + 3) by AMI_1:54
.= if=0(a,I,J).insloc (card I + card J + 3) by A23,A24,GRFUNC_1:8
.= halt SCM+FSA by Th61;
then A26: s3 is halting by AMI_1:def 20;
now let k be Nat;
assume A27: CurInstr (Computation s3).k = halt SCM+FSA;
assume not pseudo-LifeSpan(s00,I0) + 1 <= k;
then A28: k <= pseudo-LifeSpan(s00,I0) by NAT_1:38;
A29: IC s3 = insloc 0 by Th31;
A30: insloc 0 in dom if=0(a,I,J) by Th54;
A31: InsCode halt SCM+FSA = 0 & InsCode (a =0_goto insloc (card J + 3)) = 7
by SCMFSA_2:48,124;
CurInstr (Computation s3).0 = CurInstr s3 by AMI_1:def 19
.= s3.insloc 0 by A29,AMI_1:def 17
.= if=0(a,I,J).insloc 0 by A30,Th26
.= a =0_goto insloc (card J + 3) by Th55;
then consider k1 being Nat such that A32: k1 + 1 = k by A27,A31,NAT_1:22;
k1 < k by A32,REAL_1:69;
then A33: k1 < pseudo-LifeSpan(s00,I0) by A28,AXIOMS:22;
A34: IC (Computation s3).k = IC (Computation s4).k1 by A32,AMI_1:51
.= IC (Computation s00).k1 + (card J + 3) by A5,A6,A18,A19,A22,A33,Th51;
consider n being Nat such that
A35: IC (Computation s00).k1 = insloc n by SCMFSA_2:21;
k1 < pseudo-LifeSpan(s,I0) by A3,A33,Th50;
then insloc n in dom I0 by A3,A35,SCMFSA8A:31;
then n < card I0 by SCMFSA6A:15;
then n + (card J + 3) < card I0 + (card J + 3) by REAL_1:53;
then n + (card J + 3) < card I + (card J + 3) by SCMFSA8A:34;
then A36: n + (card J + 3) < card I + card J + 3 by XCMPLX_1:1;
card if=0(a,I,J) = card I + card J + (3 + 1) by SCMFSA8B:14
.= card I + card J + 3 + 1 by XCMPLX_1:1;
then card I + card J + 3 < card if=0(a,I,J) by REAL_1:69;
then n + (card J + 3) < card if=0(a,I,J) by A36,AXIOMS:22;
then insloc (n + (card J + 3)) in dom if=0(a,I,J) by SCMFSA6A:15;
then A37: IC (Computation s3).k in dom if=0(a,I,J) by A34,A35,SCMFSA_4:def 1;
set J1 = a =0_goto insloc (card J + 3) ';' J ';'
Goto insloc (card I + 1) ';' I;
card J1
= card (Macro (a =0_goto insloc (card J + 3)) ';' J ';'
Goto insloc (card I + 1) ';' I) by SCMFSA6A:def 5
.= card (Macro (a =0_goto insloc (card J + 3)) ';' J ';'
Goto insloc (card I + 1)) + card I by SCMFSA6A:61
.= card (Macro (a =0_goto insloc (card J + 3)) ';' J) +
card Goto insloc (card I + 1) + card I by SCMFSA6A:61
.= card (Macro (a =0_goto insloc (card J + 3)) ';' J) + 1 + card I
by SCMFSA8A:29
.= card Macro (a =0_goto insloc (card J + 3)) + card J + 1 + card I
by SCMFSA6A:61
.= 2 + card J + 1 + card I by SCMFSA7B:6
.= card J + (2 + 1) + card I by XCMPLX_1:1
.= card I + card J + 3 by XCMPLX_1:1;
then insloc (n + (card J + 3)) in dom J1 by A36,SCMFSA6A:15;
then IC (Computation s3).k in dom J1 by A34,A35,SCMFSA_4:def 1;
then A38: IC (Computation s3).k in dom Directed J1 by SCMFSA6A:14;
Directed J1 c= if=0(a,I,J) by A4,SCMFSA6A:55;
then A39: if=0(a,I,J).IC (Computation s3).k = (Directed J1).IC (Computation
s3).k
by A38,GRFUNC_1:8;
A40: (Directed J1).IC (Computation s3).k in rng Directed J1 by A38,FUNCT_1:def
5;
CurInstr (Computation s3).k
= (Computation s3).k.IC (Computation s3).k by AMI_1:def 17
.= s3.IC (Computation s3).k by AMI_1:54
.= if=0(a,I,J).IC (Computation s3).k by A37,Th26;
hence contradiction by A27,A39,A40,SCMFSA7B:def 6;
end;
then A41: LifeSpan s3 = pseudo-LifeSpan(s00,I0) + 1 by A25,A26,SCM_1:def 2;
set s1 = s +* (I1 +* Start-At insloc 0);
s +* Initialized if=0(a,I,J) =
Initialize s +* (if=0(a,I,J) +* Start-At insloc 0) &
s +* Initialized I1 = Initialize s +* (I1 +* Start-At insloc 0)
by SCMFSA8A:13;
then A42: s +* Initialized if=0(a,I,J) = s3 & s +* Initialized I1 = s1 by Th15;
A43: I1 is_halting_on s & LifeSpan s1 = pseudo-LifeSpan(s,I0) by A3,Th58;
then A44: s1 is halting by SCMFSA7B:def 8;
A45: Directed I0 = I0 by SCMFSA8A:40;
I0 ';' SCM+FSA-Stop = I1 & Directed I0 is_pseudo-closed_on s
by A3,SCMFSA8A:40,41;
then A46: (Computation s00).pseudo-LifeSpan(s,I0) | D =
(Computation s1).pseudo-LifeSpan(s,I0) | D by A45,Th58;
thus IExec(if=0(a,I,J),ss) | D = IExec(if=0(a,I,J),s) | D by Th17
.= (Result (s +* Initialized if=0(a,I,J)) +* s | A) | D by SCMFSA6B:def 1
.= (Result s3) | D by A42,Th35
.= (Computation s3).(LifeSpan s3) | D by A26,SCMFSA6B:16
.= (Computation s4).pseudo-LifeSpan(s00,I0) | D by A41,AMI_1:51
.= (Computation s00).pseudo-LifeSpan(s00,I0) | D by A5,A6,A18,A19,A22,Th51
.= (Computation s1).(LifeSpan s1) | D by A3,A43,A46,Th50
.= (Result s1) | D by A44,SCMFSA6B:16
.= (Result (s +* Initialized I1) +* s | A) | D by A42,Th35
.= IExec(I1,s) | D by SCMFSA6B:def 1
.= IExec(I1,ss) | D by Th17;
end;
theorem Th68: ::TMP71'
for s being State of SCM+FSA, I,J being Macro-Instruction,
a being read-write Int-Location
st s.a > 0 & Directed I is_pseudo-closed_on s holds
if>0(a,I,J) is_halting_on s & if>0(a,I,J) is_closed_on s &
LifeSpan (s +* (if>0(a,I,J) +* Start-At insloc 0)) =
LifeSpan (s +* (I ';' SCM+FSA-Stop +* Start-At insloc 0)) + 1
proof
let s be State of SCM+FSA;
let I,J be Macro-Instruction;
let a be read-write Int-Location;
set I0 = Directed I;
set I1 = I ';' SCM+FSA-Stop;
set s00 = s +* (I0 +* Start-At insloc 0);
set s3 = s +* (if>0(a,I,J) +* Start-At insloc 0);
set s4 = (Computation s3).1;
set C3 = Computation s3;
set i = a >0_goto insloc (card J + 3);
assume A1: s.a > 0;
assume A2: I0 is_pseudo-closed_on s;
A3: if>0(a,I,J) = a >0_goto insloc (card J + 3) ';' J ';'
Goto insloc (card I + 1) ';' I ';' SCM+FSA-Stop by SCMFSA8B:def 2;
A4: I0 +* Start-At insloc 0 c= s00 by FUNCT_4:26;
s | D = s00 | D by SCMFSA8A:11;
then A5: I0 is_pseudo-closed_on s00 by A2,Th52;
A6: insloc 0 in dom if>0(a,I,J) by Th54;
if>0(a,I,J) c= if>0(a,I,J) +* Start-At insloc 0 by SCMFSA8A:9;
then A7: dom if>0(a,I,J) c= dom (if>0(a,I,J) +* Start-At insloc 0)
by GRFUNC_1:8;
A8: IC SCM+FSA in dom (if>0(a,I,J) +* Start-At insloc 0) by SF_MASTR:65;
A9: now thus IC s3 = s3.IC SCM+FSA by AMI_1:def 15
.= (if>0(a,I,J) +* Start-At insloc 0).IC SCM+FSA by A8,FUNCT_4:14
.= insloc 0 by SF_MASTR:66;
end;
now thus s3.insloc 0
= (if>0(a,I,J) +* Start-At insloc 0).insloc 0 by A6,A7,FUNCT_4:14
.= if>0(a,I,J).insloc 0 by A6,SCMFSA6B:7
.= i by Th55;
end;
then A10: CurInstr s3 = i by A9,AMI_1:def 17;
A11: now thus (Computation s3).(0 + 1)
= Following (Computation s3).0 by AMI_1:def 19
.= Following s3 by AMI_1:def 19
.= Exec(i,s3) by A10,AMI_1:def 18;
end;
A12: now thus card (i ';' J ';' Goto insloc (card I + 1))
= card (Macro i ';' J ';' Goto insloc (card I + 1)) by SCMFSA6A:def 5
.= card (Macro i ';' J) + card Goto insloc (card I + 1) by SCMFSA6A:61
.= card (Macro i ';' J) + 1 by SCMFSA8A:29
.= card Macro i + card J + 1 by SCMFSA6A:61
.= card J + 2 + 1 by SCMFSA7B:6
.= card J + (2 + 1) by XCMPLX_1:1;
end;
not a in dom (if>0(a,I,J) +* Start-At insloc 0) & a in dom s
by SCMFSA6B:12,SCMFSA_2:66;
then A13: s3.a = s.a by FUNCT_4:12;
A14: if>0(a,I,J) +* Start-At insloc 0 c= s3 by FUNCT_4:26;
if>0(a,I,J) c= if>0(a,I,J) +* Start-At insloc 0 by SCMFSA8A:9;
then A15: if>0(a,I,J) c= s3 by A14,XBOOLE_1:1;
if>0(a,I,J) = i ';' J ';' Goto insloc (card I + 1) ';' I1
by A3,SCMFSA6A:62;
then ProgramPart Relocated(I1,card J + 3) c= if>0(a,I,J) by A12,Lm5;
then ProgramPart Relocated(I1,card J + 3) c= s3 by A15,XBOOLE_1:1;
then ProgramPart ProgramPart Relocated(I1,card J + 3) c= s4 by AMI_5:64;
then A16: ProgramPart Relocated(I1,card J + 3) c= s4 by AMI_5:72;
I0 c= I1 by SCMFSA6A:55;
then ProgramPart Relocated(I0,card J + 3) c= ProgramPart Relocated(I1,card
J + 3)
by Th12;
then A17: ProgramPart Relocated(I0,card J + 3) c= s4 by A16,XBOOLE_1:1;
A18: now thus IC C3.1 = C3.1.IC SCM+FSA by AMI_1:def 15
.= insloc (card J + 3) by A1,A11,A13,SCMFSA_2:97;
end;
s00,s3 equal_outside A by SCMFSA8A:14;
then A19: s00 | D = s3 | D by SCMFSA6A:39;
A20: now let a be Int-Location;
thus s00.a = s3.a by A19,SCMFSA6A:38
.= s4.a by A11,SCMFSA_2:97;
end;
now let f be FinSeq-Location;
thus s00.f = s3.f by A19,SCMFSA6A:38
.= s4.f by A11,SCMFSA_2:97;
end;
then A21: s00 | D = s4 | D by A20,SCMFSA6A:38;
if>0(a,I,J) +* Start-At insloc 0 c= s3 by FUNCT_4:26;
then A22: if>0(a,I,J) c= s3 by SCMFSA6B:5;
now thus card if>0(a,I,J) = card I + card J + (3 + 1) by SCMFSA8B:15
.= card I + card J + 3 + 1 by XCMPLX_1:1;
end;
then card I + card J + 3 < card if>0(a,I,J) by NAT_1:38;
then A23: insloc (card I + card J + 3) in dom if>0(a,I,J) by SCMFSA6A:15;
A24: now thus IC (Computation s3).(pseudo-LifeSpan(s00,I0) + 1)
= IC (Computation s4).pseudo-LifeSpan(s00,I0) by AMI_1:51
.= IC (Computation s00).pseudo-LifeSpan(s00,I0) + (card J + 3)
by A4,A5,A17,A18,A21,Th51
.= IC (Computation s00).pseudo-LifeSpan(s,I0) + (card J + 3) by A2,Th50
.= insloc card ProgramPart I0 + (card J + 3) by A2,SCMFSA8A:def 5
.= insloc card I0 + (card J + 3) by AMI_5:72
.= insloc card I + (card J + 3) by SCMFSA8A:34
.= insloc (card I + (card J + 3)) by SCMFSA_4:def 1
.= insloc (card I + card J + 3) by XCMPLX_1:1;
end;
then A25: CurInstr (Computation s3).(pseudo-LifeSpan(s00,I0) + 1)
= (Computation s3).(pseudo-LifeSpan(s00,I0) + 1).
insloc (card I + card J + 3) by AMI_1:def 17
.= s3.insloc (card I + card J + 3) by AMI_1:54
.= if>0(a,I,J).insloc (card I + card J + 3) by A22,A23,GRFUNC_1:8
.= halt SCM+FSA by Th62;
then A26: s3 is halting by AMI_1:def 20;
hence if>0(a,I,J) is_halting_on s by SCMFSA7B:def 8;
now let k be Nat;
per cases by NAT_1:19;
suppose k = 0;
then (Computation s3).k = s3 by AMI_1:def 19;
then IC (Computation s3).k = insloc 0 by Th31;
hence IC (Computation s3).k in dom if>0(a,I,J) by Th54;
suppose A27: 0 < k & k < pseudo-LifeSpan(s00,I0) + 1;
then 0 + 1 <= k by INT_1:20;
then consider k1 being Nat such that A28: 1 + k1 = k by NAT_1:28;
A29: k1 < pseudo-LifeSpan(s00,I0) by A27,A28,AXIOMS:24;
then A30: k1 < pseudo-LifeSpan(s,I0) by A2,Th50;
A31: IC (Computation s3).k = IC (Computation s4).k1 by A28,AMI_1:51
.= IC (Computation s00).k1 + (card J + 3) by A4,A5,A17,A18,A21,A29,Th51;
consider n being Nat such that
A32: IC (Computation s00).k1 = insloc n by SCMFSA_2:21;
insloc n in dom I0 by A2,A30,A32,SCMFSA8A:31;
then n < card I0 by SCMFSA6A:15;
then n + (card J + 3) < card I0 + (card J + 3) by REAL_1:53;
then n + (card J + 3) < card I + (card J + 3) by SCMFSA8A:34;
then A33: n + (card J + 3) < card I + card J + 3 by XCMPLX_1:1;
card if>0(a,I,J) = card I + card J + (3 + 1) by SCMFSA8B:15
.= card I + card J + 3 + 1 by XCMPLX_1:1;
then card I + card J + 3 < card if>0(a,I,J) by REAL_1:69;
then n + (card J + 3) < card if>0(a,I,J) by A33,AXIOMS:22;
then insloc (n + (card J + 3)) in dom if>0(a,I,J) by SCMFSA6A:15;
hence IC (Computation s3).k in
dom if>0(a,I,J) by A31,A32,SCMFSA_4:def 1
;
suppose 0 < k & pseudo-LifeSpan(s00,I0) + 1 <= k;
hence IC (Computation s3).k in dom if>0(a,I,J) by A23,A24,A25,AMI_1:52;
end;
hence if>0(a,I,J) is_closed_on s by SCMFSA7B:def 7;
now let k be Nat;
assume A34: CurInstr (Computation s3).k = halt SCM+FSA;
assume not pseudo-LifeSpan(s00,I0) + 1 <= k;
then A35: k <= pseudo-LifeSpan(s00,I0) by NAT_1:38;
A36: IC s3 = insloc 0 by Th31;
A37: insloc 0 in dom if>0(a,I,J) by Th54;
A38: InsCode halt SCM+FSA = 0 & InsCode (a >0_goto insloc (card J + 3)) = 8
by SCMFSA_2:49,124;
CurInstr (Computation s3).0 = CurInstr s3 by AMI_1:def 19
.= s3.insloc 0 by A36,AMI_1:def 17
.= if>0(a,I,J).insloc 0 by A37,Th26
.= a >0_goto insloc (card J + 3) by Th55;
then consider k1 being Nat such that A39: k1 + 1 = k by A34,A38,NAT_1:22;
k1 < k by A39,REAL_1:69;
then A40: k1 < pseudo-LifeSpan(s00,I0) by A35,AXIOMS:22;
A41: IC (Computation s3).k = IC (Computation s4).k1 by A39,AMI_1:51
.= IC (Computation s00).k1 + (card J + 3) by A4,A5,A17,A18,A21,A40,Th51;
consider n being Nat such that
A42: IC (Computation s00).k1 = insloc n by SCMFSA_2:21;
k1 < pseudo-LifeSpan(s,I0) by A2,A40,Th50;
then insloc n in dom I0 by A2,A42,SCMFSA8A:31;
then n < card I0 by SCMFSA6A:15;
then n + (card J + 3) < card I0 + (card J + 3) by REAL_1:53;
then n + (card J + 3) < card I + (card J + 3) by SCMFSA8A:34;
then A43: n + (card J + 3) < card I + card J + 3 by XCMPLX_1:1;
card if>0(a,I,J) = card I + card J + (3 + 1) by SCMFSA8B:15
.= card I + card J + 3 + 1 by XCMPLX_1:1;
then card I + card J + 3 < card if>0(a,I,J) by REAL_1:69;
then n + (card J + 3) < card if>0(a,I,J) by A43,AXIOMS:22;
then insloc (n + (card J + 3)) in dom if>0(a,I,J) by SCMFSA6A:15;
then A44: IC (Computation s3).k in dom if>0(a,I,J) by A41,A42,SCMFSA_4:def 1;
set J1 = a >0_goto insloc (card J + 3) ';' J ';'
Goto insloc (card I + 1) ';' I;
card J1
= card (Macro (a >0_goto insloc (card J + 3)) ';' J ';'
Goto insloc (card I + 1) ';' I) by SCMFSA6A:def 5
.= card (Macro (a >0_goto insloc (card J + 3)) ';' J ';'
Goto insloc (card I + 1)) + card I by SCMFSA6A:61
.= card (Macro (a >0_goto insloc (card J + 3)) ';' J) +
card Goto insloc (card I + 1) + card I by SCMFSA6A:61
.= card (Macro (a >0_goto insloc (card J + 3)) ';' J) + 1 + card I
by SCMFSA8A:29
.= card Macro (a >0_goto insloc (card J + 3)) + card J + 1 + card I
by SCMFSA6A:61
.= 2 + card J + 1 + card I by SCMFSA7B:6
.= card J + (2 + 1) + card I by XCMPLX_1:1
.= card I + card J + 3 by XCMPLX_1:1;
then insloc (n + (card J + 3)) in dom J1 by A43,SCMFSA6A:15;
then IC (Computation s3).k in dom J1 by A41,A42,SCMFSA_4:def 1;
then A45: IC (Computation s3).k in dom Directed J1 by SCMFSA6A:14;
Directed J1 c= if>0(a,I,J) by A3,SCMFSA6A:55;
then A46: if>0(a,I,J).IC (Computation s3).k = (Directed J1).IC (Computation
s3).k
by A45,GRFUNC_1:8;
A47: (Directed J1).IC (Computation s3).k in
rng Directed J1 by A45,FUNCT_1:def 5;
CurInstr (Computation s3).k
= (Computation s3).k.IC (Computation s3).k by AMI_1:def 17
.= s3.IC (Computation s3).k by AMI_1:54
.= if>0(a,I,J).IC (Computation s3).k by A44,Th26;
hence contradiction by A34,A46,A47,SCMFSA7B:def 6;
end;
then A48: LifeSpan s3 = pseudo-LifeSpan(s00,I0) + 1 by A25,A26,SCM_1:def 2;
pseudo-LifeSpan(s,I0) =
LifeSpan (s +* (I1 +* Start-At insloc 0)) by A2,Th58;
hence LifeSpan s3 = LifeSpan (s +* (I1 +* Start-At insloc 0)) + 1
by A2,A48,Th50;
end;
theorem Th69: ::TMP7'
for s being State of SCM+FSA, I,J being Macro-Instruction,
a being read-write Int-Location
st s.intloc 0 = 1 & s.a > 0 & Directed I is_pseudo-closed_on s holds
IExec(if>0(a,I,J),s) | (Int-Locations \/ FinSeq-Locations) =
IExec(I ';' SCM+FSA-Stop,s) | (Int-Locations \/ FinSeq-Locations)
proof
let ss be State of SCM+FSA;
let I,J be Macro-Instruction;
let a be read-write Int-Location;
set I0 = Directed I;
set s = Initialize ss;
set I1 = I ';' SCM+FSA-Stop;
set s00 = s +* (I0 +* Start-At insloc 0);
set s3 = s +* (if>0(a,I,J) +* Start-At insloc 0);
set s4 = (Computation s3).1;
set C3 = Computation s3;
set i = a >0_goto insloc (card J + 3);
assume A1: ss.intloc 0 = 1;
assume ss.a > 0;
then A2: s.a > 0 by SCMFSA6C:3;
assume I0 is_pseudo-closed_on ss;
then A3: I0 is_pseudo-closed_on s by A1,Th53;
A4: if>0(a,I,J) = a >0_goto insloc (card J + 3) ';' J ';'
Goto insloc (card I + 1) ';' I ';' SCM+FSA-Stop by SCMFSA8B:def 2;
A5: I0 +* Start-At insloc 0 c= s00 by FUNCT_4:26;
s | D = s00 | D by SCMFSA8A:11;
then A6: I0 is_pseudo-closed_on s00 by A3,Th52;
A7: insloc 0 in dom if>0(a,I,J) by Th54;
if>0(a,I,J) c= if>0(a,I,J) +* Start-At insloc 0 by SCMFSA8A:9;
then A8: dom if>0(a,I,J) c= dom (if>0(a,I,J) +* Start-At insloc 0)
by GRFUNC_1:8;
A9: IC SCM+FSA in dom (if>0(a,I,J) +* Start-At insloc 0) by SF_MASTR:65;
A10: now thus IC s3 = s3.IC SCM+FSA by AMI_1:def 15
.= (if>0(a,I,J) +* Start-At insloc 0).IC SCM+FSA by A9,FUNCT_4:14
.= insloc 0 by SF_MASTR:66;
end;
now thus s3.insloc 0
= (if>0(a,I,J) +* Start-At insloc 0).insloc 0 by A7,A8,FUNCT_4:14
.= if>0(a,I,J).insloc 0 by A7,SCMFSA6B:7
.= i by Th55;
end;
then A11: CurInstr s3 = i by A10,AMI_1:def 17;
A12: now thus (Computation s3).(0 + 1)
= Following (Computation s3).0 by AMI_1:def 19
.= Following s3 by AMI_1:def 19
.= Exec(i,s3) by A11,AMI_1:def 18;
end;
A13: now thus card (i ';' J ';' Goto insloc (card I + 1))
= card (Macro i ';' J ';' Goto insloc (card I + 1)) by SCMFSA6A:def 5
.= card (Macro i ';' J) + card Goto insloc (card I + 1) by SCMFSA6A:61
.= card (Macro i ';' J) + 1 by SCMFSA8A:29
.= card Macro i + card J + 1 by SCMFSA6A:61
.= card J + 2 + 1 by SCMFSA7B:6
.= card J + (2 + 1) by XCMPLX_1:1;
end;
not a in dom (if>0(a,I,J) +* Start-At insloc 0) & a in dom s
by SCMFSA6B:12,SCMFSA_2:66;
then A14: s3.a = s.a by FUNCT_4:12;
A15: if>0(a,I,J) +* Start-At insloc 0 c= s3 by FUNCT_4:26;
if>0(a,I,J) c= if>0(a,I,J) +* Start-At insloc 0 by SCMFSA8A:9;
then A16: if>0(a,I,J) c= s3 by A15,XBOOLE_1:1;
if>0(a,I,J) = i ';' J ';' Goto insloc (card I + 1) ';' I1
by A4,SCMFSA6A:62;
then ProgramPart Relocated(I1,card J + 3) c= if>0(a,I,J) by A13,Lm5;
then ProgramPart Relocated(I1,card J + 3) c= s3 by A16,XBOOLE_1:1;
then ProgramPart ProgramPart Relocated(I1,card J + 3) c= s4 by AMI_5:64;
then A17: ProgramPart Relocated(I1,card J + 3) c= s4 by AMI_5:72;
I0 c= I1 by SCMFSA6A:55;
then ProgramPart Relocated(I0,card J + 3) c= ProgramPart Relocated(I1,card
J + 3)
by Th12;
then A18: ProgramPart Relocated(I0,card J + 3) c= s4 by A17,XBOOLE_1:1;
A19: now thus IC C3.1 = C3.1.IC SCM+FSA by AMI_1:def 15
.= insloc (card J + 3) by A2,A12,A14,SCMFSA_2:97;
end;
s00,s3 equal_outside A by SCMFSA8A:14;
then A20: s00 | D = s3 | D by SCMFSA6A:39;
A21: now let a be Int-Location;
thus s00.a = s3.a by A20,SCMFSA6A:38
.= s4.a by A12,SCMFSA_2:97;
end;
now let f be FinSeq-Location;
thus s00.f = s3.f by A20,SCMFSA6A:38
.= s4.f by A12,SCMFSA_2:97;
end;
then A22: s00 | D = s4 | D by A21,SCMFSA6A:38;
if>0(a,I,J) +* Start-At insloc 0 c= s3 by FUNCT_4:26;
then A23: if>0(a,I,J) c= s3 by SCMFSA6B:5;
now thus card if>0(a,I,J) = card I + card J + (3 + 1) by SCMFSA8B:15
.= card I + card J + 3 + 1 by XCMPLX_1:1;
end;
then card I + card J + 3 < card if>0(a,I,J) by NAT_1:38;
then A24: insloc (card I + card J + 3) in dom if>0(a,I,J) by SCMFSA6A:15;
now thus IC (Computation s3).(pseudo-LifeSpan(s00,I0) + 1)
= IC (Computation s4).pseudo-LifeSpan(s00,I0) by AMI_1:51
.= IC (Computation s00).pseudo-LifeSpan(s00,I0) + (card J + 3)
by A5,A6,A18,A19,A22,Th51
.= IC (Computation s00).pseudo-LifeSpan(s,I0) + (card J + 3) by A3,Th50
.= insloc card ProgramPart I0 + (card J + 3) by A3,SCMFSA8A:def 5
.= insloc card I0 + (card J + 3) by AMI_5:72
.= insloc card I + (card J + 3) by SCMFSA8A:34
.= insloc (card I + (card J + 3)) by SCMFSA_4:def 1
.= insloc (card I + card J + 3) by XCMPLX_1:1;
end;
then A25: CurInstr (Computation s3).(pseudo-LifeSpan(s00,I0) + 1)
= (Computation s3).(pseudo-LifeSpan(s00,I0) + 1).
insloc (card I + card J + 3) by AMI_1:def 17
.= s3.insloc (card I + card J + 3) by AMI_1:54