Copyright (c) 1996 Association of Mizar Users
environ
vocabulary FUNCT_1, RELAT_1, FUNCT_4, BOOLE, AMI_1, SCMFSA_2, SCMFSA6A, AMI_3,
CAT_1, SCM_1, INT_1, FUNCOP_1, FUNCT_7, SF_MASTR, AMI_5, FINSEQ_1, RELOC,
CARD_1, SCMFSA6B, CARD_3;
notation TARSKI, XBOOLE_0, NUMBERS, XCMPLX_0, XREAL_0, NAT_1, INT_1, RELAT_1,
FUNCT_1, FUNCT_2, FINSEQ_1, CARD_1, CQC_LANG, FUNCT_4, STRUCT_0, AMI_1,
AMI_3, SCM_1, AMI_5, FUNCT_7, SCMFSA_2, SCMFSA_4, SCMFSA_5, SCMFSA6A,
SF_MASTR;
constructors SCM_1, SCMFSA6A, SF_MASTR, FUNCT_7, SCMFSA_5, AMI_5, NAT_1,
MEMBERED;
clusters AMI_1, SCMFSA_2, FUNCT_1, SCMFSA_4, INT_1, SCMFSA6A, SF_MASTR,
CQC_LANG, RELSET_1, FRAENKEL, XREAL_0, MEMBERED, NUMBERS, ORDINAL2;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions AMI_1;
theorems RELAT_1, FUNCT_7, FUNCT_4, FUNCT_1, SCMFSA_3, REAL_1, INT_1,
CQC_LANG, AMI_3, AMI_5, TARSKI, NAT_1, SCMFSA_4, AMI_1, SCMFSA_2, AXIOMS,
FSM_1, ENUMSET1, LATTICE2, SCMFSA_5, GRFUNC_1, CARD_3, SCM_1, SCMFSA6A,
SF_MASTR, XBOOLE_0, XBOOLE_1, XCMPLX_1;
schemes NAT_1, FUNCT_2, SCMFSA6A;
begin
canceled 2;
theorem
for f, g being Function, A being set st A /\ dom f c= A /\ dom g
holds (f+*g|A)|A = g|A
proof
let f, g be Function, A be set; assume
A1: A /\ dom f c= A /\ dom g;
A2: dom (f|A) = A /\ dom f & dom (g|A) = A /\ dom g by RELAT_1:90;
thus (f+*g|A)|A = (f|A)+*(g|A)|A by AMI_5:6
.= (f|A)+*g|A by RELAT_1:101
.= g|A by A1,A2,FUNCT_4:20;
end;
begin
reserve m, n for Nat,
x for set,
i for Instruction of SCM+FSA,
I for Macro-Instruction,
a for Int-Location, f for FinSeq-Location,
l, l1 for Instruction-Location of SCM+FSA,
s,s1,s2 for State of SCM+FSA;
set SA0 = Start-At insloc 0;
theorem Th4:
Start-At insloc 0 c= Initialized I
proof
Initialized I = I +* ((intloc 0) .--> 1) +* Start-At(insloc 0)
by SCMFSA6A:def 3;
hence thesis by FUNCT_4:26;
end;
theorem Th5:
I +* Start-At insloc n c= s implies I c= s
proof assume
A1: I +* Start-At insloc n c= s;
dom I misses dom Start-At insloc n by SF_MASTR:64;
then I +* Start-At insloc n = I \/ Start-At insloc n by FUNCT_4:32;
hence thesis by A1,XBOOLE_1:11;
end;
theorem Th6:
(I +* Start-At insloc n)|the Instruction-Locations of SCM+FSA = I
proof
A1: dom I c= the Instruction-Locations of SCM+FSA by AMI_3:def 13;
the Instruction-Locations of SCM+FSA misses dom Start-At insloc n proof
assume not thesis; then consider x being set such that
A2: x in the Instruction-Locations of SCM+FSA & x in dom Start-At insloc n
by XBOOLE_0:3;
dom Start-At insloc n = {IC SCM+FSA} by AMI_3:34;
then x = IC SCM+FSA by A2,TARSKI:def 1;
hence contradiction by A2,AMI_1:48;
end;
then (I +* Start-At insloc n)|the Instruction-Locations of SCM+FSA
= I | the Instruction-Locations of SCM+FSA by AMI_5:7;
hence thesis by A1,RELAT_1:97;
end;
theorem Th7:
x in dom I implies I.x = (I +* Start-At insloc n).x
proof assume
A1: x in dom I;
A2: dom I c= the Instruction-Locations of SCM+FSA by AMI_3:def 13;
A3: dom Start-At insloc n = {IC SCM+FSA} by AMI_3:34;
x <> IC SCM+FSA by A1,A2,AMI_1:48;
then not x in dom Start-At insloc n by A3,TARSKI:def 1;
hence thesis by FUNCT_4:12;
end;
theorem Th8:
Initialized I c= s implies I +* Start-At insloc 0 c= s
proof assume
A1: Initialized I c= s;
Initialized I = I +* ((intloc 0) .--> 1) +* Start-At(insloc 0)
by SCMFSA6A:def 3;
then Start-At(insloc 0) c= Initialized I by FUNCT_4:26;
then A2: Start-At(insloc 0) c= s by A1,XBOOLE_1:1;
I c= Initialized I by SCMFSA6A:26;
then A3: I c= s by A1,XBOOLE_1:1;
dom I misses dom Start-At insloc 0 by SF_MASTR:64;
then I +* Start-At insloc 0 = I \/ Start-At insloc 0 by FUNCT_4:32;
hence I +* Start-At insloc 0 c= s by A2,A3,XBOOLE_1:8;
end;
theorem Th9:
not a in dom Start-At l
proof assume
A1: a in dom Start-At l;
dom Start-At l = {IC SCM+FSA} by AMI_3:34;
then a = IC SCM+FSA by A1,TARSKI:def 1;
hence contradiction by SCMFSA_2:81;
end;
theorem Th10:
not f in dom Start-At l
proof assume
A1: f in dom Start-At l;
dom Start-At l = {IC SCM+FSA} by AMI_3:34;
then f = IC SCM+FSA by A1,TARSKI:def 1;
hence contradiction by SCMFSA_2:82;
end;
theorem
not l1 in dom Start-At l
proof assume
A1: l1 in dom Start-At l;
dom Start-At l = {IC SCM+FSA} by AMI_3:34;
then l1 = IC SCM+FSA by A1,TARSKI:def 1;
hence contradiction by AMI_1:48;
end;
theorem Th12:
not a in dom (I+*Start-At l)
proof assume
a in dom (I+*Start-At l);
then a in dom I \/ dom Start-At l by FUNCT_4:def 1;
then A1: a in dom I or a in dom Start-At l by XBOOLE_0:def 2;
A2: dom I c= the Instruction-Locations of SCM+FSA by AMI_3:def 13;
a in Int-Locations by SCMFSA_2:9;
hence contradiction by A1,A2,Th9,SCMFSA_2:13,XBOOLE_0:3;
end;
theorem Th13:
not f in dom (I+*Start-At l)
proof assume
f in dom (I+*Start-At l);
then f in dom I \/ dom Start-At l by FUNCT_4:def 1;
then A1: f in dom I or f in dom Start-At l by XBOOLE_0:def 2;
A2: dom I c= the Instruction-Locations of SCM+FSA by AMI_3:def 13;
f in FinSeq-Locations by SCMFSA_2:10;
hence contradiction by A1,A2,Th10,SCMFSA_2:14,XBOOLE_0:3;
end;
theorem Th14:
s+*I+*Start-At insloc 0 = s+*Start-At insloc 0+*I
proof
A1: dom I misses dom Start-At insloc 0 by SF_MASTR:64;
then I+*Start-At insloc 0 = I \/ Start-At insloc 0 by FUNCT_4:32
.= Start-At insloc 0 +* I by A1,FUNCT_4:32;
hence s+*I+*Start-At insloc 0
= s+*(Start-At insloc 0+*I) by FUNCT_4:15
.= s+*Start-At insloc 0+*I by FUNCT_4:15;
end;
begin :: General theory
reserve N for non empty with_non-empty_elements set;
theorem
s = Following s implies for n holds (Computation s).n = s
proof assume
A1: s = Following s;
defpred X[set] means (Computation s).$1 = s;
A2: X[0] by AMI_1:def 19;
A3: for n st X[n] holds X[n+1] by A1,AMI_1:def 19;
thus for n holds X[n] from Ind(A2, A3);
end;
theorem Th16:
for S being halting IC-Ins-separated definite
(non empty non void AMI-Struct over N),
s being State of S st s is halting
holds Result s = (Computation s).LifeSpan s
proof
let S be halting IC-Ins-separated definite
(non empty non void AMI-Struct over N);
let s be State of S;
assume
A1: s is halting;
then A2: CurInstr (Computation s).LifeSpan s = halt S by SCM_1:def 2;
consider m such that
A3: Result s = (Computation s).m and
A4: CurInstr Result s = halt S by A1,AMI_1:def 22;
LifeSpan s <= m by A1,A3,A4,SCM_1:def 2;
hence Result s = (Computation s).LifeSpan s by A2,A3,AMI_1:52;
end;
definition let N;
let S be IC-Ins-separated definite (non empty non void AMI-Struct over N);
let s be State of S, l be Instruction-Location of S, i be Instruction of S;
redefine func s+*(l,i) -> State of S;
coherence
proof
A1: dom(s+*(l,i)) = dom s by FUNCT_7:32;
A2: dom s = dom the Object-Kind of S by CARD_3:18;
now let x be set;
assume
A3: x in dom the Object-Kind of S;
per cases;
suppose
A4: x = l;
then A5: (s+*(l,i)).x = i by A2,A3,FUNCT_7:33;
(the Object-Kind of S).x
= ObjectKind l by A4,AMI_1:def 6
.= the Instructions of S by AMI_1:def 14;
hence (s+*(l,i)).x in (the Object-Kind of S).x by A5;
suppose x <> l;
then (s+*(l,i)).x = s.x by FUNCT_7:34;
hence (s+*(l,i)).x in (the Object-Kind of S).x by A3,CARD_3:18;
end;
hence s+*(l,i) is State of S by A1,A2,CARD_3:18;
end;
end;
definition
let s be State of SCM+FSA, li be Int-Location, k be Integer;
redefine func s+*(li,k) -> State of SCM+FSA;
coherence proof
A1: dom(s+*(li,k)) = dom s by FUNCT_7:32;
A2: dom s = dom the Object-Kind of SCM+FSA by CARD_3:18;
now let x be set;
assume
A3: x in dom the Object-Kind of SCM+FSA;
per cases;
suppose
A4: x = li;
then A5: (s+*(li,k)).x = k by A2,A3,FUNCT_7:33;
(the Object-Kind of SCM+FSA).x
= ObjectKind li by A4,AMI_1:def 6
.= INT by SCMFSA_2:26;
hence (s+*(li,k)).x in (the Object-Kind of SCM+FSA).x by A5,INT_1:12;
suppose x <> li;
then (s+*(li,k)).x = s.x by FUNCT_7:34;
hence (s+*(li,k)).x in (the Object-Kind of SCM+FSA).x by A3,CARD_3:18;
end;
hence s+*(li,k) is State of SCM+FSA by A1,A2,CARD_3:18;
end;
end;
theorem Th17:
for S being steady-programmed IC-Ins-separated definite
(non empty non void AMI-Struct over N)
for s being State of S, n
holds s|the Instruction-Locations of S
= ((Computation s).n)|the Instruction-Locations of S
proof
let S be steady-programmed IC-Ins-separated definite
(non empty non void AMI-Struct over N);
let s be State of S;
defpred X[Nat] means s|the Instruction-Locations of S
= ((Computation s).$1)|the Instruction-Locations of S;
A1: X[0] by AMI_1:def 19;
A2: now let n;
assume X[n];
then s|the Instruction-Locations of S
= Exec(CurInstr((Computation s).n),(Computation s).n)
|the Instruction-Locations of S by SCMFSA_3:5
:: poprawic SCMFSA_3:5
.= (Following((Computation s).n))|the Instruction-Locations of S
by AMI_1:def 18
.= ((Computation s).(n+1))|the Instruction-Locations of S by AMI_1:def 19;
hence X[n+1];
end;
thus for n holds X[n] from Ind(A1,A2);
end;
begin
definition let I be Macro-Instruction, s be State of SCM+FSA;
func IExec(I,s) -> State of SCM+FSA equals
:Def1:
Result(s+*Initialized I) +* s|the Instruction-Locations of SCM+FSA;
coherence by AMI_5:82;
end;
definition let I be Macro-Instruction;
attr I is paraclosed means
:Def2: for s being State of SCM+FSA, n being Nat
st I +* Start-At insloc 0 c= s
holds IC (Computation s).n in dom I;
attr I is parahalting means
:Def3: I +* Start-At insloc 0 is halting;
attr I is keeping_0 means
:Def4: ::Lkeep
for s being State of SCM+FSA st I +* Start-At insloc 0 c= s
for k being Nat holds ((Computation s).k).intloc 0 = s.intloc 0;
end;
Lm1:
Macro halt SCM+FSA is parahalting
proof
set m = Macro halt SCM+FSA;
set m1 = m +* Start-At insloc 0;
let s;
assume
A1: m1 c= s;
A2: dom(Start-At insloc 0) = {IC SCM+FSA} by AMI_3:34;
then A3: IC SCM+FSA in dom (Start-At insloc 0) by TARSKI:def 1;
then A4: IC SCM+FSA in dom m1 by FUNCT_4:13;
A5: m = (insloc 0,insloc 1) --> (halt SCM+FSA, halt SCM+FSA) by SCMFSA6A:def 2;
insloc 0 <> insloc 1 by SCMFSA_2:18;
then A6: m.insloc 0 = halt SCM+FSA by A5,FUNCT_4:66;
A7: dom m = {insloc 0,insloc 1} by A5,FUNCT_4:65;
now assume dom m /\ dom (Start-At insloc 0) is non empty;
then consider x being set such that
A8: x in dom m /\ dom (Start-At insloc 0) by XBOOLE_0:def 1;
x in dom m & x in dom (Start-At insloc 0) by A8,XBOOLE_0:def 3;
then (x=insloc 0 or x=insloc 1) & x=IC SCM+FSA by A2,A7,TARSKI:def 1,def
2;
hence contradiction by AMI_1:48;
end;
then dom m misses dom (Start-At insloc 0) by XBOOLE_0:def 7;
then A9: m c= m1 by FUNCT_4:33;
dom m = {insloc 0,insloc 1} by A5,FUNCT_4:65;
then A10: insloc 0 in dom m by TARSKI:def 2;
then A11: insloc 0 in dom m1 by FUNCT_4:13;
A12: IC m1 = m1.IC SCM+FSA by A4,AMI_3:def 16
.= (Start-At insloc 0).IC SCM+FSA by A3,FUNCT_4:14
.= insloc 0 by AMI_3:50;
take 0;
thus CurInstr((Computation s).0) = CurInstr s by AMI_1:def 19
.= s.IC s by AMI_1:def 17
.= s.IC m1 by A1,A4,AMI_5:60
.= m1.insloc 0 by A1,A11,A12,GRFUNC_1:8
.= halt SCM+FSA by A6,A9,A10,GRFUNC_1:8;
end;
definition
cluster parahalting Macro-Instruction;
existence by Lm1;
end;
theorem Th18:
for I being parahalting Macro-Instruction
st I +* Start-At insloc 0 c= s holds s is halting
proof
let I be parahalting Macro-Instruction; assume
A1: I +* Start-At insloc 0 c= s;
I +* Start-At insloc 0 is halting by Def3;
hence s is halting by A1,AMI_1:def 26;
end;
theorem Th19:
for I being parahalting Macro-Instruction
st Initialized I c= s holds s is halting
proof
let I be parahalting Macro-Instruction; assume
A1: Initialized I c= s;
A2: I +* Start-At insloc 0 c= I \/ Start-At insloc 0 by FUNCT_4:30;
Initialized I = I +* ((intloc 0) .--> 1) +* Start-At(insloc 0)
by SCMFSA6A:def 3;
then A3: Start-At insloc 0 c= Initialized I by FUNCT_4:26;
A4: I +* Start-At insloc 0 is halting by Def3;
I c= Initialized I by SCMFSA6A:26;
then I \/ Start-At insloc 0 c= Initialized I by A3,XBOOLE_1:8;
then I +* Start-At insloc 0 c= Initialized I by A2,XBOOLE_1:1;
then I +* Start-At insloc 0 c= s by A1,XBOOLE_1:1;
hence s is halting by A4,AMI_1:def 26;
end;
definition let I be parahalting Macro-Instruction;
cluster Initialized I -> halting;
coherence proof
let s be State of SCM+FSA; assume Initialized I c= s;
hence s is halting by Th19;
end;
end;
theorem Th20:
s2 +*(IC s2, goto IC s2) is not halting
proof set s1 = s2 +*(IC s2, goto IC s2);
A1: IC SCM+FSA <> IC s2 by AMI_1:48;
A2: IC s2 in dom s2 by SCMFSA_2:4;
defpred X[Nat] means IC((Computation s1).$1) = IC s1;
A3: X[0] by AMI_1:def 19;
A4: IC s1 = s1.IC SCM+FSA by AMI_1:def 15
.= s2.IC SCM+FSA by A1,FUNCT_7:34
.= IC s2 by AMI_1:def 15;
A5: now let n;
assume
A6: X[n];
A7: CurInstr((Computation s1).n)
= ((Computation s1).n).IC((Computation s1).n) by AMI_1:def 17
.= s1.IC s1 by A6,AMI_1:54
.= goto IC s2 by A2,A4,FUNCT_7:33;
IC((Computation s1).(n+1))
= IC Following((Computation s1).n) by AMI_1:def 19
.= IC Exec(goto IC s2,(Computation s1).n) by A7,AMI_1:def 18
.= (Exec(goto IC s2,(Computation s1).n)).IC SCM+FSA by AMI_1:def 15
.= IC s1 by A4,SCMFSA_2:95;
hence X[n+1];
end;
A8: for n holds X[n] from Ind(A3,A5);
let n;
CurInstr((Computation s1).n)
= ((Computation s1).n).IC((Computation s1).n) by AMI_1:def 17
.= ((Computation s1).n).IC s1 by A8
.= s1.IC s1 by AMI_1:54
.= goto IC s2 by A2,A4,FUNCT_7:33;
hence CurInstr((Computation s1).n) <> halt SCM+FSA by SCMFSA_2:47,124
;
end;
theorem Th21:
s1,s2 equal_outside the Instruction-Locations of SCM+FSA &
I c= s1 & I c= s2 &
(for m st m < n holds IC((Computation s2).m) in dom I)
implies
for m st m <= n holds
(Computation s1).m, (Computation s2 ).m equal_outside
the Instruction-Locations of SCM+FSA
proof assume that
A1: s1,s2 equal_outside the Instruction-Locations of SCM+FSA and
A2: I c= s1 and
A3: I c= s2 and
A4: for m st m < n holds IC((Computation s2).m) in dom I;
defpred X[Nat] means $1 <= n implies
(Computation s1).$1, (Computation s2 ).$1 equal_outside
the Instruction-Locations of SCM+FSA;
(Computation s1).0 = s1 & (Computation s2 ).0 = s2 by AMI_1:def 19;
then A5: X[0] by A1;
A6: for m st X[m] holds X[m+1]
proof let m such that
A7: X[m];
A8: (Computation s1).(m+1) = Following((Computation s1).m) by AMI_1:def 19
.= Exec(CurInstr((Computation s1).m),(Computation s1).m)
by AMI_1:def 18;
A9: (Computation s2).(m+1) = Following((Computation s2).m) by AMI_1:def 19
.= Exec(CurInstr((Computation s2).m),(Computation s2).m)
by AMI_1:def 18;
assume A10: m+1 <= n;
then m < n by NAT_1:38;
then A11: IC((Computation s2).m) in dom I by A4;
A12: IC ((Computation s1).m) = IC ((Computation s2).m) by A7,A10,NAT_1:38,
SCMFSA6A:29;
CurInstr((Computation s1).m)
= ((Computation s1).m).IC ((Computation s1).m) by AMI_1:def 17
.= s1.IC((Computation s1).m) by AMI_1:54
.= I.IC((Computation s1).m) by A2,A11,A12,GRFUNC_1:8
.= s2.IC((Computation s2).m) by A3,A11,A12,GRFUNC_1:8
.= ((Computation s2).m).IC ((Computation s2).m) by AMI_1:54
.= CurInstr((Computation s2).m) by AMI_1:def 17;
then (Computation s1).(m+1), (Computation s2 ).(m+1) equal_outside
the Instruction-Locations of SCM+FSA by A7,A8,A9,A10,NAT_1:38,SCMFSA6A:32;
hence thesis;
end;
thus for m holds X[m] from Ind(A5,A6);
end;
definition
cluster parahalting -> paraclosed Macro-Instruction;
coherence proof
let I be Macro-Instruction; assume
A1: I is parahalting;
let s be State of SCM+FSA, n be Nat;
assume
A2: I +* Start-At insloc 0 c= s;
defpred X[Nat] means not IC (Computation s).$1 in dom I;
assume not IC (Computation s).n in dom I;
then A3: ex n st X[n];
consider n such that
A4: X[n] and
A5: for m st X[m] holds n <= m from Min(A3);
set s2 = (Computation s).n,
s0 = s +*(IC s2, goto IC s2), s1 = s2 +*(IC s2, goto IC s2);
set IAt = I +* Start-At insloc 0;
dom I misses dom Start-At insloc 0 by SF_MASTR:64;
then A6: I c= IAt by FUNCT_4:33;
A7: IAt is halting by A1,Def3;
(IAt)|the Instruction-Locations of SCM+FSA = I by Th6;
then dom I = dom(IAt)/\the Instruction-Locations of SCM+FSA
by RELAT_1:90;
then not IC s2 in dom IAt by A4,XBOOLE_0:def 3;
then A8: IAt c= s0 by A2,SCMFSA6A:1;
then A9: s0 is halting by A7,AMI_1:def 26;
s,s0 equal_outside the Instruction-Locations of SCM+FSA by SCMFSA6A:3;
then A10: s0,s equal_outside the Instruction-Locations of SCM+FSA by FUNCT_7:28
;
A11: I c= s0 by A6,A8,XBOOLE_1:1;
A12: I c= s by A2,A6,XBOOLE_1:1;
for m st m < n holds IC((Computation s).m) in dom I by A5;
then A13: (Computation s0).n,s2 equal_outside
the Instruction-Locations of SCM+FSA by A10,A11,A12,Th21;
s2,s1 equal_outside the Instruction-Locations of SCM+FSA by SCMFSA6A:3;
then A14: (Computation s0).n,s1 equal_outside
the Instruction-Locations of SCM+FSA by A13,FUNCT_7:29;
A15: s|the Instruction-Locations of SCM+FSA
= s2|the Instruction-Locations of SCM+FSA by Th17;
(Computation s0).n|the Instruction-Locations of SCM+FSA
= s0|the Instruction-Locations of SCM+FSA by Th17
.= s1|the Instruction-Locations of SCM+FSA by A15,SCMFSA6A:5;
then A16: (Computation s0).n = s1 by A14,SCMFSA6A:2;
s1 is not halting by Th20;
hence contradiction by A9,A16,SCM_1:27;
end;
cluster keeping_0 -> paraclosed Macro-Instruction;
coherence proof
let I be Macro-Instruction; assume
A17: I is keeping_0;
let s be State of SCM+FSA, n be Nat;
assume
A18: I +* Start-At insloc 0 c= s;
A19: dom I c= the Instruction-Locations of SCM+FSA by AMI_3:def 13;
defpred X[Nat] means not IC (Computation s).$1 in dom I;
assume not IC (Computation s).n in dom I;
then A20: ex n st X[n];
consider n such that
A21: X[n] and
A22: for m st X[m] holds n <= m from Min(A20);
set FI = FirstNotUsed(I);
set s2 = (Computation s).n;
reconsider s00 = s +*(IC s2, intloc 0 := FI) as State of SCM+FSA;
reconsider s0 = s00+* (FI, (s.intloc 0)+1) as State of SCM+FSA;
not I is keeping_0 proof
take s0;
set IS = I +* Start-At insloc 0;
A23: dom IS = dom I \/ dom Start-At insloc 0 by FUNCT_4:def 1
.= dom I \/ {IC SCM+FSA} by AMI_3:34;
IC s2 <> IC SCM+FSA by AMI_1:48;
then not IC s2 in {IC SCM+FSA} by TARSKI:def 1;
then not IC s2 in dom IS by A21,A23,XBOOLE_0:def 2;
then A24: IS c= s00 by A18,SCMFSA6A:1;
A25: not FI in dom I by A19,SCMFSA_2:84;
FI <> IC SCM+FSA by SCMFSA_2:81;
then not FI in {IC SCM+FSA} by TARSKI:def 1;
then not FI in dom IS by A23,A25,XBOOLE_0:def 2;
hence
A26: I +* Start-At insloc 0 c= s0 by A24,SCMFSA6A:1;
take k = n+1;
set s02 = (Computation s0).n;
A27: (for m st m < n holds IC (Computation s).m in dom I) by A22;
A28: not FI in UsedIntLoc I by SF_MASTR:54;
A29: not IC s2 in UsedIntLoc I proof assume not thesis; then IC s2 is
Int-Location by SCMFSA_2:11;
hence contradiction by SCMFSA_2:84;
end;
A30: s0 | UsedIntLoc I = s00 | UsedIntLoc I by A28,SCMFSA6A:4
.= s | UsedIntLoc I by A29,SCMFSA6A:4;
A31: not FI in UsedInt*Loc I proof assume not thesis; then FI is
FinSeq-Location by SCMFSA_2:12;
hence contradiction by SCMFSA_2:83;
end;
A32: not IC s2 in UsedInt*Loc I proof assume not thesis; then IC s2 is
FinSeq-Location by SCMFSA_2:12;
hence contradiction by SCMFSA_2:85;
end;
A33: s0 | UsedInt*Loc I = s00 | UsedInt*Loc I by A31,SCMFSA6A:4
.= s | UsedInt*Loc I by A32,SCMFSA6A:4;
then A34: (for m st m < n holds IC (Computation s0).m in dom I)
by A18,A26,A27,A30,SF_MASTR:73;
A35: IC s02 = IC s2 by A18,A26,A27,A30,A33,SF_MASTR:73;
FI in dom s00 by SCMFSA_2:66;
then s0.FI = (s.intloc 0)+1 by FUNCT_7:33;
then A36: s02.FI = (s.intloc 0)+1 by A26,A28,A34,SF_MASTR:69;
A37: IC s2 in dom s by SCMFSA_2:5;
IC s2 <> FI & IC s2 in dom s00 by SCMFSA_2:5,84;
then s0.IC s2 = s00.IC s2 by FUNCT_7:34
.= intloc 0 := FI by A37,FUNCT_7:33;
then A38: s02.IC s02 = intloc 0 := FI by A35,AMI_1:54;
A39: intloc 0 <> IC s2 & intloc 0 in dom s by SCMFSA_2:66,84;
A40: s0.intloc 0 = s00.intloc 0 by FUNCT_7:34
.= s.intloc 0 by A39,FUNCT_7:34;
A41: (s.intloc 0) < (s.intloc 0)+1 by REAL_1:69;
(Computation s0).k = Following s02 by AMI_1:def 19
.= Exec(CurInstr s02, s02) by AMI_1:def 18
.= Exec(intloc 0 := FI, s02) by A38,AMI_1:def 17;
hence ((Computation s0).k).intloc 0 <> s0.intloc 0 by A36,A40,A41,SCMFSA_2:89
;
end;
hence contradiction by A17;
end;
end;
theorem
for I being parahalting Macro-Instruction,
a being read-write Int-Location
holds not a in UsedIntLoc I implies (IExec(I, s)).a = s.a
proof let I be parahalting Macro-Instruction,
a be read-write Int-Location; assume
A1: not a in UsedIntLoc I;
A2: IExec(I,s)
= Result(s+*Initialized I) +* s|the Instruction-Locations of SCM+FSA
by Def1;
not a in the Instruction-Locations of SCM+FSA by SCMFSA_2:84;
then not a in dom (s|the Instruction-Locations of SCM+FSA) by RELAT_1:86;
then A3: (IExec(I, s)).a = (Result(s+*Initialized I)).a by A2,FUNCT_4:12;
A4: Initialized I c= s+*Initialized I by FUNCT_4:26;
then s+*Initialized I is halting by Th19;
then consider n such that
A5: Result(s+*Initialized I) = (Computation (s+*Initialized I)).n
& CurInstr(Result(s+*Initialized I)) = halt SCM+FSA by AMI_1:def 22;
A6: I+*Start-At insloc 0 c= s+*Initialized I by A4,Th8;
then A7: (for m st m < n holds IC (Computation (s+*Initialized I)).m in dom I)
by Def2;
A8: not a in dom Initialized I & a in dom s by SCMFSA6A:48,SCMFSA_2:66;
thus (IExec(I, s)).a = (s+*Initialized I).a by A1,A3,A5,A6,A7,SF_MASTR:69
.= s.a by A8,FUNCT_4:12;
end;
theorem
for I being parahalting Macro-Instruction
holds not f in UsedInt*Loc I implies (IExec(I, s)).f = s.f
proof let I be parahalting Macro-Instruction; assume
A1: not f in UsedInt*Loc I;
A2: IExec(I,s)
= Result(s+*Initialized I) +* s|the Instruction-Locations of SCM+FSA
by Def1;
not f in the Instruction-Locations of SCM+FSA by SCMFSA_2:85;
then not f in dom (s|the Instruction-Locations of SCM+FSA) by RELAT_1:86;
then A3: (IExec(I, s)).f = (Result(s+*Initialized I)).f by A2,FUNCT_4:12;
A4: Initialized I c= s+*Initialized I by FUNCT_4:26;
then s+*Initialized I is halting by Th19;
then consider n such that
A5: Result(s+*Initialized I) = (Computation (s+*Initialized I)).n
& CurInstr(Result(s+*Initialized I)) = halt SCM+FSA by AMI_1:def 22;
A6: I+*Start-At insloc 0 c= s+*Initialized I by A4,Th8;
then A7: (for m st m < n holds IC (Computation (s+*Initialized I)).m in dom I)
by Def2;
A8: not f in dom Initialized I & f in dom s by SCMFSA6A:49,SCMFSA_2:67;
thus (IExec(I, s)).f = (s+*Initialized I).f by A1,A3,A5,A6,A7,SF_MASTR:71
.= s.f by A8,FUNCT_4:12;
end;
theorem Th24:
IC s = l & s.l = goto l implies s is not halting
proof
set S = s; assume that
A1: IC S = l and
A2: S.l = goto l;
A3: CurInstr S = goto l by A1,A2,AMI_1:def 17;
defpred X[Nat] means (Computation S).$1 = S;
A4: X[0] by AMI_1:def 19;
A5: for m st X[m] holds X[m+1]
proof let m;
A6: IC Exec(goto l,S) = Exec(goto l, S).IC SCM+FSA by AMI_1:def 15
.= IC S by A1,SCMFSA_2:95;
A7: for a being Int-Location holds Exec(goto l,S).a = S.a by SCMFSA_2:95;
A8: for f being FinSeq-Location holds Exec(goto l,S).f = S.f by SCMFSA_2:95;
A9: for i being Instruction-Location of SCM+FSA holds Exec(goto l,S).i = S.i
by AMI_1:def 13;
assume (Computation S).m = S;
hence (Computation S).(m+1) = Following S by AMI_1:def 19
.= Exec(goto l,S) by A3,AMI_1:def 18
.= S by A6,A7,A8,A9,SCMFSA_2:86;
end;
A10: for m holds X[m] from Ind(A4,A5);
let m;
CurInstr((Computation S).m) = goto l by A3,A10;
hence CurInstr((Computation S).m) <> halt SCM+FSA by SCMFSA_2:47,124;
end;
definition
cluster parahalting -> non empty Macro-Instruction;
coherence
proof let I be Macro-Instruction such that
A1: I is parahalting and
A2: I is empty;
reconsider I as parahalting Macro-Instruction by A1;
deffunc U(set) = goto insloc 0;
deffunc V(set) = 1;
deffunc W(set) = <*>INT;
consider S be State of SCM+FSA such that
A3: IC S = insloc 0 and
A4: for i being Nat holds
S.insloc i = U(i) & S.intloc i = V(i) & S.fsloc i = W(i) from SCMFSAEx;
A5: I c= S by A2,XBOOLE_1:2;
A6: intloc 0 in dom S by SCMFSA_2:66;
S.intloc 0 = 1 by A4;
then (intloc 0) .--> 1 c= S by A6,SCMFSA6A:7;
then A7: I +* ((intloc 0) .--> 1) c= S by A5,SCMFSA6A:6;
A8: IC SCM+FSA in dom S by AMI_5:25;
S.IC SCM+FSA = insloc 0 by A3,AMI_1:def 15;
then IC SCM+FSA .--> insloc 0 c= S by A8,SCMFSA6A:7;
then A9: Start-At(insloc 0) c= S by AMI_3:def 12;
Initialized I = I +* ((intloc 0) .--> 1) +* Start-At(insloc 0)
by SCMFSA6A:def 3;
then Initialized I c= S by A7,A9,SCMFSA6A:6;
then A10: S is halting by AMI_1:def 26;
S.insloc 0 = goto insloc 0 by A4;
hence contradiction by A3,A10,Th24;
end;
end;
theorem Th25: ::T9'
for I being parahalting Macro-Instruction holds dom I <> {}
proof
let I be parahalting Macro-Instruction;
assume A1: dom I = {};
defpred P[set,set] means ex k being Nat st k = $1 & $2 = goto insloc 0;
A2: for x be set st x in NAT holds
ex y being set st y in the Instructions of SCM+FSA & P[x,y];
consider f be Function of NAT,the Instructions of SCM+FSA such that
A3: for x being set st x in NAT holds P[x,f.x] from FuncEx1(A2);
deffunc U(Nat) = f.$1;
deffunc V(set) = 1;
deffunc W(set) = <*>INT;
consider s be State of SCM+FSA such that
A4: IC s = insloc 0 and
A5: for i being Nat holds
s.insloc i = U(i) &
s.intloc i = V(i) & s.fsloc i = W(i) from SCMFSAEx;
A6: dom s = Int-Locations \/ FinSeq-Locations \/ {IC SCM+FSA} \/
the Instruction-Locations of SCM+FSA by AMI_3:36,SCMFSA_2:8;
then A7: dom s
= {IC SCM+FSA} \/ ((Int-Locations \/ FinSeq-Locations) \/
the Instruction-Locations of SCM+FSA) by XBOOLE_1:4;
A8: dom s = FinSeq-Locations \/ {IC SCM+FSA} \/ Int-Locations \/
(the Instruction-Locations of SCM+FSA) by A6,XBOOLE_1:4
.= FinSeq-Locations \/ {IC SCM+FSA} \/
(the Instruction-Locations of SCM+FSA) \/ Int-Locations by XBOOLE_1:4;
P[0,f.0] by A3;
then s.insloc 0 = goto insloc 0 by A5;
then s +*(IC s, goto IC s) = s by A4,FUNCT_7:37;
then A9: s is not halting by Th20;
A10: {IC SCM+FSA} c= dom s by A7,XBOOLE_1:7;
intloc 0 in Int-Locations by SCMFSA_2:9;
then intloc 0 in dom s by A8,XBOOLE_0:def 2;
then for x be set st x in {intloc 0} holds x in dom s by TARSKI:def 1;
then A11: {intloc 0} c= dom s by TARSKI:def 3;
A12: dom Initialized I = dom I \/ {intloc 0} \/ {IC SCM+FSA} by SCMFSA6A:43
.= {intloc 0} \/ {IC SCM+FSA} by A1;
then A13: dom Initialized I c= dom s by A10,A11,XBOOLE_1:8;
now let x be set;
assume A14: x in dom Initialized I;
A15: dom Initialized I = {intloc 0, IC SCM+FSA} by A12,ENUMSET1:41;
per cases by A14,A15,TARSKI:def 2;
suppose A16: x = intloc 0;
hence (Initialized I).x = 1 by SCMFSA6A:46
.= s.x by A5,A16;
suppose A17: x = IC SCM+FSA;
hence (Initialized I).x = IC s by A4,SCMFSA6A:46
.= s.x by A17,AMI_1:def 15;
end;
then Initialized I c= s by A13,GRFUNC_1:8;
hence contradiction by A9,AMI_1:def 26;
end;
theorem Th26: ::T9
for I being parahalting Macro-Instruction holds insloc 0 in dom I
proof
let I be parahalting Macro-Instruction;
dom I is non empty by Th25;
then consider x being set such that A1: x in dom I by XBOOLE_0:def 1;
dom I c= the Instruction-Locations of SCM+FSA by AMI_3:def 13;
then consider n being Nat such that A2: insloc n = x by A1,SCMFSA_2:21;
per cases by NAT_1:19;
suppose n = 0;
hence insloc 0 in dom I by A1,A2;
suppose 0 < n;
hence insloc 0 in dom I by A1,A2,SCMFSA_4:def 4;
end;
theorem Th27: ::T0
for J being parahalting Macro-Instruction st J +* Start-At insloc 0 c= s1
for n being Nat st ProgramPart Relocated(J,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 J be parahalting Macro-Instruction; assume
A1: J +* Start-At insloc 0 c= s1;
set JAt = J +* Start-At insloc 0;
let n be Nat; assume that
A2: ProgramPart Relocated(J,n) c= s2 and
A3: IC s2 = insloc n and
A4: 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);
A5: ProgramPart Relocated(J,n)
= Relocated(J,n) | the Instruction-Locations of SCM+FSA by AMI_5:def 6;
A6: P[0]
proof
A7: IC SCM+FSA in dom JAt by SF_MASTR:65;
insloc 0 in dom J by Th26;
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 A8: 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 A1,A7,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 A3,AMI_1:def 19;
dom J misses dom Start-At insloc 0 by SF_MASTR:64;
then A9: J c= JAt by FUNCT_4:33;
then A10: dom J c= dom JAt by GRFUNC_1:8;
A11: insloc 0 in dom J by Th26;
A12: s1.IC s1 = s1.(s1.IC SCM+FSA) by AMI_1:def 15
.= s1.(JAt.IC SCM+FSA) by A1,A7,GRFUNC_1:8
.= s1.insloc 0 by SF_MASTR:66
.= JAt.insloc 0 by A1,A10,A11,GRFUNC_1:8
.= J.insloc 0 by A9,A11,GRFUNC_1:8;
ProgramPart J = J by AMI_5:72;
then A13: insloc 0 in dom ProgramPart J by Th26;
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 A12,A13,SCMFSA_5:7
.= Relocated(J,n).insloc (0 + n) by SCMFSA_4:def 1
.= (ProgramPart Relocated(J,n)).insloc n by A5,FUNCT_1:72
.= s2.IC s2 by A2,A3,A8,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 A4,AMI_1:def 19
.= C2.0 | (Int-Locations \/ FinSeq-Locations) by AMI_1:def 19;
end;
A14: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume A15: P[k];
A16: C1.(k + 1) = Following C1.k by AMI_1:def 19
.= Exec(CurInstr C1.k,C1.k) by AMI_1:def 18;
A17: C2.(k + 1) = Following C2.k by AMI_1:def 19
.= Exec(CurInstr C2.k,C2.k) by AMI_1:def 18;
hence A18: IC C1.(k + 1) + n
= IC C2.(k + 1) by A15,A16,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 A19: J c= JAt by FUNCT_4:33;
then A20: dom J c= dom JAt by GRFUNC_1:8;
A21: IC C1.(k + 1) in dom J by A1,Def2;
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 A22: l in dom ProgramPart J by A21,XBOOLE_0:def 3;
A23: 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 A1,A20,A21,GRFUNC_1:8
.= J.l by A19,A21,GRFUNC_1:8;
IC C2.(k + 1) in dom Relocated(J,n) by A18,A21,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 A24: IC C2.(k + 1) in dom ProgramPart Relocated(J,n) by A5,FUNCT_1:68;
thus IncAddr(CurInstr C1.(k + 1),n)
= Relocated(J,n).(l + n) by A22,A23,SCMFSA_5:7
.= (ProgramPart Relocated(J,n)).(IC C2.(k + 1)) by A5,A18,FUNCT_1:72
.= s2.IC C2.(k + 1) by A2,A24,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 A15,A16,A17,
SCMFSA6A:41;
end;
for k being Nat holds P[k] from Ind(A6,A14);
hence thesis;
end;
theorem Th28: ::T13
for I being parahalting Macro-Instruction st
I +* Start-At insloc 0 c= s1 & I +* Start-At insloc 0 c= s2 &
s1,s2 equal_outside the Instruction-Locations of SCM+FSA holds
for k being Nat holds
(Computation s1).k, (Computation s2).k
equal_outside the Instruction-Locations of SCM+FSA &
CurInstr (Computation s1).k = CurInstr (Computation s2).k
proof
let I be parahalting Macro-Instruction; assume that
A1: I +* Start-At insloc 0 c= s1 and
A2: I +* Start-At insloc 0 c= s2 and
A3: s1,s2 equal_outside the Instruction-Locations of SCM+FSA;
A4: I c= s1 by A1,Th5;
A5: I c= s2 by A2,Th5;
hereby let k be Nat;
for m being Nat st m < k holds IC((Computation s2).m) in dom I
by A2,Def2;
hence (Computation s1).k, (Computation s2).k equal_outside
the Instruction-Locations of SCM+FSA by A3,A4,A5,Th21;
then A6: IC (Computation s1).k = IC (Computation s2).k by SCMFSA6A:29;
A7: IC (Computation s1).k in dom I by A1,Def2;
A8: IC (Computation s2).k in dom I by A2,Def2;
thus CurInstr (Computation s2).k
= ((Computation s2).k).IC (Computation s2).k by AMI_1:def 17
.= s2.IC (Computation s2).k by AMI_1:54
.= I.IC (Computation s2).k by A5,A8,GRFUNC_1:8
.= s1.IC (Computation s1).k by A4,A6,A7,GRFUNC_1:8
.= ((Computation s1).k).IC (Computation s1).k by AMI_1:54
.= CurInstr (Computation s1).k by AMI_1:def 17;
end;
end;
theorem Th29: ::T14
for I being parahalting Macro-Instruction st
I +* Start-At insloc 0 c= s1 & I +* Start-At insloc 0 c= s2 &
s1,s2 equal_outside the Instruction-Locations of SCM+FSA holds
LifeSpan s1 = LifeSpan s2 &
Result s1, Result s2 equal_outside the Instruction-Locations of SCM+FSA
proof
let I be parahalting Macro-Instruction; assume that
A1: I +* Start-At insloc 0 c= s1 and
A2: I +* Start-At insloc 0 c= s2 and
A3: s1,s2 equal_outside the Instruction-Locations of SCM+FSA;
A4: s1 is halting by A1,Th18;
A5: now let l be Nat; assume
A6: CurInstr (Computation s2).l = halt SCM+FSA;
CurInstr (Computation s1).l = CurInstr (Computation s2).l by A1,A2,A3,Th28
;
hence LifeSpan s1 <= l by A4,A6,SCM_1:def 2;
end;
A7: CurInstr (Computation s2).LifeSpan s1
= CurInstr (Computation s1).LifeSpan s1 by A1,A2,A3,Th28
.= halt SCM+FSA by A4,SCM_1:def 2;
A8: s2 is halting by A2,Th18;
hence LifeSpan s1 = LifeSpan s2 by A5,A7,SCM_1:def 2;
then A9: Result s2 = (Computation s2).LifeSpan s1 by A8,Th16;
Result s1 = (Computation s1).LifeSpan s1 by A4,Th16;
hence Result s1, Result s2 equal_outside
the Instruction-Locations of SCM+FSA by A1,A2,A3,A9,Th28;
end;
theorem Th30: ::T27
for I being parahalting Macro-Instruction
holds IC IExec(I,s) = IC Result (s +* Initialized I)
proof
let I be parahalting Macro-Instruction;
A1: dom s = Int-Locations \/ FinSeq-Locations \/ {IC SCM+FSA} \/
the Instruction-Locations of SCM+FSA by SCMFSA6A:34;
A2: IExec(I,s) = Result (s +* Initialized I)
+* s | the Instruction-Locations of SCM+FSA by Def1;
dom (s | the Instruction-Locations of SCM+FSA)
= dom s /\ the Instruction-Locations of SCM+FSA by RELAT_1:90
.= the Instruction-Locations of SCM+FSA by A1,XBOOLE_1:21;
then A3: not IC SCM+FSA in dom (s | the Instruction-Locations of SCM+FSA)
by AMI_1:48;
thus IC IExec(I,s) = IExec(I,s).IC SCM+FSA by AMI_1:def 15
.= (Result (s +* Initialized I)).IC SCM+FSA by A2,A3,FUNCT_4:12
.= IC Result (s +* Initialized I) by AMI_1:def 15;
end;
theorem Th31:
for I being non empty Macro-Instruction
holds insloc 0 in dom I & insloc 0 in dom Initialized I &
insloc 0 in dom (I +* Start-At insloc 0)
proof
let I be non empty Macro-Instruction;
dom I <> {} by RELAT_1:64; then consider iloc being set such that
A1: iloc in dom I by XBOOLE_0:def 1;
dom I c= the Instruction-Locations of SCM+FSA by AMI_3:def 13;
then consider i being Nat such that
A2: iloc = insloc i by A1,SCMFSA_2:21; 0 < i or 0 = i by NAT_1:18;
hence
A3: insloc 0 in dom I by A1,A2,SCMFSA_4:def 4;
I c= Initialized I by SCMFSA6A:26;
then dom I c= dom Initialized I by RELAT_1:25;
hence insloc 0 in dom Initialized I by A3;
dom (I +* Start-At insloc 0) = dom I \/ dom Start-At insloc 0
by FUNCT_4:def 1;
hence thesis by A3,XBOOLE_0:def 2;
end;
theorem Th32:
x in dom Macro i iff x = insloc 0 or x = insloc 1
proof
(Macro i) = (insloc 0,insloc 1) --> (i,halt SCM+FSA) by SCMFSA6A:def 2;
then dom Macro i = {insloc 0, insloc 1} by FUNCT_4:65;
hence thesis by TARSKI:def 2;
end;
theorem Th33:
(Macro i).(insloc 0) = i &
(Macro i).(insloc 1) = halt SCM+FSA &
(Initialized Macro i).insloc 0 = i &
(Initialized Macro i).insloc 1 = halt SCM+FSA &
((Macro i) +* Start-At insloc 0).insloc 0 = i
proof
A1: insloc 0 <> insloc 1 by SCMFSA_2:18;
thus
A2: (Macro i).(insloc 0)
= ((insloc 0,insloc 1) --> (i,halt SCM+FSA)).(insloc 0) by SCMFSA6A:def 2
.= i by A1,FUNCT_4:66;
thus
A3: (Macro i).(insloc 1)
= ((insloc 0,insloc 1) --> (i,halt SCM+FSA)).(insloc 1) by SCMFSA6A:def 2
.= halt SCM+FSA by A1,FUNCT_4:66;
A4: insloc 0 in dom Macro i & insloc 1 in dom Macro i by Th32;
A5: Macro i c= Initialized Macro i by SCMFSA6A:26;
hence (Initialized Macro i).insloc 0 = i by A2,A4,GRFUNC_1:8;
thus (Initialized Macro i).insloc 1 = halt SCM+FSA by A3,A4,A5,GRFUNC_1:8;
dom (Macro i) misses dom (Start-At insloc 0) by SF_MASTR:64;
then Macro i c= (Macro i) +* Start-At insloc 0 by FUNCT_4:33;
hence thesis by A2,A4,GRFUNC_1:8;
end;
theorem
Initialized I c= s implies IC s = insloc 0
proof assume
A1: Initialized I c= s;
A2: IC Initialized I = insloc 0 by SCMFSA6A:25;
IC SCM+FSA in dom Initialized I by SCMFSA6A:24;
hence IC s = insloc 0 by A1,A2,AMI_5:60;
end;
Lm2: Macro halt SCM+FSA is keeping_0 parahalting proof
set Mi = Macro halt SCM+FSA;
hereby let s be State of SCM+FSA; assume
A1: Mi +* Start-At insloc 0 c= s;
let k be Nat;
A2: insloc 0 in dom (Mi +* Start-At insloc 0) by Th31;
A3: CurInstr((Computation s).0)
= CurInstr s by AMI_1:def 19
.= s.IC s by AMI_1:def 17
.= s.insloc 0 by A1,SF_MASTR:67
.= (Mi +* Start-At insloc 0).insloc 0 by A1,A2,GRFUNC_1:8
.= halt SCM+FSA by Th33;
A4: s = (Computation s).0 by AMI_1:def 19;
0 <= k by NAT_1:18;
hence ((Computation s).k).intloc 0 = s.intloc 0 by A3,A4,AMI_1:52;
end;
thus Mi is parahalting by Lm1;
end;
definition
cluster keeping_0 parahalting Macro-Instruction;
existence by Lm2;
end;
theorem
for I being keeping_0 parahalting Macro-Instruction
holds IExec(I, s).intloc 0 = 1
proof
let I be keeping_0 parahalting Macro-Instruction;
A1: Initialized I c= s+*Initialized I by FUNCT_4:26;
then s+*Initialized I is halting by Th19; then consider n such that
A2: Result(s+*Initialized I) = (Computation (s+*Initialized I)).n &
CurInstr(Result(s+*Initialized I)) = halt SCM+FSA by AMI_1:def 22;
A3: intloc 0 in dom (Initialized I) by SCMFSA6A:45;
A4: I +* Start-At insloc 0 c= s+*Initialized I by A1,Th8;
not intloc 0 in the Instruction-Locations of SCM+FSA proof assume
A5: intloc 0 in the Instruction-Locations of SCM+FSA;
intloc 0 in Int-Locations by SCMFSA_2:9;
hence contradiction by A5,SCMFSA_2:13,XBOOLE_0:3;
end;
then A6: not intloc 0 in dom(s|the Instruction-Locations of SCM+FSA) by RELAT_1
:86;
thus IExec(I, s).intloc 0
= (Result(s+*Initialized I)
+* s|the Instruction-Locations of SCM+FSA).intloc 0 by Def1
.= (Result(s+*Initialized I)).intloc 0 by A6,FUNCT_4:12
.= (s+*Initialized I).intloc 0 by A2,A4,Def4
.= (Initialized I).intloc 0 by A3,FUNCT_4:14
.= 1 by SCMFSA6A:46;
end;
begin :: The composition of macroinstructions
theorem Th36:
for I being paraclosed Macro-Instruction, J being Macro-Instruction
st I +* Start-At insloc 0 c= s & s is halting
for m st m <= LifeSpan s
holds (Computation s).m,(Computation(s+*(I ';' J))).m
equal_outside the Instruction-Locations of SCM+FSA
proof let I be paraclosed Macro-Instruction, J be Macro-Instruction;
assume that
A1: I +* Start-At insloc 0 c= s and
A2: s is halting;
defpred X[Nat] means
$1 <= LifeSpan s implies (Computation s).$1,(Computation(s+*(I ';' J))).$1
equal_outside the Instruction-Locations of SCM+FSA;
(Computation s).0 = s &
(Computation(s+*(I ';' J))).0 = s+*(I ';' J) by AMI_1:def 19;
then A3: X[0] by SCMFSA6A:27;
A4: for m st X[m] holds X[m+1]
proof let m;
assume
A5: m <= LifeSpan s
implies (Computation s).m,(Computation(s+*(I ';' J))).m
equal_outside the Instruction-Locations of SCM+FSA;
assume A6: m+1 <= LifeSpan s;
then A7: m < LifeSpan s by NAT_1:38;
set Cs = Computation s, CsIJ = Computation(s+*(I ';' J));
A8: Cs.(m+1) = Following Cs.m by AMI_1:def 19
.= Exec(CurInstr Cs.m,Cs.m) by AMI_1:def 18;
A9: CsIJ.(m+1) = Following CsIJ.m by AMI_1:def 19
.= Exec(CurInstr CsIJ.m,CsIJ.m) by AMI_1:def 18;
A10: IC(Cs.m) = IC(CsIJ.m) by A5,A6,NAT_1:38,SCMFSA6A:29;
A11: IC Cs.m in dom I by A1,Def2;
dom I misses dom Start-At insloc 0 by SF_MASTR:64;
then I c= I +* Start-At insloc 0 by FUNCT_4:33;
then I c= s by A1,XBOOLE_1:1;
then A12: I c= Cs.m by AMI_3:38;
I ';' J c= s+*(I ';' J) by FUNCT_4:26;
then A13: I ';' J c= CsIJ.m by AMI_3:38;
dom(I ';' J)
= dom(Directed I +* ProgramPart Relocated(J, card I)) by SCMFSA6A:def 4
.= dom Directed I \/ dom ProgramPart Relocated(J, card I) by FUNCT_4:def 1
.= dom I \/ dom ProgramPart Relocated(J, card I) by SCMFSA6A:14;
then A14: dom I c= dom(I ';' J) by XBOOLE_1:7;
A15: CurInstr(Cs.m) = (Cs.m).IC(Cs.m) by AMI_1:def 17
.= I.IC(Cs.m) by A11,A12,GRFUNC_1:8;
then I.IC(Cs.m) <> halt SCM+FSA by A2,A7,SCM_1:def 2;
then CurInstr(Cs.m) = (I ';' J).IC(Cs.m) by A11,A15,SCMFSA6A:54
.= (CsIJ.m).IC(Cs.m) by A11,A13,A14,GRFUNC_1:8
.= CurInstr(CsIJ.m) by A10,AMI_1:def 17;
hence (Computation s).(m+1),(Computation(s+*(I ';' J))).(m+1)
equal_outside the Instruction-Locations of SCM+FSA by A5,A6,A8,A9,NAT_1:38
,SCMFSA6A:32;
end;
thus for m holds X[m] from Ind(A3,A4);
end;
theorem Th37: ::Lemma01
for I being paraclosed Macro-Instruction
st s +*I is halting & Directed I c= s & Start-At insloc 0 c= s holds
IC (Computation s).(LifeSpan (s +*I) + 1)
= insloc card I
proof
let I be paraclosed Macro-Instruction;
assume that
A1: s +*I is halting and
A2: Directed I c= s and
A3: Start-At insloc 0 c= s;
set sISA0 = s +*(I +* Start-At insloc 0);
A4: I +* Start-At insloc 0 c= sISA0 by FUNCT_4:26;
A5: sISA0 = s +*I +* Start-At insloc 0 by FUNCT_4:15
.= s +* Start-At insloc 0 +*I by Th14
.= s +* I by A3,AMI_5:10;
set s2 = sISA0 +* Directed I;
A6: dom Directed I = dom I by SCMFSA6A:14;
A7: s2 = s +*I +* Start-At insloc 0 +* Directed I by FUNCT_4:15
.= s +* Start-At insloc 0 +*I +* Directed I by Th14
.= s +*I +* Directed I by A3,AMI_5:10
.= s +*(I +* Directed I) by FUNCT_4:15
.= s +*Directed I by A6,FUNCT_4:20
.= s by A2,AMI_5:10;
set m = LifeSpan sISA0;
set A = the Instruction-Locations of SCM+FSA;
now let k be Nat;
set s1 = sISA0 +* (I ';' I);
assume A8: k <= m;
then A9: (Computation sISA0).k, (Computation s1).k equal_outside A by A1,A4,A5,
Th36;
A10: Directed I, I ';' I equal_outside A by SCMFSA6A:42;
defpred X[Nat] means
$1 <= k implies (Computation s1).$1, (Computation s2).$1 equal_outside A;
A11: (Computation s1).0 = s1 by AMI_1:def 19;
(Computation s2).0 = s2 by AMI_1:def 19;
then (Computation s2).0, (Computation s1).0 equal_outside A
by A10,A11,SCMFSA6A:12;
then A12: X[0] by FUNCT_7:28;
A13: for n being Nat st X[n] holds X[n+1]
proof let n be Nat;
A14: dom I c= dom (I ';' I) by SCMFSA6A:56;
A15: Directed I c= I ';' I by SCMFSA6A:55;
assume A16: n <= k implies
(Computation s1).n,(Computation s2).n equal_outside A;
assume A17: n + 1 <= k;
A18: n <= n + 1 by NAT_1:37;
then n <= k by A17,AXIOMS:22;
then n <= m by A8,AXIOMS:22;
then (Computation sISA0).n, (Computation s1).n equal_outside A by A1,A4,
A5,Th36;
then IC (Computation sISA0).n = IC (Computation s1).n by SCMFSA6A:29;
then A19: IC (Computation s1).n in dom I by A4,Def2;
A20: IC (Computation s1).n = IC (Computation s2).n by A16,A17,A18,AXIOMS:
22,SCMFSA6A:29;
then A21: IC (Computation s2).n in dom Directed I by A19,SCMFSA6A:
14;
now thus
CurInstr (Computation s1).n
= ((Computation s1).n).IC (Computation s1).n by AMI_1:def 17
.= s1.IC (Computation s1).n by AMI_1:54;
end;
then CurInstr (Computation s1).n
= (I ';' I).IC (Computation s1).n by A14,A19,FUNCT_4:14;
then A22: CurInstr (Computation s1).n
= (Directed I).IC (Computation s1).n by A15,A20,A21,GRFUNC_1:8;
A23: CurInstr (Computation s2).n
= ((Computation s2).n).IC (Computation s2).n by AMI_1:def 17
.= s2.IC (Computation s2).n by AMI_1:54
.= (Directed I).IC (Computation s2).n by A21,FUNCT_4:14;
A24: (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;
(Computation s2).(n + 1) = Following (Computation s2).n by AMI_1:def
19
.= Exec(CurInstr (Computation s2).n,(Computation s2).n)
by AMI_1:def 18;
hence (Computation s1).(n + 1), (Computation s2).(n + 1)
equal_outside A by A16,A17,A18,A20,A22,A23,A24,AXIOMS:22,SCMFSA6A:
32;
end;
for n being Nat holds X[n] from Ind(A12,A13);
then (Computation s1).k, (Computation s2).k equal_outside A;
hence (Computation sISA0).k, (Computation s2).k equal_outside A
by A9,FUNCT_7:29;
end;
then A25: (Computation sISA0).m, (Computation s2).m equal_outside A;
set l1 = IC (Computation sISA0).m;
A26: IC (Computation sISA0).m in dom I by A4,Def2;
then IC (Computation s2).m in dom I by A25,SCMFSA6A:29;
then A27: IC (Computation s2).m in dom Directed I by SCMFSA6A:14;
A28: l1 = IC (Computation s2).m by A25,SCMFSA6A:29;
set IAt = I +* Start-At insloc 0;
dom I misses dom Start-At insloc 0 by SF_MASTR:64;
then I c= I +* Start-At insloc 0 by FUNCT_4:33;
then dom I c= dom IAt by GRFUNC_1:8;
then sISA0.l1 = (IAt).l1 by A4,A26,GRFUNC_1:8;
then A29: I.l1 = sISA0.l1 by A26,Th7
.= (Computation sISA0).m.IC (Computation sISA0).m by AMI_1:54
.= CurInstr (Computation sISA0).m by AMI_1:def 17
.= halt SCM+FSA by A1,A5,SCM_1:def 2;
{halt SCM+FSA} = dom (halt SCM+FSA .--> goto insloc card I)
by CQC_LANG:5;
then A30: halt SCM+FSA in dom (halt SCM+FSA .--> goto insloc card I)
by TARSKI:def 1;
A31: (halt SCM+FSA .--> goto insloc card I).halt SCM+FSA
= goto insloc card I by CQC_LANG:6;
A32: s2.l1 = (Directed I).l1 by A27,A28,FUNCT_4:14
.= (((id the Instructions of SCM+FSA) +* (halt SCM+FSA .-->
goto insloc card I))*I).l1 by SCMFSA6A:def 1
.= ((id the Instructions of SCM+FSA) +* (halt SCM+FSA .-->
goto insloc card I)).(halt SCM+FSA) by A26,A29,FUNCT_1:23
.= goto insloc card I by A30,A31,FUNCT_4:14;
A33: CurInstr (Computation s2).m
= (Computation s2).m.l1 by A28,AMI_1:def 17
.= goto insloc card I by A32,AMI_1:54;
(Computation s2).(m + 1)
= Following (Computation s2).m by AMI_1:def 19
.= Exec(goto insloc card I,(Computation s2).m) by A33,AMI_1:def 18;
then IC (Computation s2).(m + 1)
= Exec(goto insloc card I,(Computation s2).m).IC SCM+FSA
by AMI_1:def 15
.= insloc card I by SCMFSA_2:95;
hence IC (Computation s).(LifeSpan (s+*I) + 1) = insloc card I
by A5,A7;
end;
theorem Th38: ::Lemma02
for I being paraclosed Macro-Instruction
st s +*I is halting & Directed I c= s & Start-At insloc 0 c= s
holds
(Computation s).(LifeSpan (s +*I)) |
(Int-Locations \/ FinSeq-Locations) =
(Computation s).(LifeSpan (s +*I) + 1) |
(Int-Locations \/ FinSeq-Locations)
proof
let I be paraclosed Macro-Instruction; assume that
A1: s +*I is halting and
A2: Directed I c= s and
A3: Start-At insloc 0 c= s;
set sISA0 = s +*(I +* Start-At insloc 0);
A4: I +* Start-At insloc 0 c= sISA0 by FUNCT_4:26;
A5: sISA0 = s +*I +* Start-At insloc 0 by FUNCT_4:15
.= s +* Start-At insloc 0 +*I by Th14
.= s +* I by A3,AMI_5:10;
set s2 = sISA0 +* Directed I;
A6: dom Directed I = dom I by SCMFSA6A:14;
s2 = s +*I +* Start-At insloc 0 +* Directed I by FUNCT_4:15
.= s +* Start-At insloc 0 +*I +* Directed I by Th14
.= s +*I +* Directed I by A3,AMI_5:10
.= s +*(I +* Directed I) by FUNCT_4:15
.= s +*Directed I by A6,FUNCT_4:20;
then A7: s2 = s by A2,AMI_5:10;
set m = LifeSpan sISA0;
set A = the Instruction-Locations of SCM+FSA;
now let k be Nat;
set s1 = sISA0 +* (I ';' I);
assume A8: k <= m;
then A9: (Computation sISA0).k, (Computation s1).k equal_outside A by A1,A4,
A5,Th36;
defpred X[Nat] means
$1 <= k implies (Computation s1).$1, (Computation s2).$1 equal_outside A;
A10: Directed I, I ';' I equal_outside A by SCMFSA6A:42;
A11: (Computation s1).0 = s1 by AMI_1:def 19;
(Computation s2).0 = s2 by AMI_1:def 19;
then (Computation s2).0, (Computation s1).0 equal_outside A
by A10,A11,SCMFSA6A:12;
then A12: X[0] by FUNCT_7:28;
A13: for n being Nat st X[n] holds X[n+1]
proof let n be Nat;
A14: dom I c= dom (I ';' I) by SCMFSA6A:56;
A15: Directed I c= I ';' I by SCMFSA6A:55;
assume A16: n <= k implies
(Computation s1).n,(Computation s2).n equal_outside A;
assume A17: n + 1 <= k;
A18: n <= n + 1 by NAT_1:37;
then n <= k by A17,AXIOMS:22;
then n <= m by A8,AXIOMS:22;
then (Computation sISA0).n, (Computation s1).n equal_outside A by A1,A4,
A5,Th36;
then IC (Computation sISA0).n = IC (Computation s1).n by SCMFSA6A:29;
then A19: IC (Computation s1).n in dom I by A4,Def2;
A20: IC (Computation s1).n = IC (Computation s2).n by A16,A17,A18,AXIOMS:
22,SCMFSA6A:29;
then A21: IC (Computation s2).n in dom Directed I by A19,SCMFSA6A:
14;
A22: CurInstr (Computation s1).n
= ((Computation s1).n).IC (Computation s1).n by AMI_1:def 17
.= s1.IC (Computation s1).n by AMI_1:54
.= (I ';' I).IC (Computation s1).n by A14,A19,FUNCT_4:14
.= (Directed I).IC (Computation s1).n by A15,A20,A21,GRFUNC_1:8;
A23: CurInstr (Computation s2).n
= ((Computation s2).n).IC (Computation s2).n by AMI_1:def 17
.= s2.IC (Computation s2).n by AMI_1:54
.= (Directed I).IC (Computation s2).n by A21,FUNCT_4:14;
A24: (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;
(Computation s2).(n + 1) = Following (Computation s2).n by AMI_1:def
19
.= Exec(CurInstr (Computation s2).n,(Computation s2).n)
by AMI_1:def 18;
hence (Computation s1).(n + 1), (Computation s2).(n + 1)
equal_outside A by A16,A17,A18,A20,A22,A23,A24,AXIOMS:22,SCMFSA6A:
32;
end;
for n being Nat holds X[n] from Ind(A12,A13);
then (Computation s1).k, (Computation s2).k equal_outside A;
hence (Computation sISA0).k, (Computation s2).k equal_outside A
by A9,FUNCT_7:29;
end;
then A25: (Computation sISA0).m, (Computation s2).m equal_outside A;
set l1 = IC (Computation sISA0).m;
A26: IC (Computation sISA0).m in dom I by A4,Def2;
then IC (Computation s2).m in dom I by A25,SCMFSA6A:29;
then A27: IC (Computation s2).m in dom Directed I by SCMFSA6A:14;
A28: l1 = IC (Computation s2).m by A25,SCMFSA6A:29;
set IAt = I +* Start-At insloc 0;
dom I misses dom Start-At insloc 0 by SF_MASTR:64;
then I c= I +* Start-At insloc 0 by FUNCT_4:33;
then dom I c= dom IAt by GRFUNC_1:8;
then sISA0.l1 = (IAt).l1 by A4,A26,GRFUNC_1:8;
then A29: I.l1 = sISA0.l1 by A26,Th7
.= (Computation sISA0).m.IC (Computation sISA0).m by AMI_1:54
.= CurInstr (Computation sISA0).m by AMI_1:def 17
.= halt SCM+FSA by A1,A5,SCM_1:def 2;
{halt SCM+FSA} = dom (halt SCM+FSA .--> goto insloc card I)
by CQC_LANG:5;
then A30: halt SCM+FSA in dom (halt SCM+FSA .--> goto insloc card I)
by TARSKI:def 1;
A31: (halt SCM+FSA .--> goto insloc card I).halt SCM+FSA
= goto insloc card I by CQC_LANG:6;
A32: s2.l1 = (Directed I).l1 by A27,A28,FUNCT_4:14
.= (((id the Instructions of SCM+FSA) +* (halt SCM+FSA .-->
goto insloc card I))*I).l1 by SCMFSA6A:def 1
.= ((id the Instructions of SCM+FSA) +* (halt SCM+FSA .-->
goto insloc card I)).(halt SCM+FSA) by A26,A29,FUNCT_1:23
.= goto insloc card I by A30,A31,FUNCT_4:14;
A33: CurInstr (Computation s2).m
= (Computation s2).m.l1 by A28,AMI_1:def 17
.= goto insloc card I by A32,AMI_1:54;
(Computation s2).(m + 1)
= Following (Computation s2).m by AMI_1:def 19
.= Exec(goto insloc card I,(Computation s2).m) by A33,AMI_1:def 18;
then (for a being Int-Location holds
(Computation s2).(m + 1).a = (Computation s2).m.a) &
for f being FinSeq-Location holds
(Computation s2).(m + 1).f = (Computation s2).m.f by SCMFSA_2:95;
hence (Computation s).(LifeSpan (s +*I)) |
(Int-Locations \/ FinSeq-Locations) =
(Computation s).(LifeSpan (s +*I) + 1) |
(Int-Locations \/ FinSeq-Locations)
by A5,A7,SCMFSA6A:38;
end;
theorem Th39: ::Lemma0
for I being parahalting Macro-Instruction
st Initialized I c= s holds
for k being Nat st k <= LifeSpan s holds
CurInstr (Computation (s +* Directed I)).k <> halt SCM+FSA
proof
let I be parahalting Macro-Instruction;
assume A1: Initialized I c= s;
then A2: s is halting by AMI_1:def 26;
A3: I +* Start-At insloc 0 c= s by A1,Th8;
set s2 = s +* Directed I;
set m = LifeSpan s;
set A = the Instruction-Locations of SCM+FSA;
A4: now let k be Nat;
set s1 = s +* (I ';' I);
assume A5: k <= m;
then A6: (Computation s).k, (Computation s1).k equal_outside A by A2,A3,Th36
;
A7: Directed I, I ';' I equal_outside A by SCMFSA6A:42;
defpred X[Nat] means
$1 <= k implies (Computation s1).$1, (Computation s2).$1 equal_outside A;
A8: (Computation s1).0 = s1 by AMI_1:def 19;
(Computation s2).0 = s2 by AMI_1:def 19;
then (Computation s2).0, (Computation s1).0 equal_outside A
by A7,A8,SCMFSA6A:12;
then A9: X[0] by FUNCT_7:28;
A10: for n being Nat st X[n] holds X[n+1]
proof let n be Nat;
A11: dom I c= dom (I ';' I) by SCMFSA6A:56;
A12: Directed I c= I ';' I by SCMFSA6A:55;
assume A13: n <= k implies
(Computation s1).n,(Computation s2).n equal_outside A;
assume A14: n + 1 <= k;
A15: n <= n + 1 by NAT_1:37;
then n <= k by A14,AXIOMS:22;
then n <= m by A5,AXIOMS:22;
then (Computation s).n, (Computation s1).n equal_outside A by A2,A3,Th36;
then IC (Computation s).n = IC (Computation s1).n by SCMFSA6A:29;
then A16: IC (Computation s1).n in dom I by A3,Def2;
A17: IC (Computation s1).n = IC (Computation s2).n by A13,A14,A15,AXIOMS:
22,SCMFSA6A:29;
then A18: IC (Computation s2).n in dom Directed I by A16,SCMFSA6A:
14;
A19: CurInstr (Computation s1).n
= ((Computation s1).n).IC (Computation s1).n by AMI_1:def 17
.= s1.IC (Computation s1).n by AMI_1:54
.= (I ';' I).IC (Computation s1).n by A11,A16,FUNCT_4:14
.= (Directed I).IC (Computation s1).n by A12,A17,A18,GRFUNC_1:8;
A20: CurInstr (Computation s2).n
= ((Computation s2).n).IC (Computation s2).n by AMI_1:def 17
.= s2.IC (Computation s2).n by AMI_1:54
.= (Directed I).IC (Computation s2).n by A18,FUNCT_4:14;
A21: (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;
(Computation s2).(n + 1) = Following (Computation s2).n by AMI_1:def
19
.= Exec(CurInstr (Computation s2).n,(Computation s2).n)
by AMI_1:def 18;
hence (Computation s1).(n + 1), (Computation s2).(n + 1)
equal_outside A by A13,A14,A15,A17,A19,A20,A21,AXIOMS:22,SCMFSA6A:
32;
end;
for n being Nat holds X[n] from Ind(A9,A10);
then (Computation s1).k, (Computation s2).k equal_outside A;
hence (Computation s).k, (Computation s2).k equal_outside A
by A6,FUNCT_7:29;
end;
then A22: (Computation s).m, (Computation s2).m equal_outside A;
set l1 = IC (Computation s).m;
A23: IC (Computation s).m in dom I by A3,Def2;
then IC (Computation s2).m in dom I by A22,SCMFSA6A:29;
then A24: IC (Computation s2).m in dom Directed I by SCMFSA6A:14;
A25: l1 = IC (Computation s2).m by A22,SCMFSA6A:29;
I c= Initialized I by SCMFSA6A:26;
then dom I c= dom Initialized I by GRFUNC_1:8;
then s.l1 = (Initialized I).l1 by A1,A23,GRFUNC_1:8;
then A26: I.l1 = s.l1 by A23,SCMFSA6A:50
.= (Computation s).m.IC (Computation s).m by AMI_1:54
.= CurInstr (Computation s).m by AMI_1:def 17
.= halt SCM+FSA by A2,SCM_1:def 2;
{halt SCM+FSA} = dom (halt SCM+FSA .--> goto insloc card I)
by CQC_LANG:5;
then A27: halt SCM+FSA in dom (halt SCM+FSA .--> goto insloc card I)
by TARSKI:def 1;
A28: (halt SCM+FSA .--> goto insloc card I).halt SCM+FSA
= goto insloc card I by CQC_LANG:6;
A29: s2.l1 = (Directed I).l1 by A24,A25,FUNCT_4:14
.= (((id the Instructions of SCM+FSA) +* (halt SCM+FSA .-->
goto insloc card I))*I).l1 by SCMFSA6A:def 1
.= ((id the Instructions of SCM+FSA) +* (halt SCM+FSA .-->
goto insloc card I)).(halt SCM+FSA) by A23,A26,FUNCT_1:23
.= goto insloc card I by A27,A28,FUNCT_4:14;
A30: CurInstr (Computation s2).m
= (Computation s2).m.l1 by A25,AMI_1:def 17
.= goto insloc card I by A29,AMI_1:54;
hereby let k be Nat;
assume A31: k <= LifeSpan s;
set lk = IC (Computation s).k;
per cases;
suppose k <> LifeSpan s;
A32: (Computation s).k, (Computation s2).k equal_outside A by A4,A31;
A33: IC (Computation s).k in dom I by A3,Def2;
A34: lk = IC (Computation s2).k by A32,SCMFSA6A:29;
A35: dom I = dom Directed I by SCMFSA6A:14;
assume A36: CurInstr (Computation (s +* Directed I)).k = halt SCM+FSA;
A37: CurInstr (Computation s2).k
= (Computation s2).k.lk by A34,AMI_1:def 17
.= s2.lk by AMI_1:54
.= (Directed I).lk by A33,A35,FUNCT_4:14;
(Directed I).lk in rng Directed I by A33,A35,FUNCT_1:def 5;
hence contradiction by A36,A37,SCMFSA6A:18;
suppose A38: k = LifeSpan s;
assume CurInstr (Computation (s +* Directed I)).k = halt SCM+FSA;
hence contradiction by A30,A38,SCMFSA_2:47,124;
end;
end;
theorem Th40:
for I being paraclosed Macro-Instruction
st s +* (I +* Start-At insloc 0) is halting
for J being Macro-Instruction, k being Nat
st k <= LifeSpan (s +* (I +* Start-At insloc 0))
holds (Computation (s +* (I +* Start-At insloc 0))).k,
(Computation (s +* ((I ';' J) +* Start-At insloc 0))).k
equal_outside the Instruction-Locations of SCM+FSA
proof let I be paraclosed Macro-Instruction; assume
A1: s +* (I +* Start-At insloc 0) is halting;
let J be Macro-Instruction;
set s1 = s +* (I +* Start-At insloc 0);
A2: I +* Start-At insloc 0 c= s1 by FUNCT_4:26;
set s2 = s +* ((I ';' J) +* Start-At insloc 0);
A3: (I ';' J) +* Start-At insloc 0 c= s2 by FUNCT_4:26;
A4: s1 = s +* I +* SA0 by FUNCT_4:15 .= s+*SA0+*I by Th14;
A5: s2 = s +* (I ';' J) +* SA0 by FUNCT_4:15
.= s+*SA0+*(I ';' J) by Th14;
s+*SA0, s+*SA0+*I
equal_outside the Instruction-Locations of SCM+FSA by SCMFSA6A:27;
then A6: s+*SA0+*I, s+*SA0
equal_outside the Instruction-Locations of SCM+FSA by FUNCT_7:28;
defpred X[Nat] means
$1 <= LifeSpan s1
implies (Computation s1).$1, (Computation s2).$1
equal_outside the Instruction-Locations of SCM+FSA;
A7: s+*SA0, s+*SA0+*(I ';' J)
equal_outside the Instruction-Locations of SCM+FSA by SCMFSA6A:27;
(Computation s1).0 = s1 & (Computation(s2)).0 = s2 by AMI_1:def 19;
then A8: X[0] by A4,A5,A6,A7,FUNCT_7:29;
A9: for m st X[m] holds X[m+1]
proof let m;
assume
A10: m <= LifeSpan s1
implies (Computation s1).m,(Computation(s2)).m
equal_outside the Instruction-Locations of SCM+FSA;
assume A11: m+1 <= LifeSpan s1;
then A12: m < LifeSpan s1 by NAT_1:38;
set Cs = Computation s1, CsIJ = Computation s2;
A13: Cs.(m+1) = Following Cs.m by AMI_1:def 19
.= Exec(CurInstr Cs.m,Cs.m) by AMI_1:def 18;
A14: CsIJ.(m+1) = Following CsIJ.m by AMI_1:def 19
.= Exec(CurInstr CsIJ.m,CsIJ.m) by AMI_1:def 18;
A15: IC(Cs.m) = IC(CsIJ.m) by A10,A11,NAT_1:38,SCMFSA6A:29;
A16: IC Cs.m in dom I by A2,Def2;
dom I misses dom Start-At insloc 0 by SF_MASTR:64;
then I c= I +* Start-At insloc 0 by FUNCT_4:33;
then I c= s1 by A2,XBOOLE_1:1;
then A17: I c= Cs.m by AMI_3:38;
dom (I ';' J) misses dom SA0 by SF_MASTR:64;
then (I ';' J) c= (I ';' J)+*SA0 by FUNCT_4:33;
then (I ';' J) c= s2 by A3,XBOOLE_1:1;
then A18: I ';' J c= CsIJ.m by AMI_3:38;
dom(I ';' J)
= dom(Directed I +* ProgramPart Relocated(J, card I)) by SCMFSA6A:def 4
.= dom Directed I \/ dom ProgramPart Relocated(J, card I) by FUNCT_4:def 1
.= dom I \/ dom ProgramPart Relocated(J, card I) by SCMFSA6A:14;
then A19: dom I c= dom(I ';' J) by XBOOLE_1:7;
A20: CurInstr(Cs.m) = (Cs.m).IC(Cs.m) by AMI_1:def 17
.= I.IC(Cs.m) by A16,A17,GRFUNC_1:8;
then I.IC(Cs.m) <> halt SCM+FSA by A1,A12,SCM_1:def 2;
then CurInstr(Cs.m) = (I ';' J).IC(Cs.m) by A16,A20,SCMFSA6A:54
.= (CsIJ.m).IC(Cs.m) by A16,A18,A19,GRFUNC_1:8
.= CurInstr(CsIJ.m) by A15,AMI_1:def 17;
hence (Computation s1).(m+1),(Computation(s2)).(m+1)
equal_outside the Instruction-Locations of SCM+FSA by A10,A11,A13,A14,
NAT_1:38,SCMFSA6A:32;
end;
thus for k being Nat holds X[k] from Ind(A8, A9);
end;
Lm3:
for I being keeping_0 parahalting Macro-Instruction,
J being parahalting Macro-Instruction,
s being State of SCM+FSA st Initialized (I ';' J) c= s holds
IC (Computation s).(LifeSpan (s +* I) + 1) = insloc card I &
(Computation s).(LifeSpan (s +* I) + 1)
| (Int-Locations \/ FinSeq-Locations)
= ((Computation (s +* I)).(LifeSpan (s +* I)) +* Initialized J)
| (Int-Locations \/ FinSeq-Locations) &
ProgramPart Relocated(J,card I) c=
(Computation s).(LifeSpan (s +* I) + 1) &
(Computation s).(LifeSpan (s +* I) + 1).intloc 0 = 1 &
s is halting &
LifeSpan s
= LifeSpan (s +* I) + 1 + LifeSpan (Result (s +* I) +* Initialized J) &
(J is keeping_0 implies (Result s).intloc 0 = 1)
proof
let I be keeping_0 parahalting Macro-Instruction;
let J be parahalting Macro-Instruction;
let s be State of SCM+FSA;
set s1 = s +* I;
set s3 = (Computation s1).(LifeSpan s1) +* Initialized J;
set m1 = LifeSpan s1;
set m3 = LifeSpan s3;
set D = Int-Locations \/ FinSeq-Locations;
assume
A1: Initialized (I ';' J) c= s;
then A2: Initialized I c= s +* I by SCMFSA6A:52;
then A3: I +* Start-At insloc 0 c= s +* I by Th8;
(I ';' J) +* SA0 c= s by A1,Th8;
then A4: s = s +*((I ';' J) +* SA0) by AMI_5:10;
A5: SA0 c= (I ';' J) +* SA0 by FUNCT_4:26;
(I ';' J) +* SA0 c= s by A1,Th8;
then A6: Start-At insloc 0 c= s by A5,XBOOLE_1:1;
then A7: s +* I = s +*Start-At insloc 0 +* I by AMI_5:10
.= s +*I+*Start-At insloc 0 by Th14
.= s +*(I+*Start-At insloc 0) by FUNCT_4:15;
A8: s +* I is halting by A3,Th18;
A9: s3 | D = ((Computation s1).m1 | D) +* (Initialized J) | D by AMI_5:6;
A10: intloc 0 in dom Initialized I by SCMFSA6A:45;
A11: now let x be set;
assume x in dom ((Initialized J) | D);
then A12: x in dom (Initialized J) /\ D by FUNCT_1:68;
then A13: x in dom Initialized J & x in D by XBOOLE_0:def 3;
per cases by A13,SCMFSA6A:44;
suppose A14: x in dom J;
dom J c= the Instruction-Locations of SCM+FSA by AMI_3:def 13;
hence ((Initialized J) | D).x = ((Computation s1).m1 | D).x by A13,
A14,SCMFSA6A:37;
suppose A15: x = intloc 0;
thus ((Initialized J) | D).x = (Initialized J).x by A13,FUNCT_1:72
.= 1 by A15,SCMFSA6A:46
.= (Initialized I).x by A15,SCMFSA6A:46
.= s1.x by A2,A10,A15,GRFUNC_1:8
.= ((Computation s1).m1).x by A3,A15,Def4
.= ((Computation s1).m1 | D).x by A13,FUNCT_1:72;
suppose x = IC SCM+FSA;
hence ((Initialized J) | D).x = ((Computation s1).m1 | D).x by A12,
SCMFSA6A:37,XBOOLE_0:def 3;
end;
Initialized J c= s3 by FUNCT_4:26;
then dom Initialized J c= dom s3 by GRFUNC_1:8;
then A16: dom Initialized J c= the carrier of SCM+FSA by AMI_3:36;
dom ((Initialized J) | D) = dom Initialized J /\ D by RELAT_1:90;
then dom ((Initialized J) | D) c= (the carrier of SCM+FSA) /\ D
by A16,XBOOLE_1:26;
then dom ((Initialized J) | D) c= dom ((Computation s1).m1) /\ D
by AMI_3:36;
then dom ((Initialized J) | D) c= dom ((Computation s1).m1 | D)
by RELAT_1:90;
then (Initialized J) | D c= (Computation s1).m1 | D by A11,GRFUNC_1:8;
then A17: (Computation s1).m1 | D = s3 | D by A9,LATTICE2:8;
(Computation s1).m1, (Computation s).m1
equal_outside the Instruction-Locations of SCM+FSA
by A4,A7,A8,Th40;
then A18: (Computation s).m1 | D = s3 | D by A17,SCMFSA6A:39;
Initialized J c= s3 by FUNCT_4:26;
then A19: s3 is halting by Th19;
A20: dom Directed I = dom I by SCMFSA6A:14;
A21: Directed I c= I ';' J by SCMFSA6A:55;
I ';' J c= Initialized (I ';' J) by SCMFSA6A:26;
then A22: Directed I c= Initialized (I ';' J) by A21,XBOOLE_1:1;
A23: s1 +* Directed I = s +* (I +* Directed I) by FUNCT_4:15
.= s +* Directed I by A20,FUNCT_4:20
.= s +* Initialized (I ';' J) +* Directed I by A1,LATTICE2:8
.= s +* (Initialized (I ';' J) +* Directed I) by FUNCT_4:15
.= s +* Initialized (I ';' J) by A22,LATTICE2:8
.= s by A1,LATTICE2:8;
then A24: Directed I c= s by FUNCT_4:26;
hence
A25: IC (Computation s).(LifeSpan (s +* I) + 1) = insloc card I
by A6,A8,Th37;
thus
A26: (Computation s).(m1 + 1) | D = s3 | D
by A6,A8,A18,A24,Th38;
reconsider m = m1 + 1 + m3 as Nat;
set s4 = (Computation s).(m1 + 1);
Initialized J c= s3 by FUNCT_4:26;
then A27: J +* Start-At insloc 0 c= s3 by Th8;
I ';' J c= Initialized (I ';' J) by SCMFSA6A:26;
then A28: I ';' J c= s by A1,XBOOLE_1:1;
I ';' J = Directed I +* ProgramPart Relocated(J,card I)
by SCMFSA6A:def 4;
then ProgramPart Relocated(J,card I) c= I ';' J by FUNCT_4:26;
then ProgramPart Relocated(J,card I) c= s by A28,XBOOLE_1:1;
hence
A29: ProgramPart Relocated(J,card I) c= s4 by AMI_3:38;
A30: intloc 0 in dom Initialized J by SCMFSA6A:45;
intloc 0 in Int-Locations by SCMFSA_2:9;
then A31: intloc 0 in D by XBOOLE_0:def 2;
hence
s4.intloc 0 = (s3 | D).intloc 0 by A26,FUNCT_1:72
.= s3.intloc 0 by A31,FUNCT_1:72
.= (Initialized J).intloc 0 by A30,FUNCT_4:14
.= 1 by SCMFSA6A:46;
A32: now let k be Nat;
assume m1 + 1 + k < m;
then A33: k < m3 by AXIOMS:24;
assume A34: CurInstr (Computation s).(m1 + 1 + k) = halt SCM+FSA;
IncAddr(CurInstr (Computation s3).k,card I)
= CurInstr (Computation s4).k by A25,A26,A27,A29,Th27
.= halt SCM+FSA by A34,AMI_1:51;
then InsCode CurInstr (Computation s3).k
= 0 by SCMFSA_2:124,SCMFSA_4:22;
then CurInstr (Computation s3).k = halt SCM+FSA by SCMFSA_2:122;
hence contradiction by A19,A33,SCM_1:def 2;
end;
IncAddr(CurInstr (Computation s3).m3,card I)
= CurInstr (Computation s4).m3 by A25,A26,A27,A29,Th27;
then IncAddr(CurInstr (Computation s3).m3,card I)
= CurInstr (Computation s).(m1 + 1 + m3) by AMI_1:51;
then A35: CurInstr((Computation s).m)
= IncAddr (halt SCM+FSA,card I) by A19,SCM_1:def 2
.= halt SCM+FSA by SCMFSA_4:8;
now let k be Nat; assume A36: k < m;
per cases;
suppose k <= m1;
hence CurInstr (Computation s).k <> halt SCM+FSA by A2,A23,Th39;
suppose m1 < k;
then m1 + 1 <= k by NAT_1:38;
then consider kk being Nat such that A37: m1 + 1 + kk = k by NAT_1:28;
thus CurInstr (Computation s).k <> halt SCM+FSA by A32,A36,A37;
end;
then A38: for k being Nat st CurInstr (Computation s).k = halt SCM+FSA
holds m <= k;
thus
A39: s is halting by A35,AMI_1:def 20;
then A40: LifeSpan s = m by A35,A38,SCM_1:def 2;
s1 = s +* Initialized I by A1,SCMFSA6A:51;
then Initialized I c= s1 by FUNCT_4:26;
then s1 is halting by Th19;
hence LifeSpan s
= LifeSpan (s +* I) + 1 + LifeSpan (Result (s +* I) +* Initialized J) by A40
,Th16
;
A41: Initialized J c= s3 by FUNCT_4:26;
then A42: J +* Start-At insloc 0 c= s3 by Th8;
hereby assume A43: J is keeping_0;
A44: (Computation s3).m3 | (Int-Locations \/ FinSeq-Locations)
= (Computation s4).m3 | (Int-Locations \/ FinSeq-Locations) by A25,A26
,A27,A29,Th27;
thus (Result s).intloc 0
= (Computation s).m.intloc 0 by A39,A40,Th16
.= (Computation s4).m3.intloc 0 by AMI_1:51
.= (Computation s3).m3.intloc 0 by A44,SCMFSA6A:38
.= s3.intloc 0 by A42,A43,Def4
.= (Initialized J).intloc 0 by A30,A41,GRFUNC_1:8
.= 1 by SCMFSA6A:46;
end;
end;
definition
let I, J be parahalting Macro-Instruction;
cluster I ';' J -> parahalting;
coherence
proof
let s be State of SCM+FSA; assume
A1: (I ';' J) +* Start-At insloc 0 c= s;
then A2: s = s +*((I ';' J) +* SA0) by AMI_5:10;
set SAt = Start-At insloc 0;
A3: dom I misses dom SAt by SF_MASTR:64;
SAt c= (I ';' J) +* SAt by FUNCT_4:26;
then A4: SAt c= s by A1,XBOOLE_1:1;
then s +*SAt = s by AMI_5:10;
then s +*(SAt +* I) = s +* I by FUNCT_4:15;
then s +* (I +* SAt) = s +* I by A3,FUNCT_4:36;
then A5: I +* SAt c= s +* I by FUNCT_4:26;
A6: s +* I = s +*Start-At insloc 0 +* I by A4,AMI_5:10
.= s +*I+*Start-At insloc 0 by Th14
.= s +*(I+*Start-At insloc 0) by FUNCT_4:15;
A7: s +* I is halting by A5,Th18;
set JAt = J +* SAt;
set s1 = s +* I;
set s3 = (Computation s1).(LifeSpan s1) +* JAt;
set m1 = LifeSpan s1;
set m3 = LifeSpan s3;
set D = Int-Locations \/ FinSeq-Locations;
reconsider kk = JAt | D as Function;
A8: s3 | D = ((Computation s1).m1 | D) +* kk by AMI_5:6;
A9: now let x be set;
assume x in dom (JAt | D);
then A10: x in dom JAt /\ D by FUNCT_1:68;
then A11: x in dom JAt & x in D by XBOOLE_0:def 3;
then x in dom J \/ dom SAt by FUNCT_4:def 1;
then x in dom J \/ {IC SCM+FSA} by AMI_3:34;
then A12: x in dom J or x in {IC SCM+FSA} by XBOOLE_0:def 2;
per cases by A12,TARSKI:def 1;
suppose A13: x in dom J;
dom J c= the Instruction-Locations of SCM+FSA by AMI_3:def 13;
hence kk.x = ((Computation s1).m1 | D).x by A11,A13,SCMFSA6A:37;
suppose x = IC SCM+FSA;
hence kk.x = ((Computation s1).m1 | D).x by A10,SCMFSA6A:37,XBOOLE_0:
def 3;
end;
JAt c= s3 by FUNCT_4:26;
then dom JAt c= dom s3 by GRFUNC_1:8;
then A14: dom JAt c= the carrier of SCM+FSA by AMI_3:36;
dom (JAt | D) = dom JAt /\ D by RELAT_1:90;
then dom (JAt | D) c= (the carrier of SCM+FSA) /\ D
by A14,XBOOLE_1:26;
then dom (JAt | D) c= dom ((Computation s1).m1) /\ D
by AMI_3:36;
then dom (JAt | D) c= dom ((Computation s1).m1 | D)
by RELAT_1:90;
then JAt | D c= (Computation s1).m1 | D by A9,GRFUNC_1:8;
then A15: (Computation s1).m1 | D = s3 | D by A8,LATTICE2:8;
(Computation s1).m1, (Computation s).m1
equal_outside the Instruction-Locations of SCM+FSA
by A2,A6,A7,Th40;
then A16: (Computation s).m1 | D = s3 | D by A15,SCMFSA6A:39;
JAt c= s3 & JAt is halting by Def3,FUNCT_4:26;
then A17: s3 is halting by AMI_1:def 26;
A18: dom Directed I = dom I by SCMFSA6A:14;
A19: Directed I c= I ';' J by SCMFSA6A:55;
dom (I ';' J) misses dom Start-At insloc 0 by SF_MASTR:64;
then A20: I ';' J c= (I ';' J) +* SAt by FUNCT_4:33;
then A21: Directed I c= (I ';' J) +* SAt by A19,XBOOLE_1:1;
s1 +* Directed I = s +* (I +* Directed I) by FUNCT_4:15
.= s +* Directed I by A18,FUNCT_4:20
.= s +* ((I ';' J) +* SAt) +* Directed I
by A1,LATTICE2:8
.= s +* (((I ';' J) +* SAt) +* Directed I) by FUNCT_4:15
.= s +* ((I ';' J) +* SAt) by A21,LATTICE2:8
.= s by A1,LATTICE2:8;
then A22: Directed I c= s by FUNCT_4:26;
then A23: IC (Computation s).(LifeSpan (s +* I) + 1) = insloc card I
by A4,A7,Th37;
A24: (Computation s).(m1 + 1) | D = s3 | D
by A4,A7,A16,A22,Th38;
reconsider m = m1 + 1 + m3 as Nat;
set s4 = (Computation s).(m1 + 1);
A25: JAt c= s3 by FUNCT_4:26;
A26: I ';' J c= s by A1,A20,XBOOLE_1:1;
I ';' J = Directed I +* ProgramPart Relocated(J,card I)
by SCMFSA6A:def 4;
then ProgramPart Relocated(J,card I) c= I ';' J by FUNCT_4:26;
then ProgramPart Relocated(J,card I) c= s by A26,XBOOLE_1:1;
then A27: ProgramPart Relocated(J,card I) c= s4 by AMI_3:38;
take m;
IncAddr(CurInstr (Computation s3).m3,card I)
= CurInstr (Computation s4).m3 by A23,A24,A25,A27,Th27;
then IncAddr(CurInstr (Computation s3).m3,card I)
= CurInstr (Computation s).(m1 + 1 + m3) by AMI_1:51;
hence CurInstr((Computation s).m)
= IncAddr (halt SCM+FSA,card I) by A17,SCM_1:def 2
.= halt SCM+FSA by SCMFSA_4:8;
end;
end;
theorem Th41:
for I being keeping_0 Macro-Instruction
st not s +* (I +* Start-At insloc 0) is halting
for J being Macro-Instruction, k being Nat
holds (Computation (s +* (I +* Start-At insloc 0))).k,
(Computation (s +* ((I ';' J) +* Start-At insloc 0))).k
equal_outside the Instruction-Locations of SCM+FSA
proof
let I be keeping_0 Macro-Instruction; assume
A1: not s +* (I +* Start-At insloc 0) is halting;
let J be Macro-Instruction;
set s1 = s +* (I +* Start-At insloc 0);
A2: I +* Start-At insloc 0 c= s1 by FUNCT_4:26;
set s2 = s +* ((I ';' J) +* Start-At insloc 0);
A3: (I ';' J) +* Start-At insloc 0 c= s2 by FUNCT_4:26;
A4: s1 = s +* I +* SA0 by FUNCT_4:15 .= s+*SA0+*I by Th14;
A5: s2 = s +* (I ';' J) +* SA0 by FUNCT_4:15
.= s+*SA0+*(I ';' J) by Th14;
s+*SA0, s+*SA0+*I
equal_outside the Instruction-Locations of SCM+FSA by SCMFSA6A:27;
then A6: s+*SA0+*I, s+*SA0
equal_outside the Instruction-Locations of SCM+FSA by FUNCT_7:28;
defpred X[Nat] means(Computation s1).$1,(Computation(s2)).$1
equal_outside the Instruction-Locations of SCM+FSA;
A7: s+*SA0, s+*SA0+*(I ';' J)
equal_outside the Instruction-Locations of SCM+FSA by SCMFSA6A:27;
(Computation s1).0 = s1 & (Computation(s2)).0 = s2 by AMI_1:def 19;
then A8: X[0] by A4,A5,A6,A7,FUNCT_7:29;
A9: for m st X[m] holds X[m+1]
proof let m; assume
A10: (Computation s1).m,(Computation(s2)).m
equal_outside the Instruction-Locations of SCM+FSA;
set Cs = Computation s1, CsIJ = Computation s2;
A11: Cs.(m+1) = Following Cs.m by AMI_1:def 19
.= Exec(CurInstr Cs.m,Cs.m) by AMI_1:def 18;
A12: CsIJ.(m+1) = Following CsIJ.m by AMI_1:def 19
.= Exec(CurInstr CsIJ.m,CsIJ.m) by AMI_1:def 18;
A13: IC(Cs.m) = IC(CsIJ.m) by A10,SCMFSA6A:29;
A14: IC Cs.m in dom I by A2,Def2;
dom I misses dom Start-At insloc 0 by SF_MASTR:64;
then I c= I +* Start-At insloc 0 by FUNCT_4:33;
then I c= s1 by A2,XBOOLE_1:1;
then A15: I c= Cs.m by AMI_3:38;
dom (I ';' J) misses dom SA0 by SF_MASTR:64;
then (I ';' J) c= (I ';' J)+*SA0 by FUNCT_4:33;
then (I ';' J) c= s2 by A3,XBOOLE_1:1;
then A16: I ';' J c= CsIJ.m by AMI_3:38;
dom(I ';' J)
= dom(Directed I +* ProgramPart Relocated(J, card I)) by SCMFSA6A:def 4
.= dom Directed I \/ dom ProgramPart Relocated(J, card I) by FUNCT_4:def 1
.= dom I \/ dom ProgramPart Relocated(J, card I) by SCMFSA6A:14;
then A17: dom I c= dom(I ';' J) by XBOOLE_1:7;
A18: CurInstr(Cs.m) = (Cs.m).IC(Cs.m) by AMI_1:def 17
.= I.IC(Cs.m) by A14,A15,GRFUNC_1:8;
then I.IC(Cs.m) <> halt SCM+FSA by A1,AMI_1:def 20;
then CurInstr(Cs.m) = (I ';' J).IC(Cs.m) by A14,A18,SCMFSA6A:54
.= (CsIJ.m).IC(Cs.m) by A14,A16,A17,GRFUNC_1:8
.= CurInstr(CsIJ.m) by A13,AMI_1:def 17;
hence (Computation s1).(m+1),(Computation(s2)).(m+1)
equal_outside the Instruction-Locations of SCM+FSA by A10,A11,A12,
SCMFSA6A:32;
end;
thus for k being Nat holds X[k] from Ind(A8, A9);
end;
theorem Th42:
for I being keeping_0 Macro-Instruction
st s +* I is halting
for J being paraclosed Macro-Instruction
st (I ';' J) +* Start-At insloc 0 c= s
for k being Nat
holds (Computation (Result(s +*I)
+* (J +* Start-At insloc 0))).k
+* Start-At (IC (Computation ((Result(s +*I))
+* (J +* Start-At insloc 0))).k + card I),
(Computation (s +* (I ';' J))).
(LifeSpan (s +* I)+1+k)
equal_outside the Instruction-Locations of SCM+FSA
proof
let I be keeping_0 Macro-Instruction; assume
A1: s +* I is halting;
let J be paraclosed Macro-Instruction; assume
A2: (I ';' J) +* SA0 c= s;
set ISA0 = I +* Start-At insloc 0;
set sISA0 = s +* ISA0;
set RI = Result(s +* ISA0);
set JSA0 = (J +* Start-At insloc 0);
set RIJ = RI +* JSA0;
set sIJSA0 = s +* ((I ';' J) +* Start-At insloc 0);
A3: s = sIJSA0 by A2,AMI_5:10;
A4: I ';' J = Directed I +* ProgramPart Relocated(J, card I) by SCMFSA6A:def 4;
A5: Directed I c= I ';' J by SCMFSA6A:55;
A6: sIJSA0 = s +*(I ';' J) +* Start-At insloc 0 by FUNCT_4:15;
then sIJSA0 = s +*Start-At insloc 0 +*(I ';' J) by Th14;
then A7: (I ';' J) c= s by A3,FUNCT_4:26;
then A8: Directed I c= s by A5,XBOOLE_1:1;
A9: SA0 c= s by A3,A6,FUNCT_4:26;
A10: sISA0 = s +*I +* Start-At insloc 0 by FUNCT_4:15
.= s +* Start-At insloc 0 +*I by Th14
.= s +* I by A9,AMI_5:10;
A11: sIJSA0 = s +*(I ';' J) +* Start-At insloc 0 by FUNCT_4:15
.= s +* Start-At insloc 0 +*(I ';' J) by Th14
.= s +* (I ';' J) by A9,AMI_5:10;
A12: now
set s1 = RIJ +* Start-At (IC RIJ + card I);
set s2 = (Computation sIJSA0).(LifeSpan sISA0+1+0);
thus IC s1 = IC RIJ + card I by AMI_5:79
.= IC (RI +* J +* SA0) + card I by FUNCT_4:15
.= insloc 0 + card I by AMI_5:79
.= insloc (0+card I) by SCMFSA_4:def 1
.= IC s2 by A1,A3,A8,A9,A10,Th37;
A13:(Computation sISA0).(LifeSpan sISA0), (Computation sIJSA0).(LifeSpan sISA0)
equal_outside the Instruction-Locations of SCM+FSA
by A1,A10,Th40;
A14: (Computation s).(LifeSpan sISA0) | (Int-Locations \/ FinSeq-Locations) =
(Computation s).(LifeSpan sISA0+1) | (Int-Locations \/ FinSeq-Locations)
by A1,A8,A9,A10,Th38;
hereby let a be Int-Location;
A15: not a in dom JSA0 by Th12;
not a in dom Start-At (IC RIJ + card I) by Th9;
hence s1.a = RIJ.a by FUNCT_4:12
.= RI.a by A15,FUNCT_4:12
.= (Computation sISA0).(LifeSpan sISA0).a by A1,A10,Th16
.= (Computation sIJSA0).(LifeSpan sISA0).a by A13,SCMFSA6A:30
.= s2.a by A3,A14,SCMFSA6A:38;
end;
let f be FinSeq-Location;
A16: not f in dom JSA0 by Th13;
not f in dom Start-At (IC RIJ + card I) by Th10;
hence s1.f = RIJ.f by FUNCT_4:12
.= RI.f by A16,FUNCT_4:12
.= (Computation sISA0).(LifeSpan sISA0).f by A1,A10,Th16
.= (Computation sIJSA0).(LifeSpan sISA0).f by A13,SCMFSA6A:31
.= s2.f by A3,A14,SCMFSA6A:38;
end;
defpred X[Nat] means
(Computation RIJ).$1 +* Start-At (IC (Computation RIJ).$1 + card I),
(Computation sIJSA0).(LifeSpan sISA0+1+$1)
equal_outside the Instruction-Locations of SCM+FSA;
(Computation RIJ).0 = RIJ by AMI_1:def 19;
then A17: X[0] by A12,SCMFSA6A:28;
A18: for n being Nat st X[n] holds X[n+1]
proof let k be Nat; assume
A19: (Computation RIJ).k +* Start-At (IC (Computation RIJ).k + card I),
(Computation sIJSA0).(LifeSpan sISA0+1+k)
equal_outside the Instruction-Locations of SCM+FSA;
set k1 = k+1;
set CRk = (Computation RIJ).k;
set CRSk = CRk +* Start-At (IC CRk + card I);
set CIJk = (Computation sIJSA0).(LifeSpan sISA0+1+k);
set CRk1 = (Computation RIJ).k1;
set CRSk1 = CRk1 +* Start-At (IC CRk1 + card I);
set CIJk1 = (Computation sIJSA0).(LifeSpan sISA0+1+k1);
A20: IncAddr(CurInstr CRk, card I) = CurInstr CIJk proof
A21: now thus CurInstr CIJk = CIJk.IC CIJk by AMI_1:def 17
.= CIJk.IC CRSk by A19,SCMFSA6A:29
.= CIJk.(IC CRk + card I) by AMI_5:79;
end;
JSA0 c= RIJ by FUNCT_4:26;
then A22: IC CRk in dom J by Def2;
then A23: IC CRk in dom IncAddr(J, card I) by SCMFSA_4:def 6;
then A24: Shift(IncAddr(J, card I), card I).(IC CRk + card I)
= IncAddr(J, card I).IC CRk by SCMFSA_4:30
.= IncAddr(pi(J, IC CRk), card I) by A22,SCMFSA_4:24;
ProgramPart Relocated(J, card I) c= I ';' J by A4,FUNCT_4:26;
then A25: ProgramPart Relocated(J, card I) c= sIJSA0 by A3,A7,XBOOLE_1:1;
A26: now thus ProgramPart Relocated(J, card I)
= IncAddr(Shift(ProgramPart(J), card I), card I) by SCMFSA_5:2
.= IncAddr(Shift(J, card I), card I) by AMI_5:72
.= Shift(IncAddr(J, card I), card I) by SCMFSA_4:35;
end;
dom Shift(IncAddr(J, card I), card I) =
{ il+card I where il is Instruction-Location of SCM+FSA:
il in dom IncAddr(J, card I)} by SCMFSA_4:31;
then A27: IC CRk + card I in dom Shift(IncAddr(J, card I), card I) by A23;
A28: now RIJ = RI +* J +* Start-At insloc 0 by FUNCT_4:15
.= RI +* Start-At insloc 0 +* J by Th14;
then J c= RIJ by FUNCT_4:26;
hence J c= CRk by AMI_3:38;
end;
pi(J, IC CRk) = J.IC CRk by A22,AMI_5:def 5
.= CRk.IC CRk by A22,A28,GRFUNC_1:8;
hence IncAddr(CurInstr CRk, card I)
= IncAddr(pi(J, IC CRk), card I) by AMI_1:def 17
.= sIJSA0.(IC CRk + card I) by A24,A25,A26,A27,GRFUNC_1:8
.= CurInstr CIJk by A21,AMI_1:54;
end;
A29: now CIJk1 =(Computation sIJSA0).(LifeSpan sISA0+1+k+1) by XCMPLX_1:1;
then CIJk1 = Following CIJk by AMI_1:def 19;
hence CIJk1 = Exec(CurInstr CIJk, CIJk) by AMI_1:def 18;
end;
CIJk, CRSk equal_outside the Instruction-Locations of SCM+FSA
by A19,FUNCT_7:28;
then Exec(CurInstr CIJk, CIJk),
Exec(IncAddr(CurInstr CRk,card I), CRSk)
equal_outside the Instruction-Locations of SCM+FSA
by A20,SCMFSA6A:32;
then A30: Exec(CurInstr CIJk, CIJk),
Following(CRk) +* Start-At (IC Following(CRk) + card I)
equal_outside the Instruction-Locations of SCM+FSA by SCMFSA_4:28;
A31: now
IC CRSk1 = IC CRk1 + card I by AMI_5:79
.= IC Following CRk + card I by AMI_1:def 19;
hence IC CRSk1 =
IC (Following(CRk) +* Start-At (IC Following(CRk) + card I))
by AMI_5:79
.= IC CIJk1 by A29,A30,SCMFSA6A:29;
end;
A32: now let a be Int-Location;
thus CRSk1.a = CRk1.a by SCMFSA_3:11
.= (Following CRk).a by AMI_1:def 19
.= (Following(CRk) +* Start-At (IC Following(CRk) + card I)).a
by SCMFSA_3:11
.= CIJk1.a by A29,A30,SCMFSA6A:30;
end;
now let f be FinSeq-Location;
thus CRSk1.f = CRk1.f by SCMFSA_3:12
.= (Following CRk).f by AMI_1:def 19
.= (Following(CRk) +* Start-At (IC Following(CRk) + card I)).f
by SCMFSA_3:12
.= CIJk1.f by A29,A30,SCMFSA6A:31;
end;
hence (Computation RIJ).k1 +* Start-At (IC (Computation RIJ).k1 + card I),
(Computation sIJSA0).(LifeSpan sISA0+1+k1)
equal_outside the Instruction-Locations of SCM+FSA by A31,A32,SCMFSA6A:28;
end;
for k being Nat holds X[k] from Ind(A17, A18);
hence for k being Nat
holds (Computation (Result(s +*I)
+* (J +* Start-At insloc 0))).k
+* Start-At (IC (Computation ((Result(s +*I))
+* (J +* Start-At insloc 0))).k + card I),
(Computation (s +* (I ';' J))).
(LifeSpan (s +* I)+1+k)
equal_outside the Instruction-Locations of SCM+FSA by A10,A11;
end;
definition
let I, J be keeping_0 Macro-Instruction;
cluster I ';' J -> keeping_0;
coherence
proof set SA0 = Start-At insloc 0;
let s be State of SCM+FSA; assume
A1: (I ';' J) +* SA0 c= s;
then A2: s +* ((I ';' J) +* SA0) = s by AMI_5:10;
SA0 c= (I ';' J) +* SA0 by FUNCT_4:26;
then A3: SA0 c= s by A1,XBOOLE_1:1;
A4: s +*((I ';' J) +* Start-At insloc 0)
= s +*(I ';' J) +* Start-At insloc 0 by FUNCT_4:15
.= s +* Start-At insloc 0 +*(I ';' J) by Th14
.= s +* (I ';' J) by A3,AMI_5:10;
A5: I +* SA0 c= s +* (I +* SA0) by FUNCT_4:26;
dom SA0 = {IC SCM+FSA} & intloc 0 <> IC SCM+FSA by AMI_3:34,SCMFSA_2:81;
then not intloc 0 in dom I & not intloc 0 in dom SA0
by SCMFSA6A:47,TARSKI:def 1;
then not intloc 0 in dom I \/ dom SA0 by XBOOLE_0:def 2;
then A6: not intloc 0 in dom (I +* SA0) by FUNCT_4:def 1;
per cases;
suppose A7: s +* (I +* SA0) is halting;
A8: s +* (I +* SA0) = s +*I +* SA0 by FUNCT_4:15
.= s +* SA0 +* I by Th14
.= s +* I by A3,AMI_5:10;
let k be Nat;
hereby
per cases;
suppose A9: k <= LifeSpan(s +* (I +* SA0));
A10: (Computation (s +* (I +* SA0))).k.intloc 0
= (s +* (I +* SA0)).intloc 0 by A5,Def4
.= s.intloc 0 by A6,FUNCT_4:12;
(Computation (s +* (I +* Start-At insloc 0))).k,
(Computation (s +* ((I ';' J) +* Start-At insloc 0))).k
equal_outside the Instruction-Locations of SCM+FSA by A7,A9,Th40
;
hence ((Computation s).k).intloc 0 = s.intloc 0 by A2,A10,SCMFSA6A:30;
suppose A11: k > LifeSpan(s +* (I +* SA0));
set LS = LifeSpan(s +* (I +* SA0));
consider p being Nat such that
A12: k = LS + p & 1 <= p by A11,FSM_1:1;
consider r being Nat such that
A13: p = 1 + r by A12,NAT_1:28;
A14: k = LS + 1 + r by A12,A13,XCMPLX_1:1;
dom SA0 = {IC SCM+FSA} & intloc 0 <> IC SCM+FSA
by AMI_3:34,SCMFSA_2:81;
then not intloc 0 in dom J & not intloc 0 in dom SA0
by SCMFSA6A:47,TARSKI:def 1;
then not intloc 0 in dom J \/ dom SA0 by XBOOLE_0:def 2;
then A15: not intloc 0 in dom (J +* SA0) by FUNCT_4:def 1;
J +* SA0 c= Result(s +*(I+*SA0)) +* (J +* SA0) by FUNCT_4:26;
then A16: (Computation (Result(s +*(I+*SA0)) +* (J +* SA0))).r.intloc 0
= (Result(s +*(I+*SA0)) +* (J +* SA0)).intloc 0 by Def4
.= (Result(s +*(I+*SA0))).intloc 0 by A15,FUNCT_4:12
.= (Computation(s +*(I+*SA0))).(LifeSpan (s +*(I+*SA0)))
.intloc 0 by A7,Th16
.= (s +*(I+*SA0)).intloc 0 by A5,Def4
.= s.intloc 0 by A6,FUNCT_4:12;
set Rr = (Computation (Result(s +*(I+*SA0)) +* (J +* SA0))).r;
set Sr = Start-At (IC ((Computation (Result(s +*(I+*SA0))
+* (J +* SA0)))).r + card I);
dom Sr = {IC SCM+FSA} & intloc 0 <> IC SCM+FSA
by AMI_3:34,SCMFSA_2:81;
then not intloc 0 in dom Sr by TARSKI:def 1;
then A17: (Rr +* Sr).intloc 0 = Rr.intloc 0 by FUNCT_4:12;
Rr +* Sr,
(Computation (s +* ((I ';' J) +* Start-At insloc 0))).(LS+1+r)
equal_outside the Instruction-Locations of SCM+FSA
by A1,A4,A7,A8,Th42;
hence ((Computation s).k).intloc 0 = s.intloc 0 by A2,A14,A16,A17,SCMFSA6A:
30;
end;
suppose A18: not s +* (I +* SA0) is halting;
let k be Nat;
I +* SA0 c= s +* (I +* SA0) by FUNCT_4:26;
then A19: (Computation (s +* (I +* SA0))).k.intloc 0
= (s +* (I +* SA0)).intloc 0 by Def4
.= s.intloc 0 by A6,FUNCT_4:12;
(Computation (s +* (I +* SA0))).k,
(Computation (s +* ((I ';' J) +* SA0))).k
equal_outside the Instruction-Locations of SCM+FSA by A18,Th41;
hence ((Computation s).k).intloc 0 = s.intloc 0 by A2,A19,SCMFSA6A:30;
end;
end;
theorem Th43: ::T22
for I being keeping_0 parahalting Macro-Instruction,
J being parahalting Macro-Instruction
holds
LifeSpan (s +* Initialized (I ';' J))
= LifeSpan (s +* Initialized I) + 1
+ LifeSpan (Result (s +* Initialized I) +* Initialized J)
proof
let I be keeping_0 parahalting Macro-Instruction;
let J be parahalting Macro-Instruction;
A1: Initialized (I ';' J) c= s +* Initialized (I ';' J) by FUNCT_4:26;
then A2: LifeSpan (s +* Initialized (I ';' J))
= LifeSpan (s +* Initialized (I ';' J) +* I) + 1
+ LifeSpan (Result (s +* Initialized (I ';' J) +* I) +* Initialized J)
by Lm3;
Initialized I c= s +* Initialized I by FUNCT_4:26;
then A3: I +* SA0 c= s +* Initialized I by Th8;
Initialized I c= s +* Initialized (I ';' J) +* I by A1,SCMFSA6A:52;
then A4:I +* SA0 c= s +* Initialized (I ';' J) +* I by Th8;
A5: s +* Initialized (I ';' J), s +* Initialized (I ';' J) +* I equal_outside
the Instruction-Locations of SCM+FSA by SCMFSA6A:27;
s +* Initialized I, s +* Initialized (I ';' J) equal_outside
the Instruction-Locations of SCM+FSA by SCMFSA6A:53;
then s +* Initialized I, s +* Initialized (I ';' J) +* I
equal_outside the Instruction-Locations of SCM+FSA by A5,FUNCT_7:29;
then A6: LifeSpan (s +* Initialized I)
= LifeSpan (s +* Initialized (I ';' J) +* I) &
Result (s +* Initialized I), Result (s +* Initialized (I ';' J) +* I)
equal_outside the Instruction-Locations of SCM+FSA by A3,A4,Th29;
then A7: Result (s +* Initialized (I ';' J) +* I), Result (s +* Initialized I)
equal_outside the Instruction-Locations of SCM+FSA by FUNCT_7:28;
Initialized J c= Result (s +* Initialized (I ';' J) +* I) +* Initialized J
by FUNCT_4:26;
then A8: J +* SA0 c= Result (s +* Initialized (I ';' J) +* I) +* Initialized J
by Th8;
Initialized J c= Result (s +* Initialized I) +* Initialized J
by FUNCT_4:26;
then A9: J +* SA0 c= Result (s +* Initialized I) +* Initialized J
by Th8;
Result (s +* Initialized (I ';' J) +* I) +* Initialized J,
Result (s +* Initialized I) +* Initialized J
equal_outside the Instruction-Locations of SCM+FSA by A7,SCMFSA6A:11;
hence LifeSpan (s +* Initialized (I ';' J))
= LifeSpan (s +* Initialized I) + 1
+ LifeSpan (Result (s +* Initialized I) +* Initialized J)
by A2,A6,A8,A9,Th29;
end;
theorem
for I being keeping_0 parahalting Macro-Instruction,
J being parahalting Macro-Instruction
holds
IExec(I ';' J,s) =
IExec(J,IExec(I,s)) +* Start-At (IC IExec(J,IExec(I,s)) + card I)
proof
let I be keeping_0 parahalting Macro-Instruction;
let J be parahalting Macro-Instruction;
set ps = s | the Instruction-Locations of SCM+FSA;
set s1 = s +* Initialized I;
set s2 = s +* Initialized (I ';' J);
set s3 = (Computation s1).(LifeSpan s1) +* Initialized J;
set m1 = LifeSpan s1;
set m3 = LifeSpan s3;
set A = the Instruction-Locations of SCM+FSA;
set D = (Int-Locations \/ FinSeq-Locations);
set C1 = Computation s1;
set C2 = Computation s2;
set C3 = Computation s3;
A1: Initialized I c= s1 by FUNCT_4:26;
then A2: s1 is halting by Th19;
A3: I +* Start-At insloc 0 c= s1 by A1,Th8;
A4: Initialized (I ';' J) c= s2 by FUNCT_4:26;
then A5: s2 is halting by Th19;
SA0 c= Initialized (I ';' J) & Initialized (I ';' J) c= s2
by Th4,FUNCT_4:26;
then A6: SA0 c= s2 by XBOOLE_1:1;
I +* SA0 c= s2 +*(I +* SA0) by FUNCT_4:26;
then I +* SA0 c= s2 +*I +* SA0 by FUNCT_4:15;
then I +* SA0 c= s2 +* SA0 +*I by Th14;
then I +* SA0 c= s2 +*I by A6,AMI_5:10;
then A7: s2 +* I is halting by Th18;
Initialized J c= s3 by FUNCT_4:26;
then A8: s3 is halting by Th19;
A9: dom ps = dom s /\ A by RELAT_1:90
.= (Int-Locations \/ FinSeq-Locations \/ {IC SCM+FSA} \/ A) /\
A by SCMFSA6A:34
.= A by XBOOLE_1:21;
C1.m1, C1.m1 +* ps equal_outside dom ps by FUNCT_7:31;
then A10: C1.m1 +* Initialized J, C1.m1 +* ps +* Initialized J
equal_outside dom ps by SCMFSA6A:11;
then A11: C1.m1 +* ps +* Initialized J, C1.m1 +* Initialized J
equal_outside dom ps by FUNCT_7:28;
Result (IExec(I,s) +* Initialized J), Result s3 equal_outside A
proof
Initialized J c= IExec(I,s) +* Initialized J by FUNCT_4:26;
then A12: J +* SA0 c= IExec(I,s) +* Initialized J by Th8;
Initialized J c= s3 by FUNCT_4:26;
then A13: J +* SA0 c= s3 by Th8;
IExec(I,s) = Result (s +* Initialized I) +* ps by Def1
.= C1.m1 +* ps by A2,Th16;
hence thesis by A9,A11,A12,A13,Th29;
end;
then A14: Result (IExec(I,s) +* Initialized J) +* ps = Result s3 +* ps
by A9,SCMFSA6A:13;
A15: s3 = Result s1 +* Initialized J by A2,Th16;
A16: IExec(I ';' J,s)
= Result (s +* Initialized (I ';' J)) +* ps by Def1
.= C2.LifeSpan s2 +* ps by A5,Th16
.= C2.(m1 + 1 + m3) +* ps by A15,Th43;
IExec(I,s) | A = (Result (s +* Initialized I) +* ps) | A by Def1
.= ps by SCMFSA6A:40;
then A17: IExec(J,IExec(I,s))
= Result (IExec(I,s) +* Initialized J) +* ps by Def1
.= C3.m3 +* ps by A8,A14,Th16;
Initialized I c= s2 +* I by A4,SCMFSA6A:52;
then A18: I +* Start-At insloc 0 c= s2 +* I by Th8;
A19: s1,s2 equal_outside A by SCMFSA6A:53;
s2,s2 +* I equal_outside A by SCMFSA6A:27;
then s1,s2 +* I equal_outside A by A19,FUNCT_7:29;
then A20: LifeSpan (s2 +* I) = m1 by A3,A18,Th29;
then A21: IC C2.(m1 + 1) = insloc card I &
C2.(m1 + 1) | D
= ((Computation (s2 +* I)).m1 +* Initialized J) | D &
ProgramPart Relocated(J,card I) c= C2.(m1 + 1) &
C2.(m1 + 1).intloc 0 = 1 by A4,Lm3;
A22: (Computation C2.(m1 + 1)).m3 | D = C3.m3 | D &
IC (Computation C2.(m1 + 1)).m3 = IC C3.m3 + card I
proof
Initialized J c= s3 by FUNCT_4:26;
then A23: J +* Start-At insloc 0 c= s3 by Th8;
A24: I ';' J c= Initialized (I ';' J) by SCMFSA6A:26;
s1 +* (I ';' J) = s +* (Initialized I +* (I ';' J)) by FUNCT_4:15
.= s2 by SCMFSA6A:58;
then A25: (Computation s1).m1, (Computation s2).m1 equal_outside A
by A2,A3,Th36;
(Computation (s2 +* I)).m1, (Computation ((s2 +* I) +* (I ';' J))).m1
equal_outside A by A7,A18,A20,Th36;
then (Computation (s2 +* I)).m1 | D
= (Computation ((s2 +* I) +* (I ';' J))).m1 | D by SCMFSA6A:39
.= (Computation ((s2 +* (I +* (I ';' J))))).m1 | D by FUNCT_4:15
.= (Computation (s2 +* (I ';' J))).m1 | D by SCMFSA6A:57
.= (Computation (s +* (Initialized (I ';' J) +* (I ';' J)))).m1 | D
by FUNCT_4:15
.= (Computation s2).m1 | D by A24,LATTICE2:8
.= (Computation s1).m1 | D by A25,SCMFSA6A:39;
then ((Computation (s2 +* I)).m1 +* Initialized J) | D
=(Computation s1).m1 | D +* (Initialized J) | D by AMI_5:6
.= ((Computation s1).m1 +* Initialized J) | D by AMI_5:6;
hence thesis by A21,A23,Th27;
end;
A26: IExec(I ';' J,s) | D = IExec(J,IExec(I,s)) | D
proof
A27: dom ps misses D by A9,SCMFSA_2:13,14,XBOOLE_1:70;
hence IExec(I ';' J,s) | D
= C2.(m1 + 1 + m3) | D by A16,AMI_5:7
.= C3.m3 | D by A22,AMI_1:51
.= IExec(J,IExec(I,s)) | D by A17,A27,AMI_5:7;
end;
A28: IExec(I,s) = Result s1 +* ps by Def1;
A29: Result s1 = C1.m1 by A2,Th16;
Initialized J c= Result s1 +* Initialized J by FUNCT_4:26;
then A30: J +* SA0 c= Result s1 +* Initialized J by Th8;
Initialized J c= IExec(I,s) +* Initialized J by FUNCT_4:26;
then J +* SA0 c= IExec(I,s) +* Initialized J by Th8;
then Result (Result s1 +* Initialized J), Result (IExec(I,s) +* Initialized
J)
equal_outside A by A9,A10,A28,A29,A30,Th29;
then A31: IC Result (Result s1 +* Initialized J)
= IC Result (IExec(I,s) +* Initialized J) by SCMFSA6A:29;
A32: IC IExec(I ';' J,s) = IC Result (s +* Initialized (I ';' J)) by Th30
.= IC C2.LifeSpan s2 by A5,Th16
.= IC C2.(m1 + 1 + m3) by A15,Th43
.= IC C3.m3 + card I by A22,AMI_1:51
.= IC Result s3 + card I by A8,Th16
.= IC Result (Result s1 +* Initialized J) + card I by A2,Th16
.= IC IExec(J,IExec(I,s)) + card I by A31,Th30;
hereby
A33: dom IExec(I ';' J,s) = the carrier of SCM+FSA by AMI_3:36
.= dom (IExec(J,IExec(I,s)) +* Start-At (IC IExec(J,IExec(I,s)) + card I))
by AMI_3:36;
reconsider l = IC IExec(J,IExec(I,s)) + card I
as Instruction-Location of SCM+FSA;
A34: dom Start-At l = {IC SCM+FSA} by AMI_3:34;
now let x be set;
assume A35: x in dom IExec(I ';' J,s);
per cases by A35,SCMFSA6A:35;
suppose A36: x is Int-Location;
then A37: IExec(I ';' J,s).x = IExec(J,IExec(I,s)).x by A26,SCMFSA6A:38;
x <> IC SCM+FSA by A36,SCMFSA_2:81;
then not x in dom Start-At l by A34,TARSKI:def 1;
hence IExec(I ';' J,s).x
= (IExec(J,IExec(I,s)) +* Start-At (IC IExec(J,IExec(I,s)) + card I)).x
by A37,FUNCT_4:12;
suppose A38: x is FinSeq-Location;
then A39: IExec(I ';' J,s).x = IExec(J,IExec(I,s)).x by A26,SCMFSA6A:38;
x <> IC SCM+FSA by A38,SCMFSA_2:82;
then not x in dom Start-At l by A34,TARSKI:def 1;
hence IExec(I ';' J,s).x
= (IExec(J,IExec(I,s)) +* Start-At (IC IExec(J,IExec(I,s)) + card I)).x
by A39,FUNCT_4:12;
suppose A40: x = IC SCM+FSA;
then x in {IC SCM+FSA} by TARSKI:def 1;
then A41: x in dom Start-At l by AMI_3:34;
thus IExec(I ';' J,s).x
= l by A32,A40,AMI_1:def 15
.= (Start-At l).IC SCM+FSA by AMI_3:50
.= (IExec(J,IExec(I,s)) +* Start-At (IC IExec(J,IExec(I,s)) + card I)).x
by A40,A41,FUNCT_4:14;
suppose A42: x is Instruction-Location of SCM+FSA;
IExec(I ';' J,s) | A = ps by A16,SCMFSA6A:40
.= IExec(J,IExec(I,s)) | A by A17,SCMFSA6A:40;
then A43: IExec(I ';' J,s).x = IExec(J,IExec(I,s)).x by A42,SCMFSA6A:36;
x <> IC SCM+FSA by A42,AMI_1:48;
then not x in dom Start-At l by A34,TARSKI:def 1;
hence IExec(I ';' J,s).x
= (IExec(J,IExec(I,s)) +* Start-At (IC IExec(J,IExec(I,s)) + card I)).x
by A43,FUNCT_4:12;
end;
hence thesis by A33,FUNCT_1:9;
end;
end;