:: Composition of Machines, Instructions and Programs
:: by Andrzej Trybulec
::
:: Received May 20, 2010
:: Copyright (c) 2010-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies SUBSET_1, XBOOLE_0, FUNCT_1, NUMBERS, CARD_1, FUNCOP_1, FUNCT_4,
RELAT_1, TARSKI, CAT_1, FINSET_1, NAT_1, AFINSQ_1, AMISTD_1, AMISTD_2,
ARYTM_1, VALUED_1, PARTFUN1, ZFMISC_1, AMI_1, ARYTM_3, EXTPRO_1, PBOOLE,
COMPOS_1, RELOC, TURING_1, XXREAL_0, SCMFSA_7, INT_1, SCMPDS_4, ORDINAL4,
SCMFSA6A, FINSEQ_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, MCART_1, SUBSET_1, SETFAM_1,
ORDINAL1, PBOOLE, FUNCT_7, CARD_1, CARD_3, XXREAL_0, XCMPLX_0, RELAT_1,
FUNCT_1, PARTFUN1, FINSET_1, NUMBERS, INT_1, NAT_1, NAT_D, FUNCOP_1,
FUNCT_4, FINSEQ_1, FUNCT_2, DOMAIN_1, VALUED_0, VALUED_1, AFINSQ_1,
STRUCT_0, COMPOS_0;
constructors SETFAM_1, DOMAIN_1, FUNCT_4, XXREAL_0, RELSET_1, FUNCT_7,
PRE_POLY, PBOOLE, AFINSQ_1, NAT_D, WELLORD2, STRUCT_0, COMPOS_0,
XTUPLE_0;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, FUNCOP_1,
FUNCT_4, FINSET_1, XREAL_0, RELSET_1, PBOOLE, AFINSQ_1, VALUED_1,
XCMPLX_0, NAT_1, MEMBERED, CARD_1, XXREAL_0, ORDINAL5, COMPOS_0,
XTUPLE_0;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
definitions TARSKI, XBOOLE_0, AFINSQ_1;
equalities FUNCOP_1, AFINSQ_1, VALUED_1, COMPOS_0, XTUPLE_0;
expansions TARSKI, XBOOLE_0;
theorems ZFMISC_1, FUNCT_2, TARSKI, FUNCT_4, FUNCOP_1, FINSET_1, FUNCT_1,
GRFUNC_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, ORDINAL1, MCART_1,
PARTFUN1, CARD_1, AFINSQ_1, XREAL_1, VALUED_1, CARD_2, PRE_CIRC, XREAL_0,
NAT_1, XXREAL_0, NAT_D, INT_1, WELLORD2, ENUMSET1, AFINSQ_2, COMPOS_0;
schemes FRAENKEL, CLASSES1, FUNCT_7, DOMAIN_1;
begin :: General concepts
reserve x,A for set, i,j,k,m,n, l, l1, l2 for Nat;
reserve D for non empty set, z for Nat;
definition
struct COM-Struct(#
InstructionsF -> Instructions
#);
end;
definition
::$CD 7
func Trivial-COM -> strict COM-Struct means
:Def1:
the InstructionsF of it = {[0,{},{}]};
existence
proof
take S=COM-Struct(#{[0,{},{}]} #);
thus thesis;
end;
uniqueness;
end;
definition
let S be COM-Struct;
mode Instruction of S is Element of the InstructionsF of S;
end;
definition
::$CD
let S be COM-Struct;
func halt S -> Instruction of S equals
halt the InstructionsF of S;
coherence;
end;
:: Definicje musi zachowac, zeby nie musiec pisac
:: halt SCM-Instr, zamiast halt SCM, zreszta wyrzucenie jej
:: spowodowaloby problemy z typowaniem.
definition
let S be COM-Struct;
let I be (the InstructionsF of S)-valued Function;
attr I is halt-free means
:Def3: not halt S in rng I;
end;
begin :: General theory
reserve S for COM-Struct;
reserve ins for Element of the InstructionsF of S;
definition
let S be COM-Struct;
mode Instruction-Sequence of S is
(the InstructionsF of S)-valued ManySortedSet of NAT;
end;
definition
let S be COM-Struct;
let P be Instruction-Sequence of S, k be Nat;
redefine func P.k -> Instruction of S; :: redefines . (FUNCT_1, definition)
coherence
proof
A1: k in NAT by ORDINAL1:def 12;
dom P = NAT by PARTFUN1:def 2;
then
A2: P.k in rng P by A1,FUNCT_1:3;
rng P c= the InstructionsF of S by RELAT_1:def 19;
hence P.k is Instruction of S by A2;
end;
end;
begin
definition
let S be (COM-Struct);
let p be NAT-defined (the InstructionsF of S)-valued Function, l be set;
pred p halts_at l means
l in dom p & p.l = halt S;
end;
definition
let S be COM-Struct;
let s be Instruction-Sequence of S, l be Nat;
redefine pred s halts_at l means :: redefines halts_at (COMPOS_1, definition)
s.l = halt S;
compatibility
proof
thus s halts_at l implies s.l = halt S;
assume
A1: s.l = halt S;
l in NAT by ORDINAL1:def 12;
hence l in dom s by PARTFUN1:def 2;
thus s.l = halt S by A1;
end;
end;
begin :: Closedness of finite partial states
notation
let S be COM-Struct;
let i be Instruction of S;
synonym Load i for <%i%>;
end;
registration
let S;
cluster initial 1-element NAT-defined
(the InstructionsF of S)-valued for Function;
existence
proof
set p = <%the Instruction of S%>;
take p;
thus thesis;
end;
end;
definition
let S be COM-Struct;
mode preProgram of S is finite
NAT-defined (the InstructionsF of S)-valued Function;
end;
definition
let S be COM-Struct,
F be non empty preProgram of S;
attr F is halt-ending means
:Def6:
F.(LastLoc F) = halt S;
attr F is unique-halt means
:Def7:
for f being Nat st
F.f = halt S & f in dom F holds f = LastLoc F;
end;
registration
let S be COM-Struct;
cluster halt-ending -> non halt-free for non empty preProgram of S;
coherence
proof let I be non empty preProgram of S;
assume I is halt-ending;
then
A1: I.(LastLoc I) = halt S;
LastLoc I in dom I by VALUED_1:30;
hence halt S in rng I by A1,FUNCT_1:3;
end;
end;
registration
let S be COM-Struct;
cluster trivial initial non empty for preProgram of S;
existence
proof
reconsider F = <%halt S%> as initial non empty preProgram of S;
take F;
thus thesis;
end;
end;
definition
let S be COM-Struct;
mode Program of S is initial non empty preProgram of S;
end;
::$CT
theorem
for ins being Element of the InstructionsF of Trivial-COM holds
InsCode ins = 0
proof
let ins be Element of the InstructionsF of Trivial-COM;
the InstructionsF of Trivial-COM = {[0,{},{}]} by Def1;
then ins = [0,{},{}] by TARSKI:def 1;
hence thesis;
end;
begin :: Addenda
definition
let S be COM-Struct;
func Stop S -> preProgram of S equals
Load halt S;
coherence;
end;
:: registration
:: let S be COM-Struct;
:: cluster Stop S -> initial non empty;
:: coherence;
:: end;
registration
let S be COM-Struct;
cluster Stop S ->
initial non empty NAT-defined (the InstructionsF of S)-valued trivial;
coherence;
end;
Lm2: for S being COM-Struct holds card Stop S -' 1 = 0
proof let S be COM-Struct;
thus card Stop S -' 1 = card Stop S - 1 by PRE_CIRC:20
.= 1 - 1 by AFINSQ_1:34
.= 0;
end;
Lm3: for S being COM-Struct holds LastLoc Stop S = 0
proof
let S be COM-Struct;
card Stop S -' 1 = 0 by Lm2;
hence thesis by AFINSQ_1:70;
end;
registration
let S be COM-Struct;
cluster Stop S -> halt-ending unique-halt;
coherence
proof
thus (Stop S).(LastLoc Stop S) = (0 .--> halt S).0 by Lm3
.= halt S by FUNCOP_1:72;
let l be Nat such that (Stop S).l = halt S;
assume l in dom Stop S;
then l in {0};
then l = 0 by TARSKI:def 1;
hence thesis by Lm3;
end;
end;
registration let S;
cluster halt-ending unique-halt trivial for Program of S;
existence
proof
take F= Stop S;
thus thesis;
end;
end;
definition let S;
mode MacroInstruction of S is halt-ending unique-halt Program of S;
end;
registration
let S be COM-Struct;
cluster initial non empty for preProgram of S;
existence
proof
take Stop S;
thus thesis;
end;
end;
theorem Th2:
0 in dom Stop S by TARSKI:def 1;
theorem
card Stop S = 1 by AFINSQ_1:34;
reserve k, m for Nat,
x, x1, x2, x3, y, y1, y2, y3, X,Y,Z for set;
Lm4: -1 < k;
Lm5: for a, b, c being Element of NAT st 1 <= a & 2 <= b holds
k < a - 1 or a <= k & k <= a + b - 3 or k = a + b - 2 or
a + b - 2 < k or k = a - 1
proof
let a, b, c be Element of NAT such that
A1: 1 <= a and
A2: 2 <= b and
A3: a - 1 <= k and
A4: a > k or k > a + b - 3 and
A5: k <> a + b - 2 and
A6: k <= a + b - 2;
A7: a - 1 is Element of NAT by A1,INT_1:5;
now per cases by A4;
case k < a;
then k < a - 1 + 1;
hence k <= a - 1 by A7,NAT_1:13;
end;
case
A8: a + b - 3 < k;
1 + 2 <= a + b by A1,A2,XREAL_1:7;
then
A9: a + b - 3 is Element of NAT by INT_1:5;
k < a + b - 3 + 1 by A5,A6,XXREAL_0:1;
hence k <= a - 1 by A8,A9,NAT_1:13;
end;
end;
hence thesis by A3,XXREAL_0:1;
end;
begin :: Properties of AMI-Struct
theorem Th4:
for I being Instruction of Trivial-COM holds JumpPart I = 0
proof
let I be Instruction of Trivial-COM;
the InstructionsF of Trivial-COM = {[0,0,0]} by Def1;
then I = [0,0,0] by TARSKI:def 1;
hence thesis;
end;
theorem
for T being InsType of the InstructionsF of Trivial-COM
holds JumpParts T = {0}
proof
let T be InsType of the InstructionsF of Trivial-COM;
set A = { JumpPart I where I is Instruction of Trivial-COM:
InsCode I = T };
{0} = A
proof
hereby
let a be object;
assume a in {0};
then
A1: a = 0 by TARSKI:def 1;
the InstructionsF of Trivial-COM = {[0,0,0]} by Def1;
then
A2: InsCodes the InstructionsF of Trivial-COM = {0} by MCART_1:92;
A3: T = 0 by A2,TARSKI:def 1;
[0,0,0] = halt Trivial-COM;
then reconsider I = [0,0,0] as Instruction of Trivial-COM;
A4: JumpPart I = 0;
InsCode I = 0;
hence a in A by A1,A3,A4;
end;
let a be object;
assume a in A;
then ex I being Instruction of Trivial-COM st a = JumpPart I &
InsCode I = T;
then a = 0 by Th4;
hence thesis by TARSKI:def 1;
end;
hence thesis;
end;
registration
let S be COM-Struct;
cluster trivial -> unique-halt for non empty preProgram of S;
coherence
proof
let F be non empty non empty preProgram of S;
assume
A1: F is trivial;
let f be Nat such that F.f = halt S and
A2: f in dom F;
consider x being object such that
A3: F = {x} by A1,ZFMISC_1:131;
x in F by A3,TARSKI:def 1;
then consider a, b being object such that
A4: [a,b] = x by RELAT_1:def 1;
A5: LastLoc F in dom F by VALUED_1:30;
A6: dom F = {a} by A3,A4,RELAT_1:9;
hence f = a by A2,TARSKI:def 1
.= LastLoc F by A5,A6,TARSKI:def 1;
end;
end;
::$CT
theorem Th6:
for F being MacroInstruction of S st card F = 1 holds F = Stop S
proof let F be MacroInstruction of S;
assume
A1: card F = 1;
then consider x being object such that
A2: F = {x} by CARD_2:42;
x in F by A2,TARSKI:def 1;
then consider a, b being object such that
A3: [a,b] = x by RELAT_1:def 1;
A4: dom F = {a} by A2,A3,RELAT_1:9;
A5: 0 in dom F by AFINSQ_1:65;
then
A6: a = 0 by A4;
card F -' 1 = card F - 1 by PRE_CIRC:20
.= 0 by A1;
then LastLoc F = 0 by AFINSQ_1:70;
then F.0 = halt S by Def6;
then halt S in rng F by A5,FUNCT_1:def 3;
then halt S in {b} by A2,A3,RELAT_1:9;
then F = {[0,halt S]} by A2,A3,A6,TARSKI:def 1
.= 0 .--> halt S by FUNCT_4:82;
hence thesis;
end;
theorem
for S being COM-Struct holds LastLoc Stop S = 0 by Lm3;
begin :: On the composition of macro instructions
definition
::$CD 4
let S be COM-Struct, p be preProgram of S, k be Nat;
A1: dom p c= NAT by RELAT_1:def 18;
func IncAddr(p,k) ->
NAT-defined (the InstructionsF of S)-valued finite Function
means
:Def9:
dom it = dom p &
for m being Nat st m in dom p holds it.m = IncAddr(p/.m,k);
existence
proof
defpred P[object,object] means ex m being Element of NAT st $1 = m &
$2 = IncAddr(p/.m,k);
A2: for e being object st e in dom p ex u being object st P[e,u]
proof
let e be object;
assume e in dom p;
then reconsider l=e as Element of NAT by A1;
consider m being Nat such that
A3: l = m;
take IncAddr(p/.m,k);
thus thesis by A3;
end;
consider f being Function such that
A4: dom f = dom p and
A5: for e being object st e in dom p holds P[e,f.e] from CLASSES1:sch 1(A2);
A6: rng f c= the InstructionsF of S
proof let e be object;
assume e in rng f;
then consider u being object such that
A7: u in dom f and
A8: e = f.u by FUNCT_1:def 3;
P[u,f.u] by A7,A5,A4;
hence e in the InstructionsF of S by A8;
end;
reconsider f as
NAT-defined (the InstructionsF of S)-valued finite Function
by A1,A4,A6,FINSET_1:10,RELAT_1:def 18,def 19;
take f;
thus dom f = dom p by A4;
let m be Nat;
assume m in dom p;
then ex j being Element of NAT st m = j &
f.m = IncAddr(p/.j,k) by A5;
hence thesis;
end;
uniqueness
proof
let IT1,IT2 be NAT-defined (the InstructionsF of S)-valued finite Function
such that
A9: dom IT1 = dom p and
A10: for m being Nat st m in dom p holds
IT1.m = IncAddr(p/.m,k) and
A11: dom IT2 = dom p and
A12: for m being Nat st m in dom p holds
IT2.m = IncAddr(p/.m,k);
for x being object st x in dom p holds IT1.x = IT2.x
proof
let x be object;
assume
A13: x in dom p;
then reconsider l=x as Element of NAT by A1;
consider m being Nat such that
A14: l = m;
reconsider m as Element of NAT by ORDINAL1:def 12;
thus IT1.x = IncAddr(p/.m,k) by A10,A13,A14
.= IT2.x by A12,A13,A14;
end;
hence thesis by A9,A11,FUNCT_1:2;
end;
end;
registration
let S be COM-Struct, F be preProgram of S, k be Nat;
cluster IncAddr(F,k) -> NAT-defined (the InstructionsF of S)-valued;
coherence;
end;
registration
let S be COM-Struct, F be empty preProgram of S, k be Nat;
cluster IncAddr(F,k) -> empty;
coherence
proof
assume not thesis;
then reconsider f = IncAddr(F,k) as non empty Function;
A1: dom f <> {};
dom IncAddr(F,k) = dom F by Def9;
hence thesis by A1;
end;
end;
registration
let S be COM-Struct, F be non empty preProgram of S, k be Nat;
cluster IncAddr(F,k) -> non empty;
coherence
proof
dom IncAddr(F,k) = dom F by Def9;
hence thesis;
end;
end;
registration
let S be COM-Struct, F be initial preProgram of S, k be Nat;
cluster IncAddr(F,k) -> initial;
coherence
proof
dom IncAddr(F,k) = dom F by Def9;
hence thesis by AFINSQ_1:67;
end;
end;
::$CT 6
registration let S be COM-Struct, F be preProgram of S;
reduce IncAddr(F,0) to F;
reducibility
proof
for m being Nat st m in dom F holds
F.m = IncAddr(F/.m,0)
proof
let m be Nat;
assume m in dom F;
then F/.m = F.m by PARTFUN1:def 6;
hence thesis by COMPOS_0:3;
end;
hence thesis by Def9;
end;
end;
::$CT
theorem Th8:
for S being COM-Struct, F being preProgram of S
holds IncAddr(IncAddr(F,k),m) = IncAddr(F,k+m)
proof
let S be COM-Struct, F be preProgram of S;
A1: dom IncAddr(IncAddr(F,k),m) = dom IncAddr(F,k) by Def9
.= dom F by Def9;
A2: dom IncAddr(F,k+m) = dom F by Def9;
for x being object st x in dom F holds
IncAddr(IncAddr(F,k),m).x = IncAddr(F,k+m).x
proof
let x be object such that
A3: x in dom F;
reconsider x as Element of NAT by A3,ORDINAL1:def 12;
A4: x in dom IncAddr(F,k) by A3,Def9;
A5: IncAddr(F/.x,k) = IncAddr(F,k).x
by A3,Def9
.= IncAddr(F,k)/.x by A4,PARTFUN1:def 6;
IncAddr(IncAddr(F,k),m).x
= IncAddr(IncAddr(F,k)/.x,m) by A4,Def9
.= IncAddr(F/.x,k+m) by A5,COMPOS_0:7
.= IncAddr(F,k+m).x by A3,Def9;
hence thesis;
end;
hence thesis by A1,A2,FUNCT_1:2;
end;
definition
let S be COM-Struct, p be preProgram of S, k be Nat;
func Reloc(p,k) ->
finite NAT-defined (the InstructionsF of S)-valued Function
equals Shift(IncAddr(p,k),k);
coherence;
end;
theorem Th9:
for S being COM-Struct, F being Program of S,
G being non empty preProgram of S
holds dom CutLastLoc F misses dom Reloc(G,card F -' 1)
proof
let S be COM-Struct, F be Program of S, G be non empty preProgram of S;
set k = card F -' 1;
assume not thesis;
then consider il being object such that
A1: il in dom CutLastLoc F /\ dom Reloc(G,k) by XBOOLE_0:4;
A2: il in dom CutLastLoc F by A1,XBOOLE_0:def 4;
A3: il in dom Reloc(G,k) by A1,XBOOLE_0:def 4;
dom Reloc(G,k) = { (m+k) where m is Nat:
m in dom IncAddr(G,k) } by VALUED_1:def 12;
then consider m being Nat such that
A4: il = (m+k) and m in dom IncAddr(G,k) by A3;
reconsider f = CutLastLoc F as non empty NAT-defined finite Function
by A1;
m+k <= LastLoc f by A2,A4,VALUED_1:32;
then
A5: m+k <= card f -' 1 by AFINSQ_1:70;
A6: card f = card F - 1 by VALUED_1:38
.= card F -' 1 by PRE_CIRC:20;
per cases;
suppose k - 1 >= 0;
then m + k <= k - 1 by A5,A6,XREAL_0:def 2;
then m + k - k <= k - 1 - k by XREAL_1:9;
hence thesis by Lm4;
end;
suppose k - 1 < 0;
then m + k = 0 or m + k < 0 by A5,A6,XREAL_0:def 2;
hence thesis by A6;
end;
end;
theorem Th10:
for F being unique-halt Program of S,
I being Nat st I in dom CutLastLoc F
holds (CutLastLoc F).I <> halt S
proof
let F be unique-halt Program of S,
I be Nat such that
A1: I in dom CutLastLoc F and
A2: (CutLastLoc F).I = halt S;
A3: dom CutLastLoc F c= dom F by GRFUNC_1:2;
F.I = halt S by A1,A2,GRFUNC_1:2;
then
A4: I = LastLoc F by A1,A3,Def7;
dom CutLastLoc F = (dom F) \ {LastLoc F} by VALUED_1:36;
then not I in {LastLoc F} by A1,XBOOLE_0:def 5;
hence thesis by A4,TARSKI:def 1;
end;
definition
let S be COM-Struct;
let F, G be non empty preProgram of S;
func F ';' G -> preProgram of S equals
CutLastLoc F +* Reloc(G,card F -' 1);
coherence;
end;
registration
let S be COM-Struct, F, G be non empty preProgram of S;
cluster F ';' G -> non empty
(the InstructionsF of S)-valued NAT-defined;
coherence;
end;
theorem Th11:
for S being COM-Struct, F being Program of S,
G being non empty preProgram of S
holds card (F ';' G) = card F + card G - 1 &
card (F ';' G) = card F + card G -' 1
proof
let S be COM-Struct, F be Program of S, G be non empty preProgram of S;
set k = card F -' 1;
dom IncAddr(G,k),dom Reloc(G,k) are_equipotent by VALUED_1:27;
then
A1: IncAddr(G,k),Reloc(G,k) are_equipotent by PRE_CIRC:21;
dom CutLastLoc F misses dom Reloc(G,k) by Th9;
hence card (F ';' G)
= card CutLastLoc F + card Reloc(G,k) by PRE_CIRC:22
.= card CutLastLoc F + card IncAddr(G,k) by A1,CARD_1:5
.= card CutLastLoc F + card dom IncAddr(G,k) by CARD_1:62
.= card CutLastLoc F + card dom G by Def9
.= card CutLastLoc F + card G by CARD_1:62
.= card F - 1 + card G by VALUED_1:38
.= card F + card G - 1;
hence thesis by XREAL_0:def 2;
end;
registration
let S be COM-Struct;
let F, G be Program of S;
cluster F ';' G -> initial;
coherence
proof
set P = F ';' G;
let f,n be Nat such that
A1: n in dom P and
A2: f < n;
set k = card F -' 1;
A3: dom P = dom CutLastLoc F \/ dom Reloc(G,k) by FUNCT_4:def 1;
per cases by A1,A3,XBOOLE_0:def 3;
suppose n in dom CutLastLoc F;
then f in dom CutLastLoc F by A2,AFINSQ_1:def 12;
hence thesis by A3,XBOOLE_0:def 3;
end;
suppose n in dom Reloc(G,k);
then n in { w+k where w is Nat:
w in dom IncAddr(G,k) } by VALUED_1:def 12;
then consider m being Nat such that
A4: n = (m+k) and
A5: m in dom IncAddr(G,k);
A6: m in dom G by A5,Def9;
now per cases;
case
A7: f < k;
then f < card F - 1 by PRE_CIRC:20;
then 1+f < 1 + (card F - 1) by XREAL_1:6;
then
A8: 1+f in dom F by AFINSQ_1:66;
f < 1+f by NAT_1:19;
then
A9: f in dom F by A8,AFINSQ_1:def 12;
f <> LastLoc F by A7,AFINSQ_1:70;
then not f in {LastLoc F} by TARSKI:def 1;
then f in (dom F) \ {LastLoc F} by A9,XBOOLE_0:def 5;
hence f in dom CutLastLoc F by VALUED_1:36;
end;
case f >= k;
then consider l1 being Nat such that
A10: f = k + l1 by NAT_1:10;
reconsider l1 as Element of NAT by ORDINAL1:def 12;
A11: dom Reloc(G,k) = { w+k where w is Nat: w in dom IncAddr(G,k) }
by VALUED_1:def 12;
l1 < m or l1 = m by A10,A4,A2,XREAL_1:6;
then l1 in dom G by A6,AFINSQ_1:def 12;
then l1 in dom IncAddr(G,k) by Def9;
hence f in dom Reloc(G,k) by A11,A10;
end;
end;
hence thesis by A3,XBOOLE_0:def 3;
end;
end;
end;
theorem
for S being COM-Struct, F, G being Program of S
holds dom F c= dom (F ';' G)
proof
let S be COM-Struct, F, G be Program of S;
set P = F ';' G;
A1: dom P = dom CutLastLoc F \/ dom Reloc(G,card F -' 1)
by FUNCT_4:def 1;
A2: dom F = dom CutLastLoc F \/ {LastLoc F} by VALUED_1:37;
let x be object;
assume
A3: x in dom F;
per cases by A2,A3,XBOOLE_0:def 3;
suppose x in dom CutLastLoc F;
hence thesis by A1,XBOOLE_0:def 3;
end;
suppose
A4: x in {LastLoc F};
then
A5: x = LastLoc F by TARSKI:def 1;
reconsider f = x as Element of NAT by A4;
A6: f = card F -' 1 by A5,AFINSQ_1:70
.= card F - 1 + (0 qua Nat) by PRE_CIRC:20;
card P = card F + card G - 1 by Th11
.= card F - 1 + card G;
then f < card P by A6,XREAL_1:6;
hence thesis by AFINSQ_1:66;
end;
end;
registration
let S being COM-Struct, F, G being Program of S;
cluster F ';' G -> initial non empty;
coherence;
end;
theorem Th13:
for S being COM-Struct, F, G being Program of S
holds CutLastLoc F c= CutLastLoc (F ';' G)
proof
let S be COM-Struct, F, G be Program of S;
set k = card F -' 1;
set P = F ';' G;
A1: dom P = dom CutLastLoc F \/ dom Reloc(G,k) by FUNCT_4:def 1;
A2: dom CutLastLoc F =
{ m where m is Element of NAT: m < card CutLastLoc F } by AFINSQ_1:68;
A3: card CutLastLoc P = card P - 1 by VALUED_1:38
.= card F + card G - 1 - 1 by Th11
.= card F - 1 + (card G - 1);
A4: for m being Element of NAT
st m < card CutLastLoc F holds m < card CutLastLoc P
proof
let m be Element of NAT such that
A5: m < card CutLastLoc F;
A6: card CutLastLoc F = card F - 1 by VALUED_1:38;
1 <= card G by NAT_1:14;
then 1 - 1 <= card G - 1 by XREAL_1:9;
then card F - 1 + (0 qua Nat) <= card F - 1 + (card G - 1) by XREAL_1:6;
hence thesis by A3,A5,A6,XXREAL_0:2;
end;
A7: dom CutLastLoc F c= dom CutLastLoc P
proof
let x be object;
assume x in dom CutLastLoc F;
then consider m being Element of NAT such that
A8: x = m and
A9: m < card CutLastLoc F by A2;
m < card CutLastLoc P by A4,A9;
hence thesis by A8,AFINSQ_1:66;
end;
for x being object st x in dom CutLastLoc F holds
(CutLastLoc F).x = (CutLastLoc P).x
proof
let x be object;
assume
A10: x in dom CutLastLoc F;
then consider m being Element of NAT such that
A11: x = m and
A12: m < card CutLastLoc F by A2;
A13: dom Reloc(G,k) = { w+k where w is Nat:
w in dom IncAddr(G,k) } by VALUED_1:def 12;
A14: now
assume x in dom Reloc(G,k);
then consider w being Nat such that
A15: x = w+k and w in dom IncAddr(G,k) by A13;
m < card F - 1 by A12,VALUED_1:38;
then
m < k by PRE_CIRC:20;
hence contradiction by A11,A15,NAT_1:11;
end;
A16: x in dom P by A1,A10,XBOOLE_0:def 3;
now
assume x = LastLoc P;
then
A17: m = card P -' 1 by A11,AFINSQ_1:70
.= card P - 1 by PRE_CIRC:20;
card CutLastLoc P = card P - 1 by VALUED_1:38;
hence contradiction by A4,A12,A17;
end;
then not x in {LastLoc P} by TARSKI:def 1;
then not x in dom ( LastLoc P .--> P.LastLoc P );
then x in dom P \ dom ( LastLoc P .--> P.LastLoc P ) by A16,XBOOLE_0:def 5;
hence (CutLastLoc P).x = (CutLastLoc F +* Reloc(G,k)).x
by GRFUNC_1:32
.= (CutLastLoc F).x by A14,FUNCT_4:11;
end;
hence thesis by A7,GRFUNC_1:2;
end;
theorem Th14:
for S being COM-Struct, F, G being Program of S
holds (F ';' G).LastLoc F = IncAddr(G,card F -' 1).0
proof
let S be COM-Struct, F, G be Program of S;
set k = card F -' 1;
A1: LastLoc F = (0 qua Nat)+k by AFINSQ_1:70;
A2: 0 in dom IncAddr(G,k) by AFINSQ_1:65;
dom Reloc(G,k) = {(m+k) where m is Nat: m in dom IncAddr(G,k)}
by VALUED_1:def 12;
then LastLoc F in dom Reloc(G,k) by A1,A2;
hence (F ';' G).LastLoc F = (Reloc(G,k)).LastLoc F by FUNCT_4:13
.= IncAddr(G,k).0 by A1,A2,VALUED_1:def 12;
end;
Lm6:
for S being COM-Struct, F, G being Program of S,
f being Nat st f < card F - 1
holds F.f = (F ';' G).f
proof
let S be COM-Struct, F, G be Program of S, f be Nat;
set k = card F -' 1, P = F ';' G;
assume f < card F - 1;
then f < card CutLastLoc F by VALUED_1:38;
then
A1: f in dom CutLastLoc F by AFINSQ_1:66;
dom CutLastLoc F misses dom Reloc(G,k) by Th9;
then dom CutLastLoc F /\ dom Reloc(G,k) = {};
then not f in dom Reloc(G,k)
by A1,XBOOLE_0:def 4;
hence P.f = (CutLastLoc F).f by FUNCT_4:11
.= F.f by A1,GRFUNC_1:2;
end;
theorem
for S being COM-Struct, F, G being Program of S,
f being Nat st f < card F - 1
holds IncAddr(F,card F -' 1).f = IncAddr(F ';' G, card F -' 1).f
proof
let S be COM-Struct, F, G be Program of S, f be Nat;
set k = card F -' 1, P = F ';' G;
assume
A1: f < card F - 1;
then f < card CutLastLoc F by VALUED_1:38;
then
A2: f in dom CutLastLoc F by AFINSQ_1:66;
A3: dom CutLastLoc F c= dom F by GRFUNC_1:2;
CutLastLoc F c= CutLastLoc P by Th13;
then CutLastLoc F c= P by XBOOLE_1:1;
then
A4: dom CutLastLoc F c= dom P by GRFUNC_1:2;
A5: F.f = F/.f by A2,A3,PARTFUN1:def 6;
A6: P.f = F.f by Lm6,A1;
thus IncAddr(F,k).f = IncAddr(F/.f,k) by A2,A3,Def9
.= IncAddr(P/.f,k) by A2,A4,A5,A6,PARTFUN1:def 6
.= IncAddr(P,k).f by A2,A4,Def9;
end;
registration
let S be COM-Struct;
let F be Program of S;
let G be halt-ending Program of S;
cluster F ';' G -> halt-ending;
coherence
proof
set P = F ';' G, k = card F -' 1;
A1: dom Reloc(G,k) = { (m+k) where m is Nat:
m in dom IncAddr(G,k) } by VALUED_1:def 12;
A2: card G -' 1 = LastLoc G by AFINSQ_1:70;
then
A3: card G -' 1 in dom G by VALUED_1:30;
then
A4: card G -' 1 in dom IncAddr(G,k) by Def9;
then
A5: k + (card G -' 1) in dom Reloc(G,k) by A1;
A6: G/.(card G -' 1) = G.(card G -' 1) by A2,PARTFUN1:def 6,VALUED_1:30
.= halt S by A2,Def6;
A7: card G - 1 >= 0 by NAT_1:14,XREAL_1:48;
then k + (card G - 1) >= k+(0 qua Nat) by XREAL_1:6;
then
A8: k + card G -' 1 = k + card G - 1 by XREAL_0:def 2
.= k + (card G - 1)
.= k + (card G -' 1) by A7,XREAL_0:def 2;
thus P.(LastLoc P) = P.(card P -' 1) by AFINSQ_1:70
.= P.(card F + card G -' 1 -' 1) by Th11
.= P.(k + card G -' 1) by NAT_1:14,NAT_D:38
.= Reloc(G,k).(k + (card G -' 1)) by A5,A8,FUNCT_4:13
.= IncAddr(G,k).(card G -' 1) by A4,VALUED_1:def 12
.= IncAddr(G/.(card G -' 1),k) by A3,Def9
.= halt S by A6,COMPOS_0:4;
end;
end;
registration
let S be COM-Struct;
let F be MacroInstruction of S;
let G be unique-halt Program of S;
cluster F ';' G -> unique-halt;
coherence
proof
set P = F ';' G, k = card F -' 1;
A1: dom P = dom CutLastLoc F \/ dom Reloc(G,k) by FUNCT_4:def 1;
A2: dom Reloc(G,k) = { (m+k) where m is Nat:
m in dom IncAddr(G,k) } by VALUED_1:def 12;
A3: card G - 1 >= 0 by NAT_1:14,XREAL_1:48;
then k + (card G - 1) >= k+(0 qua Nat) by XREAL_1:6;
then
A4: k + card G -' 1 = k + card G - 1 by XREAL_0:def 2
.= k + (card G - 1)
.= k + (card G -' 1) by A3,XREAL_0:def 2;
let f be Nat such that
A5: P.f = halt S and
A6: f in dom P;
per cases by A1,A6,XBOOLE_0:def 3;
suppose
A7: f in dom CutLastLoc F;
then
A8: (CutLastLoc F).f <> halt S by Th10;
dom CutLastLoc F misses dom Reloc(G,k) by Th9;
then CutLastLoc F c= P by FUNCT_4:32;
hence thesis by A5,A7,A8,GRFUNC_1:2;
end;
suppose
A9: f in dom Reloc(G,k);
then consider m being Nat such that
A10: f = m+k and
A11: m in dom IncAddr(G,k) by A2;
A12: m in dom G by A11,Def9;
then
A13: G/.m = G.m by PARTFUN1:def 6;
IncAddr(G/.m,k) = IncAddr(G,k).m by A12,Def9
.= Reloc(G,k).(m+k) by A11,VALUED_1:def 12
.= halt S by A5,A9,A10,FUNCT_4:13;
then G.m = halt S by A13,COMPOS_0:12;
then m = LastLoc G by A12,Def7
.= (card G -' 1) by AFINSQ_1:70;
then m+k = card F + card G -' 1 -' 1 by A4,NAT_1:14,NAT_D:38
.= card P -' 1 by Th11;
hence thesis by A10,AFINSQ_1:70;
end;
end;
end;
definition
let S be COM-Struct;
let F, G be MacroInstruction of S;
redefine func F ';' G -> MacroInstruction of S; :: redefines ';' (COMPOS_1, definition)
coherence;
end;
registration let S be COM-Struct, k;
reduce IncAddr(Stop S, k) to Stop S;
reducibility
proof
A1: dom IncAddr(Stop S, k) = dom Stop S by Def9
.= {0};
A2: dom Stop S = {0};
for x being object st x in {0} holds IncAddr(Stop S, k).x = (Stop S). x
proof
let x be object;
assume
A3: x in {0};
then
A4: x = 0 by TARSKI:def 1;
then
A5: (Stop S)/.0 = (Stop S).0 by A2,A3,PARTFUN1:def 6
.= halt S;
thus IncAddr(Stop S, k).x
= IncAddr((Stop S)/.0,k) by A2,A3,A4,Def9
.= halt S by A5,COMPOS_0:4
.= (Stop S).x by A4;
end;
hence thesis by A1,A2,FUNCT_1:2;
end;
end;
::$CT
theorem Th16:
for k being Nat
for S being COM-Struct
holds Shift(Stop S, k) = k .--> halt S
proof
let k be Nat;
let S be COM-Struct;
A1: dom Shift(Stop S,k) =
{(m+k) where m is Nat: m in dom Stop S} by VALUED_1:def 12;
A2: 0 in dom Stop S by TARSKI:def 1;
A3: dom Shift(Stop S,k) = {k}
proof
hereby
let x be object;
assume x in dom Shift(Stop S,k);
then consider m being Nat such that
A4: x = (m+k) and
A5: m in dom Stop S by A1;
m in {0} by A5;
then m = 0 by TARSKI:def 1;
hence x in {k} by A4,TARSKI:def 1;
end;
let x be object;
assume x in {k};
then x = (0 qua Nat)+k by TARSKI:def 1;
hence thesis by A1,A2;
end;
A6: dom (k .--> halt S) = {k};
for x being object st x in {k} holds
(Shift(Stop S, k)).x = (k .--> halt S).x
proof
let x be object;
assume x in {k};
then
A7: x = (0 qua Nat)+k by TARSKI:def 1;
0 in dom Stop S by TARSKI:def 1;
hence (Shift(Stop S, k)).x = (Stop S).0 by A7,VALUED_1:def 12
.= halt S
.= (k .--> halt S).x by A7,FUNCOP_1:72;
end;
hence thesis by A3,A6,FUNCT_1:2;
end;
registration let S be COM-Struct, F being MacroInstruction of S;
reduce F ';' Stop S to F;
reducibility
proof
set k = card F -' 1;
A1: dom F = dom CutLastLoc F \/ {LastLoc F} by VALUED_1:37;
dom Shift(Stop S,k) = dom (k .--> halt S) by Th16
.= {k}
.= {LastLoc F} by AFINSQ_1:70;
then
A2: dom (F ';' Stop S) = dom F by A1,FUNCT_4:def 1;
for x being object st x in dom F holds (F ';' Stop S).x = F.x
proof
let x be object such that
A3: x in dom F;
dom CutLastLoc F misses dom Reloc(Stop S,k) by Th9;
then
A4: {} = dom CutLastLoc F /\ dom Reloc(Stop S,k);
per cases by A1,A3,XBOOLE_0:def 3;
suppose
A5: x in dom CutLastLoc F;
then not x in dom Reloc(Stop S,k) by A4,XBOOLE_0:def 4;
hence (F ';' Stop S).x = (CutLastLoc F).x by FUNCT_4:11
.= F.x by A5,GRFUNC_1:2;
end;
suppose x in {LastLoc F};
then
A6: x = LastLoc F by TARSKI:def 1;
then
A7: x = k by AFINSQ_1:70;
A8: 0 in dom Stop S by TARSKI:def 1;
dom Shift(Stop S,k)
= { (m+k) where m is Nat: m in dom Stop S }
by VALUED_1:def 12;
then (0 qua Nat)+k in dom Shift(Stop S,k) by A8;
hence (F ';' Stop S).x = Shift(Stop S,(0 qua Nat)+k).x
by A7,FUNCT_4:13
.= (Stop S).0 by A7,A8,VALUED_1:def 12
.= halt S
.= F.x by A6,Def6;
end;
end;
hence thesis by A2,FUNCT_1:2;
end;
end;
theorem
for S being COM-Struct,
F being MacroInstruction of S
holds F ';' Stop S = F;
registration let S be COM-Struct, F be MacroInstruction of S;
reduce Stop S ';' F to F;
reducibility
proof
card Stop S -' 1 = 0 by Lm2;
hence Stop S ';' F = {} +* Reloc(F,0)
.= Reloc(F,0)
.= F;
end;
end;
theorem
for S being COM-Struct,
F being MacroInstruction of S
holds Stop S ';' F = F;
theorem
for S being COM-Struct, F, G, H being MacroInstruction of S
holds F ';' G ';' H = F ';' (G ';' H)
proof
let S be COM-Struct, F, G, H be MacroInstruction of S;
per cases;
suppose
A1: F = Stop S;
hence F ';' G ';' H = Stop S ';' G ';' H
.= F ';' (G ';' H) by A1;
end;
suppose
A2: G = Stop S;
hence F ';' G ';' H = F ';' Stop S ';' H
.= F ';' (G ';' H) by A2;
end;
suppose that
A3: F <> Stop S and
A4: G <> Stop S;
set X = {k where k is Element of NAT:
k < card F + card G + card H - 1 - 1};
A5: card (F ';' G ';' H) = card (F ';' G) + card H - 1 by Th11
.= card F + card G - 1 + card H - 1 by Th11
.= card F + card G + card H - 1 - 1;
A6: card (F ';' (G ';' H)) = card F + card (G ';' H) - 1 by Th11
.= card F + (card G + card H - 1) - 1 by Th11
.= card F + card G + card H - 1 - 1;
A7: dom (F ';' G ';' H) = X by A5,AFINSQ_1:68;
A8: dom (F ';' (G ';' H)) = X by A6,AFINSQ_1:68;
for x being object st x in X holds (F ';' G ';' H).x = (F ';' (G ';' H)).x
proof
let x be object;
assume x in X;
then consider k being Element of NAT such that
A9: x = k and
A10: k < card F + card G + card H - 1 - 1;
A11: dom Reloc(G ';' H,card F -' 1) =
{ m+(card F -' 1) where m is Nat:
m in dom IncAddr(G ';' H,card F -' 1) } by VALUED_1:def 12;
A12: dom Reloc(H,card (F ';' G) -' 1) =
{ m+(card (F ';' G) -' 1) where m is Nat:
m in dom IncAddr(H,card (F ';' G) -' 1) } by VALUED_1:def 12;
A13: dom Reloc(H,card G -' 1) =
{ m+(card G -' 1) where m is Nat:
m in dom IncAddr(H,card G -' 1) } by VALUED_1:def 12;
A14: card (F ';' G) -' 1 = card (F ';' G) - 1 by PRE_CIRC:20
.= card F + card G - 1 - 1 by Th11;
then card (F ';' G) -' 1 = card F - 1 + (card G - 1);
then
A15: card (F ';' G) -' 1 = (card G -' 1) + (card F - 1) by PRE_CIRC:20
.= (card G -' 1) + (card F -' 1) by PRE_CIRC:20;
A16: dom Reloc(G,card F -' 1) =
{ m+(card F -' 1) where m is Nat:
m in dom IncAddr(G,card F -' 1) } by VALUED_1:def 12;
A17: card F -' 1 = card F - 1 by PRE_CIRC:20;
A18: card G -' 1 = card G - 1 by PRE_CIRC:20;
A19: for W being MacroInstruction of S st W <> Stop S holds 2 <= card W
proof
let W be MacroInstruction of S;
assume
A20: W <> Stop S;
assume 2 > card W;
then 1 + 1 > card W;
then card W <= 1 by NAT_1:13;
hence contradiction by A20,Th6,NAT_1:25;
end;
then 2 <= card F by A3;
then
A21: 1 <= card F by XXREAL_0:2;
A22: 2 <= card G by A4,A19;
per cases by A21,A22,Lm5;
suppose
A23: k < card F - 1;
A24: CutLastLoc F c= CutLastLoc (F ';' G) by Th13;
A25: now
assume x in dom Reloc(G ';' H,card F -' 1);
then consider m being Nat such that
A26: x = m+(card F -' 1) and
m in dom IncAddr(G ';' H,card F -' 1) by A11;
k = m + (card F - 1) by A9,A26,PRE_CIRC:20;
then m + (card F - 1) < card F -' 1 by A23,PRE_CIRC:20;
then m + (card F -' 1) < card F -' 1 by PRE_CIRC:20;
hence contradiction by NAT_1:11;
end;
A27: now
assume x in dom
Reloc(H,card (F ';' G) -' 1);
then consider m being Nat such that
A28: x = m+(card (F ';' G) -' 1) and
m in dom IncAddr(H,card (F ';' G) -' 1) by A12;
m + (card G -' 1) + (card F -' 1) < card F -' 1
by A23,A9,A15,A28,PRE_CIRC:20;
hence contradiction by NAT_1:11;
end;
k < card CutLastLoc F by A23,VALUED_1:38;
then
A29: x in dom CutLastLoc F by A9,AFINSQ_1:66;
thus (F ';' G ';' H).x = (CutLastLoc (F ';' G)).x by A27,FUNCT_4:11
.= (CutLastLoc F).x by A24,A29,GRFUNC_1:2
.= (F ';' (G ';' H)).x by A25,FUNCT_4:11;
end;
suppose
A30: k = card F - 1;
A31: now
assume x in dom Reloc(H,card (F ';' G) -' 1);
then consider m being Nat such that
A32: x = m+(card (F ';' G) -' 1) and
m in dom IncAddr(H,card (F ';' G) -' 1) by A12;
m + (card G -' 1) + (card F -' 1) = card F -' 1 by A30,A15,A32,A9,
PRE_CIRC:20;
then card G -' 1 = 0;
then card G - 1 = 0 by PRE_CIRC:20;
hence contradiction by A4,Th6;
end;
A33: 0 in dom IncAddr(G ';' H,card F -' 1) by AFINSQ_1:65;
A34: 0 in dom IncAddr(G,card F -' 1) by AFINSQ_1:65;
A35: 0 in dom G by AFINSQ_1:65;
A36: 0 in dom (G ';' H) by AFINSQ_1:65;
k = (0 qua Nat) + (card F -' 1) by A30,PRE_CIRC:20;
then
A37: x in dom Reloc(G ';' H,card F -' 1) by A9,A11,A33;
A38: k = card F -' 1 by A30,PRE_CIRC:20;
A39: x = (0 qua Nat)+k by A9;
0 in dom IncAddr(G,card F -' 1) by AFINSQ_1:65;
then
A40: x in dom Reloc(G,card F -' 1) by A16,A38,A39;
then x in dom CutLastLoc F \/ dom Reloc(G,card F -' 1)
by XBOOLE_0:def 3;
then
A41: x in dom (F ';' G) by FUNCT_4:def 1;
now
A42: dom (LastLoc (F ';' G) .--> (F ';' G).LastLoc (F ';' G ))
= {LastLoc (F ';' G)}
.= {card (F ';' G) -' 1} by AFINSQ_1:70;
assume x in dom (LastLoc (F ';' G) .--> (F ';' G).LastLoc (F ';' G ));
then x = card (F ';' G) -' 1 by A42,TARSKI:def 1;
then card G - 1 = 0 by A38,A9,A15,PRE_CIRC:20;
hence contradiction by A4,Th6;
end;
then
A43: x in dom (F ';' G) \
dom (LastLoc (F ';' G) .--> (F ';' G).LastLoc (F ';' G ))
by A41,XBOOLE_0:def 5;
1 <= card G by NAT_1:14;
then card G > 1 by A4,Th6,XXREAL_0:1;
then
A44: card G - 1 > 1 - 1 by XREAL_1:9;
then card G -' 1 > 1 - 1 by PRE_CIRC:20;
then
A45: not 0 in dom Reloc(H,card G -' 1) by VALUED_1:29;
card CutLastLoc G <> {} by A44,VALUED_1:38;
then
A46: 0 in dom CutLastLoc G by AFINSQ_1:65,CARD_1:27;
A47: G/.0 = G.0 by A35,PARTFUN1:def 6
.= (CutLastLoc G).0 by A46,GRFUNC_1:2
.= (G ';' H).0 by A45,FUNCT_4:11
.= (G ';' H)/.0 by A36,PARTFUN1:def 6;
thus (F ';' G ';' H).x = ((F ';' G) \
( LastLoc (F ';' G) .--> (F ';' G).LastLoc (F ';' G ))).x by A31,
FUNCT_4:11
.= (CutLastLoc F +* Reloc(G,card F -' 1)).x by A43,GRFUNC_1:32
.= Reloc(G,card F -' 1).x by A40,FUNCT_4:13
.= IncAddr(G,card F -' 1).0 by A34,A38,A39,VALUED_1:def 12
.= IncAddr((G ';' H)/.0,card F -' 1) by A35,A47,Def9
.= IncAddr(G ';' H,card F -' 1).0 by A36,Def9
.= Reloc(G ';' H,card F -' 1).x
by A33,A38,A39,VALUED_1:def 12
.= (F ';' (G ';' H)).x by A37,FUNCT_4:13;
end;
suppose that
A48: card F <= k and
A49: k <= card F + card G - 3;
A50: now
assume
x in dom Reloc(H,card (F ';' G) -' 1);
then consider m being Nat such that
A51: x = m+(card (F ';' G) -' 1) and
m in dom IncAddr(H,card (F ';' G) -' 1) by A12;
m + ((card G -' 1) + (card F -' 1))
<= - 1 + ((card G -' 1) + (card F -' 1)) by A9,A15,A17,A18,A49,A51;
hence contradiction by XREAL_1:6;
end;
card F -' 1 <= card F by NAT_D:35;
then
A52: x = k -' (card F -' 1) + (card F -' 1)
by A9,A48,XREAL_1:235,XXREAL_0:2;
A53: card F - card F <= k - card F by A48,XREAL_1:9;
card F - 1 < card F - 0 by XREAL_1:15;
then k - (card F - 1) >= 0 by A53,XREAL_1:15;
then
A54: k - (card F -' 1) >= 0 by PRE_CIRC:20;
A55: card F + card G - 3 < card F + card G - 3 + 1 by XREAL_1:29;
then
A56: k < (card G - 1) + (card F - 1) by A49,XXREAL_0:2;
k - (card F - 1) + (card F - 1) < (card G - 1) + (card F - 1)
by A49,A55,XXREAL_0:2;
then k - (card F - 1) < card G - 1 by XREAL_1:7;
then k - (card F -' 1) < card G - 1 by PRE_CIRC:20;
then k -' (card F -' 1) < card G - 1 by A54,XREAL_0:def 2;
then k -' (card F -' 1) < card CutLastLoc G by VALUED_1:38;
then
A57: k -' (card F -' 1) in dom CutLastLoc G by AFINSQ_1:66;
then k -' (card F -' 1) in
dom CutLastLoc G \/ dom Reloc(H,card G -' 1)
by XBOOLE_0:def 3;
then
A58: k -' (card F -' 1) in dom (G ';' H) by FUNCT_4:def 1;
then
A59: k -' (card F -' 1) in dom IncAddr(G ';' H,card F -' 1)
by Def9;
then
A60: x in dom Reloc(G ';' H,card F -' 1) by A11,A52;
card G + card F - 2 < card F + card G - 1 by XREAL_1:15;
then k < card F + card G - 1 by A56,XXREAL_0:2;
then k < card (F ';' G) by Th11;
then
A61: x in dom (F ';' G) by A9,AFINSQ_1:66;
now
assume x in dom (LastLoc (F ';' G) .--> (F ';' G).LastLoc (F ';' G));
then x in {LastLoc (F ';' G)};
then x = LastLoc (F ';' G) by TARSKI:def 1
.= card (F ';' G) -' 1 by AFINSQ_1:70;
then k = (card G - 1) + (card F - 1) by A9,A15,A18,PRE_CIRC:20;
hence contradiction by A49,A55;
end;
then
A62: x in dom (F ';' G) \
dom (LastLoc (F ';' G) .--> (F ';' G).LastLoc (F ';' G))
by A61,XBOOLE_0:def 5;
A63: dom CutLastLoc G c= dom G by GRFUNC_1:2;
then k -' (card F -' 1) in dom G by A57;
then
A64: k -' (card F -' 1) in dom IncAddr(G,card F -' 1) by Def9;
then
A65: x in dom Reloc(G,card F -' 1) by A16,A52;
A66: now
assume k -' (card F -' 1) in dom Reloc(H,card G -' 1);
then consider m being Nat such that
A67: k -' (card F -' 1) = m+(card G -' 1) and
m in dom IncAddr(H,card G -' 1) by A13;
A68: m = k -' (card F -' 1) - (card G -' 1) by A67
.= k - (card F -' 1) - (card G -' 1) by A54,XREAL_0:def 2
.= k - (card F - 1) - (card G -' 1) by PRE_CIRC:20
.= k - (card F - 1) - (card G - 1) by PRE_CIRC:20
.= k - (card F + card G - 2);
k - (card F + card G - 2)
<= card F + card G - 3 - (card F + card G - 2) by A49,XREAL_1:9;
hence contradiction by A68,Lm4;
end;
A69: (G ';' H)/.(k -' (card F -' 1))
= (CutLastLoc G +* Reloc(H,card G -' 1))
.(k -' (card F -' 1)) by A58,PARTFUN1:def 6
.= (CutLastLoc G).(k -' (card F -' 1)) by A66,FUNCT_4:11
.= G.(k -' (card F -' 1)) by A57,GRFUNC_1:2;
thus (F ';' G ';' H).x
= ((F ';' G) \ (LastLoc (F ';' G) .--> (F ';' G).LastLoc (F ';' G))).x
by A50,FUNCT_4:11
.= (CutLastLoc F +* Reloc(G,card F -' 1)).x by A62,GRFUNC_1:32
.= Reloc(G,card F -' 1).x by A65,FUNCT_4:13
.= IncAddr(G,card F -' 1).(k -' (card F -' 1))
by A52,A64,VALUED_1:def 12
.= IncAddr(G/.(k -' (card F -' 1)),card F -' 1)
by A57,A63,Def9
.= IncAddr((G ';' H)/.(k -' (card F -' 1)),card F -' 1)
by A57,A63,A69,PARTFUN1:def 6
.= IncAddr(G ';' H,card F -' 1).(k -' (card F -' 1))
by A58,Def9
.= Reloc(G ';' H,card F -' 1).x
by A52,A59,VALUED_1:def 12
.= (F ';' (G ';' H)).x by A60,FUNCT_4:13;
end;
suppose
A70: k = card F + card G - 2;
then
A71: x = (k -' (card (F ';' G) -' 1) + (card (F ';' G) -' 1))
by A9,A14,XREAL_1:235;
k - (card (F ';' G) -' 1) = 0 by A14,A70;
then
A72: k -' (card (F ';' G) -' 1) = 0 by XREAL_0:def 2;
then
A73: k -' (card (F ';' G) -' 1) in dom IncAddr(H,card (F ';' G)
-' 1) by AFINSQ_1:65;
then
A74: x in dom Reloc(H,card (F ';' G) -' 1)
by A12,A71;
A75: x = (card G -' 1) + (card F -' 1) by A9,A17,A18,A70;
card G - 1 + (0 qua Nat) < card G - 1 + card H by XREAL_1:6;
then card G -' 1 < card G + card H - 1 by PRE_CIRC:20;
then card G -' 1 < card (G ';' H) by Th11;
then
A76: (card G -' 1) in dom (G ';' H) by AFINSQ_1:66;
then
A77: (card G -' 1) in dom IncAddr(G ';' H,card F -' 1) by Def9;
then
A78: x in dom Reloc(G ';' H,card F -' 1) by A11,A75;
A79: 0 in dom H by AFINSQ_1:65;
A80: (G ';' H)/.(card G -' 1) = (G ';' H).(card G -' 1)
by A76,PARTFUN1:def 6;
A81: 0 in dom IncAddr(H,card G -' 1) by AFINSQ_1:65;
then
A82: IncAddr(H,card G -' 1)/.0
= IncAddr(H,card G -' 1).0 by PARTFUN1:def 6
.= IncAddr(H/.0,(card G -' 1)) by A79,Def9;
(G ';' H)/.(card G -' 1)
= (G ';' H).LastLoc G by A80,AFINSQ_1:70
.= IncAddr(H,card G -' 1).0 by Th14
.= IncAddr(H,card G -' 1)/.0 by A81,PARTFUN1:def 6;
then
A83: IncAddr((G ';' H)/.(card G -' 1),card F -' 1)
= IncAddr(H/.0,card (F ';' G) -' 1) by A15,A82,COMPOS_0:7;
thus (F ';' G ';' H).x
= Reloc(H,card (F ';' G) -' 1).x
by A74,FUNCT_4:13
.= IncAddr(H,card (F ';' G) -' 1).(k -' (card (F ';' G) -' 1))
by A71,A73,VALUED_1:def 12
.= IncAddr(H/.0,card (F ';' G) -' 1) by A72,A79,Def9
.= IncAddr(G ';' H,card F -' 1).(card G -' 1) by A76,A83,Def9
.= Reloc(G ';' H,card F -' 1).x
by A75,A77,VALUED_1:def 12
.= (F ';' (G ';' H)).x by A78,FUNCT_4:13;
end;
suppose
A84: card F + card G - 2 < k;
then
A85: x = (k -' (card (F ';' G) -' 1) + (card (F ';' G) -' 1))
by A9,A14,XREAL_1:235;
k + (0 qua Nat) < card F + card G - (1 + 1) + card H by A10;
then k - (card F + card G - (1 + 1)) < card H - 0 by XREAL_1:21;
then k -' (card (F ';' G) -' 1) < card H by A14,XREAL_0:def 2;
then
A86: k -' (card (F ';' G) -' 1) in dom H by AFINSQ_1:66;
then
A87: k -' (card (F ';' G) -' 1) in dom IncAddr(H,card (F ';' G)
-' 1) by Def9;
then
A88: x in dom Reloc(H,card (F ';' G) -' 1)
by A12,A85;
A89: card F -' 1 <= (card G -' 1) + (card F -' 1) by NAT_1:11;
then
A90: k >= card F -' 1 by A14,A15,A84,XXREAL_0:2;
A91: x = k -' (card F -' 1) + (card F -' 1) by A9,A14,A15,A84,A89,
XREAL_1:235,XXREAL_0:2;
A92: k - (card F -' 1) >= 0 by A90,XREAL_1:48;
A93: k - (card F -' 1) < card F + card G + card H - 1 - 1 - (card F -' 1)
by A10,XREAL_1:9;
then
A94: k -' (card F -' 1) < card F + card G + card H - card F - 1
by A17,A92,XREAL_0:def 2;
k -' (card F -' 1) < card F - card F + card G + card H - 1
by A17,A92,A93,XREAL_0:def 2;
then k -' (card F -' 1) < card (G ';' H) by Th11;
then
A95: k -' (card F -' 1) in dom (G ';' H) by AFINSQ_1:66;
then k -' (card F -' 1) in dom IncAddr(G ';' H,card F -' 1)
by Def9;
then
A96: x in dom Reloc(G ';' H,card F -' 1) by A11,A91;
A97: k -' (card F -' 1) in dom IncAddr(G ';' H,card F -' 1)
by A95,Def9;
A98: k - (card F -' 1) >= card (F ';' G) -' 1 - (card F -' 1)
by A14,A84,XREAL_1:9;
then
A99: k -' (card F -' 1) >= (card F -' 1) + (card G -' 1) - ( card F -' 1)
by A14,A15,A84,A89,XREAL_1:233,XXREAL_0:2;
A100: k -' (card F -' 1) >= card G -' 1 by A14,A15,A84,A89,A98,XREAL_1:233
,XXREAL_0:2;
A101: k -' (card F -' 1) =
k -' (card F -' 1) -' (card G -' 1) + (card G -' 1) by A99,XREAL_1:235;
k -' (card F -' 1) - (card G -' 1) < card G + card H - 1 - (card G -
1) by A18,A94,XREAL_1:9;
then k -' (card F -' 1) -' (card G -' 1) <
card H + (card G - 1) - (card G - 1) by A100,XREAL_1:233;
then k -' (card F -' 1) -' (card G -' 1) in dom H by AFINSQ_1:66;
then
A102: k -' (card F -' 1) -' (card G -' 1) in
dom IncAddr(H,card G -' 1) by Def9;
then
A103: k -' (card F -' 1) in
dom Reloc(H,card G -' 1) by A13,A101;
A104: k -' (card F -' 1) -' (card G -' 1)
= k -' (card F -' 1) - (card G -' 1) by A99,XREAL_1:233
.= k - (card F -' 1) - (card G -' 1) by A14,A15,A84,A89,XREAL_1:233
,XXREAL_0:2
.= k - ((card F -' 1) + (card G -' 1))
.= k -' (card (F ';' G) -' 1) by A14,A15,A84,XREAL_1:233;
A105: (G ';' H)/.(k -' (card F -' 1))
= ((CutLastLoc G) +* Reloc(H,card G -' 1)).
(k -' (card F -' 1)) by A95,PARTFUN1:def 6
.= Reloc(H,card G -' 1).(k -' (card F -' 1))
by A103,FUNCT_4:13
.= IncAddr(H,card G -' 1).(k -' (card (F ';' G) -' 1)) by A101,A102,A104,
VALUED_1:def 12
.= IncAddr(H/.(k -' (card (F ';' G) -' 1)),card G -' 1)
by A86,Def9;
thus (F ';' G ';' H).x
= Reloc(H,card (F ';' G) -' 1).x
by A88,FUNCT_4:13
.= IncAddr(H,card (F ';' G) -' 1).(k -' (card (F ';' G) -' 1))
by A85,A87,VALUED_1:def 12
.= IncAddr(H/.(k -' (card (F ';' G) -' 1)),card (F ';' G) -' 1)
by A86,Def9
.= IncAddr((G ';' H)/.(k -' (card F -' 1)),card F -' 1)
by A15,A105,COMPOS_0:7
.= IncAddr(G ';' H,card F -' 1).(k -' (card F -' 1))
by A95,Def9
.= Reloc(G ';' H,card F -' 1).x
by A91,A97,VALUED_1:def 12
.= (F ';' (G ';' H)).x by A96,FUNCT_4:13;
end;
end;
hence thesis by A7,A8,FUNCT_1:2;
end;
end;
::$CT 2
begin :: Addenda
reserve i, j, k for Nat,
n for Nat,
l,il for Nat;
theorem Th20:
for k being Nat holds
for p being finite NAT-defined (the InstructionsF of S)-valued Function
holds dom Reloc(p,k) = dom Shift(p,k)
proof let k be Nat;
let p be finite NAT-defined (the InstructionsF of S)-valued Function;
A1: dom IncAddr(p,k) = dom p by Def9;
thus dom Reloc(p,k)
= { m+k where m is Nat :m in dom p} by A1,VALUED_1:def 12
.= dom Shift(p,k) by VALUED_1:def 12;
end;
theorem Th21:
for k being Nat holds
for p being finite NAT-defined (the InstructionsF of S)-valued Function
holds dom Reloc(p,k) = { j+k where j is Nat:j in dom p }
proof
let k be Nat;
let p be finite NAT-defined (the InstructionsF of S)-valued Function;
thus dom Reloc(p,k) = dom Shift(p,k) by Th20
.= { j+k where j is Nat:j in dom p } by VALUED_1:def 12;
end;
theorem Th22:
for i,j being Nat holds
for p being NAT-defined (the InstructionsF of S)-valued finite Function
holds Shift(IncAddr(p,i),j) = IncAddr(Shift(p,j),i)
proof
let i,j be Nat;
let p be NAT-defined (the InstructionsF of S)-valued finite Function;
set f = Shift(IncAddr(p,i),j);
set g = IncAddr(Shift(p,j),i);
dom(IncAddr(p,i)) = dom p by Def9;
then dom(Shift(p,j)) = { m+j where m is Nat:
m in dom (IncAddr(p,i)) } by VALUED_1:def 12
.= dom f by VALUED_1:def 12;
then
A1: dom f = dom g by Def9;
now
let x be object;
A2: dom f c= NAT by RELAT_1:def 18;
assume
A3: x in dom f;
then reconsider x9=x as Element of NAT by A2;
reconsider xx=x9 as Element of NAT;
x in { m+j where m is Nat:
m in dom IncAddr(p,i) } by A3,VALUED_1:def 12;
then consider m being Nat such that
A4: x = m+j and
A5: m in dom IncAddr(p,i);
A6: m in dom p by A5,Def9;
dom Shift(p,j) = { mm+j where mm is Nat:
mm in dom p} by VALUED_1:def 12;
then
A7: x9 in dom Shift(p,j) by A4,A6;
reconsider mm=m as Element of NAT by ORDINAL1:def 12;
A8: p/.mm = p.m by A6,PARTFUN1:def 6
.= Shift(p,j).(m + j) by A6,VALUED_1:def 12
.= Shift(p,j)/.xx by A4,A7,PARTFUN1:def 6;
thus f.x = IncAddr(p,i).(m) by A5,A4,VALUED_1:def 12
.= IncAddr(Shift(p,j)/.xx,i) by A6,A8,Def9
.= g.x by A7,Def9;
end;
hence thesis by A1,FUNCT_1:2;
end;
theorem
for g being NAT-defined (the InstructionsF of S)-valued finite Function
for k being Nat holds
for I being Instruction of S holds
il in dom g & I = g.il implies
IncAddr(I, k) = Reloc(g, k).(il + k)
proof
let g be NAT-defined (the InstructionsF of S)-valued finite Function;
let k be Nat;
let I be Instruction of S;
assume that
A1: il in dom g and
A2: I = g.il;
reconsider ii = il as Element of NAT by ORDINAL1:def 12;
A3: il in dom IncAddr(g,k) by A1,Def9;
thus (Reloc(g, k)).(il + k)
= (IncAddr(g,k)).ii by A3,VALUED_1:def 12
.= IncAddr((g)/.ii,k) by A1,Def9
.= IncAddr(I,k) by A1,A2,PARTFUN1:def 6;
end;
reserve
i,j,k for Instruction of S,
I,J,K for Program of S;
definition
let S be COM-Struct;
let i be Instruction of S;
redefine func Load i -> preProgram of S; :: redefines Load (COMPOS_1, synonym) → <% (AFINSQ_1, definition)
coherence;
end;
reserve k1,k2 for Integer;
reserve l,l1,loc for Nat;
definition
let S be COM-Struct;
let I be initial preProgram of S;
func stop I -> preProgram of S equals
I ^ Stop S;
coherence;
end;
registration let S be COM-Struct;
let I be initial preProgram of S;
cluster stop I -> initial non empty;
correctness;
end;
reserve i1,i2 for Instruction of S;
theorem
0 in dom stop I by AFINSQ_1:66;
begin :: SCMFSA6A
reserve
i,j,k for Instruction of S,
I,J,K for Program of S;
definition
let S be COM-Struct;
let i be Instruction of S;
func Macro i -> preProgram of S equals
stop Load i;
coherence;
end;
registration let S;
let i;
cluster Macro i -> initial non empty;
coherence;
end;
begin :: SCMFSA7B
reserve m for Nat;
registration
let S be COM-Struct;
cluster Stop S -> halt-ending;
coherence;
end;
registration
let S be COM-Struct;
cluster non halt-free for Program of S;
existence
proof
take Stop S;
thus thesis;
end;
end;
registration
let S be COM-Struct;
let p be NAT-defined (the InstructionsF of S)-valued Function,
q be non halt-free
NAT-defined (the InstructionsF of S)-valued Function;
cluster p +* q -> non halt-free;
coherence
proof
A1: halt S in rng q by Def3;
rng q c= rng(p +* q) by FUNCT_4:18;
hence halt S in rng(p +* q) by A1;
end;
end;
registration
let S be COM-Struct;
let p be finite non halt-free
NAT-defined (the InstructionsF of S)-valued Function,
k be Nat;
cluster Reloc(p,k) -> non halt-free;
coherence
proof
A1: dom p c= NAT by RELAT_1:def 18;
halt S in rng p by Def3;
then consider x being object such that
A2: x in dom p and
A3: p.x = halt S by FUNCT_1:def 3;
A4: x in dom IncAddr(p,k) by A2,Def9;
A5: dom IncAddr(p,k) c= NAT by RELAT_1:def 18;
reconsider m =x as Element of NAT by A1,A2;
IncAddr(p,k).m = IncAddr(p/.m,k) by A2,Def9
.= IncAddr(halt S,k) by A3,A2,PARTFUN1:def 6
.= halt S by COMPOS_0:4;
then halt S in rng IncAddr(p,k) by A4,FUNCT_1:3;
hence halt S in rng Reloc(p,k) by A5,VALUED_1:26;
end;
end;
registration
let S be COM-Struct;
cluster non halt-free non empty for Program of S;
existence
proof
take Stop S;
thus thesis;
end;
end;
::$CT 4
theorem Th25:
for S being COM-Struct
for p,q being
finite NAT-defined (the InstructionsF of S)-valued Function
holds IncAddr(p +* q, n) = IncAddr(p,n) +* IncAddr(q,n)
proof
let S be COM-Struct;
let p,q be
finite NAT-defined (the InstructionsF of S)-valued Function;
A1: dom IncAddr(q,n) = dom q by Def9;
A2: now
let m be Nat such that
A3: m in dom(p +* q);
per cases;
suppose
A4: m in dom q;
A5: (p+*q)/.m = (p +* q). m by A3,PARTFUN1:def 6
.= q. m by A4,FUNCT_4:13
.= q/.m by A4,PARTFUN1:def 6;
thus (IncAddr(p,n) +* IncAddr(q,n)). m = IncAddr(q,n). m by A1,A4,
FUNCT_4:13
.= IncAddr((p+*q)/.m,n) by A4,A5,Def9;
end;
suppose
A6: not m in dom q;
m in dom p \/ dom q by A3,FUNCT_4:def 1;
then
A7: m in dom p by A6,XBOOLE_0:def 3;
A8: (p+*q)/.m = (p +* q). m by A3,PARTFUN1:def 6
.= p. m by A6,FUNCT_4:11
.= p/.m by A7,PARTFUN1:def 6;
thus (IncAddr(p,n) +* IncAddr(q,n)). m = IncAddr(p,n). m by A1,A6,
FUNCT_4:11
.= IncAddr((p+*q)/.m,n) by A7,A8,Def9;
end;
end;
dom IncAddr(p,n) = dom p by Def9;
then dom(IncAddr(p,n) +* IncAddr(q,n)) = dom p \/ dom q by A1,FUNCT_4:def 1
.= dom(p +* q) by FUNCT_4:def 1;
hence IncAddr(p +* q, n) = IncAddr(p,n) +* IncAddr(q,n)
by A2,Def9;
end;
theorem
for S being COM-Struct
for p,q being finite NAT-defined (the InstructionsF of S)-valued Function,
k be Nat
holds Reloc(p+*q,k) = Reloc(p,k)+*Reloc(q,k)
proof
let S be COM-Struct;
let p,q be finite NAT-defined (the InstructionsF of S)-valued Function,
k be Nat;
A1: Reloc(p+*q,k) = IncAddr(Shift(p+*q,k),k) by Th22;
A2: Reloc(p,k) = IncAddr(Shift(p,k),k) by Th22;
A3: Reloc(q,k) = IncAddr(Shift(q,k),k) by Th22;
thus Reloc(p+*q,k)
= IncAddr(Shift(p,k) +* Shift(q,k),k) by A1,VALUED_1:23
.= Reloc(p,k)+*Reloc(q,k) by A2,A3,Th25;
end;
theorem
for S being COM-Struct
for p being finite NAT-defined (the InstructionsF of S)-valued Function,
m,n be Nat
holds Reloc(Reloc(p,m), n) = Reloc(p, m + n)
proof
let S being COM-Struct;
let p being finite NAT-defined (the InstructionsF of S)-valued Function,
m,n be Nat;
thus Reloc(Reloc(p,m),n)
= Shift(Shift(IncAddr(IncAddr(p,m),n),m),n) by Th22
.= Shift(Shift(IncAddr(p, m + n),m),n) by Th8
.= Reloc(p, m + n) by VALUED_1:21;
end;
theorem
for S being COM-Struct
for P,Q being NAT-defined (the InstructionsF of S)-valued finite Function,
k being Nat st
P c= Q holds Reloc(P,k) c= Reloc(Q,k)
proof
let S be COM-Struct;
let P,Q be NAT-defined (the InstructionsF of S)-valued finite Function;
let k be Nat;
set rP = Reloc(P,k);
set rQ = Reloc(Q,k);
A1: dom Reloc(P,k) = {m + k where m is Nat: m in dom P} by Th21;
A2: dom Shift(P,k) = {m + k where m is Nat:
m in dom P} by VALUED_1:def 12;
A3: dom Shift(Q,k) = {m + k where m is Nat:
m in dom Q} by VALUED_1:def 12;
A4: rQ = IncAddr(Shift(Q,k),k) by Th22;
assume
A5: P c= Q;
then
A6: Shift(P,k) c= Shift(Q,k) by VALUED_1:20;
A7: dom P c= dom Q by A5,GRFUNC_1:2;
A8: now
let x be object;
assume x in dom Reloc(P,k);
then consider m1 being Nat such that
A9: x = m1 + k and
A10: m1 in dom P by A1;
A11: (m1 + k) in dom Shift(Q,k) by A7,A3,A10;
A12: (m1 + k) in dom Shift(P,k) by A2,A10;
then
A13: Shift(P,k)/.(m1+k) = Shift(P,k). (
m1 + k) by PARTFUN1:def 6
.= Shift(Q,k). (m1 + k) by A6,A12,GRFUNC_1:2
.= Shift(Q,k)/.(m1+k) by A11,PARTFUN1:def 6;
thus (rP).x = IncAddr(Shift(P,k),k).x by Th22
.= IncAddr(Shift(Q,k)/.(m1+k),k) by A12,A13,A9,Def9
.= (rQ).x by A9,A11,A4,Def9;
end;
A14: dom Shift(P,k) c= dom Shift(Q,k) by A6,GRFUNC_1:2;
now
let x be object;
assume x in dom rP;
then x in dom Shift(P,k) by Th20;
then x in dom Shift(Q,k) by A14;
hence x in dom rQ by Th20;
end;
then dom rP c= dom rQ;
hence thesis by A8,GRFUNC_1:2;
end;
registration let S be COM-Struct;
let P be preProgram of S;
reduce Reloc(P,0) to P;
reducibility;
end;
theorem
for S being COM-Struct
for P being preProgram of S holds Reloc(P,0) = P;
theorem
for S being COM-Struct
for k being Nat holds
for P being preProgram of S holds
il in dom P iff il + k in dom Reloc(P,k)
proof
let S be COM-Struct;
let k be Nat;
let P be preProgram of S;
A1: dom Reloc(P,k) = { j+k where j is Nat: j in dom P } by Th21;
reconsider il1 = il as Element of NAT by ORDINAL1:def 12;
il1 in dom P implies il1 + k in dom Reloc(P,k) by A1;
hence il in dom P implies il + k in dom Reloc(P,k);
assume il + k in dom Reloc(P,k);
then ex j being Nat st il + k = j+k & j in dom P by A1;
hence thesis;
end;
theorem
for S be COM-Struct
for i being Instruction of S
for f being Function of the InstructionsF of S, the InstructionsF of S
st f = (id the InstructionsF of S) +* (halt S .--> i)
for s being finite NAT-defined (the InstructionsF of S)-valued Function
holds IncAddr(f*s,n)
= ((id the InstructionsF of S) +* (halt S .--> IncAddr(i,n)))* IncAddr(s,n)
proof
let S be COM-Struct;
let i be Instruction of S;
let f be Function of the InstructionsF of S, the InstructionsF of
S such that
A1: f = (id the InstructionsF of S) +* (halt S .--> i);
let s be finite NAT-defined (the InstructionsF of S)-valued Function;
rng(halt S .--> IncAddr(i,n)) = {IncAddr(i,n)} by FUNCOP_1:8;
then
A2: rng((id the InstructionsF of S) +* (halt S .--> IncAddr(i,n))
) c= rng(id the InstructionsF of S) \/ {IncAddr(i,n)} by FUNCT_4:17;
A3: rng(id the InstructionsF of S) \/ {IncAddr(i,n)} = the InstructionsF
of S by ZFMISC_1:40;
A4: dom(halt S .--> IncAddr(i,n)) = {halt S};
then
dom((id the InstructionsF of S) +* (halt S .--> IncAddr(i,n))
) = dom(id the InstructionsF of S) \/ {halt S} by FUNCT_4:def 1
.= the InstructionsF of S by ZFMISC_1:40;
then reconsider g = (id the InstructionsF of S) +* (halt S .-->
IncAddr(i,n)) as Function of the InstructionsF of S,the InstructionsF of
S by A2,A3,RELSET_1:4;
A5: dom IncAddr(s,n) = dom s by Def9
.= dom(f*s) by FUNCT_2:123;
A6: dom(halt S .--> i) = {halt S};
A7: now
let m be Nat;
assume
A8: m in dom(f*s);
then
A9: m in dom s by FUNCT_2:123;
per cases;
suppose
A10: s. m = halt S;
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
A11: IncAddr(s,n). m = IncAddr(s/.mm,n) by A9,Def9
.= IncAddr(halt S,n) by A9,A10,PARTFUN1:def 6
.= halt S by COMPOS_0:4;
A12: halt S in {halt S} by TARSKI:def 1;
A13: (f*s)/.m = (f*s). m by A8,PARTFUN1:def 6
.= f.halt S by A9,A10,FUNCT_1:13
.= (halt S .--> i).halt S by A1,A6,A12,FUNCT_4:13
.= i by FUNCOP_1:72;
thus (g*IncAddr(s,n)). m = g.(IncAddr(s,n). m) by A5,A8,FUNCT_1:13
.= (halt S .--> IncAddr(i,n)).(IncAddr(s,n). m) by A4,A11,A12,
FUNCT_4:13
.= IncAddr((f*s)/.m,n) by A11,A13,FUNCOP_1:72;
end;
suppose
A14: s. m <> halt S;
A15: s/.m = s. m by A9,PARTFUN1:def 6;
A16: not IncAddr(s/.m,n) = halt S by A14,A15,COMPOS_0:12;
A17: not s/.m in {halt S} by A14,A15,TARSKI:def 1;
A18: not IncAddr(s/.m,n) in {halt S} by A16,TARSKI:def 1;
A19: (f*s)/.m = (f*s). m by A8,PARTFUN1:def 6
.= f.(s. m) by A9,FUNCT_1:13
.= (id the InstructionsF of S).(s/.m) by A1,A6,A15,A17,FUNCT_4:11
.= s/.m;
thus (g*IncAddr(s,n)). m = g.(IncAddr(s,n). m) by A5,A8,FUNCT_1:13
.= g.IncAddr(s/.m,n) by A9,Def9
.= (id the InstructionsF of S).IncAddr(s/.m,n) by A4,A18,FUNCT_4:11
.= IncAddr((f*s)/.m,n) by A19;
end;
end;
dom(g*IncAddr(s,n)) = dom IncAddr(s,n) by FUNCT_2:123;
hence thesis by A5,A7,Def9;
end;
reserve I,J for Program of S;
theorem
dom I misses dom Reloc(J, card I)
proof
assume
A1: dom I meets dom Reloc(J, card I);
dom Reloc(J, card I) = dom Shift(J,card I) by Th20
.= { l+card I where l is Nat: l in dom J } by VALUED_1:def 12;
then consider x being object such that
A2: x in dom I and
A3: x in { l+card I where l is Nat: l in dom J } by A1,XBOOLE_0:3;
consider l being Nat such that
A4: x = l+card I and
l in dom J by A3;
l+card I < card I by A2,A4,AFINSQ_1:66;
hence contradiction by NAT_1:11;
end;
theorem
for I being preProgram of S holds card Reloc(I, m) = card I
proof let I be preProgram of S;
deffunc U(Nat) = $1;
set B = { l where l is Element of NAT: U(l) in dom I};
A1: for x being set st x in dom I ex d being Element of NAT st x = U(d)
proof
let x be set;
assume
A2: x in dom I;
dom I c= NAT by RELAT_1:def 18;
then reconsider l = x as Element of NAT by A2;
reconsider d = l as Element of NAT;
l = U(d);
hence thesis;
end;
A3: for d1,d2 being Element of NAT st U(d1) = U(d2) holds d1 = d2;
A4: dom I,B are_equipotent from FUNCT_7:sch 3(A1,A3);
defpred Z[Nat] means $1 in dom I;
deffunc V(Nat) = $1+m;
defpred X[Nat] means U($1) in dom I;
set D = { l where l is Element of NAT: X[l]};
set C = { V(l) where l is Element of NAT: l in B };
defpred X[set] means not contradiction;
D is Subset of NAT from DOMAIN_1:sch 7;
then
A5: B c= NAT;
A6: for d1,d2 be Element of NAT st V(d1) = V(d2) holds d1 = d2;
A7: B,C are_equipotent from FUNCT_7:sch 4(A5,A6);
set C = { V(l) where l is Element of NAT:
l in { n where n is Element of NAT: Z[n]} & X[l] },
A = { V(l) where l is Element of NAT: Z[l] & X[l] };
A8: C = { l+m where l is Element of NAT: l in B }
proof
thus C c= { l+m where l is Element of NAT: l in B }
proof
let e be object;
assume e in C;
then ex l being Element of NAT st e = V(l) & l in B;
hence thesis;
end;
let e be object;
assume e in { l+m where l is Element of NAT: l in B };
then ex l being Element of NAT st e = l+m & l in B;
hence thesis;
end;
A = { l+m where l is Nat: l in dom I }
proof
thus A c= { l+m where l is Nat: l in dom I }
proof
let e be object;
assume e in A;
then ex l being Element of NAT st e = V(l) & l in dom I;
hence thesis;
end;
let e be object;
assume e in { l+m where l is Nat: l in dom I };
then consider l being Nat such that
A9: e = l+m & l in dom I;
reconsider l as Element of NAT by ORDINAL1:def 12;
l in dom I by A9;
hence thesis by A9;
end;
then
A10: dom Shift(I,m) = A by VALUED_1:def 12;
C = A from FRAENKEL:sch 14;
then
A11: dom Shift(I,m),dom I are_equipotent by A4,A7,A8,A10,WELLORD2:15;
thus card Reloc(I,m) = card dom Reloc(I,m) by CARD_1:62
.= card dom Shift(I,m) by Th20
.= card dom I by A11,CARD_1:5
.= card I by CARD_1:62;
end;
:: from SCMPDS_5, 2011.05.16, A.T.
reserve i for Instruction of S,
I for Program of S;
theorem
x in dom Load i iff x = 0 by TARSKI:def 1;
reserve loc for Nat;
theorem
loc in dom stop I & (stop I).loc <> halt S implies loc in dom I
proof
assume that
A1: loc in dom stop I and
A2: (stop I).loc <> halt S;
set SS=Stop S, S2=Shift(SS, card I);
A3: stop I = I +* S2 by AFINSQ_1:77;
assume not loc in dom I;
then loc in dom S2 by A1,A3,FUNCT_4:12;
then loc in {l1+ card I where l1 is Nat : l1 in dom SS} by VALUED_1:def 12;
then consider l1 being Nat such that
A4: loc=l1+ card I and
A5: l1 in dom SS;
A6: 0 in dom Stop S by Th2;
A7: (Stop S). 0 = halt S;
l1= 0 by A5,TARSKI:def 1;
hence contradiction by A2,A4,A7,A6,AFINSQ_1:def 3;
end;
theorem
dom Load i = { 0} & (Load i).0 = i;
theorem Th37:
0 in dom Load i by TARSKI:def 1;
theorem Th38:
card Load i = 1
proof
thus card Load i = card dom Load i
.= 1 by CARD_1:30;
end;
theorem Th39:
card stop I = card I + 1
proof
thus card stop I = card I + card Stop S by AFINSQ_1:17
.= card I + 1 by AFINSQ_1:34;
end;
theorem Th40:
card Macro i = 2
proof
thus card Macro i = card Load i + card Stop S by AFINSQ_1:17
.= card (Load i) +1 by AFINSQ_1:34
.= 1+1 by Th38
.=2;
end;
theorem Th41:
0 in dom Macro i & 1 in dom Macro i
proof
card Macro i = 2 by Th40;
hence thesis by AFINSQ_1:66;
end;
theorem Th42:
(Macro i).0 = i
proof
set I=Load i;
0 in dom I by Th37;
hence (Macro i). 0 =I.0 by AFINSQ_1:def 3
.=i;
end;
theorem Th43:
(Macro i).1 = halt S
proof
A1: 0 in dom Stop S by Th2;
A2: (Stop S). 0 = halt S;
1 = (0 qua Nat) + card Load i by Th38;
hence thesis by A2,A1,AFINSQ_1:def 3;
end;
theorem Th44:
x in dom Macro i iff x= 0 or x= 1
proof
set si=Macro i, A = NAT;
A1: card si = 2 by Th40;
hereby
assume
A2: x in dom si;
reconsider l=x as Element of NAT by A2;
reconsider n = l as Element of NAT;
n < 1+1 by A1,A2,AFINSQ_1:66;
then n <= 1 by NAT_1:13;
hence x= 0 or x= 1 by NAT_1:25;
end;
thus thesis by A1,AFINSQ_1:66;
end;
theorem Th45:
dom Macro i = {0,1}
proof
for x be object holds x in dom (Macro i) iff x= 0 or x= 1 by Th44;
hence thesis by TARSKI:def 2;
end;
theorem
loc in dom I implies loc in dom stop I
proof
dom I c= dom (I ^ Stop S) by AFINSQ_1:21;
hence thesis;
end;
theorem
for I being initial preProgram of S st loc in dom I
holds (stop I).loc=I.loc by AFINSQ_1:def 3;
theorem Th48:
card I in dom stop I & (stop I).card I = halt S
proof
A1: (Stop S). 0 = halt S;
A2: 0 in dom Stop S by Th2;
set pI=stop I;
card pI=card I+1 by Th39;
then card I <card pI by XREAL_1:29;
hence card I in dom pI by AFINSQ_1:66;
pI.(0 qua Nat +card I) = halt S by A1,A2,AFINSQ_1:def 3;
hence thesis;
end;
:: from SCMPDS_7, 2011.05.27, A.T.
theorem Th49:
loc in dom I implies Shift(stop I,n).(loc+n)=Shift(I,n).(loc+n)
proof
A1: dom I c= dom (stop I) by AFINSQ_1:21;
reconsider l = loc as Element of NAT by ORDINAL1:def 12;
assume
A2: loc in dom I;
hence Shift(I,n).(loc+n)=I.l by VALUED_1:def 12
.=(stop I).l by A2,AFINSQ_1:def 3
.=Shift(stop I,n).(loc+n) by A2,A1,VALUED_1:def 12;
end;
theorem
Shift(stop I,n). n=Shift(I,n). n
proof
A1: 0 in dom I by AFINSQ_1:66;
thus Shift(stop I,n). n
=Shift(I,n).( 0 qua Nat +n) by A1,Th49
.=Shift(I,n). n;
end;
:: from SCMPDS_5, 2011.05.27,A.T.
registration let S be COM-Struct;
cluster empty for preProgram of S;
existence
proof
reconsider p = <%>the InstructionsF of S as preProgram of S;
take p;
thus thesis;
end;
end;
registration let S be COM-Struct;
cluster empty -> halt-free for preProgram of S;
coherence;
end;
definition
::$CD
let S be COM-Struct;
let IT be NAT-defined (the InstructionsF of S)-valued Function;
redefine attr IT is halt-free means :: redefines halt-free (COMPOS_1, definition)
:Def14: for x being Nat st x in dom IT holds IT.x <> halt S;
compatibility
proof
thus IT is halt-free implies
for x being Nat
st x in dom IT holds IT.x <> halt S
by FUNCT_1:3;
assume
A1: for x being Nat st x in dom IT holds IT.x <> halt S;
assume halt S in rng IT;
then consider x being object such that
A2: x in dom IT and
A3: halt S = IT.x by FUNCT_1:def 3;
thus contradiction by A2,A3,A1;
end;
end;
registration let S be COM-Struct;
cluster halt-free -> unique-halt for non empty preProgram of S;
coherence;
end;
theorem
rng Macro i = {i, halt S}
proof
thus rng Macro i = rng Load i \/ rng Stop S by AFINSQ_1:26
.= {i} \/ rng Stop S by AFINSQ_1:33
.= {i} \/ {halt S} by AFINSQ_1:33
.= {i, halt S} by ENUMSET1:1;
end;
registration let S;
let p be initial preProgram of S;
reduce CutLastLoc stop p to p;
reducibility by AFINSQ_2:83;
end;
theorem
for p being initial preProgram of S
holds CutLastLoc stop p = p;
registration let S be COM-Struct;
let p be halt-free initial preProgram of S;
cluster stop p -> unique-halt;
coherence
proof let k be Nat such that
A1: (stop p).k = halt S and
A2: k in dom stop p;
A3: dom stop p = dom CutLastLoc stop p \/ {LastLoc stop p} by VALUED_1:37;
now assume k in dom CutLastLoc stop p;
then
A4: k in dom p;
then p.k = halt S by A1,AFINSQ_1:def 3;
hence contradiction by Def14,A4;
end;
then k in {LastLoc stop p} by A2,A3,XBOOLE_0:def 3;
hence k = LastLoc stop p by TARSKI:def 1;
end;
end;
registration let S;
let I be Program of S, J be non halt-free Program of S;
cluster I ';' J -> non halt-free;
coherence;
end;
theorem
for I being Program of S holds CutLastLoc stop I = I;
theorem
InsCode halt S = 0;
theorem Th55:
for S being COM-Struct, I being initial preProgram of S
holds card stop I -' 1 = card I
proof let S be COM-Struct, I be initial preProgram of S;
thus card stop I -' 1 = card stop I - 1 by PRE_CIRC:20
.= card I + card Stop S - 1 by AFINSQ_1:17
.= card I + 1 - 1 by AFINSQ_1:34
.= card I;
end;
theorem
for S being COM-Struct, I being initial preProgram of S
holds card stop I = card I + 1
proof let S be COM-Struct, I be initial preProgram of S;
thus card stop I = card I + card Stop S by AFINSQ_1:17
.= card I + 1 by AFINSQ_1:34;
end;
theorem Th57:
LastLoc stop I = card I
proof
thus LastLoc stop I = card stop I -' 1 by AFINSQ_1:70
.= card I by Th55;
end;
registration
let S,I;
cluster stop I -> halt-ending;
coherence
proof
thus (stop I).LastLoc stop I
= (stop I).card I by Th57
.= halt S by Th48;
end;
end;
theorem
Macro IncAddr(i,n) = IncAddr(Macro i,n)
proof
A1: dom Macro IncAddr(i,n) = {0,1} by Th45
.= dom Macro i by Th45;
for m being Nat st m in dom Macro i
holds (Macro IncAddr(i,n)).m = IncAddr((Macro i)/.m,n)
proof let m be Nat;
assume m in dom Macro i;
then per cases by Th44;
suppose
A2: m = 0;
then m in dom Macro i by Th41;
then
A3: (Macro i)/.m = (Macro i).m by PARTFUN1: def 6
.= i by A2,Th42;
thus (Macro IncAddr(i,n)).m = IncAddr(i,n) by A2,Th42
.= IncAddr((Macro i)/.m,n) by A3;
end;
suppose
A4: m = 1;
then m in dom Macro i by Th41;
then
A5: (Macro i)/.m = (Macro i).m by PARTFUN1: def 6
.= halt S by A4,Th43;
thus (Macro IncAddr(i,n)).m = halt S by Th43,A4
.= IncAddr(halt S,n) by COMPOS_0:4
.= IncAddr((Macro i)/.m,n) by A5;
end;
end;
hence thesis by A1,Def9;
end;
theorem
I ';' J = (CutLastLoc I) ^ IncAddr(J,card I -' 1)
proof
card CutLastLoc I = card I -' 1 by VALUED_1:65;
hence I ';' J = (CutLastLoc I) ^ (IncAddr(J,card I -' 1)) by AFINSQ_1:77;
end;
theorem
IncAddr(Macro i,n) = IncAddr(Load i,n) ^ Stop S
proof
A1: dom Macro i = {0,1} by Th45;
A2: dom(IncAddr(Load i,n) ^ Stop S)
= len(IncAddr(Load i,n) ^ Stop S)
.= len IncAddr(Load i,n) + 1 by AFINSQ_1:75
.= len Load i + 1 by Def9
.= 1 + 1 by AFINSQ_1:34
.= {0,1} by CARD_1:50
.= dom Macro i by Th45;
for m being Nat st m in dom Macro i
holds (IncAddr(Load i,n) ^ Stop S).m = IncAddr((Macro i)/.m,n)
proof let m be Nat;
assume m in dom Macro i;
then per cases by A1,TARSKI:def 2;
suppose
A3: m = 0;
A4: 0 in dom Load i by AFINSQ_1:65;
then
A5: (Load i)/.m = (Load i).m by A3,PARTFUN1:def 6;
dom Load i c= dom(Load i ^ Stop S) by AFINSQ_1:21;
then m in dom(Load i ^ Stop S) by A4,A3;
then
A6: (Load i ^ Stop S).m = (Load i ^ Stop S)/.m by PARTFUN1:def 6;
m in dom IncAddr(Load i,n) by Def9,A4,A3;
hence (IncAddr(Load i,n) ^ Stop S).m
= IncAddr(Load i,n).m by AFINSQ_1:def 3
.= IncAddr((Load i)/.m,n) by A4,Def9,A3
.= IncAddr((stop Load i)/.m,n) by A6,A4,AFINSQ_1:def 3,A5,A3
.= IncAddr((Macro i)/.m,n);
end;
suppose
A7: m = 1;
A8: len Load i = 1 by AFINSQ_1:34;
then
A9: len IncAddr(Load i,n) = 1 by Def9;
A10: 0 in dom Stop S by AFINSQ_1:65;
len(Load i ^ Stop S)
= len Load i + len Stop S by AFINSQ_1:def 3
.= len Load i + 1 by AFINSQ_1:34
.= 1 + 1 by AFINSQ_1:34
.= {0,1} by CARD_1:50;
then 1 in dom(Load i ^ Stop S) by TARSKI:def 2;
then
A11: (Load i ^ Stop S)/.m = (Load i ^ Stop S).(1+0) by PARTFUN1:def 6,A7;
A12: (Stop S)/.0 = (Stop S).0 by A10,PARTFUN1:def 6;
thus (IncAddr(Load i,n) ^ Stop S).m
= (IncAddr(Load i,n) ^ Stop S).(1+0) by A7
.= IncAddr(Stop S,n).0 by AFINSQ_1:def 3,A9,A10
.= IncAddr((Stop S)/.0,n) by A10,Def9
.= IncAddr((stop Load i)/.m,n) by A11,A12,AFINSQ_1:def 3,A8,A10
.= IncAddr((Macro i)/.m,n);
end;
end;
hence thesis by A2,Def9;
end;
theorem
for S being COM-Struct, F, G being Program of S,
n being Nat st n < LastLoc F
holds F.n = (F ';' G).n
proof
let S be COM-Struct, F, G be Program of S, f be Nat;
assume f < LastLoc F;
then f < card F - 1 by AFINSQ_1:91;
hence thesis by Lm6;
end;