:: Towards the construction of a model of Mizar concepts
:: by Grzegorz Bancerek
::
:: Received April 21, 2008
:: Copyright (c) 2008 Association of Mizar Users
environ
vocabularies TARSKI, QC_LANG3, PBOOLE, MSUALG_1, CATALG_1, FINSEQ_1, BINOP_1,
BOOLE, CQC_LANG, FINSET_1, FUNCOP_1, CAT_4, UNIALG_2, DTCONSTR, TDGROUP,
FUNCT_1, MATRIX_1, TREES_4, TREES_2, SETFAM_1, SQUARE_1, ORDINAL2,
COMPLEX1, LATTICES, CLASSES1, RELAT_1, AMI_1, MCART_1, MSUALG_2,
MSUALG_3, MATRIX_7, FREEALG, MSAFREE, ZF_REFLE, MSATERM, PROB_1,
ORDERS_1, QUANTAL1, FINSEQ_4, ORDINAL1, WAYBEL_0, ASYMPT_0, ZF_MODEL,
OPPCAT_1, LATTICE3, CARD_5, AOFA_000, FINSEQ_2, CARD_1, PARTFUN1,
FUNCT_4, QC_LANG1, FUNCT_2, ZF_LANG, LANG1, ARYTM, CAT_3, TREES_3,
FACIRC_1, YELLOW_0, YELLOW_1, ABCMIZ_0, ABCMIZ_1, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, SETFAM_1, RELAT_1,
FUNCT_1, RELSET_1, BINOP_1, FINSUB_1, PARTFUN1, PROB_2, FACIRC_1,
ENUMSET1, FUNCT_2, FUNCT_4, CAT_3, FUNCOP_1, ARYTM_0, XCMPLX_0, XXREAL_0,
ORDINAL2, NAT_1, MEMBERED, MCART_1, FINSET_1, CARD_1, NUMBERS, CARD_3,
FINSEQ_1, FINSEQ_2, FINSOP_1, FINSEQ_4, TREES_1, TREES_2, TREES_3,
TREES_4, FUNCT_7, PROB_1, PBOOLE, MATRIX_7, STRUCT_0, LANG1, ORDINAL1,
CLASSES1, CLASSES2, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1,
YELLOW_7, DTCONSTR, MSUALG_1, MSUALG_2, PRE_CIRC, MSAFREE, EQUATION,
MSATERM, CATALG_1, MSAFREE3, AOFA_000;
constructors XBOOLE_0, SUBSET_1, ARYTM_0, XREAL_0, REAL_1, XXREAL_0, CARD_1,
RELAT_1, FUNCT_1, NAT_1, DOMAIN_1, WELLORD2, MATRIX_7, STRUCT_0,
MSUALG_1, ZF_REFLE, MATRIX_2, PBOOLE, MSAFREE, MSAFREE1, CAT_3, FINSET_1,
PROB_1, MCART_1, COMMACAT, FINSEQOP, FINSOP_1, FUNCT_6, FUNCT_7, LANG1,
TREES_9, PRE_CIRC, EQUATION, YELLOW_1, FINSEQ_2, FINSEQ_4, ENUMSET1,
MSUALG_2, MSUALG_3, MSUALG_4, RECDEF_1, DTCONSTR, MSATERM, MSUALG_6,
CATALG_1, LATTICE3, WAYBEL_0, WELLORD1, FACIRC_1, CLASSES1, MSAFREE3,
ZFMISC_1, TREES_3;
registrations XBOOLE_0, SUBSET_1, XREAL_0, ORDINAL1, ORDINAL2, RELSET_1,
FUNCT_1, FINSET_1, STRUCT_0, PBOOLE, MSUALG_1, MSUALG_2, MSUALG_3,
FINSEQ_1, TREES_9, CLASSES2, PARTFUN2, FILTER_0, FINSEQ_5, PRALG_1,
NAT_1, CARD_1, MSAFREE, CANTOR_1, TREES_3, MSAFREE1, PARTFUN1, MSATERM,
ORDERS_2, TREES_2, DTCONSTR, WAYBEL_0, YELLOW_0, YELLOW_1, LATTICE3,
MEMBERED, RELAT_1, INDEX_1, PUA2MSS1, INSTALG1, CATALG_1, MSAFREE3,
FACIRC_1, EQUATION, MSUALG_6, MSUALG_9, PRE_CIRC, WAYBEL_8;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
definitions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, FACIRC_1, FINSEQ_1, FINSEQ_2,
LANG1, LATTICE3, MSAFREE, MSAFREE3, CARD_3, PBOOLE, TREES_3, MSUALG_1,
MSUALG_2, CATALG_1, WAYBEL_0;
theorems TARSKI, XBOOLE_0, XBOOLE_1, TREES_1, PRE_CIRC, XXREAL_0, ZFMISC_1,
FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, SUBSET_1, ENUMSET1, FUNCT_4,
PROB_2, LANG1, MATRIX_7, NAT_1, MCART_1, PBOOLE, FINSET_1, RELAT_1,
RELSET_1, STRUCT_0, ORDINAL3, CARD_1, CARD_3, CARD_5, CLASSES1, ORDINAL1,
SETFAM_1, MSUALG_1, MSUALG_2, TREES_3, TREES_4, FINSEQ_3, FUNCOP_1,
MSAFREE, MSATERM, MSAFREE3, BAGORDER, PARTFUN1, LATTICE3, YELLOW_0,
WAYBEL_0, YELLOW_1, YELLOW_7, DTCONSTR, MSAFREE1, FUNCT_7, GRFUNC_1,
CARD_2;
schemes XBOOLE_0, FUNCT_1, NAT_1, FRAENKEL, WELLORD2, PBOOLE, MSATERM,
DTCONSTR, CLASSES1, FUNCT_2;
begin :: Variables
reserve i for Nat, j for Element of NAT, X,Y,x,y,z for set;
theorem ThF0:
for f being Function holds f.x c= Union f
proof
let f be Function;
x in dom f or not x in dom f; then
f.x in rng f or f.x = {} by FUNCT_1:def 4,12;
hence thesis by XBOOLE_1:2,ZFMISC_1:92;
end;
theorem
for f being Function st Union f = {} holds f.x = {} by ThF0,XBOOLE_1:3;
theorem Th89:
for f being Function
for x,y being set st f = [x,y]
holds x = y
proof let f be Function, x,y be set;
assume f = [x,y]; then
A6: {x} in f & {x,y} in f by TARSKI:def 2; then
consider a,b being set such that
A2: {x} = [a,b] by RELAT_1:def 1;
A5: {a} = {a,b} & x = {a} by A2,ZFMISC_1:8,9;
consider c,d being set such that
A4: {x,y} = [c,d] by A6,RELAT_1:def 1;
A7: x = {c} & y = {c,d} or x = {c,d} & y = {c} by A4,ZFMISC_1:10; then
c = a by A5,ZFMISC_1:8;
hence thesis by A7,A5,A6,A2,A4,FUNCT_1:def 1;
end;
theorem Lem'id:
(id X).:Y c= Y
proof
let x be set;
assume x in (id X).:Y; then
ex y being set st [y,x] in id X & y in Y by RELAT_1:def 13;
hence thesis by RELAT_1:def 10;
end;
theorem Th90:
for S being non void Signature
for X being non-empty ManySortedSet of the carrier of S
for t being Term of S, X
holds t is non pair
proof
let S be non void Signature;
let X be non-empty ManySortedSet of the carrier of S;
let t be Term of S, X;
given x,y being set such that
A1: t = [x,y];
(ex s being SortSymbol of S, v being Element of X.s st t.{} = [v,s])
or t.{} in [:the OperSymbols of S,{the carrier of S}:]
by MSATERM:2; then
(ex s being SortSymbol of S, v being Element of X.s st t.{} = [v,s])
or ex a,b being set st a in the OperSymbols of S &
b in {the carrier of S} & t.{} = [a,b] by ZFMISC_1:def 2; then
{{}} <> {{}, t.{}} by ZFMISC_1:9; then
A4: [{}, t.{}] <> {x} by ZFMISC_1:9;
{} in dom t by TREES_1:47; then
[{}, t.{}] in t by FUNCT_1:def 4; then
[{}, t.{}] = {x,y} & x = y by A1,A4,Th89,TARSKI:def 2;
hence thesis by A4,ENUMSET1:69;
end;
registration
let S be non void Signature;
let X be non empty-yielding ManySortedSet of the carrier of S;
cluster -> non pair Element of Free(S,X);
coherence
proof let e be Element of Free(S,X);
e is Term of S, X \/ ((the carrier of S) --> {0}) by MSAFREE3:9;
hence thesis by Th90;
end;
end;
theorem Th1A:
for x,y,z being set st x in {z}* & y in {z}* & Card x = Card y
holds x = y
proof
let x,y,z be set such that
A1: x in {z}* & y in {z}* and
A2: Card x = Card y;
reconsider x, y as FinSequence of {z} by A1,FINSEQ_1:def 11;
A3: dom x = Seg len x by FINSEQ_1:def 3 .= dom y by A2,FINSEQ_1:def 3;
now let i be Nat; assume i in dom x; then
A4: x .i in rng x & y.i in rng y & rng x c= {z} & rng y c= {z}
by A3,FUNCT_1:def 5;
hence x .i = z by TARSKI:def 1 .= y.i by A4,TARSKI:def 1;
end;
hence thesis by A3,FINSEQ_1:17;
end;
registration
cluster {} -> DTree-yielding;
coherence by TREES_3:23;
end;
definition
let S be non void Signature;
let A be MSAlgebra over S;
mode Subset of A is Subset of Union the Sorts of A;
mode FinSequence of A is FinSequence of Union the Sorts of A;
end;
registration
let S be non void Signature;
let X be non empty-yielding ManySortedSet of S;
cluster -> DTree-yielding FinSequence of Free(S,X);
coherence
proof let p be FinSequence of Free(S,X);
let x be set;
assume x in rng p; then
x is Element of Free(S,X);
hence thesis;
end;
end;
theorem LemExp:
for S being non void Signature
for X being non empty-yielding ManySortedSet of the carrier of S
for t being Element of Free(S,X) holds
(ex s being SortSymbol of S, v being set st
t = root-tree [v,s] & v in X.s) or
ex o being OperSymbol of S,
p being FinSequence of Free(S,X) st
t = [o,the carrier of S]-tree p & len p = len the_arity_of o &
p is DTree-yielding &
p is ArgumentSeq of Sym(o, X\/((the carrier of S)-->{0}))
proof
let S be non void Signature;
let X be non empty-yielding ManySortedSet of the carrier of S;
let t be Element of Free(S,X);
set V = X\/((the carrier of S)-->{0});
reconsider t' = t as Term of S,V by MSAFREE3:9;
defpred P[set] means $1 is Element of Free(S,X) implies
(ex s being SortSymbol of S, v being set st
$1 = root-tree [v,s] & v in X.s) or
ex o being OperSymbol of S,
p being FinSequence of Free(S,X) st
$1 = [o,the carrier of S]-tree p & len p = len the_arity_of o &
p is DTree-yielding & p is ArgumentSeq of Sym(o,V);
A1: for s being SortSymbol of S, v being Element of V.s
holds P[root-tree [v,s]]
proof
let s be SortSymbol of S;
let v be Element of V.s;
set t = root-tree [v,s];
assume
B1: t is Element of Free(S,X);
{} in dom t by TREES_1:47; then
t.{} in rng t by FUNCT_1:12; then
[v,s] in rng t by TREES_4:3; then
v in X.s by B1,MSAFREE3:36;
hence thesis;
end;
A2: for o being OperSymbol of S,
p being ArgumentSeq of Sym(o,V) st
for t being Term of S,V st t in rng p holds P[t]
holds P[[o,the carrier of S]-tree p]
proof
let o be OperSymbol of S;
let p be ArgumentSeq of Sym(o,V) such that
for t being Term of S,V st t in rng p holds P[t];
set t = [o,the carrier of S]-tree p;
assume t is Element of Free(S,X); then
consider s being set such that
B4: s in dom the Sorts of Free(S,X) & t in (the Sorts of Free(S,X)).s
by CARD_5:10;
reconsider s as Element of S by B4,PBOOLE:def 3;
B5: t = Sym(o,V)-tree p & the Sorts of Free(S,X) = S-Terms(X,V) &
the_sort_of(Sym(o,V)-tree p) = the_result_sort_of o
by MSATERM:20,MSAFREE3:25; then
s = the_result_sort_of o by B4,MSAFREE3:18; then
rng p c= Union (S-Terms(X,V)) by B4,B5,MSAFREE3:20; then
p is FinSequence of Free(S,X) &
len the_arity_of o = len p by B5,FINSEQ_1:def 4,MSATERM:22;
hence thesis;
end;
for t being Term of S,V holds P[t] from MSATERM:sch 1(A1,A2); then
P[t'];
hence (ex s being SortSymbol of S, v being set st
t = root-tree [v,s] & v in X.s) or
ex o being OperSymbol of S,
p being FinSequence of Free(S,X) st
t = [o,the carrier of S]-tree p & len p = len the_arity_of o &
p is DTree-yielding & p is ArgumentSeq of Sym(o,V);
end;
definition
let A be set;
func varcl A means:
VARCL:
A c= it &
(for x,y st [x,y] in it holds x c= it) &
for B being set st A c= B & for x,y st [x,y] in B holds x c= B
holds it c= B;
uniqueness
proof let B1, B2 be set; assume
A1: not thesis; then
B1 c= B2 & B2 c= B1;
hence thesis by A1,XBOOLE_0:def 10;
end;
existence
proof
set F = {C where C is Subset of Rank the_rank_of A:
A c= C & for x,y st [x,y] in C holds x c= C};
take D = meet F;
A1: A c= Rank the_rank_of A by CLASSES1:def 8;
A3: now let x,y; assume [x,y] in Rank the_rank_of A; then
{x} in {{x,y},{x}} & {{x,y},{x}} c= Rank the_rank_of A
by TARSKI:def 2,ORDINAL1:def 2;then
x in {x} & {x} c= Rank the_rank_of A
by TARSKI:def 1,ORDINAL1:def 2;
hence x c= Rank the_rank_of A by ORDINAL1:def 2;
end;
Rank the_rank_of A c= Rank the_rank_of A; then
A4: Rank the_rank_of A in F by A1,A3;
hereby let x; assume
A5: x in A;
now let C be set; assume C in F; then
ex B being Subset of Rank the_rank_of A st C = B & A c= B &
for x,y st [x,y] in B holds x c= B;
hence x in C by A5;
end;
hence x in D by A4,SETFAM_1:def 1;
end;
hereby let x,y; assume
A6: [x,y] in D;
thus x c= D
proof let z; assume
A7: z in x;
now let X; assume X in F; then
[x,y] in X &
ex B being Subset of Rank the_rank_of A st X = B & A c= B &
for x,y st [x,y] in B holds x c= B by A6,SETFAM_1:def 1; then
x c= X;
hence z in X by A7;
end;
hence z in D by A4,SETFAM_1:def 1;
end;
end;
let B being set; assume
A8: A c= B & for x,y st [x,y] in B holds x c= B;
set C = B /\ Rank the_rank_of A;
reconsider C as Subset of Rank the_rank_of A by XBOOLE_1:17;
A9: A c= C by A1,A8,XBOOLE_1:19;
now let x,y; assume [x,y] in C; then
[x,y] in B & [x,y] in Rank the_rank_of A by XBOOLE_0:def 3; then
x c= B & x c= Rank the_rank_of A by A3,A8;
hence x c= C by XBOOLE_1:19;
end; then
C in F by A9; then
D c= C & C c= B by SETFAM_1:4,XBOOLE_1:17;
hence D c= B by XBOOLE_1:1;
end;
projectivity;
end;
theorem Th11:
varcl {} = {}
proof
{} c= {} &
(for x,y st [x,y] in {} holds x c= {}) &
for B being set st {} c= B & for x,y st [x,y] in B holds x c= B
holds {} c= B;
hence thesis by VARCL;
end;
theorem Th13:
for A,B being set st A c= B holds varcl A c= varcl B
proof let A, B be set such that
A1: A c= B;
B c= varcl B by VARCL; then
A c= varcl B & (for x,y st [x,y] in varcl B holds x c= varcl B)
by A1,VARCL,XBOOLE_1:1;
hence thesis by VARCL;
end;
theorem Th14:
for A being set holds
varcl union A = union {varcl a where a is Element of A: not contradiction}
proof let A be set;
set X = {varcl a where a is Element of A: not contradiction};
A0: union A c= union X
proof let x; assume x in union A; then
consider Y such that
A3: x in Y & Y in A by TARSKI:def 4;
reconsider Y as Element of A by A3;
Y c= varcl Y by VARCL; then
varcl Y in X & x in varcl Y by A3;
hence thesis by TARSKI:def 4;
end;
now let x,y be set; assume [x,y] in union X; then
consider Y being set such that
A1: [x,y] in Y & Y in X by TARSKI:def 4;
consider a being Element of A such that
A2: Y = varcl a by A1;
x c= Y & Y c= union X by A1,A2,VARCL,ZFMISC_1:92;
hence x c= union X by XBOOLE_1:1;
end;
hence varcl union A c= union X by A0,VARCL;
let x; assume x in union X; then
consider Y being set such that
A4: x in Y & Y in X by TARSKI:def 4;
consider a being Element of A such that
A5: Y = varcl a by A4;
A is empty or A is not empty; then
a in A or a is empty by SUBSET_1:def 2; then
a c= union A by XBOOLE_1:2,ZFMISC_1:92; then
Y c= varcl union A by A5,Th13;
hence thesis by A4;
end;
scheme Sch14{A() -> set, F(set) -> set, P[set]}:
varcl union {F(z) where z is Element of A(): P[z]}
= union {varcl F(z) where z is Element of A(): P[z]}
proof
set Z = {F(z) where z is Element of A(): P[z]};
set X = {varcl F(z) where z is Element of A(): P[z]};
A0: union Z c= union X
proof let x; assume x in union Z; then
consider Y such that
A3: x in Y & Y in Z by TARSKI:def 4;
consider z being Element of A() such that
A4: Y = F(z) & P[z] by A3;
Y c= varcl Y by VARCL; then
varcl Y in X & x in varcl Y by A3,A4;
hence thesis by TARSKI:def 4;
end;
now let x,y be set; assume [x,y] in union X; then
consider Y being set such that
A1: [x,y] in Y & Y in X by TARSKI:def 4;
consider z being Element of A() such that
A2: Y = varcl F(z) & P[z] by A1;
x c= Y & Y c= union X by A1,A2,VARCL,ZFMISC_1:92;
hence x c= union X by XBOOLE_1:1;
end;
hence varcl union Z c= union X by A0,VARCL;
let x; assume x in union X; then
consider Y being set such that
A4: x in Y & Y in X by TARSKI:def 4;
consider z being Element of A() such that
A5: Y = varcl F(z) & P[z] by A4;
F(z) in Z by A5; then
Y c= varcl union Z by A5,Th13,ZFMISC_1:92;
hence thesis by A4;
end;
theorem Th10:
varcl (X \/ Y) = (varcl X) \/ (varcl Y)
proof set A = {varcl a where a is Element of {X,Y}: not contradiction};
X \/ Y = union {X,Y} by ZFMISC_1:93; then
A1: varcl (X \/ Y) = union A by Th14;
A = {varcl X, varcl Y}
proof
thus
now let x; assume x in A; then
consider a being Element of {X,Y} such that
A2: x = varcl a;
a = X or a = Y by TARSKI:def 2;
hence x in {varcl X, varcl Y} by A2,TARSKI:def 2;
end;
let x; assume x in {varcl X, varcl Y}; then
x = varcl X & X in {X,Y} or
x = varcl Y & Y in {X,Y} by TARSKI:def 2;
hence x in A;
end;
hence thesis by A1,ZFMISC_1:93;
end;
theorem Th8:
for A being non empty set
st for a being Element of A holds varcl a = a
holds varcl meet A = meet A
proof let B be non empty set; set A = meet B; assume
A1: for a being Element of B holds varcl a = a;
now thus A c= A;
let x,y; assume
A2: [x,y] in A;
now let Y; assume Y in B; then
[x,y] in Y & Y = varcl Y by A1,A2,SETFAM_1:def 1;
hence x c= Y by VARCL;
end;
hence x c= A by SETFAM_1:6;
end;
hence varcl A c= A by VARCL;
thus thesis by VARCL;
end;
theorem Th9:
varcl ((varcl X) /\ (varcl Y)) = (varcl X) /\ (varcl Y)
proof set A = (varcl X) /\ (varcl Y);
now thus A c= A;
let x,y; assume [x,y] in A; then
[x,y] in varcl X & [x,y] in varcl Y by XBOOLE_0:def 3; then
x c= varcl X & x c= varcl Y by VARCL;
hence x c= A by XBOOLE_1:19;
end;
hence varcl ((varcl X) /\ (varcl Y)) c= (varcl X) /\ (varcl Y) by VARCL;
thus thesis by VARCL;
end;
registration
let A be empty set;
cluster varcl A -> empty;
coherence by Th11;
end;
deffunc F(set,set) =
{[varcl A, j] where A is Subset of $2, j is Element of NAT: A is finite};
definition
func Vars means:
VARSdef:
ex V being ManySortedSet of NAT st
it = Union V &
V.0 = {[{}, i] where i is Element of NAT: not contradiction} &
for n being Nat holds V.(n+1) =
{[varcl A, j] where A is Subset of V.n, j is Element of NAT: A is finite};
existence
proof consider f being Function such that
A1: dom f = NAT and
A2: f.0 = {[{}, i] where i is Element of NAT: not contradiction} and
A3: for n being Nat holds f.(n+1) = F(n,f.n)
from NAT_1:sch 11;
reconsider f as ManySortedSet of NAT by A1,PBOOLE:def 3;
take Union f, V = f;
thus Union f = Union V;
thus V.0 = {[{}, i] where i is Element of NAT: not contradiction} by A2;
let n be Nat;
thus thesis by A3;
end;
uniqueness
proof let A1, A2 be set;
given V1 being ManySortedSet of NAT such that
A1: A1 = Union V1 and
A2: V1.0 = {[{}, i] where i is Element of NAT: not contradiction} and
A3: for n being Nat holds V1.(n+1) = F(n,V1.n);
given V2 being ManySortedSet of NAT such that
B1: A2 = Union V2 and
B2: V2.0 = {[{}, i] where i is Element of NAT: not contradiction} and
B3: for n being Nat holds V2.(n+1) = F(n,V2.n);
C1: dom V1 = NAT by PBOOLE:def 3;
C2: dom V2 = NAT by PBOOLE:def 3;
V1 = V2 from NAT_1:sch 15(C1,A2,A3,C2,B2,B3);
hence thesis by A1,B1;
end;
end;
theorem Lem1:
for V being ManySortedSet of NAT st
V.0 = {[{}, i] where i is Element of NAT: not contradiction} &
for n being Nat holds
V.(n+1) = {[varcl A, j] where A is Subset of V.n, j is Element of NAT:
A is finite}
for i,j being Element of NAT st i <= j holds V.i c= V.j
proof let V be ManySortedSet of NAT such that
A1: V.0 = {[{}, i] where i is Element of NAT: not contradiction} and
A2: for n being Nat holds
V.(n+1) = {[varcl A, j] where A is Subset of V.n, j is Element of NAT:
A is finite};
defpred Q[Nat] means V.0 c= V.$1;
B2: now let j; assume Q[j];
B3: V.(j+1) = {[varcl A, k] where A is Subset of V.j, k is Element of NAT:
A is finite} by A2;
thus Q[j+1]
proof let x; assume x in V.0; then
(ex i being Element of NAT st x = [{}, i]) & {} c= V.j
by A1,XBOOLE_1:2;
hence thesis by B3,Th11;
end;
end;
defpred P[Nat] means for i st i <= $1 holds V.i c= V.$1;
A4: P[ 0 ] by NAT_1:3;
A5: now let j; assume
B4: P[j];
B5: V.j c= V.(j+1)
proof per cases by NAT_1:6;
suppose j = 0;
hence thesis by B2;
end;
suppose ex k being Nat st j = k+1; then
consider k being Nat such that
B6: j = k+1;
reconsider k as Element of NAT by ORDINAL1:def 13;
B7: V.j = {[varcl A, n] where A is Subset of V.k, n is Element of NAT:
A is finite} by A2,B6;
B8: V.(j+1) = {[varcl A, n] where A is Subset of V.j,n is Element of NAT:
A is finite} by A2;
B9: V.k c= V.j by B4,B6,NAT_1:11;
let x; assume x in V.j; then
consider A being Subset of V.k, n being Element of NAT such that
C1: x = [varcl A, n] & A is finite by B7;
A c= V.j by B9,XBOOLE_1:1;
hence thesis by B8,C1;
end;
end;
thus P[j+1]
proof
let i; assume i <= j+1; then
i = j+1 or V.i c= V.j by B4,NAT_1:8;
hence V.i c= V.(j+1) by B5,XBOOLE_1:1;
end;
end;
for j holds P[j] from NAT_1:sch 1(A4,A5);
hence thesis;
end;
theorem Lem2:
for V being ManySortedSet of NAT st
V.0 = {[{}, i] where i is Element of NAT: not contradiction} &
for n being Nat holds
V.(n+1) = {[varcl A, j] where A is Subset of V.n, j is Element of NAT:
A is finite}
for A being finite Subset of Vars
ex i being Element of NAT st A c= V.i
proof let V be ManySortedSet of NAT such that
A1: V.0 = {[{}, i] where i is Element of NAT: not contradiction} and
A2: for n being Nat holds
V.(n+1) = {[varcl A, j] where A is Subset of V.n, j is Element of NAT:
A is finite};
let A be finite Subset of Vars;
A3: Vars = Union V by A1,A2,VARSdef;
defpred P[set,set] means $1 in V.$2;
A4: now let x; assume x in A; then
consider Y such that
A5: x in Y & Y in rng V by A3,TARSKI:def 4;
consider i being set such that
A6: i in dom V & Y = V.i by A5,FUNCT_1:def 5;
take i; thus i in NAT & P[x,i] by A5,A6,PBOOLE:def 3;
end;
consider f being Function such that
A8: dom f = A & rng f c= NAT and
A9: for x st x in A holds P[x,f.x] from WELLORD2:sch 1(A4);
per cases;
suppose A = {}; then A c= V.0 by XBOOLE_1:2;
hence thesis;
end;
suppose A <> {}; then
reconsider B = rng f as finite non empty Subset of NAT
by A8,FINSET_1:26,RELAT_1:65;
reconsider i = max B as Element of NAT by ORDINAL1:def 13;
take i;
let x be set; assume
B1: x in A; then
B2: f.x in B by A8,FUNCT_1:def 5; then
reconsider j = f.x as Element of NAT;
j <= i by B2,PRE_CIRC:def 1; then
V.j c= V.i & x in V.j by A1,A2,A9,B1,Lem1;
hence thesis;
end;
end;
theorem Th15:
{[{}, i] where i is Element of NAT: not contradiction} c= Vars
proof consider V being ManySortedSet of NAT such that
A1: Vars = Union V and
A2: V.0 = {[{}, i] where i is Element of NAT: not contradiction} and
for n being Nat holds
V.(n+1) = {[varcl A, j] where A is Subset of V.n, j is Element of NAT:
A is finite} by VARSdef;
dom V = NAT by PBOOLE:def 3; then
V.0 in rng V by FUNCT_1:def 5;
hence thesis by A1,A2,ZFMISC_1:92;
end;
theorem Lem3:
for A being finite Subset of Vars, i being Nat holds [varcl A, i] in Vars
proof let A be finite Subset of Vars, i be Nat;
consider V being ManySortedSet of NAT such that
A4: Vars = Union V and
A1: V.0 = {[{}, k] where k is Element of NAT: not contradiction} and
A2: for n being Nat holds
V.(n+1) = {[varcl b, j] where b is Subset of V.n, j is Element of NAT:
b is finite} by VARSdef;
consider j being Element of NAT such that
A3: A c= V.j by A1,A2,Lem2;
V.(j+1) = {[varcl B, k] where B is Subset of V.j, k is Element of NAT:
B is finite} & i in NAT by A2,ORDINAL1:def 13; then
[varcl A, i] in V.(j+1) & dom V = NAT by A3,PBOOLE:def 3;
hence thesis by A4,CARD_5:10;
end;
theorem Th16:
Vars = {[varcl A, j] where A is Subset of Vars, j is Element of NAT:
A is finite}
proof consider V being ManySortedSet of NAT such that
A1: Vars = Union V and
A2: V.0 = {[{}, i] where i is Element of NAT: not contradiction} and
A0: for n being Nat holds V.(n+1) =
{[varcl A, j] where A is Subset of V.n, j is Element of NAT: A is finite}
by VARSdef;
set X = {[varcl A, j] where A is Subset of Vars, j is Element of NAT:
A is finite};
B1: dom V = NAT by PBOOLE:def 3;
defpred P[Nat] means V.$1 c= X;
A3: P[ 0]
proof let x; assume x in V.0; then
{} c= Vars & ex i being Element of NAT st x = [{}, i]
by A2,XBOOLE_1:2;
hence thesis by Th11;
end;
A4: now let i be Element of NAT; assume P[i];
A6: V.(i+1) = {[varcl A, j] where A is Subset of V.i, j is Element of NAT:
A is finite} by A0;
thus P[i+1]
proof let x; assume x in V.(i+1); then
consider A being Subset of V.i, j being Element of NAT such that
A7: x = [varcl A, j] & A is finite by A6;
V.i in rng V by B1,FUNCT_1:def 5; then
V.i c= Vars by A1,ZFMISC_1:92; then
A c= Vars by XBOOLE_1:1;
hence thesis by A7;
end;
end;
A8: for i being Element of NAT holds P[i] from NAT_1:sch 1(A3,A4);
now let x; assume x in rng V; then
ex y st y in NAT & x = V.y by B1,FUNCT_1:def 5;
hence x c= X by A8;
end;
hence Vars c= X by A1,ZFMISC_1:94;
let x; assume x in X; then
ex A being Subset of Vars, j being Element of NAT st
x = [varcl A, j] & A is finite;
hence thesis by Lem3;
end;
theorem Th17:
varcl Vars = Vars
proof consider V being ManySortedSet of NAT such that
A1: Vars = Union V and
A2: V.0 = {[{}, i] where i is Element of NAT: not contradiction} and
A3: for n being Nat holds V.(n+1) =
{[varcl A, j] where A is Subset of V.n, j is Element of NAT: A is finite}
by VARSdef;
defpred P[Nat] means varcl(V.$1) = V.$1;
now let x,y; assume [x,y] in V.0; then
ex i being Element of NAT st [x,y] = [{}, i] by A2; then
x = {} by ZFMISC_1:33;
hence x c= V.0 by XBOOLE_1:2;
end; then
varcl (V.0) c= V.0 & V.0 c= varcl (V.0) by VARCL; then
B1: P[ 0] by XBOOLE_0:def 10;
B2: now let i; assume
B3: P[i];
reconsider i' = i as Element of NAT by ORDINAL1:def 13;
B4: V.(i+1) = {[varcl A, j] where A is Subset of V.i, j is Element of NAT:
A is finite} by A3;
now let x,y; assume [x,y] in V.(i+1); then
consider A being Subset of V.i, j being Element of NAT such that
B5: [x,y] = [varcl A, j] & A is finite by B4;
x = varcl A & i <= i+1 by B5,NAT_1:11,ZFMISC_1:33; then
x c= V.i & V.i' c= V.(i'+1) by A2,A3,B3,Th13,Lem1;
hence x c= V.(i+1) by XBOOLE_1:1;
end; then
varcl (V.(i+1)) c= V.(i+1) & V.(i+1) c= varcl (V.(i+1)) by VARCL;
hence P[i+1] by XBOOLE_0:def 10;
end;
B3: P[i] from NAT_1:sch 2(B1,B2);
A4: varcl Vars = union {varcl a where a is Element of rng V: not contradiction}
by A1,Th14;
thus
now let x; assume x in varcl Vars; then
consider Y such that
A5: x in Y & Y in {varcl a where a is Element of rng V: not contradiction}
by A4,TARSKI:def 4;
consider a being Element of rng V such that
A6: Y = varcl a by A5;
consider i being set such that
A7: i in dom V & a = V.i by FUNCT_1:def 5;
reconsider i as Element of NAT by A7,PBOOLE:def 3;
varcl (V.i) = a by B3,A7;
hence x in Vars by A1,A5,A6,A7,CARD_5:10;
end;
thus Vars c= varcl Vars by VARCL;
end;
theorem Lem4:
for X st the_rank_of X is finite holds X is finite
proof let X; assume the_rank_of X is finite; then
the_rank_of X in NAT by CARD_1:103; then
Rank the_rank_of X is finite & X c= Rank the_rank_of X
by CARD_3:57,CLASSES1:def 8;
hence thesis by FINSET_1:13;
end;
theorem Lem5:
the_rank_of varcl X = the_rank_of X
proof
A1: X c= Rank the_rank_of X by CLASSES1:def 8;
set a = the_rank_of X;
a c= succ a & succ a c= succ succ a by ORDINAL3:1; then
a c= succ succ a by XBOOLE_1:1; then
A2: Rank a c= Rank succ succ a by CLASSES1:43;
now let x,y; assume [x,y] in Rank the_rank_of X; then
x in Rank a by A2,CLASSES1:51;
hence x c= Rank the_rank_of X by ORDINAL1:def 2;
end; then
varcl X c= Rank a by A1,VARCL;
hence the_rank_of varcl X c= a by CLASSES1:73;
X c= varcl X by VARCL;
hence thesis by CLASSES1:75;
end;
theorem Lem6:
for X being finite Subset of Rank omega holds X in Rank omega
proof
let X be finite Subset of Rank omega;
deffunc F(set) = the_rank_of $1;
consider f being Function such that
A1: dom f = X and
A2: for x st x in X holds f.x = F(x) from FUNCT_1:sch 3;
A3: rng f c= NAT
proof let y; assume y in rng f; then
consider x such that
A4: x in X & y = f.x by A1,FUNCT_1:def 5;
the_rank_of x in omega by A4,CLASSES1:74;
hence thesis by A2,A4;
end;
per cases;
suppose X = {}; then
the_rank_of X = {} & {} in omega & omega is ordinal
by CLASSES1:79,ORDINAL1:def 12;
hence thesis by CLASSES1:74;
end;
suppose X <> {}; then
reconsider Y = rng f as finite non empty Subset of NAT
by A1,A3,RELAT_1:65,FINSET_1:26;
reconsider mY = max Y as Element of NAT by ORDINAL1:def 13;
set i = 1+mY;
X c= Rank i
proof let x; assume x in X; then
A5: f.x in Y & f.x = the_rank_of x by A1,A2,FUNCT_1:def 5; then
reconsider j = f.x as Element of NAT;
j <= mY by A5,PRE_CIRC:def 1; then
j c= mY by NAT_1:40; then
j in succ mY by ORDINAL1:34; then
succ j c= succ mY & succ mY = i & j in succ j
by NAT_1:39,ORDINAL1:33;
hence thesis by A5,CLASSES1:74;
end; then
the_rank_of X c= i by CLASSES1:73; then
the_rank_of X in succ i & i+1 c= omega & i+1 = succ i
by ORDINAL1:def 2,34,NAT_1:39;
hence thesis by CLASSES1:74;
end;
end;
theorem Lem7:
Vars c= Rank omega
proof consider V being ManySortedSet of NAT such that
A1: Vars = Union V and
A2: V.0 = {[{}, i] where i is Element of NAT: not contradiction} and
A3: for n being Nat holds V.(n+1) =
{[varcl a, j] where a is Subset of V.n, j is Element of NAT: a is finite}
by VARSdef;
let x; assume x in Vars; then
consider i being set such that
A4: i in dom V & x in V.i by A1,CARD_5:10;
reconsider i as Element of NAT by A4,PBOOLE:def 3;
defpred P[Nat] means V.$1 c= Rank omega;
A5: P[ 0]
proof let x; assume x in V.0; then
consider i being Element of NAT such that
B1: x = [{}, i] by A2;
i+1 = succ i by NAT_1:39; then
B3: {} c= i & i in i+1 by XBOOLE_1:2,ORDINAL1:10; then
{} in i+1 & the_rank_of {} = {} & the_rank_of i = i
by ORDINAL1:22,CLASSES1:81; then
{} in Rank (i+1) & i in Rank (i+1) by B3,CLASSES1:74; then
B2: x in Rank succ succ (i+1) by B1,CLASSES1:51;
succ (i+1) = i+1+1 & succ (i+1+1) = i+1+1+1 by NAT_1:39; then
succ succ (i+1) c= omega by ORDINAL1:def 2; then
Rank succ succ (i+1) c= Rank omega by CLASSES1:43;
hence thesis by B2;
end;
A6: now let n be Element of NAT such that
C1: P[n];
C2: V.(n+1) = {[varcl a, j] where a is Subset of V.n, j is Element of NAT:
a is finite} by A3;
thus P[n+1]
proof let x; assume x in V.(n+1); then
consider a being Subset of V.n, j being Element of NAT such that
C3: x = [varcl a, j] & a is finite by C2;
a c= Rank omega by C1,XBOOLE_1:1; then
a in Rank omega by C3,Lem6; then
reconsider i = the_rank_of a as Element of NAT by CLASSES1:74;
reconsider k = j \/ i as Element of NAT by ORDINAL3:15;
C5: the_rank_of varcl a = i & the_rank_of j = j by Lem5,CLASSES1:81;
i c= k & j c= k & k in succ k by XBOOLE_1:7,ORDINAL1:10; then
i in succ k & j in succ k & succ k = k+1
by ORDINAL1:22,NAT_1:39; then
varcl a in Rank (k+1) & j in Rank (k+1) by C5,CLASSES1:74; then
C6: x in Rank succ succ (k+1) by C3,CLASSES1:51;
succ (k+1) = k+1+1 & succ (k+1+1) = k+1+1+1 by NAT_1:39; then
succ succ (k+1) c= omega by ORDINAL1:def 2; then
Rank succ succ (k+1) c= Rank omega by CLASSES1:43;
hence thesis by C6;
end;
end;
for n being Element of NAT holds P[n] from NAT_1:sch 1(A5,A6); then
V.i c= Rank omega;
hence thesis by A4;
end;
theorem Th18:
for A being finite Subset of Vars holds
varcl A is finite Subset of Vars
proof let A be finite Subset of Vars;
A c= Rank omega by Lem7,XBOOLE_1:1; then
A in Rank omega by Lem6; then
the_rank_of A in omega by CLASSES1:74; then
the_rank_of varcl A in omega by Lem5; then
the_rank_of varcl A is finite by CARD_1:103;
hence thesis by Lem4,Th13,Th17;
end;
registration
cluster Vars -> non empty;
correctness
proof consider j being Element of NAT;
[{},j] in {[{}, i] where i is Element of NAT: not contradiction};
hence thesis by Th15;
end;
end;
definition
mode variable is Element of Vars;
end;
registration
let x be variable;
cluster x`1 -> finite;
coherence
proof x in Vars; then
consider A being Subset of Vars, j being Element of NAT such that
A1: x = [varcl A,j] & A is finite by Th16;
x`1 = varcl A by A1,MCART_1:7;
hence thesis by A1,Th18;
end;
end;
notation
let x be variable;
synonym vars x for x`1;
end;
definition
let x be variable;
redefine func vars x -> Subset of Vars;
coherence
proof x in Vars; then
consider A being Subset of Vars, j being Element of NAT such that
A1: x = [varcl A,j] & A is finite by Th16;
x`1 = varcl A by A1,MCART_1:7;
hence thesis by A1,Th18;
end;
end;
theorem
[{}, i] in Vars
proof i in NAT by ORDINAL1:def 13; then
[{}, i] in {[{}, j]: not contradiction};
hence thesis by Th15;
end;
theorem Lem8:
for A being Subset of Vars holds
varcl {[varcl A, j]} = (varcl A) \/ {[varcl A, j]}
proof let A be Subset of Vars;
A2: {[varcl A, j]} c= (varcl A) \/ {[varcl A, j]} &
varcl A c= (varcl A) \/ {[varcl A, j]} by XBOOLE_1:7;
now let x,y; assume
[x,y] in (varcl A) \/ {[varcl A, j]}; then
[x,y] in varcl A or [x,y] in {[varcl A, j]} by XBOOLE_0:def 2; then
[x,y] in varcl A or [x,y] = [varcl A, j] by TARSKI:def 1; then
x c= varcl A or x = varcl A by VARCL,ZFMISC_1:33;
hence x c= (varcl A) \/ {[varcl A, j]} by A2,XBOOLE_1:1;
end;
hence varcl {[varcl A, j]} c= (varcl A) \/ {[varcl A, j]} by A2,VARCL;
A1: {[varcl A, j]} c= varcl {[varcl A, j]} by VARCL;
[varcl A, j] in {[varcl A, j]} by TARSKI:def 1; then
varcl A c= varcl {[varcl A, j]} by A1,VARCL;
hence thesis by A1,XBOOLE_1:8;
end;
theorem Th82:
for x being variable holds varcl {x} = (vars x) \/ {x}
proof let x be variable; x in Vars; then
consider A being Subset of Vars, j such that
A1: x = [varcl A, j] & A is finite by Th16;
varcl {x} = (varcl A) \/ {x} by A1,Lem8;
hence thesis by A1,MCART_1:7;
end;
theorem
for x being variable holds [(vars x) \/ {x}, i] in Vars
proof let x be variable; x in Vars; then
consider A being Subset of Vars, j such that
A1: x = [varcl A, j] & A is finite by Th16;
varcl {x} = (varcl A) \/ {x} & vars x = varcl A & i in NAT
by A1,Lem8,MCART_1:7,ORDINAL1:def 13;
hence thesis by Th16;
end;
begin :: Quasi loci
notation
let R be Relation, A be set;
synonym R dom A for R|A;
end;
definition
func QuasiLoci -> FinSequenceSet of Vars means:
QuasiLociDef:
for p being FinSequence of Vars holds
p in it iff p is one-to-one &
for i st i in dom p holds (p.i)`1 c= rng (p dom i);
existence
proof defpred P[set] means ex p being Function st p = $1 & p is one-to-one &
for i st i in dom p holds (p.i)`1 c= rng (p|i);
consider L being set such that
A1: x in L iff x in Vars* & P[ x ] from XBOOLE_0:sch 1;
L is FinSequenceSet of Vars
proof let x; assume x in L; then
x in Vars* by A1;
hence thesis by FINSEQ_1:def 11;
end; then
reconsider L as FinSequenceSet of Vars;
take L; let p be FinSequence of Vars;
p in L iff p in Vars* & ex q being Function st q = p & q is one-to-one &
for i st i in dom q holds (q.i)`1 c= rng (q|i) by A1;
hence thesis by FINSEQ_1:def 11;
end;
correctness
proof let L1, L2 be FinSequenceSet of Vars such that
A1: for p being FinSequence of Vars holds
p in L1 iff p is one-to-one &
for i st i in dom p holds (p.i)`1 c= rng (p|(i qua set)) and
A2: for p being FinSequence of Vars holds
p in L2 iff p is one-to-one &
for i st i in dom p holds (p.i)`1 c= rng (p|(i qua set));
thus
now let x; assume
A3: x in L1; then
reconsider p = x as FinSequence of Vars by FINSEQ_2:def 3;
p is one-to-one &
for i st i in dom p holds (p.i)`1 c= rng (p|(i qua set)) by A1,A3;
hence x in L2 by A2;
end;
let x; assume
A4: x in L2; then
reconsider p = x as FinSequence of Vars by FINSEQ_2:def 3;
p is one-to-one &
for i st i in dom p holds (p.i)`1 c= rng (p|(i qua set)) by A2,A4;
hence x in L1 by A1;
end;
end;
theorem Th31:
<*>Vars in QuasiLoci
proof
for i st i in dom {} holds ((<*>Vars).i)`1 c= rng ((<*>Vars)|(i qua set));
hence thesis by QuasiLociDef;
end;
registration
cluster QuasiLoci -> non empty;
correctness by Th31;
end;
definition
mode quasi-loci is Element of QuasiLoci;
end;
registration
cluster -> one-to-one quasi-loci;
coherence by QuasiLociDef;
end;
theorem Th32:
for l being one-to-one FinSequence of Vars holds
l is quasi-loci iff
for i being Nat, x being variable st i in dom l & x = l.i
for y being variable st y in vars x
ex j being Nat st j in dom l & j < i & y = l.j
proof let l be one-to-one FinSequence of Vars;
thus
now assume
A1: l is quasi-loci;
let i be Nat, x be variable such that
A2: i in dom l & x = l.i;
let y be variable such that
A3: y in vars x;
vars x c= rng (l|(i qua set)) by A1,A2,QuasiLociDef; then
consider z such that
A4: z in dom (l dom i) & y = (l dom i).z by A3,FUNCT_1:def 5;
dom (l dom i) = dom l /\ i by RELAT_1:90; then
A5: z in dom l & z in i by A4,XBOOLE_0:def 3; then
reconsider z as Element of NAT;
reconsider j = z as Nat;
take j; Card z = z & Card i = i by CARD_1:def 5;
hence j in dom l & j < i & y = l.j by A4,A5,NAT_1:42,FUNCT_1:70;
end;
assume
A6: for i being Nat, x being variable st i in dom l & x = l.i
for y being variable st y in vars x
ex j being Nat st j in dom l & j < i & y = l.j;
now let i; assume
A8: i in dom l; then
l.i in rng l & rng l c= Vars by FUNCT_1:def 5; then
reconsider x = l.i as variable;
thus (l.i)`1 c= rng (l dom i)
proof let y; assume y in (l.i)`1; then
A7: y in vars x; then
reconsider y as variable;
consider j being Nat such that
A9: j in dom l & j < i & y = l.j by A6,A7,A8;
Card i = i & Card j = j by CARD_1:def 5; then
j in i by A9,NAT_1:42;
hence thesis by A9,FUNCT_1:73;
end;
end;
hence thesis by QuasiLociDef;
end;
theorem Th7:
for l being quasi-loci, x being variable holds
l^<*x*> is quasi-loci iff not x in rng l & vars x c= rng l
proof let l be quasi-loci, x be variable;
A1: (l^<*x*>).(1+len l) = x by FINSEQ_1:59;
A2: dom (l^<*x*>) = Seg (len l + len <*x*>) by FINSEQ_1:def 7
.= Seg (len l + 1) by FINSEQ_1:56;
1 <= 1+len l & 1+len l <= 1+len l by NAT_1:11; then
A3: 1+len l in dom (l^<*x*>) by A2;
A4: dom l = Seg len l by FINSEQ_1:def 3;
thus
now assume
B1: l^<*x*> is quasi-loci;
thus not x in rng l
proof assume x in rng l; then
consider a being set such that
B2: a in dom l & x = l.a by FUNCT_1:def 5;
reconsider a as Element of NAT by B2;
B3: (l^<*x*>).a = x by B2,FINSEQ_1:def 7;
a <= len l & len l < 1+len l & dom l c= dom (l^<*x*>)
by A4,B2,FINSEQ_1:3,39,NAT_1:13;
hence thesis by A1,A3,B1,B3,B2,FUNCT_1:def 8;
end;
thus vars x c= rng l
proof let a be set; assume
C1: a in vars x; then
reconsider a as variable;
consider j being Nat such that
C2: j in dom (l^<*x*>) & j < 1+len l & a = (l^<*x*>).j
by A1,A3,B1,C1,Th32;
reconsider j as Element of NAT by ORDINAL1:def 13;
j <= len l & j >= 1 by A2,C2,NAT_1:13,FINSEQ_1:3; then
C3: j in dom l by A4; then
a = l.j by C2,FINSEQ_1:def 7;
hence thesis by C3,FUNCT_1:def 5;
end;
end;
assume
D1: not x in rng l & vars x c= rng l;
EE: (l^<*x*>) is one-to-one
proof let a,b be set; assume
E1: a in dom (l^<*x*>) & b in dom (l^<*x*>) & (l^<*x*>).a = (l^<*x*>).b;
then reconsider a,b as Element of NAT;
E2: a >= 1 & b >= 1 & a <= 1+len l & b <= 1+len l by A2,E1,FINSEQ_1:3; then
(a <= len l or a = 1+len l) & (b <= len l or b = 1+len l)
by NAT_1:8; then
(a in dom l or a = 1+len l) & (b in dom l or b = 1+len l) by A4,E2; then
(a in dom l & l.a = (l^<*x*>).a & l.a in rng l or a = 1+len l) &
(b in dom l & l.b = (l^<*x*>).b & l.b in rng l or b = 1+len l)
by FUNCT_1:def 5,FINSEQ_1:def 7;
hence thesis by FINSEQ_1:59,D1,E1,FUNCT_1:def 8;
end;
now let i be Nat, z be variable; assume
D2: i in dom (l^<*x*>) & z = (l^<*x*>).i; then
D3: i >= 1 & i <= 1+len l & i is Element of NAT by A2,FINSEQ_1:3; then
i <= len l or i = 1+len l by NAT_1:8; then
D9: i in dom l or i = 1+len l & z = x by A4,D2,D3,FINSEQ_1:59;
let y be variable; assume
D5: y in vars z;
thus ex j being Nat st j in dom (l^<*x*>) & j < i & y = (l^<*x*>).j
proof per cases by D9,D2,FINSEQ_1:def 7;
suppose
D8: i = 1+len l & z = x; then
consider k being set such that
D6: k in dom l & y = l.k by D1,D5,FUNCT_1:def 5;
reconsider k as Element of NAT by D6;
take k; dom l c= dom (l^<*x*>) & k <= len l by A4,D6,FINSEQ_1:3,39;
hence thesis by D6,D8,FINSEQ_1:def 7,NAT_1:13;
end;
suppose i in dom l & z = l.i; then
consider j being Nat such that
D7: j in dom l & j < i & y = l.j by D5,Th32;
take j;
dom l c= dom (l^<*x*>) & j is Element of NAT
by ORDINAL1:def 13,FINSEQ_1:39;
hence thesis by D7,FINSEQ_1:def 7;
end;
end;
end;
hence thesis by EE,Th32;
end;
theorem Th6:
for p,q being FinSequence st p^q is quasi-loci
holds p is quasi-loci & q is FinSequence of Vars
proof let p,q be FinSequence; assume
A1: p^q is quasi-loci; then
A2: p is one-to-one FinSequence of Vars by FINSEQ_1:50,FINSEQ_3:98;
now
let i be Nat, x be variable such that
A3: i in dom p & x = p.i;
let y be variable such that
A4: y in vars x;
dom p c= dom (p^q) by FINSEQ_1:39; then
i in dom (p^q) & x = (p^q).i by A3,FINSEQ_1:def 7; then
consider j being Nat such that
A5: j in dom (p^q) & j < i & y = (p^q).j by A1,A4,Th32;
take j;
A6: dom p = Seg len p & dom (p^q) = Seg len (p^q) by FINSEQ_1:def 3; then
A7: j >= 1 & i <= len p by A3,A5,FINSEQ_1:3; then
j < len p by A5,XXREAL_0:2;
hence j in dom p & j < i by A5,A6,A7;
hence y = p.j by A5,FINSEQ_1:def 7;
end;
hence thesis by A1,A2,Th32,FINSEQ_1:50;
end;
theorem
for l being quasi-loci holds varcl rng l = rng l
proof let l be quasi-loci;
now let x,y; assume
A2: [x,y] in rng l; then
reconsider xy = [x,y] as variable;
consider i being set such that
A3: i in dom l & xy = l.i by A2,FUNCT_1:def 5;
reconsider i as Nat by A3,ORDINAL1:def 13;
A5: vars xy = x by MCART_1:7;
thus x c= rng l
proof let a be set; assume
A6: a in x; then
reconsider a as variable by A5;
ex j being Nat st j in dom l & j < i & a = l.j by A3,A5,A6,Th32;
hence thesis by FUNCT_1:def 5;
end;
end;
hence varcl rng l c= rng l by VARCL;
thus rng l c= varcl rng l by VARCL;
end;
theorem Th33:
for x being variable holds
<*x*> is quasi-loci iff vars x = {}
proof let x be variable;
A1: <*x*> = (<*>Vars)^<*x*> by FINSEQ_1:47;
A2: rng {} = {};
vars x c= {} implies vars x = {} by XBOOLE_1:3;
hence thesis by A1,A2,Th7,Th31;
end;
theorem Th34:
for x,y being variable holds
<*x,y*> is quasi-loci iff vars x = {} & x <> y & vars y c= {x}
proof let x,y be variable;
A2: rng <*x*> = {x} by FINSEQ_1:55;
A3: <*x*> is quasi-loci iff vars x = {} by Th33;
y in {x} iff y = x by TARSKI:def 1;
hence thesis by A2,A3,Th6,Th7;
end;
theorem
for x,y,z being variable holds
<*x,y,z*> is quasi-loci iff vars x = {} & x <> y & vars y c= {x} &
x <> z & y <> z & vars z c= {x,y}
proof let x,y,z be variable;
A2: rng <*x,y*> = {x,y} by FINSEQ_2:147;
A3: <*x,y*> is quasi-loci iff vars x = {} & x <> y & vars y c= {x} by Th34;
z in {x,y} iff z = x or z = y by TARSKI:def 2;
hence thesis by A2,A3,Th6,Th7;
end;
definition
let l be quasi-loci;
redefine func l" -> PartFunc of Vars, NAT;
coherence
proof dom (l") = rng l & rng (l") = dom l by FUNCT_1:55;
hence thesis by RELSET_1:11;
end;
end;
begin :: Mizar Constructor Signature
definition
func a_Type equals 0; coherence;
func an_Adj equals 1; coherence;
func a_Term equals 2; coherence;
func * equals 0; coherence;
func non_op equals 1; coherence;
:: func an_ExReg equals 3; coherence;
:: func a_CondReg equals 4; coherence;
:: func a_FuncReg equals 5; coherence;
end;
definition
let C be Signature;
attr C is constructor means:
CONSTRSIGN:
the carrier of C = {a_Type, an_Adj, a_Term} &
{*, non_op} c= the OperSymbols of C &
(the Arity of C).* = <*an_Adj, a_Type*> &
(the Arity of C).non_op = <*an_Adj*> &
(the ResultSort of C).* = a_Type &
(the ResultSort of C).non_op = an_Adj &
for o being Element of the OperSymbols of C st o <> * & o <> non_op
holds (the Arity of C).o in {a_Term}*;
end;
registration
cluster constructor -> non empty non void Signature;
coherence
proof let C be Signature; assume
A1: the carrier of C = {a_Type, an_Adj, a_Term};
assume {*, non_op} c= the OperSymbols of C; then
the OperSymbols of C <> {} by XBOOLE_1:3;
hence thesis by A1,STRUCT_0:def 1,MSUALG_1:def 5;
end;
end;
definition
func MinConstrSign -> strict Signature means:
MINdef:
it is constructor & the OperSymbols of it = {*, non_op};
existence
proof
set A = {a_Type, an_Adj, a_Term};
reconsider t = a_Type, a = an_Adj as Element of A by ENUMSET1:def 1;
reconsider aa = <*a*> as Element of A*;
set C = ManySortedSign(# A, {*, non_op},
(*, non_op) --> (<*a,t*>, aa),
(*, non_op) --> (t, a) #);
reconsider C as non void non empty strict ManySortedSign
by MSUALG_1:def 5;
take C;
thus the carrier of C = {a_Type, an_Adj, a_Term} &
{*, non_op} c= the OperSymbols of C;
thus (the Arity of C).* = <*an_Adj, a_Type*> by FUNCT_4:66;
thus (the Arity of C).non_op = <*an_Adj*> by FUNCT_4:66;
thus (the ResultSort of C).* = a_Type by FUNCT_4:66;
thus (the ResultSort of C).non_op = an_Adj by FUNCT_4:66;
thus thesis by TARSKI:def 2;
end;
correctness
proof let C1, C2 be strict Signature such that
A1: C1 is constructor & the OperSymbols of C1 = {*, non_op} and
A2: C2 is constructor & the OperSymbols of C2 = {*, non_op};
set A = {a_Type, an_Adj, a_Term};
A3: the carrier of C1 = A & the carrier of C2 = A by A1,A2,CONSTRSIGN;
A4: (the Arity of C1).* = <*an_Adj, a_Type*> &
(the Arity of C2).* = <*an_Adj, a_Type*> by A1,A2,CONSTRSIGN;
A5: (the Arity of C1).non_op = <*an_Adj*> &
(the Arity of C2).non_op = <*an_Adj*> by A1,A2,CONSTRSIGN;
A6: (the ResultSort of C1).* = a_Type &
(the ResultSort of C2).* = a_Type by A1,A2,CONSTRSIGN;
A7: (the ResultSort of C1).non_op = an_Adj &
(the ResultSort of C2).non_op = an_Adj by A1,A2,CONSTRSIGN;
dom the Arity of C1 = {*, non_op} & dom the Arity of C2 = {*, non_op}
by A1,A2,FUNCT_2:def 1; then
A8: the Arity of C1 = (*, non_op) --> (<*an_Adj, a_Type*>, <*an_Adj*>) &
the Arity of C2 = (*, non_op) --> (<*an_Adj, a_Type*>, <*an_Adj*>)
by A4,A5,FUNCT_4:69;
dom the ResultSort of C1 = {*, non_op} &
dom the ResultSort of C2 = {*, non_op} by A1,A2,A3,FUNCT_2:def 1; then
the ResultSort of C1 = (*, non_op) --> (a_Type, an_Adj) &
the ResultSort of C2 = (*, non_op) --> (a_Type, an_Adj)
by A6,A7,FUNCT_4:69;
hence thesis by A1,A2,A3,A8;
end;
end;
registration
cluster MinConstrSign -> constructor;
coherence by MINdef;
end;
registration
cluster constructor strict Signature;
existence proof take MinConstrSign; thus thesis; end;
end;
definition
mode ConstructorSignature is constructor Signature;
end;
:: theorem ::?
:: for C being ConstructorSignature holds the carrier of C = 3
:: by CONSTRSIGN,YELLOW11:1;
definition
let C be ConstructorSignature;
let o be OperSymbol of C;
attr o is constructor means:
CNSTR2:
o <> * & o <> non_op;
end;
theorem
for S being ConstructorSignature
for o being OperSymbol of S st o is constructor
holds the_arity_of o = (len the_arity_of o) |-> a_Term
proof let S be ConstructorSignature;
let o be OperSymbol of S such that
A1: o <> * & o <> non_op;
reconsider t = a_Term as Element of {a_Term} by TARSKI:def 1;
len ((len the_arity_of o)|->a_Term) = len the_arity_of o &
the_arity_of o in {a_Term}* & (len the_arity_of o)|->t in {a_Term}*
by A1,CONSTRSIGN,FINSEQ_1:def 11,FINSEQ_2:69;
hence thesis by Th1A;
end;
definition
let C be non empty non void Signature;
attr C is initialized means:
INITIALIZED:
ex m, a being OperSymbol of C st
the_result_sort_of m = a_Type & the_arity_of m = {} & :: set
the_result_sort_of a = an_Adj & the_arity_of a = {}; :: empty
end;
definition
let C be ConstructorSignature;
A1: the carrier of C = {a_Type, an_Adj, a_Term} by CONSTRSIGN;
func a_Type C -> SortSymbol of C equals a_Type;
coherence by A1,ENUMSET1:def 1;
func an_Adj C -> SortSymbol of C equals an_Adj;
coherence by A1,ENUMSET1:def 1;
func a_Term C -> SortSymbol of C equals a_Term;
coherence by A1,ENUMSET1:def 1;
A2: {*, non_op} c= the OperSymbols of C by CONSTRSIGN;
A3: * in {*, non_op} & non_op in {*, non_op} by TARSKI:def 2;
func non_op C -> OperSymbol of C equals non_op;
coherence by A2,A3;
func ast C -> OperSymbol of C equals *;
coherence by A2,A3;
end;
theorem ::?
for C being ConstructorSignature holds
the_arity_of non_op C = <*an_Adj C*> &
the_result_sort_of non_op C = an_Adj C &
the_arity_of ast C = <*an_Adj C, a_Type C*> &
the_result_sort_of ast C = a_Type C by CONSTRSIGN;
definition
func Modes equals [:{a_Type},[:QuasiLoci,NAT:]:]; correctness;
func Attrs equals [:{an_Adj},[:QuasiLoci,NAT:]:]; correctness;
func Funcs equals [:{a_Term},[:QuasiLoci,NAT:]:]; correctness;
end;
registration
cluster Modes -> non empty; coherence;
cluster Attrs -> non empty; coherence;
cluster Funcs -> non empty; coherence;
end;
definition
func Constructors -> non empty set equals
Modes \/ Attrs \/ Funcs;
coherence;
end;
theorem
{*, non_op} misses Constructors
proof assume not thesis; then consider x such that
A1: x in {*, non_op} and
A2: x in Constructors by XBOOLE_0:3;
x in Modes \/ Attrs or x in Funcs by A2,XBOOLE_0:def 2; then
x in Modes or x in Attrs or x in Funcs by XBOOLE_0:def 2; then
consider Y,Z being set such that
A3: x in [:Y,Z:];
consider y,z such that
A4: y in Y & z in Z & [y,z] = x by A3,ZFMISC_1:def 2;
x = * or x = non_op by A1,TARSKI:def 2; then
the_rank_of x = 0 or the_rank_of x = 1 by CLASSES1:81; then
the_rank_of x c= 1 & 1 in succ 1 & succ {} = 0+1
by ORDINAL1:10,XBOOLE_1:2; then
the_rank_of x in succ succ {} by ORDINAL1:22; then
x in Rank succ succ {} by CLASSES1:74;
hence thesis by A4,CLASSES1:33,51;
end;
definition
let x be Element of [:QuasiLoci, NAT:];
redefine
func x`1 -> quasi-loci; coherence by MCART_1:10;
func x`2 -> Element of NAT; coherence by MCART_1:10;
end;
notation
let c be Element of Constructors;
synonym kind_of c for c`1;
end;
definition
let c be Element of Constructors;
redefine
func kind_of c -> Element of {a_Type, an_Adj, a_Term};
coherence
proof
c in Modes \/ Attrs or c in Funcs by XBOOLE_0:def 2; then
c in Modes or c in Attrs or c in Funcs by XBOOLE_0:def 2; then
c`1 in {a_Type} or c`1 in {an_Adj} or c`1 in {a_Term} by MCART_1:10; then
c`1 = a_Type or c`1 = an_Adj or c`1 = a_Term by TARSKI:def 1;
hence thesis by ENUMSET1:def 1;
end;
func c`2 -> Element of [:QuasiLoci, NAT:];
coherence
proof
c in Modes \/ Attrs or c in Funcs by XBOOLE_0:def 2; then
c in Modes or c in Attrs or c in Funcs by XBOOLE_0:def 2;
hence thesis by MCART_1:10;
end;
end;
definition
let c be Element of Constructors;
func loci_of c -> quasi-loci equals c`2`1; coherence;
func index_of c -> Nat equals c`2`2; coherence;
end;
theorem
for c being Element of Constructors holds
(kind_of c = a_Type iff c in Modes) &
(kind_of c = an_Adj iff c in Attrs) &
(kind_of c = a_Term iff c in Funcs)
proof
let x be Element of Constructors;
A1: x in Modes \/ Attrs or x in Funcs by XBOOLE_0:def 2;
(x in Modes implies x`1 in {a_Type}) &
(x in Attrs implies x`1 in {an_Adj}) &
(x in Funcs implies x`1 in {a_Term}) by MCART_1:10;
hence thesis by A1,XBOOLE_0:def 2,TARSKI:def 1;
end;
definition
func MaxConstrSign -> strict ConstructorSignature means:
MAXdef:
the OperSymbols of it = {*, non_op} \/ Constructors &
for o being OperSymbol of it st o is constructor
holds (the ResultSort of it).o = o`1 &
Card ((the Arity of it).o) = Card o`2`1;
existence
proof
set S = {a_Type, an_Adj, a_Term};
set O = {*, non_op} \/ Constructors;
deffunc F(Element of Constructors) = (len loci_of $1)|->a_Term;
consider f being ManySortedSet of Constructors such that
A1: for c being Element of Constructors holds f.c = F(c) from PBOOLE:sch 5;
deffunc G(Element of Constructors) = kind_of $1;
consider g being ManySortedSet of Constructors such that
A2: for c being Element of Constructors holds g.c = G(c) from PBOOLE:sch 5;
reconsider t = a_Type, a = an_Adj, tr = a_Term as Element of S
by ENUMSET1:def 1;
reconsider aa = <*a*> as Element of S*;
set A = f+*(*, non_op)-->(<*a,t*>, aa);
set R = g+*(*, non_op)-->(t, a);
B0: dom (*, non_op)-->(<*a,t*>, aa) = {*, non_op} &
dom (*, non_op)-->(t, a) = {*, non_op} &
dom f = Constructors & dom g = Constructors
by FUNCT_4:65,PBOOLE:def 3; then
A3: dom A = O & dom R = O by FUNCT_4:def 1;
rng f c= S*
proof let y; assume y in rng f; then
consider x such that
B1: x in Constructors & y = f.x by B0,FUNCT_1:def 5;
reconsider x as Element of Constructors by B1;
y = (len loci_of x)|->tr by A1,B1;
hence thesis by FINSEQ_1:def 11;
end; then
A5: rng f \/ rng (*, non_op)-->(<*a,t*>, aa) c= (S*) \/ (S*) by XBOOLE_1:13;
rng g c= S
proof let y; assume y in rng g; then
consider x such that
B2: x in Constructors & y = g.x by B0,FUNCT_1:def 5;
reconsider x as Element of Constructors by B2;
y = kind_of x by A2,B2;
hence thesis;
end; then
A6: rng g \/ rng (*, non_op)-->(t, a) c= S \/ S by XBOOLE_1:13;
rng A c= rng f \/ rng (*, non_op)-->(<*a,t*>, aa) by FUNCT_4:18; then
reconsider A as Function of O, S* by A3,FUNCT_2:4,A5,XBOOLE_1:1;
rng R c= rng g \/ rng (*, non_op)-->(t, a) by FUNCT_4:18; then
reconsider R as Function of O, S by A3,FUNCT_2:4,A6,XBOOLE_1:1;
reconsider Max = ManySortedSign(# S, O, A, R #) as
non empty non void strict Signature by MSUALG_1:def 5;
Max is constructor
proof thus the carrier of Max = {a_Type, an_Adj, a_Term};
thus {*, non_op} c= the OperSymbols of Max by XBOOLE_1:7;
B3: * in {*, non_op} & non_op in {*, non_op} by TARSKI:def 2;
hence (the Arity of Max).* = ((*, non_op)-->(<*a,t*>, aa)).*
by B0,FUNCT_4:14
.= <*an_Adj, a_Type*> by FUNCT_4:66;
thus (the Arity of Max).non_op = ((*, non_op)-->(<*a,t*>, aa)).non_op
by B0,B3,FUNCT_4:14
.= <*an_Adj*> by FUNCT_4:66;
thus (the ResultSort of Max).* = ((*, non_op)-->(t, a)).*
by B0,B3,FUNCT_4:14
.= a_Type by FUNCT_4:66;
thus (the ResultSort of Max).non_op = ((*, non_op)-->(t, a)).non_op
by B0,B3,FUNCT_4:14
.= an_Adj by FUNCT_4:66;
let o be Element of the OperSymbols of Max;
assume o <> * & o <> non_op; then
B4: not o in {*, non_op} by TARSKI:def 2; then
reconsider c = o as Element of Constructors by XBOOLE_0:def 2;
reconsider tr as Element of {a_Term} by TARSKI:def 1;
(the Arity of Max).o = f.c by B0,B4,FUNCT_4:def 1
.= (len loci_of c)|->tr by A1;
hence (the Arity of Max).o in {a_Term}* by FINSEQ_1:def 11;
end; then
reconsider Max as strict ConstructorSignature;
take Max;
thus the OperSymbols of Max = {*, non_op} \/ Constructors;
let o being OperSymbol of Max; assume o <> * & o <> non_op; then
C1: not o in {*, non_op} by TARSKI:def 2; then
reconsider c = o as Element of Constructors by XBOOLE_0:def 2;
thus (the ResultSort of Max).o = g.c by B0,C1,FUNCT_4:def 1 .= o`1 by A2;
thus Card ((the Arity of Max).o) = Card (f.c) by B0,C1,FUNCT_4:def 1
.= Card (F(c) qua set) by A1
.= Card o`2`1 by FINSEQ_2:69;
end;
uniqueness
proof let it1, it2 be strict ConstructorSignature such that
A1: the OperSymbols of it1 = {*, non_op} \/ Constructors and
A2: for o being OperSymbol of it1 st o is constructor
holds (the ResultSort of it1).o = o`1 &
Card ((the Arity of it1).o) = Card o`2`1 and
A3: the OperSymbols of it2 = {*, non_op} \/ Constructors and
A4: for o being OperSymbol of it2 st o is constructor
holds (the ResultSort of it2).o = o`1 &
Card ((the Arity of it2).o) = Card o`2`1;
set S = {a_Type, an_Adj, a_Term};
set O = {*, non_op} \/ Constructors;
A5: the carrier of it1 = S & the carrier of it2 = S by CONSTRSIGN;
BB: now let c be Element of Constructors;
reconsider o1 = c as OperSymbol of it1 by A1,XBOOLE_0:def 2;
reconsider o2 = o1 as OperSymbol of it2 by A1,A3;
assume
B3: c <> * & c <> non_op; then
o1 is constructor & o2 is constructor by CNSTR2; then
B1: Card ((the Arity of it1).o1) = Card (c`2`1 qua set) &
Card ((the Arity of it2).o2) = Card (c`2`1 qua set) by A2,A4;
(the Arity of it1).o1 in {a_Term}* & (the Arity of it2).o2 in {a_Term}*
by B3,CONSTRSIGN; then
reconsider p1 = (the Arity of it1).o1, p2 = (the Arity of it2).o2
as FinSequence of {a_Term} by FINSEQ_1:def 11;
B2: dom p1 = Seg len p1 & dom p2 = Seg len p2 by FINSEQ_1:def 3;
now let i be Nat; assume i in dom p1; then
p1.i in rng p1 & rng p1 c= {a_Term} &
p2.i in rng p2 & rng p2 c= {a_Term} by B1,B2,FUNCT_1:def 5; then
p1.i = a_Term & p2.i = a_Term by TARSKI:def 1;
hence p1.i = p2.i;
end;
hence (the Arity of it1).c = (the Arity of it2).c by B1,B2,FINSEQ_1:17;
end;
now let o be OperSymbol of it1;
o in {*, non_op} or not o in {*, non_op}; then
o = * or o = non_op or o in Constructors & o <> * & o <> non_op
by A1,XBOOLE_0:def 2,TARSKI:def 2; then
(the Arity of it1).o = <*an_Adj,a_Type*> &
(the Arity of it2).o = <*an_Adj,a_Type*> or
(the Arity of it1).o = <*an_Adj*> & (the Arity of it2).o = <*an_Adj*> or
(the Arity of it1).o = (the Arity of it2).o
by BB,CONSTRSIGN;
hence (the Arity of it1).o = (the Arity of it2).o;
end; then
A6: the Arity of it1 = the Arity of it2 by A1,A3,A5,FUNCT_2:113;
now let o be OperSymbol of it1;
reconsider o' = o as OperSymbol of it2 by A1,A3;
not o in {*, non_op} or o in {*,non_op}; then
o = * or o = non_op or o in Constructors & o is constructor &
o' is constructor by A1,CNSTR2,XBOOLE_0:def 2,TARSKI:def 2; then
(the ResultSort of it1).o = a_Type &
(the ResultSort of it2).o = a_Type or
(the ResultSort of it1).o = an_Adj &
(the ResultSort of it2).o = an_Adj or
(the ResultSort of it1).o = o`1 & (the ResultSort of it2).o = o`1
by A2,A4,CONSTRSIGN;
hence (the ResultSort of it1).o = (the ResultSort of it2).o;
end;
hence thesis by A6,A1,A3,A5,FUNCT_2:113;
end;
end;
registration
cluster MinConstrSign -> non initialized;
correctness
proof given m, a being OperSymbol of MinConstrSign such that
the_result_sort_of m = a_Type and
A2: the_arity_of m = {} and
the_result_sort_of a = an_Adj & the_arity_of a = {};
the OperSymbols of MinConstrSign = {*, non_op} by MINdef; then
m = * or m = non_op by TARSKI:def 2;
hence contradiction by A2,CONSTRSIGN;
end;
cluster MaxConstrSign -> initialized;
correctness
proof set m = [a_Type, [{}, 0]], a = [an_Adj, [{}, 0]];
a_Type in {a_Type} & an_Adj in {an_Adj} &
[<*> Vars, 0] in [:QuasiLoci, NAT:]
by Th31,ZFMISC_1:def 2,TARSKI:def 1; then
m in Modes & a in Attrs by ZFMISC_1:def 2; then
m in Modes \/ Attrs & a in Modes \/ Attrs by XBOOLE_0:def 2; then
m in Constructors & a in Constructors &
the OperSymbols of MaxConstrSign = {*, non_op} \/ Constructors
by MAXdef,XBOOLE_0:def 2; then
reconsider m,a as OperSymbol of MaxConstrSign by XBOOLE_0:def 2;
A1: m is constructor & a is constructor by CNSTR2;
take m, a;
thus the_result_sort_of m
= m`1 by A1,MAXdef
.= a_Type by MCART_1:7;
len the_arity_of m = Card m`2`1 by A1,MAXdef .= Card [{}, 0]`1 by MCART_1:7
.= 0 by MCART_1:7,CARD_1:47;
hence the_arity_of m = {} by CARD_2:59;
thus the_result_sort_of a
= a`1 by A1,MAXdef
.= an_Adj by MCART_1:7;
len the_arity_of a = Card a`2`1 by A1,MAXdef .= Card [{}, 0]`1 by MCART_1:7
.= 0 by MCART_1:7,CARD_1:47;
hence the_arity_of a = {} by CARD_2:59;
end;
end;
registration
cluster initialized strict ConstructorSignature;
correctness proof take MaxConstrSign; thus thesis; end;
end;
registration
let C be initialized ConstructorSignature;
cluster constructor OperSymbol of C;
existence
proof
consider m, a being OperSymbol of C such that
A1: the_result_sort_of m = a_Type & the_arity_of m = {} and
the_result_sort_of a = an_Adj & the_arity_of a = {} by INITIALIZED;
take m;
thus m <> * by A1,CONSTRSIGN;
thus thesis by A1,CONSTRSIGN;
end;
end;
begin :: Mizar Expressions
definition
let C be ConstructorSignature;
A0: the carrier of C = {a_Type, an_Adj, a_Term} by CONSTRSIGN;
func MSVars C -> ManySortedSet of the carrier of C means:
MSVARS:
it.a_Type = {} &
it.an_Adj = {} &
it.a_Term = Vars;
uniqueness
proof let V1,V2 be ManySortedSet of the carrier of C such that
A1: V1.a_Type = {} & V1.an_Adj = {} & V1.a_Term = Vars and
A2: V2.a_Type = {} & V2.an_Adj = {} & V2.a_Term = Vars;
now let x; assume x in the carrier of C; then
x = a_Type or x = an_Adj or x = a_Term by A0,ENUMSET1:def 1;
hence V1.x = V2.x by A1,A2;
end;
hence thesis by PBOOLE:3;
end;
existence
proof
deffunc F(set) = IFEQ($1, a_Term, Vars, {});
consider V being ManySortedSet of the carrier of C such that
A1: for x st x in the carrier of C holds V.x = F(x) from PBOOLE:sch 4;
take V;
A2: IFEQ(a_Type, a_Term, Vars, {}) = {} &
IFEQ(an_Adj, a_Term, Vars, {}) = {} &
IFEQ(a_Term, a_Term, Vars, {}) = Vars by FUNCOP_1:def 8;
a_Type in the carrier of C &
an_Adj in the carrier of C &
a_Term in the carrier of C by A0,ENUMSET1:def 1;
hence thesis by A1,A2;
end;
end;
:: theorem ::?
:: for C being ConstructorSignature
:: for x being variable holds
:: (C variables_in root-tree [x, a_Term]).a_Term C = {x} by MSAFREE3:11;
registration
let C be ConstructorSignature;
cluster MSVars C -> non empty-yielding;
coherence
proof take a_Term;
the carrier of C = {a_Type, an_Adj, a_Term} by CONSTRSIGN;
hence a_Term in the carrier of C by ENUMSET1:def 1;
thus thesis by MSVARS;
end;
end;
registration
let C be initialized ConstructorSignature;
cluster Free(C, MSVars C) -> non-empty;
correctness
proof set X = MSVars C;
consider m, a being OperSymbol of C such that
A1: the_result_sort_of m = a_Type & the_arity_of m = {} and
A2: the_result_sort_of a = an_Adj & the_arity_of a = {} by INITIALIZED;
A3: root-tree [m, the carrier of C] in (the Sorts of Free(C, X)).a_Type
by A1,MSAFREE3:6;
A4: root-tree [a, the carrier of C] in (the Sorts of Free(C, X)).an_Adj
by A2,MSAFREE3:6;
consider x being variable;
a_Term C = a_Term & (MSVars C).a_Term = Vars by MSVARS; then
A5: root-tree [x, a_Term] in (the Sorts of Free(C, X)).a_Term by MSAFREE3:5;
assume the Sorts of Free(C, X) is not non-empty; then
{} in rng the Sorts of Free(C, X) by RELAT_1:def 9; then
consider s being set such that
A6: s in dom the Sorts of Free(C, X) & {} = (the Sorts of Free(C, X)).s
by FUNCT_1:def 5;
s in the carrier of C by A6,PBOOLE:def 3; then
s in {a_Type, an_Adj, a_Term} by CONSTRSIGN;
hence thesis by A3,A4,A5,A6,ENUMSET1:def 1;
end;
end;
definition
let S be non void Signature;
let X be non empty-yielding ManySortedSet of the carrier of S;
let t be Element of Free(S,X);
attr t is ground means
Union (S variables_in t) = {};
attr t is compound means:
COMP:
t.{} in [:the OperSymbols of S, {the carrier of S}:];
end;
reserve C for initialized ConstructorSignature,
s for SortSymbol of C,
o for OperSymbol of C,
c for constructor OperSymbol of C;
definition
let C; mode expression of C is Element of Free(C, MSVars C);
end;
definition
let C, s;
mode expression of C, s -> expression of C means:
ELEMENT:
it in (the Sorts of Free(C, MSVars C)).s;
existence
proof consider t being Element of (the Sorts of Free(C, MSVars C)).s;
dom the Sorts of Free(C, MSVars C) = the carrier of C by PBOOLE:def 3; then
t in Union the Sorts of Free(C, MSVars C) by CARD_5:10;
hence thesis;
end;
end;
theorem Th42:
z is expression of C, s iff z in (the Sorts of Free(C, MSVars C)).s
proof
A1: dom the Sorts of Free(C, MSVars C) = the carrier of C by PBOOLE:def 3;
(the Sorts of Free(C, MSVars C)).s c= Union the Sorts of Free(C, MSVars C)
proof let x;
thus thesis by A1,CARD_5:10;
end;
hence thesis by ELEMENT;
end;
definition
let C;
let c such that
A: len the_arity_of c = 0;
func c term -> expression of C equals
[c, the carrier of C]-tree {};
coherence
proof
A1: root-tree [c, the carrier of C] in
(the Sorts of Free(C, MSVars C)).the_result_sort_of c
by MSAFREE3:6,A,CARD_2:59;
dom the Sorts of Free(C, MSVars C) = the carrier of C by PBOOLE:def 3; then
root-tree [c, the carrier of C] in Union (the Sorts of Free(C, MSVars C))
by A1,CARD_5:10;
hence thesis by TREES_4:20;
end;
end;
theorem Th43a:
for o st len the_arity_of o = 1
for a being expression of C st
ex s st s = (the_arity_of o).1 & a is expression of C, s
holds
[o, the carrier of C]-tree <*a*> is expression of C, the_result_sort_of o
proof
let o be OperSymbol of C such that
A: len the_arity_of o = 1;
set X = MSVars C;
set Y = X \/ ((the carrier of C)-->{0});
let a be expression of C;
given s being SortSymbol of C such that
A0: s = (the_arity_of o).1 & a is expression of C, s;
reconsider ta = a as Term of C,Y by MSAFREE3:9;
A2: dom <*ta*> = Seg 1 & dom <*s*> = Seg 1 by FINSEQ_1:55;
A4: the_arity_of o = <*s*> by A,A0,FINSEQ_1:57;
B1: the Sorts of Free(C, X) = C-Terms(X, Y) by MSAFREE3:25;
now let i be Nat; assume i in dom <*ta*>; then
A3: i = 1 by A2,TARSKI:def 1,FINSEQ_1:4;
let t be Term of C, Y; assume t = <*ta*>.i; then
the Sorts of Free(C, X) c= the Sorts of FreeMSA Y & t = a
by B1,A3,FINSEQ_1:57,PBOOLE:def 23; then
(the Sorts of Free(C, X)).s c= (the Sorts of FreeMSA Y).s &
t in (the Sorts of Free(C, X)).s by A0,Th42,PBOOLE:def 5;
hence the_sort_of t = (the_arity_of o).i by A0,A3,MSAFREE3:8;
end; then
reconsider p = <*ta*> as ArgumentSeq of Sym(o, Y) by A2,A4,MSATERM:25;
A5: variables_in (Sym(o, Y)-tree p) c= X
proof let s be set; assume s in the carrier of C; then
reconsider s' = s as SortSymbol of C;
let x; assume x in (variables_in (Sym(o, Y)-tree p)).s; then
consider t being DecoratedTree such that
B2: t in rng p & x in (C variables_in t).s' by MSAFREE3:12;
C variables_in a c= X & rng p = {a} by FINSEQ_1:55,MSAFREE3:28; then
(C variables_in a).s' c= X.s' & t = a by B2,TARSKI:def 1,PBOOLE:def 5;
hence thesis by B2;
end;
set s' = the_result_sort_of o;
A7: the_sort_of (Sym(o, Y)-tree p) = the_result_sort_of o by MSATERM:20;
(the Sorts of Free(C, X)).s' =
{t where t is Term of C,Y: the_sort_of t = s' & variables_in t c= X}
by B1,MSAFREE3:def 6; then
[o, the carrier of C]-tree <*a*> in (the Sorts of Free(C, X)).s' by A5,A7;
hence thesis by Th42;
end;
definition
let C,o such that
A: len the_arity_of o = 1;
let e be expression of C such that
B: ex s being SortSymbol of C st
s = (the_arity_of o).1 & e is expression of C, s;
func o term e -> expression of C equals:
TERM1:
[o, the carrier of C]-tree<*e*>;
coherence by A,B,Th43a;
end;
reserve a,b for expression of C, an_Adj C;
theorem ThNon:
(non_op C)term a is expression of C, an_Adj C &
(non_op C)term a = [non_op, the carrier of C]-tree <*a*>
proof
A1: the_result_sort_of non_op C = an_Adj C &
the_arity_of non_op C = <*an_Adj C*> by CONSTRSIGN; then
A2: len the_arity_of non_op C = 1 & (the_arity_of non_op C).1 = an_Adj C
by FINSEQ_1:57; then
(non_op C)term a = [non_op, the carrier of C]-tree <*a*> by TERM1;
hence thesis by A1,A2,Th43a;
end;
theorem ThNon':
(non_op C)term a = (non_op C)term b implies a = b
proof
assume (non_op C)term a = (non_op C)term b; then
[non_op, the carrier of C]-tree <*a*> = (non_op C)term b by ThNon
.= [non_op, the carrier of C]-tree <*b*> by ThNon; then
<*a*> = <*b*> by TREES_4:15;
hence a = b by FINSEQ_1:97;
end;
registration
let C,a;
cluster (non_op C)term a -> compound;
coherence
proof
(non_op C)term a = [non_op, the carrier of C]-tree <*a*> by ThNon; then
((non_op C)term a).{} = [non_op C, the carrier of C] by TREES_4:def 4;
hence ((non_op C)term a).{} in [:the OperSymbols of C, {the carrier of C}:]
by ZFMISC_1:129;
end;
end;
registration
let C;
cluster compound expression of C;
existence
proof
consider a; (non_op C)term a is compound;
hence thesis;
end;
end;
theorem Th43b:
for o st len the_arity_of o = 2
for a,b being expression of C st
ex s1,s2 being SortSymbol of C st
s1 = (the_arity_of o).1 & s2 = (the_arity_of o).2 &
a is expression of C, s1 & b is expression of C, s2
holds
[o, the carrier of C]-tree <*a,b*> is expression of C, the_result_sort_of o
proof
let o be OperSymbol of C such that
A: len the_arity_of o = 2;
set X = MSVars C;
set Y = X \/ ((the carrier of C)-->{0});
let a,b be expression of C;
given s1,s2 being SortSymbol of C such that
A0: s1 = (the_arity_of o).1 & s2 = (the_arity_of o).2 &
a is expression of C, s1 & b is expression of C, s2;
reconsider ta = a, tb = b as Term of C,Y by MSAFREE3:9;
A2: dom <*ta,tb*> = Seg 2 & dom <*s1,s2*> = Seg 2 by FINSEQ_3:29;
A4: the_arity_of o = <*s1,s2*> by A,A0,FINSEQ_1:61;
B1: the Sorts of Free(C, X) = C-Terms(X, Y) by MSAFREE3:25;
now let i be Nat; assume i in dom <*ta,tb*>; then
A3: i = 1 or i = 2 by A2,TARSKI:def 2,FINSEQ_1:4;
let t be Term of C, Y; assume t = <*ta,tb*>.i; then
the Sorts of Free(C, X) c= the Sorts of FreeMSA Y &
(i = 1 & t = a or i = 2 & t = b)
by B1,A3,FINSEQ_1:61,PBOOLE:def 23; then
(the Sorts of Free(C, X)).s1 c= (the Sorts of FreeMSA Y).s1 &
(the Sorts of Free(C, X)).s2 c= (the Sorts of FreeMSA Y).s2 &
(i = 1 & t in (the Sorts of Free(C, X)).s1 or
i = 2 & t in (the Sorts of Free(C, X)).s2) by A0,Th42,PBOOLE:def 5;
hence the_sort_of t = (the_arity_of o).i by A0,MSAFREE3:8;
end; then
reconsider p = <*ta,tb*> as ArgumentSeq of Sym(o, Y) by A2,A4,MSATERM:25;
A5: variables_in (Sym(o, Y)-tree p) c= X
proof let s be set; assume s in the carrier of C; then
reconsider s' = s as SortSymbol of C;
let x; assume x in (variables_in (Sym(o, Y)-tree p)).s; then
consider t being DecoratedTree such that
B2: t in rng p & x in (C variables_in t).s' by MSAFREE3:12;
C variables_in a c= X & C variables_in b c= X & rng p = {a,b}
by FINSEQ_2:147,MSAFREE3:28; then
(C variables_in a).s' c= X.s' & (C variables_in b).s' c= X.s' &
(t = a or t = b) by B2,TARSKI:def 2,PBOOLE:def 5;
hence thesis by B2;
end;
set s' = the_result_sort_of o;
A7: the_sort_of (Sym(o, Y)-tree p) = the_result_sort_of o by MSATERM:20;
(the Sorts of Free(C, X)).s' =
{t where t is Term of C,Y: the_sort_of t = s' & variables_in t c= X}
by B1,MSAFREE3:def 6; then
[o, the carrier of C]-tree <*a,b*> in (the Sorts of Free(C, X)).s'
by A5,A7;
hence thesis by Th42;
end;
definition
let C,o such that
A: len the_arity_of o = 2;
let e1,e2 be expression of C such that
B: ex s1,s2 being SortSymbol of C st
s1 = (the_arity_of o).1 & s2 = (the_arity_of o).2 &
e1 is expression of C, s1 & e2 is expression of C, s2;
func o term(e1,e2) -> expression of C equals:
TERM2:
[o, the carrier of C]-tree<*e1,e2*>;
coherence by A,B,Th43b;
end;
reserve t, t1,t2 for expression of C, a_Type C;
theorem ThAst:
(ast C)term(a,t) is expression of C, a_Type C &
(ast C)term(a,t) = [ *, the carrier of C]-tree <*a,t*>
proof
A1: the_result_sort_of ast C = a_Type C &
the_arity_of ast C = <*an_Adj C, a_Type C*> by CONSTRSIGN; then
A2: len the_arity_of ast C = 2 & (the_arity_of ast C).1 = an_Adj C &
(the_arity_of ast C).2 = a_Type C by FINSEQ_1:61; then
(ast C)term(a,t) = [ *, the carrier of C]-tree <*a,t*> by TERM2;
hence thesis by A1,A2,Th43b;
end;
theorem
(ast C)term(a,t1) = (ast C)term(b,t2) implies a = b & t1 = t2
proof
assume (ast C)term(a,t1) = (ast C)term(b,t2); then
[ *, the carrier of C]-tree<*a,t1*> = (ast C)term(b,t2) by ThAst
.= [ *, the carrier of C]-tree<*b,t2*> by ThAst; then
<*a,t1*> = <*b,t2*> by TREES_4:15;
hence thesis by FINSEQ_1:98;
end;
registration
let C,a,t;
cluster (ast C)term(a,t) -> compound;
coherence
proof
(ast C)term(a,t) = [ *, the carrier of C]-tree <*a,t*> by ThAst; then
((ast C)term(a,t)).{} = [ast C, the carrier of C] by TREES_4:def 4;
hence ((ast C)term(a,t)).{} in [:the OperSymbols of C, {the carrier of C}:]
by ZFMISC_1:129;
end;
end;
definition
let S be non void Signature;
let s be SortSymbol of S such that
A: ex o being OperSymbol of S st the_result_sort_of o = s;
mode OperSymbol of s -> OperSymbol of S means
the_result_sort_of it = s;
existence by A;
end;
definition
let C be ConstructorSignature;
redefine
func non_op C -> OperSymbol of an_Adj C;
coherence
proof
the_result_sort_of non_op C = an_Adj C by CONSTRSIGN;
hence ex o being OperSymbol of C st the_result_sort_of o = an_Adj C;
thus thesis by CONSTRSIGN;
end;
func ast C -> OperSymbol of a_Type C;
coherence
proof
the_result_sort_of ast C = a_Type C by CONSTRSIGN;
hence ex o being OperSymbol of C st the_result_sort_of o = a_Type C;
thus thesis by CONSTRSIGN;
end;
end;
theorem Th90A:
for s1,s2 being SortSymbol of C st s1 <> s2
for t1 being expression of C, s1
for t2 being expression of C, s2
holds t1 <> t2
proof
set X = MSVars C;
set Y = X \/ ((the carrier of C) --> {0});
consider A being MSSubset of FreeMSA Y such that
A1: Free(C, X) = GenMSAlg A & A = (Reverse Y)""X by MSAFREE3:def 2;
let s1,s2 be SortSymbol of C;
the Sorts of Free(C, X) is MSSubset of FreeMSA Y
by A1,MSUALG_2:def 10; then
the Sorts of Free(C, X) c= the Sorts of FreeMSA Y by PBOOLE:def 23; then
A2: (the Sorts of Free(C,X)).s1 c= (the Sorts of FreeMSA Y).s1 &
(the Sorts of Free(C,X)).s2 c= (the Sorts of FreeMSA Y).s2
by PBOOLE:def 5;
assume s1 <> s2; then
A3: (the Sorts of FreeMSA Y).s1 misses (the Sorts of FreeMSA Y).s2
by PROB_2:def 3;
let t1 be expression of C, s1;
let t2 be expression of C, s2;
t1 in (the Sorts of Free(C,X)).s1 & t2 in (the Sorts of Free(C,X)).s2
by ELEMENT;
hence thesis by A2,A3,XBOOLE_0:3;
end;
begin :: Quasi-terms
definition
let C;
A: (the Sorts of Free(C, MSVars C)).a_Term C c=
Union the Sorts of Free(C, MSVars C)
proof let x;
dom the Sorts of Free(C, MSVars C) = the carrier of C by PBOOLE:def 3;
hence thesis by CARD_5:10;
end;
func QuasiTerms C -> Subset of Free(C, MSVars C) equals
(the Sorts of Free(C, MSVars C)).a_Term C;
coherence by A;
end;
registration
let C;
cluster QuasiTerms C -> non empty constituted-DTrees;
coherence
proof
thus QuasiTerms C is non empty;
let x; assume x in QuasiTerms C; then
x is expression of C;
hence thesis;
end;
end;
definition
let C;
mode quasi-term of C is expression of C, a_Term C;
end;
theorem ::?
z is quasi-term of C iff z in QuasiTerms C by Th42;
definition
let x be variable;
let C;
func x-term C -> quasi-term of C equals
root-tree [x, a_Term];
coherence
proof
(MSVars C).a_Term = Vars & a_Term = a_Term C by MSVARS; then
root-tree [x, a_Term] in QuasiTerms C by MSAFREE3:5;
hence thesis by Th42;
end;
end;
theorem ThT0:
for x1,x2 being variable
for C1,C2 being initialized ConstructorSignature
st x1-term C1 = x2-term C2
holds x1 = x2
proof
let x1,x2 be variable;
let C1,C2 be initialized ConstructorSignature;
assume x1-term C1 = x2-term C2; then
[x1, a_Term] = [x2, a_Term] by TREES_4:4;
hence x1 = x2 by ZFMISC_1:33;
end;
registration
let x be variable;
let C;
cluster x-term C -> non compound;
coherence
proof
a_Term C in the carrier of C; then
a_Term C <> the carrier of C; then
(x-term C).{} = [x, a_Term C] & a_Term C nin {the carrier of C}
by TARSKI:def 1,TREES_4:3;
hence (x-term C).{} nin [:the OperSymbols of C, {the carrier of C}:]
by ZFMISC_1:106;
end;
end;
theorem Th83:
for p being DTree-yielding FinSequence holds
[c, the carrier of C]-tree p is expression of C
iff len p = len the_arity_of c & p in (QuasiTerms C)*
proof set o = c;
A0: o <> * & o <> non_op by CNSTR2;
let p be DTree-yielding FinSequence;
set V = (MSVars C) \/ ((the carrier of C) --> {0});
BB: the Sorts of Free(C, MSVars C) = C-Terms(MSVars C, V) by MSAFREE3:25;
thus
now assume
A2: [o, the carrier of C]-tree p is expression of C; then
CC: [o, the carrier of C]-tree p is Term of C, V by MSAFREE3:9; then
A3: p is ArgumentSeq of Sym(o,V) by MSATERM:1;
hence len p = len the_arity_of o by MSATERM:22;
reconsider q = p as ArgumentSeq of Sym(o,V) by CC,MSATERM:1;
A5: the_sort_of ((Sym(o,V))-tree q) = the_result_sort_of o by MSATERM:20;
A6: variables_in ((Sym(o,V))-tree q) c= MSVars C by A2,MSAFREE3:28;
(C-Terms(MSVars C,V)).the_result_sort_of o =
{t where t is Term of C,V: the_sort_of t = the_result_sort_of o &
variables_in t c= MSVars C} by MSAFREE3:def 6; then
Sym(o,V)-tree p in (C-Terms(MSVars C,V)).the_result_sort_of o
by A5,A6; then
A4: rng p c= Union (C-Terms(MSVars C,V)) by A3,MSAFREE3:20;
rng p c= QuasiTerms C
proof
let a be set; assume
B0: a in rng p; then
reconsider ta = a as expression of C by A4,MSAFREE3:25;
consider i being set such that
B1: i in dom p & a = p.i by B0,FUNCT_1:def 5;
reconsider i as Nat by B1,FINSEQ_3:25;
reconsider t = p.i as Term of C, V by A3,B1,MSATERM:22;
(the Arity of C).o in {a_Term}* by A0,CONSTRSIGN; then
dom p = dom the_arity_of o & the_arity_of o is FinSequence of {a_Term}
by A3,FINSEQ_1:def 11,MSATERM:22; then
(the_arity_of o).i in rng the_arity_of o &
rng the_arity_of o c= {a_Term C}
by B1,FUNCT_1:def 5,FINSEQ_1:def 4; then
(the_arity_of o).i = a_Term C by TARSKI:def 1; then
B2: the_sort_of t = a_Term C by A3,B1,MSATERM:23;
t = ta by B1; then
variables_in t c= MSVars C by MSAFREE3:28; then
t in {T where T is Term of C,V: the_sort_of T = a_Term C &
variables_in T c= MSVars C} by B2; then
t in (C-Terms(MSVars C,V)).a_Term C by MSAFREE3:def 6;
hence thesis by B1,MSAFREE3:24;
end; then
p is FinSequence of QuasiTerms C by FINSEQ_1:def 4;
hence p in (QuasiTerms C)* by FINSEQ_1:def 11;
end;
assume
A3: len p = len the_arity_of o;
assume
A4: p in (QuasiTerms C)*;
C-Terms(MSVars C, V) is opers_closed &
Free(C, MSVars C) = (FreeMSA V)|(C-Terms(MSVars C, V))
by MSAFREE3:22,26; then
the Sorts of Free(C, MSVars C) is ManySortedSubset of
the Sorts of FreeMSA V by MSUALG_2:def 10; then
the Sorts of Free(C, MSVars C) c= the Sorts of FreeMSA V
by PBOOLE:def 23; then
A7: QuasiTerms C c= (the Sorts of FreeMSA V).a_Term C by PBOOLE:def 5;
0B: p is FinSequence of QuasiTerms C by A4,FINSEQ_1:def 11; then
B0: rng p c= QuasiTerms C by FINSEQ_1:def 4;
now
let i be Nat; assume
B1: i in dom p; then
p.i in rng p by FUNCT_1:def 5; then
B3: p.i in QuasiTerms C by B0; then
reconsider t = p.i as expression of C;
(the Arity of C).o in {a_Term}* by A0,CONSTRSIGN; then
dom p = dom the_arity_of o & the_arity_of o is FinSequence of {a_Term}
by A3,FINSEQ_3:31,FINSEQ_1:def 11; then
(the_arity_of o).i in rng the_arity_of o &
rng the_arity_of o c= {a_Term C}
by B1,FUNCT_1:def 5,FINSEQ_1:def 4; then
B2: (the_arity_of o).i = a_Term C by TARSKI:def 1;
reconsider T = t as Term of C,V by MSAFREE3:9;
take T; thus T = p.i;
T in (the Sorts of FreeMSA V).a_Term C by B3,A7; then
T in FreeSort(V, a_Term C) by MSAFREE:def 13;
hence the_sort_of T = (the_arity_of o).i by B2,MSATERM:def 5;
end; then
A5: p is ArgumentSeq of Sym(o,V) by A3,MSATERM:24;
A6: dom the Sorts of Free(C, MSVars C) = the carrier of C by PBOOLE:def 3;
rng p c= Union (C-Terms(MSVars C, V))
by BB,0B,FINSEQ_1:def 4; then
Sym(o,V)-tree p in (C-Terms(MSVars C, V)).the_result_sort_of o
by A5,MSAFREE3:20;
hence [o, the carrier of C]-tree p is expression of C
by BB,A6,CARD_5:10;
end;
reserve p for FinSequence of QuasiTerms C;
definition
let C,c;
let p such that
A: len p = len the_arity_of c;
B: p in (QuasiTerms C)* by FINSEQ_1:def 11;
func c-trm p -> compound expression of C equals:
TERM:
[c, the carrier of C]-tree p;
coherence
proof
reconsider t = [c, the carrier of C]-tree p as expression of C by A,B,Th83;
t.{} = [c, the carrier of C] by TREES_4:def 4; then
t.{} in [:the OperSymbols of C, {the carrier of C}:] by ZFMISC_1:129;
hence thesis by COMP;
end;
end;
theorem Th43c:
len p = len the_arity_of c implies
c-trm p is expression of C, the_result_sort_of c
proof
set X = MSVars C;
set V = X\/((the carrier of C)-->{0});
assume len p = len the_arity_of c; then
A0: Sym(c,V)-tree p = c-trm p by TERM;
A1: the Sorts of Free(C,X) = C-Terms(X,V) by MSAFREE3:25;
c-trm p is Term of C,V by MSAFREE3:9; then
reconsider q = p as ArgumentSeq of Sym(c,V) by A0,MSATERM:1;
rng q c= Union the Sorts of Free(C,X) by FINSEQ_1:def 4; then
c-trm p in (C-Terms(X,V)).the_result_sort_of c by A0,A1,MSAFREE3:20;
hence c-trm p is expression of C, the_result_sort_of c by A1,ELEMENT;
end;
theorem Th100:
for e being expression of C holds
(ex x being variable st e = x-term C) or
(ex c being constructor OperSymbol of C st
ex p being FinSequence of QuasiTerms C st
len p = len the_arity_of c & e = c-trm p) or
(ex a being expression of C, an_Adj C st e = (non_op C)term a) or
(ex a being expression of C, an_Adj C st
ex t being expression of C, a_Type C st e = (ast C)term(a,t))
proof
let t be expression of C;
set X = MSVars C;
set V = X\/((the carrier of C)-->{0});
per cases by LemExp;
suppose
ex s being SortSymbol of C, v being set st
t = root-tree [v,s] & v in X.s; then
consider s being SortSymbol of C, v being set such that
01: t = root-tree [v,s] & v in X.s;
{} in dom t by TREES_1:47; then
t.{} in rng t & the carrier of C = {a_Type, an_Adj, a_Term}
by CONSTRSIGN,FUNCT_1:12; then
02: v in X.s & (s = a_Term or s = an_Adj or s = a_Type)
by 01,ENUMSET1:def 1; then
reconsider v as variable by MSVARS;
t = v-term C by 01,02,MSVARS;
hence thesis;
end;
suppose
ex o being OperSymbol of C,
p being FinSequence of Free(C,X) st
t = [o,the carrier of C]-tree p & len p = len the_arity_of o &
p is DTree-yielding & p is ArgumentSeq of Sym(o,V); then
consider o being OperSymbol of C,
p being FinSequence of Free(C,X) such that
03: t = [o, the carrier of C]-tree p & len p = len the_arity_of o and
04: p is DTree-yielding & p is ArgumentSeq of Sym(o,V);
per cases by CNSTR2;
suppose o = *; then
05: the_arity_of o = <*an_Adj,a_Type*> & o = ast C &
the_result_sort_of o = a_Type by CONSTRSIGN; then
06: dom p = dom the_arity_of o & dom the_arity_of o = Seg 2 &
len the_arity_of o = 2
by 04,MSATERM:22,FINSEQ_3:29,FINSEQ_1:61;
07: 1 in Seg 2 & 2 in Seg 2; then
p.1 in rng p & p.2 in rng p by 06,FUNCT_1:12; then
reconsider p1 = p.1, p2 = p.2 as expression of C;
reconsider t1 = p1, t2 = p2 as Term of C,V by MSAFREE3:9;
08: C variables_in p1 c= X & variables_in t1 = C variables_in t1 &
C variables_in p2 c= X & variables_in t2 = C variables_in t2
by MSAFREE3:28;
09: <*an_Adj,a_Type*>.2 = a_Type C & <*an_Adj,a_Type*>.1 = an_Adj C
by FINSEQ_1:61;
the_sort_of t1 = (the_arity_of o).1 by 04,06,07,MSATERM:23; then
t1 in {q where q is Term of C,V: the_sort_of q = an_Adj C &
variables_in q c= X} by 05,08,09; then
p1 in C-Terms(X,V).an_Adj C by MSAFREE3:def 6; then
p1 in (the Sorts of Free(C,X)).an_Adj C by MSAFREE3:25; then
reconsider a = p1 as expression of C, an_Adj C by ELEMENT;
the_sort_of t2 = (the_arity_of o).2 by 04,06,07,MSATERM:23; then
t2 in {q where q is Term of C,V: the_sort_of q = a_Type C &
variables_in q c= X} by 05,08,09; then
p2 in C-Terms(X,V).a_Type C by MSAFREE3:def 6; then
p2 in (the Sorts of Free(C,X)).a_Type C by MSAFREE3:25; then
reconsider q = p2 as expression of C, a_Type C by ELEMENT;
p = <*a,q*> by 03,06,FINSEQ_1:61; then
t = (ast C)term(a,q) by 03, 05,06,09,TERM2;
hence thesis;
end;
suppose o = non_op; then
05: the_arity_of o = <*an_Adj*> & o = non_op C &
the_result_sort_of o = an_Adj by CONSTRSIGN; then
06: dom p = dom the_arity_of o & dom the_arity_of o = Seg 1 &
len the_arity_of o = 1
by 04,MSATERM:22,FINSEQ_1:55,56;
07: 1 in Seg 1; then
p.1 in rng p by 06,FUNCT_1:12; then
reconsider p1 = p.1 as expression of C;
reconsider t1 = p1 as Term of C,V by MSAFREE3:9;
08: C variables_in p1 c= X & variables_in t1 = C variables_in t1
by MSAFREE3:28;
09: <*an_Adj*>.1 = an_Adj C by FINSEQ_1:57;
the_sort_of t1 = (the_arity_of o).1 by 04,06,07,MSATERM:23; then
t1 in {q where q is Term of C,V: the_sort_of q = an_Adj C &
variables_in q c= X} by 05,08,09; then
p1 in C-Terms(X,V).an_Adj C by MSAFREE3:def 6; then
p1 in (the Sorts of Free(C,X)).an_Adj C by MSAFREE3:25; then
reconsider a = p1 as expression of C, an_Adj C by ELEMENT;
p = <*a*> by 03,06,FINSEQ_1:57; then
t = (non_op C)term(a) by 03,05,06,09,TERM1;
hence thesis;
end;
suppose o is constructor; then
reconsider o as constructor OperSymbol of C;
t = [o, the carrier of C]-tree p by 03; then
p in (QuasiTerms C)* by Th83; then
reconsider p as FinSequence of QuasiTerms C by FINSEQ_1:def 11;
t = o-trm p by 03,TERM;
hence thesis by 03;
end;
end;
end;
theorem ThDiff01:
len p = len the_arity_of c implies c-trm p <> (non_op C)term a
proof
assume len p = len the_arity_of c; then
c-trm p = [c, the carrier of C]-tree p by TERM; then
A0: (c-trm p).{} = [c, the carrier of C] by TREES_4:def 4;
assume c-trm p = (non_op C)term a; then
c-trm p = [non_op, the carrier of C]-tree<*a*> by ThNon; then
[c, the carrier of C] = [non_op, the carrier of C] by A0,TREES_4:def 4;then
c = non_op by ZFMISC_1:33;
hence thesis by CNSTR2;
end;
theorem ThDiff02:
len p = len the_arity_of c implies c-trm p <> (ast C)term(a,t)
proof
assume len p = len the_arity_of c; then
c-trm p = [c, the carrier of C]-tree p by TERM; then
A0: (c-trm p).{} = [c, the carrier of C] by TREES_4:def 4;
assume c-trm p = (ast C)term(a,t); then
c-trm p = [ *, the carrier of C]-tree<*a,t*> by ThAst; then
[c, the carrier of C] = [ *, the carrier of C] by A0,TREES_4:def 4;then
c = * by ZFMISC_1:33;
hence thesis by CNSTR2;
end;
theorem
(non_op C)term a <> (ast C)term(b,t)
proof
assume (non_op C)term a = (ast C)term(b,t); then
(non_op C)term a = [ *, the carrier of C]-tree<*b,t*> by ThAst; then
((non_op C)term a).{} = [ *, the carrier of C] by TREES_4:def 4; then
([non_op,the carrier of C]-tree<*a*>).{} = [ *, the carrier of C]
by ThNon; then
[non_op, the carrier of C] = [ *, the carrier of C] by TREES_4:def 4;
hence thesis by ZFMISC_1:33;
end;
reserve e for expression of C;
theorem ThNon2:
e.{} = [non_op, the carrier of C] implies ex a st e = (non_op C)term a
proof assume
A0: e.{} = [non_op, the carrier of C];
non_op C in the OperSymbols of C; then
A1: e.{} in [:the OperSymbols of C, {the carrier of C}:] by A0,ZFMISC_1:129;
per cases by Th100;
suppose
ex x being variable st e = x-term C;
hence thesis by A1,COMP;
end;
suppose
ex c,p st len p = len the_arity_of c & e = c-trm p; then
consider c being constructor OperSymbol of C,
p being FinSequence of QuasiTerms C such that
A2: len p = len the_arity_of c & e = c-trm p;
e = [c, the carrier of C]-tree p by A2,TERM; then
e.{} = [c, the carrier of C] by TREES_4:def 4; then
non_op = c by A0,ZFMISC_1:33;
hence thesis by CNSTR2;
end;
suppose
ex a st e = (non_op C)term a;
hence thesis;
end;
suppose
ex a,t st e = (ast C)term(a,t); then
consider a,t such that
A3: e = (ast C)term(a,t);
e = [ *, the carrier of C]-tree <*a,t*> by A3,ThAst; then
e.{} = [ *, the carrier of C] by TREES_4:def 4;
hence thesis by A0,ZFMISC_1:33;
end;
end;
theorem ThAst2:
e.{} = [ *, the carrier of C] implies ex a, t st e = (ast C)term(a,t)
proof assume
A0: e.{} = [ *, the carrier of C];
ast C in the OperSymbols of C; then
A1: e.{} in [:the OperSymbols of C, {the carrier of C}:] by A0,ZFMISC_1:129;
per cases by Th100;
suppose
ex x being variable st e = x-term C;
hence thesis by A1,COMP;
end;
suppose
ex c,p st len p = len the_arity_of c & e = c-trm p; then
consider c being constructor OperSymbol of C,
p being FinSequence of QuasiTerms C such that
A2: len p = len the_arity_of c & e = c-trm p;
e = [c, the carrier of C]-tree p by A2,TERM; then
e.{} = [c, the carrier of C] by TREES_4:def 4; then
* = c by A0,ZFMISC_1:33;
hence thesis by CNSTR2;
end;
suppose
ex a being expression of C, an_Adj C st e = (non_op C)term a; then
consider a being expression of C, an_Adj C such that
A3: e = (non_op C)term a;
e = [non_op, the carrier of C]-tree <*a*> by A3,ThNon; then
e.{} = [non_op, the carrier of C] by TREES_4:def 4;
hence thesis by A0,ZFMISC_1:33;
end;
suppose
ex a,t st e = (ast C)term(a,t);
hence thesis;
end;
end;
begin :: Quasi-adjectives
reserve a,a' for expression of C, an_Adj C;
definition
let C,a;
func Non a -> expression of C, an_Adj C equals:
NON'OPA:
a|<* 0 *> if ex a' st a = (non_op C)term a'
otherwise (non_op C)term a;
coherence
proof
thus
now given a' being expression of C, an_Adj C such that
A0: a = (non_op C)term a';
A1: a = [non_op, the carrier of C]-tree <*a'*> by A0,ThNon;
0 < 1 & len <*a'*> = 1 by FINSEQ_1:57; then
a|<* 0*> = <*a'*>.(0+1) by A1,TREES_4:def 4;
hence a|<* 0*> is expression of C, an_Adj C by FINSEQ_1:57;
end;
thus thesis by ThNon;
end;
consistency;
end;
definition
let C,a;
attr a is positive means:
POSITIVE:
not ex a' st a = (non_op C)term a';
end;
registration
let C;
cluster positive expression of C, an_Adj C;
existence
proof consider m, a being OperSymbol of C such that
the_result_sort_of m = a_Type & the_arity_of m = {} and
A2: the_result_sort_of a = an_Adj & the_arity_of a = {} by INITIALIZED;
set X = MSVars C;
root-tree [a, the carrier of C] in (the Sorts of Free(C, X)).an_Adj &
an_Adj C = an_Adj by A2,MSAFREE3:6; then
reconsider v = root-tree [a, the carrier of C] as expression of C, an_Adj C
by Th42;
take v; given a' being expression of C, an_Adj C such that
A1: v = (non_op C)term a';
v = [non_op, the carrier of C]-tree<*a'*> by A1,ThNon; then
[non_op, the carrier of C] = v.{} by TREES_4:def 4
.= [a, the carrier of C] by TREES_4:3; then
a = non_op C by ZFMISC_1:33;
hence contradiction by A2,CONSTRSIGN;
end;
end;
theorem Th44:
for a being positive expression of C, an_Adj C
holds Non a = (non_op C)term a
proof
let a be positive expression of C, an_Adj C;
not ex a' being expression of C, an_Adj C st
a = (non_op C)term a' by POSITIVE;
hence thesis by NON'OPA;
end;
definition
let C,a;
attr a is negative means:
NEGATIVE:
ex a' st a' is positive & a = (non_op C)term a';
end;
registration
let C;
let a be positive expression of C, an_Adj C;
cluster Non a -> negative non positive;
coherence
proof
thus Non a is negative proof take a; thus thesis by Th44; end;
take a; thus thesis by Th44;
end;
end;
registration
let C;
cluster negative non positive expression of C, an_Adj C;
existence
proof consider a being positive expression of C, an_Adj C;
take Non a; thus thesis;
end;
end;
theorem Th45g:
for a being non positive expression of C, an_Adj C
ex a' being expression of C, an_Adj C
st a = (non_op C)term a' & Non a = a'
proof
let a be non positive expression of C, an_Adj C;
consider a' being expression of C, an_Adj C such that
A1: a = (non_op C)term a' by POSITIVE;
A2: a = [non_op, the carrier of C]-tree<*a'*> by A1,ThNon;
take a';
0 < 1 & len <*a'*> = 1 by FINSEQ_1:57; then
a|<* 0*> = <*a'*>.(0+1) by A2,TREES_4:def 4 .= a' by FINSEQ_1:57;
hence thesis by A1,NON'OPA;
end;
theorem Th45:
for a being negative expression of C, an_Adj C
ex a' being positive expression of C, an_Adj C
st a = (non_op C)term a' & Non a = a'
proof
let a be negative expression of C, an_Adj C;
consider a' being expression of C, an_Adj C such that
A1: a' is positive & a = (non_op C)term a' by NEGATIVE;
A2: a = [non_op, the carrier of C]-tree<*a'*> by A1,ThNon;
reconsider a' as positive expression of C, an_Adj C by A1;
take a';
0 < 1 & len <*a'*> = 1 by FINSEQ_1:57; then
a|<* 0*> = <*a'*>.(0+1) by A2,TREES_4:def 4 .= a' by FINSEQ_1:57;
hence thesis by A1,NON'OPA;
end;
theorem Th44b:
for a being non positive expression of C, an_Adj C
holds (non_op C)term (Non a) = a
proof
let a be non positive expression of C, an_Adj C;
consider a' being expression of C, an_Adj C such that
A1: a = (non_op C)term a' & Non a = a' by Th45g;
thus thesis by A1;
end;
registration
let C;
let a be negative expression of C, an_Adj C;
cluster Non a -> positive;
coherence
proof
ex a' being positive expression of C, an_Adj C st
a = (non_op C)term a' & Non a = a' by Th45;
hence thesis;
end;
end;
definition
let C,a;
attr a is regular means:
REG:
a is positive or a is negative;
end;
registration
let C;
cluster positive -> regular non negative expression of C, an_Adj C;
coherence
proof let a be expression of C, an_Adj C; assume
A1: a is positive;
hence a is regular by REG;
thus
not ex a' being expression of C, an_Adj C st a' is positive &
a = (non_op C)term a' by A1,POSITIVE;
end;
cluster negative -> regular non positive expression of C, an_Adj C;
coherence
proof let a be expression of C, an_Adj C; assume
A1: a is negative;
hence a is regular by REG;
ex a' being expression of C, an_Adj C st a' is positive &
a = (non_op C)term a' by A1,NEGATIVE;
hence
ex a' being expression of C, an_Adj C st a = (non_op C)term a';
end;
end;
registration
let C;
cluster regular expression of C, an_Adj C;
existence
proof
consider a being positive expression of C, an_Adj C;
take a; thus thesis;
end;
end;
definition
let C;
set X = {a: a is regular};
B: X c= Union the Sorts of Free(C, MSVars C)
proof let x; assume x in X; then
ex a st x = a & a is regular;
hence thesis;
end;
func QuasiAdjs C -> Subset of Free(C, MSVars C) equals {a: a is regular};
coherence by B;
end;
registration
let C;
cluster QuasiAdjs C -> non empty constituted-DTrees;
coherence
proof consider v being positive expression of C, an_Adj C;
v in {a: a is regular};
hence QuasiAdjs C is non empty;
let x; assume x in QuasiAdjs C; then
x is expression of C;
hence thesis;
end;
end;
definition
let C; mode quasi-adjective of C is regular expression of C, an_Adj C;
end;
theorem Th52:
z is quasi-adjective of C iff z in QuasiAdjs C
proof
z in QuasiAdjs C iff
ex a st z = a & a is regular;
hence thesis;
end;
theorem ::?
z is quasi-adjective of C iff
z is positive expression of C, an_Adj C or
z is negative expression of C, an_Adj C by REG;
registration
let C;
cluster non positive -> negative quasi-adjective of C;
coherence by REG;
cluster non negative -> positive quasi-adjective of C;
coherence by REG;
end;
registration
let C;
cluster positive quasi-adjective of C;
existence
proof consider a being positive expression of C, an_Adj C;
a is quasi-adjective of C;
hence thesis;
end;
cluster negative quasi-adjective of C;
existence
proof consider a being negative expression of C, an_Adj C;
a is quasi-adjective of C;
hence thesis;
end;
end;
theorem ThPos:
for a being positive quasi-adjective of C
ex v being constructor OperSymbol of C st the_result_sort_of v = an_Adj C &
ex p st len p = len the_arity_of v & a = v-trm p
proof
let e be positive quasi-adjective of C;
per cases by Th100;
suppose
ex x being variable st e = x-term C;
hence thesis by Th90A;
end;
suppose
ex c being constructor OperSymbol of C st
ex p being FinSequence of QuasiTerms C st
len p = len the_arity_of c & e = c-trm p; then
consider c being constructor OperSymbol of C,
p being FinSequence of QuasiTerms C such that
A2: len p = len the_arity_of c & e = c-trm p;
take c;
e is expression of C, the_result_sort_of c by A2,Th43c;
hence the_result_sort_of c = an_Adj C by Th90A;
take p; thus len p = len the_arity_of c & e = c-trm p by A2;
end;
suppose
ex a st e = (non_op C)term a;
hence thesis by POSITIVE;
end;
suppose
ex a,t st e = (ast C)term(a,t); then
e is expression of C, a_Type C by ThAst;
hence thesis by Th90A;
end;
end;
theorem ThPos2:
for v being constructor OperSymbol of C
st the_result_sort_of v = an_Adj C & len p = len the_arity_of v
holds v-trm p is positive quasi-adjective of C
proof
let v be constructor OperSymbol of C such that
A0: the_result_sort_of v = an_Adj C;
assume
A1: len p = len the_arity_of v; then
reconsider a = v-trm p as expression of C, an_Adj C by A0,Th43c;
a is positive
proof
assume ex a' st a = (non_op C)term a';
hence thesis by A1,ThDiff01;
end; then
a is positive expression of C, an_Adj C;
hence v-trm p is positive quasi-adjective of C;
end;
registration
let C;
let a be quasi-adjective of C;
cluster Non a -> regular;
coherence
proof per cases by REG;
suppose a is positive; then
reconsider a' = a as positive expression of C, an_Adj C;
Non a' is negative;
hence thesis;
end;
suppose a is negative; then
reconsider a' = a as negative expression of C, an_Adj C;
Non a' is positive;
hence thesis;
end;
end;
end;
theorem Th46:
for a being quasi-adjective of C
holds Non Non a = a
proof
let a be quasi-adjective of C;
per cases by REG;
suppose a is positive; then
reconsider a' = a as positive expression of C, an_Adj C;
consider b being positive expression of C, an_Adj C such that
A1: Non a' = (non_op C)term b & Non Non a' = b by Th45;
Non a' = (non_op C)term a by Th44;
hence thesis by A1,ThNon';
end;
suppose a is negative; then
reconsider a' = a as negative expression of C, an_Adj C;
ex b being positive expression of C, an_Adj C st
a' = (non_op C)term b & Non a' = b by Th45;
hence thesis by Th44;
end;
end;
theorem
for a1,a2 being quasi-adjective of C
st Non a1 = Non a2 holds a1 = a2
proof
let a1,a2 be quasi-adjective of C;
Non Non a1 = a1 & Non Non a2 = a2 by Th46;
hence thesis;
end;
theorem
for a being quasi-adjective of C
holds Non a <> a
proof
let a be quasi-adjective of C;
per cases by REG;
suppose a is positive; then
reconsider a' = a as positive quasi-adjective of C;
Non a' is negative quasi-adjective of C;
hence thesis;
end;
suppose a is negative; then
reconsider a' = a as negative quasi-adjective of C;
Non a' is positive quasi-adjective of C;
hence thesis;
end;
end;
begin :: Quasi-types
definition
let C;
let q be expression of C, a_Type C;
attr q is pure means:
PURE:
not ex a, t st q = (ast C)term(a,t);
end;
theorem ThP:
for m being OperSymbol of C
st the_result_sort_of m = a_Type & the_arity_of m = {}
ex t st t = root-tree [m, the carrier of C] & t is pure
proof
let m be OperSymbol of C such that
A2: the_result_sort_of m = a_Type & the_arity_of m = {};
set X = MSVars C;
root-tree [m, the carrier of C] in (the Sorts of Free(C, X)).a_Type &
a_Type C = a_Type by A2,MSAFREE3:6; then
reconsider T = root-tree [m, the carrier of C] as expression of C, a_Type C
by Th42;
take T; thus T = root-tree [m, the carrier of C];
given a,t such that
A1: T = (ast C)term(a,t);
T = [ *, the carrier of C]-tree<*a,t*> by A1,ThAst; then
[ *, the carrier of C] = T.{} by TREES_4:def 4
.= [m, the carrier of C] by TREES_4:3; then
m = ast C by ZFMISC_1:33;
hence contradiction by A2,CONSTRSIGN;
end;
theorem ThP2:
for v being OperSymbol of C
st the_result_sort_of v = an_Adj & the_arity_of v = {}
ex a st a = root-tree [v, the carrier of C] & a is positive
proof
let m be OperSymbol of C such that
A2: the_result_sort_of m = an_Adj & the_arity_of m = {};
set X = MSVars C;
root-tree [m, the carrier of C] in (the Sorts of Free(C, X)).an_Adj
by A2,MSAFREE3:6; then
reconsider T = root-tree [m, the carrier of C] as expression of C, an_Adj C
by Th42;
take T; thus T = root-tree [m, the carrier of C];
given a being expression of C, an_Adj C such that
A1: T = (non_op C)term a;
T = [non_op, the carrier of C]-tree<*a*> by A1,ThNon; then
[non_op, the carrier of C] = T.{} by TREES_4:def 4
.= [m, the carrier of C] by TREES_4:3; then
m = non_op by ZFMISC_1:33;
hence contradiction by A2,CONSTRSIGN;
end;
registration
let C;
cluster pure expression of C, a_Type C;
existence
proof consider m, a being OperSymbol of C such that
A2: the_result_sort_of m = a_Type & the_arity_of m = {} and
the_result_sort_of a = an_Adj & the_arity_of a = {} by INITIALIZED;
ex t being expression of C, a_Type C st
t = root-tree [m, the carrier of C] & t is pure by A2,ThP;
hence thesis;
end;
end;
reserve q for pure expression of C, a_Type C,
A for finite Subset of QuasiAdjs C;
definition
let C;
func QuasiTypes C equals {[A,t]: t is pure};
coherence;
end;
registration
let C;
cluster QuasiTypes C -> non empty;
coherence
proof consider q;
{} is finite Subset of QuasiAdjs C by XBOOLE_1:2; then
[{},q] in {[A,t]: t is pure};
hence thesis;
end;
end;
definition
let C;
mode quasi-type of C means:
QUASITYPE:
it in QuasiTypes C;
existence
proof consider T being Element of QuasiTypes C;
take T; thus thesis;
end;
end;
theorem Th54:
z is quasi-type of C iff ex A,q st z = [A,q]
proof
z in QuasiTypes C iff ex t,A st z = [A,t] & t is pure;
hence thesis by QUASITYPE;
end;
theorem Th55:
[x,y] is quasi-type of C iff
x is finite Subset of QuasiAdjs C & y is pure expression of C, a_Type C
proof
thus
now assume [x,y] is quasi-type of C; then
consider A,q such that
A1: [x,y] = [A,q] by Th54;
thus x is finite Subset of QuasiAdjs C &
y is pure expression of C, a_Type C by A1,ZFMISC_1:33;
end;
thus thesis by Th54;
end;
reserve T for quasi-type of C;
registration
let C;
cluster -> pair quasi-type of C;
coherence
proof let x be quasi-type of C;
ex A,q st x = [A,q] by Th54;
hence thesis;
end;
end;
theorem ThPure:
ex m being constructor OperSymbol of C st the_result_sort_of m = a_Type C &
ex p st len p = len the_arity_of m & q = m-trm p
proof set e = q;
per cases by Th100;
suppose
ex x being variable st e = x-term C;
hence thesis by Th90A;
end;
suppose
ex c being constructor OperSymbol of C st
ex p being FinSequence of QuasiTerms C st
len p = len the_arity_of c & e = c-trm p; then
consider c being constructor OperSymbol of C,
p being FinSequence of QuasiTerms C such that
A2: len p = len the_arity_of c & e = c-trm p;
take c;
e is expression of C, the_result_sort_of c by A2,Th43c;
hence the_result_sort_of c = a_Type C by Th90A;
take p; thus len p = len the_arity_of c & e = c-trm p by A2;
end;
suppose
ex a st e = (non_op C)term a; then
e is expression of C, an_Adj C by ThNon;
hence thesis by Th90A;
end;
suppose
ex a st
ex q being expression of C, a_Type C st e = (ast C)term(a,q);
hence thesis by PURE;
end;
end;
theorem ThPure2:
for m being constructor OperSymbol of C
st the_result_sort_of m = a_Type C & len p = len the_arity_of m
holds m-trm p is pure expression of C, a_Type C
proof
let v be constructor OperSymbol of C such that
A0: the_result_sort_of v = a_Type C;
assume
A1: len p = len the_arity_of v; then
reconsider a = v-trm p as expression of C, a_Type C by A0,Th43c;
a is pure
proof assume
ex a',t st a = (ast C)term(a',t);
hence thesis by A1,ThDiff02;
end;
hence v-trm p is pure expression of C, a_Type C;
end;
theorem
QuasiTerms C misses QuasiAdjs C &
QuasiTerms C misses QuasiTypes C &
QuasiTypes C misses QuasiAdjs C
proof
set X = MSVars C;
set Y = X \/ ((the carrier of C) --> {0});
consider A being MSSubset of FreeMSA Y such that
A1: Free(C, X) = GenMSAlg A & A = (Reverse Y)""X by MSAFREE3:def 2;
the Sorts of Free(C, X) is MSSubset of FreeMSA Y
by A1,MSUALG_2:def 10; then
A2: the Sorts of Free(C, X) c= the Sorts of FreeMSA Y by PBOOLE:def 23;
A3: QuasiTerms C c= (the Sorts of FreeMSA Y).a_Term C by A2,PBOOLE:def 5;
A4: (the Sorts of Free(C,X)).an_Adj C c= (the Sorts of FreeMSA Y).an_Adj C
by A2,PBOOLE:def 5;
QuasiAdjs C c= (the Sorts of Free(C,X)).an_Adj C
proof
let x; assume x in QuasiAdjs C; then
ex a st x = a & a is regular;
hence thesis by ELEMENT;
end; then
A5: QuasiAdjs C c= (the Sorts of FreeMSA Y).an_Adj C by A4,XBOOLE_1:1;
(the Sorts of FreeMSA Y).a_Term C misses (the Sorts of FreeMSA Y).an_Adj C
by PROB_2:def 3;
hence QuasiTerms C misses QuasiAdjs C by A3,A5,XBOOLE_1:64;
now let x be set; assume x in QuasiTerms C & x in QuasiTypes C; then
x is quasi-term of C & x is quasi-type of C by Th42,QUASITYPE;
hence contradiction;
end;
hence QuasiTerms C misses QuasiTypes C by XBOOLE_0:3;
now let x be set; assume x in QuasiAdjs C & x in QuasiTypes C; then
x is quasi-adjective of C & x is quasi-type of C by Th52,QUASITYPE;
hence contradiction;
end;
hence thesis by XBOOLE_0:3;
end;
theorem ::?
for e being set holds
(e is quasi-term of C implies e is not quasi-adjective of C) &
(e is quasi-term of C implies e is not quasi-type of C) &
(e is quasi-type of C implies e is not quasi-adjective of C)
by Th90A;
notation
let C,A,q;
synonym A ast q for [A,q];
end;
definition
let C,A,q;
redefine func A ast q -> quasi-type of C;
coherence by Th55;
end;
registration
let C,T;
cluster T`1 -> finite;
coherence
proof
ex A,q st T = [A,q] by Th54;
hence thesis by MCART_1:7;
end;
end;
notation
let C,T;
synonym adjs T for T`1;
synonym the_base_of T for T`2;
end;
definition
let C,T;
redefine func adjs T -> Subset of QuasiAdjs C;
coherence
proof
ex A,q st T = [A,q] by Th54;
hence thesis by MCART_1:7;
end;
func the_base_of T -> pure expression of C, a_Type C;
coherence
proof
ex A,q st T = [A,q] by Th54;
hence thesis by MCART_1:7;
end;
end;
theorem ::?
adjs (A ast q) = A & the_base_of (A ast q) = q by MCART_1:7;
theorem ::?
for A1,A2 being finite Subset of QuasiAdjs C
for q1,q2 being pure expression of C, a_Type C
st A1 ast q1 = A2 ast q2
holds A1 = A2 & q1 = q2 by ZFMISC_1:33;
theorem Th59:
T = (adjs T) ast the_base_of T
proof
ex A,q st T = [A,q] by Th54;
hence thesis by MCART_1:8;
end;
theorem
for T1,T2 being quasi-type of C
st adjs T1 = adjs T2 & the_base_of T1 = the_base_of T2
holds T1 = T2
proof
let T1,T2 be quasi-type of C;
T1 = (adjs T1) ast the_base_of T1 by Th59;
hence thesis by Th59;
end;
definition
let C,T;
let a be quasi-adjective of C;
func a ast T -> quasi-type of C equals
[{a} \/ adjs T, the_base_of T];
coherence
proof a in QuasiAdjs C; then
{a} c= QuasiAdjs C by ZFMISC_1:37; then
{a} \/ adjs T is Subset of QuasiAdjs C by XBOOLE_1:8;
hence thesis by Th55;
end;
end;
theorem ::?
for a being quasi-adjective of C
holds adjs (a ast T) = {a} \/ adjs T & the_base_of (a ast T) = the_base_of T
by MCART_1:7;
theorem
for a being quasi-adjective of C
holds a ast (a ast T) = a ast T
proof
let a be quasi-adjective of C;
thus a ast (a ast T)
= [{a} \/ ({a} \/ adjs T), the_base_of (a ast T)] by MCART_1:7
.= [{a} \/ {a} \/ adjs T, the_base_of (a ast T)] by XBOOLE_1:4
.= a ast T by MCART_1:7;
end;
theorem
for a,b being quasi-adjective of C
holds a ast (b ast T) = b ast (a ast T)
proof
let a,b be quasi-adjective of C;
thus a ast (b ast T)
= [{a} \/ ({b} \/ adjs T), the_base_of (b ast T)] by MCART_1:7
.= [{b} \/ ({a} \/ adjs T), the_base_of (b ast T)] by XBOOLE_1:4
.= [{b} \/ ({a} \/ adjs T), the_base_of T] by MCART_1:7
.= [{b} \/ adjs (a ast T), the_base_of T] by MCART_1:7
.= b ast (a ast T) by MCART_1:7;
end;
begin :: Variables in quasi-types
registration
let S be non void Signature;
let s be SortSymbol of S;
let X be non-empty ManySortedSet of the carrier of S;
let t be Term of S,X;
cluster (variables_in t).s -> finite;
coherence
proof
defpred P[non empty Relation] means
for s being SortSymbol of S holds (S variables_in $1).s is finite;
A1: for z being SortSymbol of S, v being Element of X.z holds P[root-tree[v,z]]
proof let z be SortSymbol of S, v be Element of X.z;
let s be SortSymbol of S;
s = z or s <> z;
hence thesis by MSAFREE3:11;
end;
A2: for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X)
st for t being Term of S,X st t in rng p holds P[t]
holds P[[o,the carrier of S]-tree p]
proof let o be OperSymbol of S, p be ArgumentSeq of Sym(o,X) such that
B1: for t being Term of S,X st t in rng p
for s being SortSymbol of S holds (S variables_in t).s is finite;
let s be SortSymbol of S;
deffunc F(Term of S,X) = (S variables_in $1).s;
set A = {F(q) where q is Term of S,X: q in rng p};
B2: rng p is finite;
B3: A is finite from FRAENKEL:sch 21(B2);
now let B be set; assume B in A; then
ex q being Term of S,X st B = (S variables_in q).s & q in rng p;
hence B is finite by B1;
end; then
B5: union A is finite by B3,FINSET_1:25;
(S variables_in ([o,the carrier of S]-tree p)).s c= union A
proof let x be set; assume
x in (S variables_in ([o,the carrier of S]-tree p)).s; then
consider t being DecoratedTree such that
B6: t in rng p & x in (S variables_in t).s by MSAFREE3:12;
consider i being set such that
B7: i in dom p & t = p.i by B6,FUNCT_1:def 5;
reconsider i as Nat by B7,ORDINAL1:def 13;
reconsider t = p.i as Term of S,X by B7,MSATERM:22;
(S variables_in t).s in A by B6,B7;
hence thesis by B6,B7,TARSKI:def 4;
end;
hence thesis by B5,FINSET_1:13;
end;
for t being Term of S,X holds P[t] from MSATERM:sch 1(A1,A2);
hence thesis;
end;
end;
registration
let S be non void Signature;
let s be SortSymbol of S;
let X be non empty-yielding ManySortedSet of the carrier of S;
let t be Element of Free(S,X);
cluster (S variables_in t).s -> finite;
coherence
proof
reconsider t as Term of S, X \/ ((the carrier of S) --> {0}) by MSAFREE3:9;
(S variables_in t).s = (variables_in t).s;
hence thesis;
end;
end;
definition
let S be non void Signature;
let X be non empty-yielding ManySortedSet of the carrier of S;
let s be SortSymbol of S;
func (X,s) variables_in ->
Function of Union the Sorts of Free(S,X), bool (X.s) means:
VARS'INF:
for t being Element of Free(S,X) holds it.t = (S variables_in t).s;
uniqueness
proof let f1,f2 be Function of Union the Sorts of Free(S,X), bool (X.s)
such that
A1: for t being Element of Free(S,X) holds f1.t = (S variables_in t).s and
A2: for t being Element of Free(S,X) holds f2.t = (S variables_in t).s;
now let x be Element of Union the Sorts of Free(S,X);
reconsider t = x as Element of Free(S,X);
thus f1.x = (S variables_in t).s by A1 .= f2.x by A2;
end;
hence thesis by FUNCT_2:113;
end;
existence
proof
defpred P[set,set] means
ex t being Element of Free(S,X) st t = $1 & $2 = (S variables_in t).s;
A3: now let x; assume x in Union the Sorts of Free(S,X); then
reconsider t = x as Element of Free(S,X);
S variables_in t c= X by MSAFREE3:28; then
(S variables_in t).s c= X.s by PBOOLE:def 5;
hence ex y st y in bool (X.s) & P[x,y];
end;
consider f being Function such that
A4: dom f = Union the Sorts of Free(S,X) & rng f c= bool (X.s) and
A5: for x st x in Union the Sorts of Free(S,X) holds P[x, f.x]
from WELLORD2:sch 1(A3);
reconsider f as Function of Union the Sorts of Free(S,X), bool (X.s)
by A4,FUNCT_2:4;
take f; let x be Element of Free(S,X);
ex t being Element of Free(S,X) st t = x & f.x = (S variables_in t).s
by A5;
hence thesis;
end;
end;
definition
let C be initialized ConstructorSignature;
let e be expression of C;
func variables_in e -> Subset of Vars equals
(C variables_in e).a_Term C;
coherence
proof
(MSVars C).a_Term C = Vars & C variables_in e c= MSVars C
by MSVARS,MSAFREE3:28;
hence thesis by PBOOLE:def 5;
end;
end;
registration
let C,e;
cluster variables_in e -> finite;
coherence;
end;
definition
let C,e;
func vars e -> finite Subset of Vars equals
varcl variables_in e;
coherence by Th18;
end;
theorem ::?
varcl vars e = vars e;
theorem ::?
for x being variable
holds variables_in (x-term C) = {x} by MSAFREE3:11;
theorem
for x being variable
holds vars (x-term C) = {x} \/ vars x
proof
let x be variable;
thus vars (x-term C) = varcl {x} by MSAFREE3:11 .= {x} \/ vars x by Th82;
end;
theorem Th84:
for p being DTree-yielding FinSequence
st e = [c, the carrier of C]-tree p
holds variables_in e =
union {variables_in t where t is quasi-term of C: t in rng p}
proof
let p be DTree-yielding FinSequence;
set X = {variables_in t where t is quasi-term of C: t in rng p};
assume
A0: e = [c, the carrier of C]-tree p; then
p in (QuasiTerms C)* by Th83; then
p is FinSequence of QuasiTerms C by FINSEQ_1:def 11; then
A2: rng p c= QuasiTerms C by FINSEQ_1:def 4;
thus variables_in e c= union X
proof let a be set; assume
a in variables_in e; then
consider t being DecoratedTree such that
A3: t in rng p & a in (C variables_in t).a_Term C by A0,MSAFREE3:12;
reconsider t as quasi-term of C by A2,A3,Th42;
a in variables_in t & variables_in t in X by A3;
hence thesis by TARSKI:def 4;
end;
let a be set; assume a in union X; then
consider Y being set such that
A4: a in Y & Y in X by TARSKI:def 4;
ex t being quasi-term of C st Y = variables_in t & t in rng p by A4;
hence thesis by A0,A4,MSAFREE3:12;
end;
theorem Th84':
for p being DTree-yielding FinSequence
st e = [c, the carrier of C]-tree p
holds vars e = union {vars t where t is quasi-term of C: t in rng p}
proof
let p be DTree-yielding FinSequence; assume
A1: e = [c, the carrier of C]-tree p;
set A = {variables_in t where t is quasi-term of C: t in rng p};
set B = {vars t where t is quasi-term of C: t in rng p};
per cases;
suppose
A3: A = {};
consider b being Element of B;
now assume B <> {}; then
b in B; then
consider t being quasi-term of C such that
A4: b = vars t & t in rng p;
variables_in t in A by A4;
hence contradiction by A3;
end;
hence vars e = union B by A1,A3,Th11,Th84,ZFMISC_1:2;
end;
suppose A <> {}; then
reconsider A as non empty set;
set D = {varcl s where s is Element of A: not contradiction};
A5: B c= D
proof let a be set; assume a in B; then
consider t being quasi-term of C such that
B1: a = vars t & t in rng p;
variables_in t in A by B1; then
reconsider s = variables_in t as Element of A;
a = varcl s by B1;
hence thesis;
end;
A6: D c= B
proof let a be set; assume a in D; then
consider s being Element of A such that
B2: a = varcl s;
s in A; then
consider t being quasi-term of C such that
B3: s = variables_in t & t in rng p;
vars t = a by B2,B3;
hence thesis by B3;
end;
thus vars e = varcl union A by A1,Th84
.= union D by Th14
.= union B by A5,A6,XBOOLE_0:def 10;
end;
end;
theorem
len p = len the_arity_of c implies
variables_in (c-trm p) =
union {variables_in t where t is quasi-term of C: t in rng p}
proof
assume len p = len the_arity_of c; then
c-trm p = [c, the carrier of C]-tree p by TERM;
hence thesis by Th84;
end;
theorem
len p = len the_arity_of c implies
vars (c-trm p) = union {vars t where t is quasi-term of C: t in rng p}
proof
assume len p = len the_arity_of c; then
c-trm p = [c, the carrier of C]-tree p by TERM;
hence thesis by Th84';
end;
theorem
for S being ManySortedSign, o being set
holds
S variables_in ([o, the carrier of S]-tree {}) = [0] the carrier of S
proof let S be ManySortedSign, o be set;
now let s be set; assume
A1: s in the carrier of S;
now let x;
rng {} = {}; then
x in (S variables_in ([o, the carrier of S]-tree {})).s iff
ex q being DecoratedTree st q in {} & x in (S variables_in q).s
by A1,MSAFREE3:12;
hence x in (S variables_in ([o, the carrier of S]-tree {})).s iff
x in ([0] the carrier of S).s by PBOOLE:5;
end;
hence (S variables_in ([o, the carrier of S]-tree {})).s =
([0] the carrier of S).s by TARSKI:2;
end;
hence thesis by PBOOLE:3;
end;
theorem Aux1:
for S being ManySortedSign, o being set, t being DecoratedTree
holds
S variables_in ([o, the carrier of S]-tree <*t*>) = S variables_in t
proof let S be ManySortedSign, o be set, t be DecoratedTree;
now let s be set; assume
A1: s in the carrier of S;
A2: t in {t} by TARSKI:def 1;
now let x;
rng <*t*> = {t} by FINSEQ_1:56; then
x in (S variables_in ([o, the carrier of S]-tree <*t*>)).s iff
ex q being DecoratedTree st q in {t} & x in (S variables_in q).s
by A1,MSAFREE3:12;
hence x in (S variables_in ([o, the carrier of S]-tree <*t*>)).s iff
x in (S variables_in t).s by A2,TARSKI:def 1;
end;
hence (S variables_in ([o, the carrier of S]-tree <*t*>)).s =
(S variables_in t).s by TARSKI:2;
end;
hence thesis by PBOOLE:3;
end;
theorem Aux1':
variables_in ((non_op C)term a) = variables_in a
proof
(non_op C)term a = [non_op, the carrier of C]-tree <*a*> by ThNon;
hence thesis by Aux1;
end;
theorem ::?
vars ((non_op C)term a) = vars a by Aux1';
theorem Aux2:
for S being ManySortedSign, o being set, t1,t2 being DecoratedTree
holds
S variables_in ([o, the carrier of S]-tree <*t1,t2*>)
= (S variables_in t1) \/ (S variables_in t2)
proof let S be ManySortedSign, o be set, t1,t2 be DecoratedTree;
now let s be set; assume
A1: s in the carrier of S;
A2: t1 in {t1,t2} & t2 in {t1,t2} by TARSKI:def 2;
now let x;
rng <*t1,t2*> = {t1,t2} by FINSEQ_2:147; then
x in (S variables_in ([o, the carrier of S]-tree <*t1,t2*>)).s iff
ex q being DecoratedTree st q in {t1,t2} & x in (S variables_in q).s
by A1,MSAFREE3:12; then
x in (S variables_in ([o, the carrier of S]-tree <*t1,t2*>)).s iff
x in (S variables_in t1).s or x in (S variables_in t2).s
by A2,TARSKI:def 2; then
x in (S variables_in ([o, the carrier of S]-tree <*t1,t2*>)).s iff
x in (S variables_in t1).s \/ (S variables_in t2).s by XBOOLE_0:def 2;
hence x in (S variables_in ([o, the carrier of S]-tree <*t1,t2*>)).s iff
x in ((S variables_in t1) \/ (S variables_in t2)).s
by A1,PBOOLE:def 7;
end;
hence (S variables_in ([o, the carrier of S]-tree <*t1,t2*>)).s =
((S variables_in t1) \/ (S variables_in t2)).s by TARSKI:2;
end;
hence thesis by PBOOLE:3;
end;
theorem Aux2':
variables_in ((ast C)term(a,t)) = (variables_in a)\/(variables_in t)
proof
(ast C)term(a,t) = [ *, the carrier of C]-tree <*a,t*> by ThAst; then
variables_in ((ast C)term(a,t))
= ((C variables_in a)\/(C variables_in t)).a_Term by Aux2;
hence thesis by PBOOLE:def 7;
end;
theorem
vars ((ast C)term(a,t)) = (vars a)\/(vars t)
proof
thus vars ((ast C)term(a,t))
= varcl((variables_in a)\/(variables_in t)) by Aux2'
.= (vars a)\/(vars t) by Th10;
end;
theorem Th71:
variables_in Non a = variables_in a
proof per cases;
suppose a is non positive; then
consider a' being expression of C, an_Adj C such that
A2: a = (non_op C)term a' & Non a = a' by Th45g;
[non_op C, the carrier of C]-tree<*a'*> = a by A2,ThNon;
hence thesis by A2,Aux1;
end;
suppose a is positive; then
Non a = (non_op C)term a by Th44
.= [non_op, the carrier of C]-tree <*a*> by ThNon;
hence thesis by Aux1;
end;
end;
theorem ::?
vars Non a = vars a by Th71;
definition
let C;
let T be quasi-type of C;
func variables_in T -> Subset of Vars equals
(union (((MSVars C, a_Term C) variables_in).:adjs T)) \/
variables_in the_base_of T;
coherence
proof
((MSVars C, a_Term C) variables_in).:adjs T is Subset of bool Vars &
union bool Vars = Vars by MSVARS,ZFMISC_1:99; then
(union (((MSVars C, a_Term C) variables_in).:adjs T)) c= Vars
by ZFMISC_1:95;
hence thesis by XBOOLE_1:8;
end;
end;
registration
let C;
let T be quasi-type of C;
cluster variables_in T -> finite;
coherence
proof
now let A be set; assume
A in ((MSVars C, a_Term C) variables_in).:adjs T; then
consider x being set such that
A2: x in Union the Sorts of Free(C, MSVars C) & x in adjs T &
A = ((MSVars C, a_Term C) variables_in).x by FUNCT_2:115;
reconsider x as expression of C by A2;
A = (C variables_in x).a_Term C by A2,VARS'INF;
hence A is finite;
end; then
A3: union (((MSVars C, a_Term C) variables_in).:adjs T) is finite
by FINSET_1:25;
thus thesis by A3,FINSET_1:14;
end;
end;
definition
let C;
let T be quasi-type of C;
func vars T -> finite Subset of Vars equals
varcl variables_in T;
coherence by Th18;
end;
theorem ::?
for T being quasi-type of C
holds varcl vars T = vars T;
theorem Th72:
for T being quasi-type of C
for a being quasi-adjective of C
holds
variables_in (a ast T) = (variables_in a) \/ (variables_in T)
proof
let T be quasi-type of C;
let a be quasi-adjective of C;
A1: dom ((MSVars C, a_Term C) variables_in)
= Union the Sorts of Free(C, MSVars C) by FUNCT_2:def 1;
thus variables_in (a ast T)
= (union (((MSVars C, a_Term C) variables_in).:adjs(a ast T)))
\/ variables_in the_base_of T by MCART_1:7
.= (union (((MSVars C, a_Term C) variables_in).:({a} \/ adjs T)))
\/ variables_in the_base_of T by MCART_1:7
.= (union ((((MSVars C, a_Term C) variables_in).:{a}) \/
(((MSVars C, a_Term C) variables_in).:adjs T)))
\/ variables_in the_base_of T by RELAT_1:153
.= (union (((MSVars C, a_Term C) variables_in).:{a})) \/
(union (((MSVars C, a_Term C) variables_in).:adjs T))
\/ variables_in the_base_of T by ZFMISC_1:96
.= (union (Im((MSVars C, a_Term C) variables_in,a))) \/
variables_in T by XBOOLE_1:4
.= (union {((MSVars C, a_Term C) variables_in).a}) \/
variables_in T by A1,FUNCT_1:117
.= (((MSVars C, a_Term C) variables_in).a) \/
variables_in T by ZFMISC_1:31
.= (variables_in a) \/ variables_in T by VARS'INF;
end;
theorem
for T being quasi-type of C
for a being quasi-adjective of C
holds
vars (a ast T) = (vars a) \/ (vars T)
proof
let T be quasi-type of C;
let a be quasi-adjective of C;
thus vars (a ast T)
= varcl((variables_in a)\/variables_in T) by Th72
.= (vars a) \/ vars T by Th10;
end;
theorem ThAA:
variables_in (A ast q) =
(union {variables_in a where a is quasi-adjective of C: a in A}) \/
(variables_in q)
proof
set X = ((MSVars C, a_Term C) variables_in).:A;
set Y = {variables_in a where a is quasi-adjective of C: a in A};
A1: X c= Y
proof
let z be set;
assume z in X; then
consider a being set such that
B1: a in dom ((MSVars C, a_Term C) variables_in) & a in A &
z = ((MSVars C, a_Term C) variables_in).a by FUNCT_1:def 12;
reconsider a as quasi-adjective of C by B1,Th52;
z = variables_in a by B1,VARS'INF;
hence thesis by B1;
end;
A2: Y c= X
proof
let z be set;
assume z in Y; then
consider a being quasi-adjective of C such that
B2: z = variables_in a & a in A;
z = ((MSVars C, a_Term C) variables_in).a &
dom ((MSVars C, a_Term C) variables_in)
= Union the Sorts of Free(C, MSVars C) by B2,VARS'INF,FUNCT_2:def 1;
hence thesis by B2,FUNCT_1:def 12;
end;
thus variables_in (A ast q)
= (union (((MSVars C, a_Term C) variables_in).:adjs(A ast q)))
\/ variables_in q by MCART_1:7
.= (union (((MSVars C, a_Term C) variables_in).:A))
\/ variables_in q by MCART_1:7
.= (union {variables_in a where a is quasi-adjective of C: a in A})
\/ (variables_in q) by A1,A2,XBOOLE_0:def 10;
end;
theorem
vars (A ast q) =
(union {vars a where a is quasi-adjective of C: a in A}) \/ (vars q)
proof
set X = {variables_in a where a is quasi-adjective of C: a in A};
set Y = {vars a where a is quasi-adjective of C: a in A};
A1: union X c= union Y
proof
let x be set; assume x in union X; then
consider Z being set such that
B0: x in Z & Z in X by TARSKI:def 4;
consider a being quasi-adjective of C such that
B1: Z = variables_in a & a in A by B0;
Z c= vars a by B1,VARCL; then
vars a in Y & x in vars a by B0,B1;
hence x in union Y by TARSKI:def 4;
end;
for x,y st [x,y] in union Y holds x c= union Y
proof
let x,y;
assume [x,y] in union Y; then
consider Z being set such that
B2: [x,y] in Z & Z in Y by TARSKI:def 4;
consider a being quasi-adjective of C such that
B3: Z = vars a & a in A by B2;
x c= Z & Z c= union Y by B2,B3,VARCL,ZFMISC_1:92;
hence x c= union Y by XBOOLE_1:1;
end; then
A3: varcl union X c= union Y by A1,VARCL;
A4: union Y c= varcl union X
proof
let x be set; assume x in union Y; then
consider Z being set such that
B4: x in Z & Z in Y by TARSKI:def 4;
consider a being quasi-adjective of C such that
B5: Z = vars a & a in A by B4;
variables_in a in X by B5; then
vars a c= varcl union X by Th13,ZFMISC_1:92;
hence thesis by B4,B5;
end;
thus vars (A ast q)
= varcl((union X) \/ (variables_in q)) by ThAA
.= (varcl union X) \/ (vars q) by Th10
.= (union Y) \/ (vars q) by A3,A4,XBOOLE_0:def 10;
end;
theorem ThAAe:
variables_in (({}QuasiAdjs C) ast q) = variables_in q
proof
set A = {}QuasiAdjs C;
set AA = {variables_in a where a is quasi-adjective of C: a in A};
AA c= {}
proof
let x;
assume x in AA; then
ex a being quasi-adjective of C st x = variables_in a & a in A;
hence thesis;
end; then
AA = {} & variables_in (A ast q) = (union AA) \/ (variables_in q)
by ThAA,XBOOLE_1:3;
hence thesis by ZFMISC_1:2;
end;
theorem ThG:
e is ground iff variables_in e = {}
proof
thus e is ground implies variables_in e = {}
proof assume
Union (C variables_in e) = {};
hence variables_in e = {} by ThF0,XBOOLE_1:3;
end;
assume that
Z1: variables_in e = {} and
Z2: Union (C variables_in e) <> {};
consider x being Element of Union (C variables_in e);
consider y such that
Z3: y in dom (C variables_in e) & x in (C variables_in e).y by Z2,CARD_5:10;
dom (C variables_in e) = the carrier of C by PBOOLE:def 3
.= {a_Type, an_Adj, a_Term} by CONSTRSIGN; then
Z4: y = a_Type or y = an_Adj or y = a_Term by Z3,ENUMSET1:def 1;
C variables_in e c= MSVars C & (MSVars C).an_Adj = {} &
(MSVars C).a_Type = {} by MSVARS,MSAFREE3:28; then
(C variables_in e).an_Adj C c= {} &
(C variables_in e).a_Type C c= {} by PBOOLE:def 5;
hence thesis by Z1,Z3,Z4;
end;
definition
let C;
let T be quasi-type of C;
attr T is ground means:
GROUND2:
variables_in T = {};
end;
registration
let C;
cluster ground pure expression of C, a_Type C;
existence
proof
consider m, a being OperSymbol of C such that
A1: the_result_sort_of m = a_Type & the_arity_of m = {} and
the_result_sort_of a = an_Adj & the_arity_of a = {} by INITIALIZED;
root-tree [m, the carrier of C] in
(the Sorts of Free(C,MSVars C)).a_Type C by A1,MSAFREE3:6; then
reconsider mm = root-tree [m, the carrier of C] as expression of C, a_Type C
by Th42;
take mm;
set p = <*>Union the Sorts of Free(C, MSVars C);
A2: mm = [m, the carrier of C]-tree p by TREES_4:20;
m <> * & m <> non_op by A1,CONSTRSIGN; then
A3: m is constructor by CNSTR2;
variables_in mm c= {}
proof
let x; assume x in variables_in mm; then
x in union {variables_in t where t is quasi-term of C: t in rng p}
by A2,A3,Th84; then
consider Y such that
A4: x in Y & Y in {variables_in t where t is quasi-term of C: t in rng p}
by TARSKI:def 4;
ex t being quasi-term of C st Y = variables_in t & t in rng p by A4;
hence thesis;
end; then
variables_in mm = {} by XBOOLE_1:3;
hence mm is ground by ThG;
ex t being expression of C, a_Type C st
t = root-tree [m, the carrier of C] & t is pure by A1,ThP;
hence thesis;
end;
cluster ground quasi-adjective of C;
existence
proof
consider m, a being OperSymbol of C such that
the_result_sort_of m = a_Type & the_arity_of m = {} and
A1: the_result_sort_of a = an_Adj & the_arity_of a = {} by INITIALIZED;
consider mm being expression of C, an_Adj C such that
A5: mm = root-tree [a, the carrier of C] & mm is positive by A1,ThP2;
reconsider mm as quasi-adjective of C by A5,REG;
take mm;
set p = <*>Union the Sorts of Free(C, MSVars C);
A2: mm = [a, the carrier of C]-tree p by A5,TREES_4:20;
a <> * & a <> non_op by A1,CONSTRSIGN; then
A3: a is constructor by CNSTR2;
variables_in mm c= {}
proof
let x; assume x in variables_in mm; then
x in union {variables_in t where t is quasi-term of C: t in rng p}
by A2,A3,Th84; then
consider Y such that
A4: x in Y & Y in {variables_in t where t is quasi-term of C: t in rng p}
by TARSKI:def 4;
ex t being quasi-term of C st Y = variables_in t & t in rng p by A4;
hence thesis;
end; then
variables_in mm = {} by XBOOLE_1:3;
hence thesis by ThG;
end;
end;
theorem ThG2:
for t being ground pure expression of C, a_Type C
holds ({} QuasiAdjs C) ast t is ground
proof
let t be ground pure expression of C, a_Type C;
set T = ({} QuasiAdjs C) ast t;
thus variables_in T = variables_in t by ThAAe .= {} by ThG;
end;
registration
let C;
let t be ground pure expression of C, a_Type C;
cluster ({} QuasiAdjs C) ast t -> ground quasi-type of C;
coherence by ThG2;
end;
registration
let C;
cluster ground quasi-type of C;
existence
proof
consider t being ground pure expression of C, a_Type C;
take ({} QuasiAdjs C) ast t; thus thesis;
end;
end;
registration
let C;
let T be ground quasi-type of C;
let a be ground quasi-adjective of C;
cluster a ast T -> ground;
coherence
proof
thus variables_in(a ast T) = (variables_in a)\/variables_in T by Th72
.= {}\/variables_in T by ThG .= {} by GROUND2;
end;
end;
begin :: Smooth Type Widening
:: Type widening is smooth iff
:: vars-function is sup-semilattice homomorphism from widening sup-semilattice
:: into VarPoset
definition
func VarPoset -> strict non empty Poset equals
(InclPoset {varcl A where A is finite Subset of Vars: not contradiction})opp;
coherence
proof consider A0 being finite Subset of Vars;
set V = {varcl A where A is finite Subset of Vars: not contradiction};
varcl A0 in V; then
reconsider V as non empty set;
reconsider P = InclPoset V as non empty Poset;
P opp is non empty;
hence thesis;
end;
end;
theorem Th22:
for x, y being Element of VarPoset holds x <= y iff y c= x
proof let x, y be Element of VarPoset;
set V = {varcl A where A is finite Subset of Vars: not contradiction};
consider A0 being finite Subset of Vars; varcl A0 in V; then
reconsider V as non empty set;
reconsider a = x, b = y as Element of (InclPoset V) opp;
x <= y iff ~a >= ~b by YELLOW_7:1;
hence thesis by YELLOW_1:3;
end;
:: registration
:: let V1,V2 be Element of VarPoset;
:: identify V1 <= V2 with V2 c= V1;
:: compatibility by Th22;
:: end;
theorem Th21:
for x holds
x is Element of VarPoset iff x is finite Subset of Vars & varcl x = x
proof let x;
set V = {varcl A where A is finite Subset of Vars: not contradiction};
consider A0 being finite Subset of Vars; varcl A0 in V; then
reconsider V as non empty set;
A2: the carrier of InclPoset V = V by YELLOW_1:1;
x is Element of VarPoset iff x in V by A2; then
x is Element of VarPoset iff
ex A being finite Subset of Vars st x = varcl A;
hence thesis by Th18;
end;
registration
cluster VarPoset -> with_infima with_suprema;
coherence
proof
set V = {varcl A where A is finite Subset of Vars: not contradiction};
consider A0 being finite Subset of Vars; varcl A0 in V; then
reconsider V as non empty set;
now let x,y; assume x in V; then
consider A1 being finite Subset of Vars such that
A2: x = varcl A1;
assume y in V; then
consider A2 being finite Subset of Vars such that
A3: y = varcl A2;
x \/ y = varcl (A1 \/ A2) by A2,A3,Th10;
hence x \/ y in V;
end; then
InclPoset V is with_suprema by YELLOW_1:11;
hence VarPoset is with_infima by LATTICE3:10;
now let x,y; assume x in V; then
consider A1 being finite Subset of Vars such that
A2: x = varcl A1;
assume y in V; then
consider A2 being finite Subset of Vars such that
A3: y = varcl A2;
reconsider V1 = varcl A1, V2 = varcl A2 as finite Subset of Vars by Th18;
x /\ y = varcl (V1 /\ V2) by A2,A3,Th9;
hence x /\ y in V;
end; then
InclPoset V is with_infima by YELLOW_1:12;
hence VarPoset is with_suprema by YELLOW_7:16;
end;
end;
theorem Th23:
for V1, V2 being Element of VarPoset holds
V1 "\/" V2 = V1 /\ V2 & V1 "/\" V2 = V1 \/ V2
proof let V1, V2 be Element of VarPoset;
set V = {varcl A where A is finite Subset of Vars: not contradiction};
consider A0 being finite Subset of Vars; varcl A0 in V; then
reconsider V as non empty set;
A1: VarPoset = (InclPoset V) opp;
A2: the carrier of InclPoset V = V by YELLOW_1:1;
reconsider v1 = V1, v2 = V2 as Element of (InclPoset V) opp;
reconsider a1 = V1, a2 = V2 as Element of InclPoset V;
V1 in V by A2; then
consider A1 being finite Subset of Vars such that
A4: V1 = varcl A1;
V2 in V by A2; then
consider A2 being finite Subset of Vars such that
A5: V2 = varcl A2;
A6: a1~ = v1 & a2~ = v2;
A7: InclPoset V is with_infima with_suprema by A1,LATTICE3:10,YELLOW_7:16;
reconsider x1 = V1, x2 = V2 as finite Subset of Vars by A4,A5,Th18;
V1 /\ V2 = varcl (x1 /\ x2) by A4,A5,Th9; then
V1 /\ V2 in V; then
a1 "/\" a2 = V1 /\ V2 by YELLOW_1:9;
hence V1 "\/" V2 = V1 /\ V2 by A6,A7,YELLOW_7:21;
V1 \/ V2 = varcl (A1 \/ A2) by A4,A5,Th10; then
a1 \/ a2 in V; then
a1 "\/" a2 = V1 \/ V2 by YELLOW_1:8;
hence thesis by A6,A7,YELLOW_7:23;
end;
registration
let V1,V2 be Element of VarPoset;
identify V1 "\/" V2 with V1 /\ V2;
compatibility by Th23;
identify V1 "/\" V2 with V1 \/ V2;
compatibility by Th23;
end;
theorem Th24:
for X being non empty Subset of VarPoset holds
ex_sup_of X, VarPoset & sup X = meet X
proof let X be non empty Subset of VarPoset;
consider a being Element of X;
meet X c= a & a is finite Subset of Vars by Th21,SETFAM_1:4; then
A1: meet X is finite & meet X c= Vars by XBOOLE_1:1,FINSET_1:13;
for a being Element of X holds varcl a = a by Th21; then
varcl meet X = meet X by Th8; then
reconsider m = meet X as Element of VarPoset by A1,Th21;
A4: now
thus X is_<=_than m
proof let n be Element of VarPoset; assume n in X; then
m c= n by SETFAM_1:4;
hence thesis by Th22;
end;
let b be Element of VarPoset; assume
A2: X is_<=_than b;
now let Y; assume
A3: Y in X; then
reconsider c = Y as Element of VarPoset;
c <= b by A2,LATTICE3:def 9,A3;
hence b c= Y by Th22;
end; then
b c= m by SETFAM_1:6;
hence m <= b by Th22;
end;
hence ex_sup_of X, VarPoset by YELLOW_0:15;
hence thesis by A4,YELLOW_0:def 9;
end;
registration
cluster VarPoset -> up-complete;
coherence
proof
for X being non empty directed Subset of VarPoset
holds ex_sup_of X, VarPoset by Th24;
hence thesis by WAYBEL_0:75;
end;
end;
theorem
Top VarPoset = {}
proof
set V = {varcl A where A is finite Subset of Vars: not contradiction};
{} Vars in V by Th11; then
VarPoset opp is lower-bounded & (Bottom InclPoset V)~ = {} &
VarPoset opp = InclPoset V by YELLOW_1:13,YELLOW_7:31;
hence thesis by YELLOW_7:33;
end;
definition
let C;
func vars-function C -> Function of QuasiTypes C, the carrier of VarPoset
means
for T being quasi-type of C holds it.T = vars T;
uniqueness
proof let f1,f2 be Function of QuasiTypes C, the carrier of VarPoset such
that
A1: for T being quasi-type of C holds f1.T = vars T and
A2: for T being quasi-type of C holds f2.T = vars T;
now let T be Element of QuasiTypes C;
reconsider t = T as quasi-type of C by QUASITYPE;
thus f1.T = vars t by A1 .= f2.T by A2;
end;
hence thesis by FUNCT_2:113;
end;
existence
proof
defpred P[set,set] means
ex T being quasi-type of C st $1 = T & $2 = vars T;
A1: for x st x in QuasiTypes C
ex y being set st P[x,y]
proof let x; assume x in QuasiTypes C; then
reconsider T = x as quasi-type of C by QUASITYPE;
take y = vars T, T; thus thesis;
end;
A2: for x,y1,y2 being set st x in QuasiTypes C & P[x,y1] &P[x,y2]
holds y1 = y2;
consider f being Function such that
A3: dom f = QuasiTypes C and
A4: for x st x in QuasiTypes C holds P[x,f.x] from FUNCT_1:sch 2(A2,A1);
rng f c= the carrier of VarPoset
proof let y; assume y in rng f; then
consider x such that
A5: x in dom f & y = f.x by FUNCT_1:def 5;
consider T being quasi-type of C such that
A6: x = T & y = vars T by A3,A4,A5;
varcl vars T = vars T; then
y is Element of VarPoset by A6,Th21;
hence thesis;
end; then
reconsider f as Function of QuasiTypes C, the carrier of VarPoset
by A3,FUNCT_2:4;
take f; let x be quasi-type of C;
x in QuasiTypes C by QUASITYPE; then
ex T being quasi-type of C st x = T & f.x = vars T by A4;
hence thesis;
end;
end;
definition
let L be non empty Poset;
attr L is smooth means
ex C being initialized ConstructorSignature,
f being Function of L, VarPoset st
the carrier of L c= QuasiTypes C &
f = (vars-function C)|the carrier of L &
for x,y being Element of L holds f preserves_sup_of {x,y};
end;
registration
let C be initialized ConstructorSignature;
let T be ground quasi-type of C;
cluster RelStr(#{T}, id {T}#) -> smooth;
coherence
proof
set L = RelStr(#{T}, id {T}#);
T in QuasiTypes C by QUASITYPE; then
A1: {T} c= QuasiTypes C by ZFMISC_1:37; then
reconsider f = (vars-function C)|{T} as Function of L, VarPoset
by FUNCT_2:38;
take C, f;
thus the carrier of L c= QuasiTypes C by A1;
thus f = (vars-function C)|the carrier of L;
let x,y be Element of L;
set F = {x,y};
assume ex_sup_of F, L;
A2: x = T & y = T by TARSKI:def 1; then
A4: F = {T} & dom f = {T} by ENUMSET1:69,FUNCT_2:def 1; then
A3: Im(f,T) = {f.x} by A2,FUNCT_1:117;
hence ex_sup_of f.:F, VarPoset by A4,YELLOW_0:38;
thus sup (f.:F) = f.x by A4,A3,YELLOW_0:39 .= f.sup F by A2,TARSKI:def 1;
end;
end;
begin :: Structural induction
scheme StructInd
{C() -> initialized ConstructorSignature, P[set], t() -> expression of C()}:
P[t()]
provided
W1: for x being variable holds P[x-term C()] and
W2: for c being constructor OperSymbol of C()
for p being FinSequence of QuasiTerms C()
st len p = len the_arity_of c &
for t being quasi-term of C() st t in rng p holds P[t]
holds P[c-trm p] and
W3: for a being expression of C(), an_Adj C() st P[a]
holds P[(non_op C())term a] and
W4: for a being expression of C(), an_Adj C() st P[a]
for t being expression of C(), a_Type C() st P[t]
holds P[(ast C())term(a,t)]
proof
defpred Q[set] means $1 is expression of C() implies P[ $1 ];
set X = MSVars C();
set V = X \/ ((the carrier of C())-->{0});
set S = C(), C = C();
B0: t() is Term of S,V by MSAFREE3:9;
B1: for s being SortSymbol of S, v being Element of V.s
holds Q[root-tree [v,s]]
proof
let s be SortSymbol of S;
let v be Element of V.s;
set t = root-tree [v,s];
assume
C1: t is expression of S;
t.{} = [v,s] & s in the carrier of C by TREES_4:3; then
C2: (t.{})`2 = s & s <> the carrier of C by MCART_1:7;
per cases by C1,Th100;
suppose ex x being variable st t = x-term C;
hence P[t] by W1;
end;
suppose ex c being constructor OperSymbol of C st
ex p being FinSequence of QuasiTerms C st
len p = len the_arity_of c & t = c-trm p; then
consider c being (constructor OperSymbol of C),
p being FinSequence of QuasiTerms C such that
C3: len p = len the_arity_of c & t = c-trm p;
t = [c, the carrier of C]-tree p by C3,TERM; then
t.{} = [c, the carrier of C] by TREES_4:def 4;
hence P[t] by C2,MCART_1:7;
end;
suppose
ex a being expression of C(), an_Adj C() st t = (non_op C)term a; then
consider a being expression of C(), an_Adj C() such that
C4: t = (non_op C)term a;
the_arity_of non_op C = <*an_Adj C*> & <*an_Adj C*>.1 = an_Adj C &
len <*an_Adj C*> = 1 by CONSTRSIGN,FINSEQ_1:57; then
t = [non_op C, the carrier of C]-tree<*a*> by C4,TERM1; then
t.{} = [non_op C, the carrier of C] by TREES_4:def 4;
hence P[t] by C2,MCART_1:7;
end;
suppose ex a being expression of C(), an_Adj C() st
ex q being expression of C, a_Type C st t = (ast C)term(a,q); then
consider a being expression of C, an_Adj C,
q being expression of C, a_Type C such that
C5: t = (ast C)term(a,q);
the_arity_of ast C = <*an_Adj C,a_Type C*> &
<*an_Adj C,a_Type C*>.1 = an_Adj C & <*an_Adj C,a_Type C*>.2 = a_Type C
& len <*an_Adj C,a_Type C*> = 2 by CONSTRSIGN,FINSEQ_1:61; then
t = [ast C, the carrier of C]-tree<*a,q*> by C5,TERM2; then
t.{} = [ast C, the carrier of C] by TREES_4:def 4;
hence P[t] by C2,MCART_1:7;
end;
end;
B2: for o being OperSymbol of S,
p being ArgumentSeq of Sym(o,V) st
for t being Term of S,V st t in rng p holds Q[t]
holds Q[[o,the carrier of S]-tree p]
proof
let o be OperSymbol of S;
let p be ArgumentSeq of Sym(o,V) such that
Z0: for t being Term of S,V st t in rng p holds Q[t];
set t = [o,the carrier of S]-tree p;
assume
C1: t is expression of S;
per cases by C1,Th100;
suppose ex x being variable st t = x-term C;
hence P[t] by W1;
end;
suppose ex c being constructor OperSymbol of C st
ex p being FinSequence of QuasiTerms C st
len p = len the_arity_of c & t = c-trm p; then
consider c being (constructor OperSymbol of C),
q being FinSequence of QuasiTerms C such that
C3: len q = len the_arity_of c & t = c-trm q;
t = [c, the carrier of C]-tree q by C3,TERM; then
C4: p = q by TREES_4:15;
now let t be quasi-term of C;
t is Term of S,V by MSAFREE3:9;
hence t in rng q implies P[t] by Z0,C4;
end;
hence P[t] by C3,W2;
end;
suppose
ex a being expression of C(), an_Adj C() st t = (non_op C)term a; then
consider a being expression of C(), an_Adj C() such that
C4: t = (non_op C)term a;
the_arity_of non_op C = <*an_Adj C*> & <*an_Adj C*>.1 = an_Adj C &
len <*an_Adj C*> = 1 by CONSTRSIGN,FINSEQ_1:57; then
t = [non_op C, the carrier of C]-tree<*a*> by C4,TERM1; then
00: p = <*a*> by TREES_4:15;
rng <*a*> = {a} & a in {a} & a is Term of S,V
by TARSKI:def 1,FINSEQ_1:56,MSAFREE3:9;
hence P[t] by C4,W3,00,Z0;
end;
suppose ex a being expression of C(), an_Adj C() st
ex q being expression of C, a_Type C st t = (ast C)term(a,q); then
consider a being expression of C, an_Adj C,
q being expression of C, a_Type C such that
C5: t = (ast C)term(a,q);
the_arity_of ast C = <*an_Adj C,a_Type C*> &
<*an_Adj C,a_Type C*>.1 = an_Adj C & <*an_Adj C,a_Type C*>.2 = a_Type C
& len <*an_Adj C,a_Type C*> = 2 by CONSTRSIGN,FINSEQ_1:61; then
t = [ast C, the carrier of C]-tree<*a,q*> by C5,TERM2; then
00: p = <*a,q*> by TREES_4:15;
rng <*a,q*> = {a,q} & a in {a,q} & q in {a,q} & a is Term of S,V &
q is Term of S,V by TARSKI:def 2,FINSEQ_2:147,MSAFREE3:9; then
P[a] & P[q] by 00,Z0;
hence P[t] by C5,W4;
end;
end;
for t being Term of S,V holds Q[t] from MSATERM:sch 1(B1,B2);
hence thesis by B0;
end;
definition
let S be ManySortedSign;
attr S is with_an_operation_for_each_sort means:
WOFES:
the carrier of S c= rng the ResultSort of S;
let X be ManySortedSet of the carrier of S;
attr X is with_missing_variables means:
WMV:
X"{{}} c= rng the ResultSort of S;
end;
theorem LemMV:
for S being non void Signature
for X being ManySortedSet of the carrier of S
holds X is with_missing_variables iff
for s being SortSymbol of S st X.s = {}
ex o being OperSymbol of S st the_result_sort_of o = s
proof
let S be non void Signature;
let X be ManySortedSet of the carrier of S;
A0: dom X = the carrier of S by PBOOLE:def 3;
hereby assume X is with_missing_variables; then
Z0: X"{{}} c= rng the ResultSort of S by WMV;
let s be SortSymbol of S;
assume X.s = {}; then
X.s in {{}} by TARSKI:def 1; then
s in X"{{}} by A0,FUNCT_1:def 13; then
consider o being set such that
Z1: o in the OperSymbols of S & (the ResultSort of S).o = s by Z0,FUNCT_2:17;
reconsider o as OperSymbol of S by Z1;
take o;
thus the_result_sort_of o = s by Z1;
end;
assume
Z2: for s being SortSymbol of S st X.s = {}
ex o being OperSymbol of S st the_result_sort_of o = s;
let x be set; assume x in X"{{}}; then
A1: x in dom X & X.x in {{}} by FUNCT_1:def 13; then
reconsider x as SortSymbol of S by A0;
X.x = {} by A1,TARSKI:def 1; then
ex o being OperSymbol of S st the_result_sort_of o = x by Z2;
hence thesis by FUNCT_2:6;
end;
registration
cluster MaxConstrSign -> with_an_operation_for_each_sort;
coherence
proof
set C = MaxConstrSign;
set m = [a_Type, [{}, 0]], a = [an_Adj, [{}, 0]], f = [a_Term, [{}, 0]];
a_Type in {a_Type} & an_Adj in {an_Adj} & a_Term in {a_Term} &
[<*> Vars, 0] in [:QuasiLoci, NAT:]
by Th31,ZFMISC_1:def 2,TARSKI:def 1; then
A0: m in Modes & a in Attrs & f in Funcs by ZFMISC_1:def 2; then
m in Modes \/ Attrs & a in Modes \/ Attrs by XBOOLE_0:def 2; then
m in Constructors & a in Constructors & f in Constructors &
the OperSymbols of MaxConstrSign = {*, non_op} \/ Constructors
by A0,MAXdef,XBOOLE_0:def 2; then
reconsider m,a,f as OperSymbol of MaxConstrSign by XBOOLE_0:def 2;
m is constructor & a is constructor & f is constructor by CNSTR2; then
(the ResultSort of C).m = m`1 & (the ResultSort of C).a = a`1 &
(the ResultSort of C).f = f`1 by MAXdef; then
A1: (the ResultSort of C).m = a_Type & (the ResultSort of C).a = an_Adj &
(the ResultSort of C).f = a_Term by MCART_1:7;
A2: the carrier of C = {a_Type, an_Adj, a_Term} by CONSTRSIGN;
let x be set; assume x in the carrier of C; then
x = a_Type or x = an_Adj or x = a_Term by A2,ENUMSET1:def 1;
hence thesis by A1,FUNCT_2:6;
end;
let C be ConstructorSignature;
cluster MSVars C -> with_missing_variables;
coherence
proof set X = MSVars C;
let x be set; assume x in X"{{}}; then
A1: x in dom X & X.x in {{}} by FUNCT_1:def 13; then
x in the carrier of C by PBOOLE:def 3; then
x in {a_Type, an_Adj, a_Term} by CONSTRSIGN; then
A2: x = a_Type or x = an_Adj or x = a_Term by ENUMSET1:def 1;
A3: X.x = {} by A1,TARSKI:def 1;
(the ResultSort of C).(ast C) = a_Type &
(the ResultSort of C).(non_op C) = an_Adj by CONSTRSIGN;
hence thesis by A2,A3,MSVARS,FUNCT_2:6;
end;
end;
registration
let S be ManySortedSign;
cluster non-empty -> with_missing_variables
ManySortedSet of the carrier of S;
coherence
proof let X be ManySortedSet of the carrier of S such that
A0: X is non-empty;
let x be set; assume x in X"{{}}; then
x in dom X & X.x in {{}} by FUNCT_1:def 13; then
X.x in rng X & X.x = {} by TARSKI:def 1,FUNCT_1:def 5;
hence thesis by A0,RELAT_1:def 9;
end;
end;
registration
let S be ManySortedSign;
cluster with_missing_variables ManySortedSet of the carrier of S;
existence
proof
consider A being non-empty ManySortedSet of the carrier of S;
take A; thus thesis;
end;
end;
registration
cluster initialized with_an_operation_for_each_sort
strict ConstructorSignature;
existence
proof take MaxConstrSign;
thus thesis;
end;
end;
registration
let C be with_an_operation_for_each_sort ManySortedSign;
cluster -> with_missing_variables ManySortedSet of the carrier of C;
coherence
proof
let X be ManySortedSet of the carrier of C;
A1: X"{{}} c= dom X by RELAT_1:167;
A2: dom X = the carrier of C by PBOOLE:def 3;
the carrier of C c= rng the ResultSort of C by WOFES;
hence X"{{}} c= rng the ResultSort of C by A1,A2,XBOOLE_1:1;
end;
end;
definition
let G be non empty DTConstrStr;
redefine
func Terminals G -> Subset of G;
coherence
proof
the carrier of G = Terminals G \/NonTerminals G by LANG1:1;
hence thesis by XBOOLE_1:7;
end;
func NonTerminals G -> Subset of G;
coherence
proof
the carrier of G = Terminals G \/NonTerminals G by LANG1:1;
hence thesis by XBOOLE_1:7;
end;
end;
theorem LemTerm0:
for D1,D2 being non empty DTConstrStr
st the Rules of D1 c= the Rules of D2
holds NonTerminals D1 c= NonTerminals D2 &
(the carrier of D1) /\ Terminals D2 c= Terminals D1 &
(Terminals D1 c= Terminals D2 implies the carrier of D1 c= the carrier of D2)
proof
let D1,D2 be non empty DTConstrStr such that
01: the Rules of D1 c= the Rules of D2;
thus
00: NonTerminals D1 c= NonTerminals D2
proof
let x be set; assume x in NonTerminals D1; then
ex s being Symbol of D1 st x = s &
ex n being FinSequence st s ==> n; then
consider s being Symbol of D1, n being FinSequence such that
02: x = s & s ==> n;
03: [s,n] in the Rules of D1 by 02,LANG1:def 1; then
[s,n] in the Rules of D2 by 01; then
reconsider s' = s as Symbol of D2 by ZFMISC_1:106;
s' ==> n by 01,03,LANG1:def 1;
hence thesis by 02;
end;
hereby let x be set; assume
x in (the carrier of D1) /\ Terminals D2; then
04: x in the carrier of D1 & x in Terminals D2 &
Terminals D2 \/ NonTerminals D2 = the carrier of D2
by XBOOLE_0:def 3,LANG1:1; then
reconsider s' = x as Symbol of D1;
reconsider s = x as Symbol of D2 by 04;
assume not x in Terminals D1; then
consider n being FinSequence such that
05: s' ==> n;
[s',n] in the Rules of D1 by 05,LANG1:def 1; then
s ==> n by 01,LANG1:def 1; then
not ex s being Symbol of D2 st x = s &
not ex n being FinSequence st s ==> n;
hence contradiction by 04;
end;
assume Terminals D1 c= Terminals D2; then
Terminals D1 \/ NonTerminals D1 c= Terminals D2 \/ NonTerminals D2
by 00,XBOOLE_1:13; then
Terminals D1 \/ NonTerminals D1 c= the carrier of D2 by LANG1:1;
hence thesis by LANG1:1;
end;
theorem LemTS0:
for D1,D2 being non empty DTConstrStr
st Terminals D1 c= Terminals D2 &
the Rules of D1 c= the Rules of D2
holds TS D1 c= TS D2
proof
let G,G' be non empty DTConstrStr such that
Z0: Terminals G c= Terminals G' and
Z1: the Rules of G c= the Rules of G';
Z2: the carrier of G' = (Terminals G') \/ NonTerminals G' &
the carrier of G c= the carrier of G' by Z0,Z1,LemTerm0,LANG1:1;
defpred P[set] means $1 in TS G';
A1: for s being Symbol of G st s in Terminals G holds P[root-tree s]
proof
let s be Symbol of G; assume
00: s in Terminals G; then
reconsider s' = s as Symbol of G' by Z0,Z2,XBOOLE_0:def 2;
root-tree s = root-tree s';
hence P[root-tree s] by 00,Z0,DTCONSTR:def 4;
end;
A2: for nt being Symbol of G,
ts being FinSequence of TS(G) st nt ==> roots ts &
for t being DecoratedTree of the carrier of G st t in rng ts
holds P[t]
holds P[nt-tree ts]
proof
let n be Symbol of G;
let s be FinSequence of TS(G) such that
01: [n, roots s] in the Rules of G and
02: for t being DecoratedTree of the carrier of G st t in rng s holds P[t];
rng s c= TS G'
proof
let x be set; assume
03: x in rng s; then
x is DecoratedTree of the carrier of G by TREES_3:def 6;
hence thesis by 02,03;
end; then
reconsider s' = s as FinSequence of TS G' by FINSEQ_1:def 4;
n in the carrier of G; then
reconsider n' = n as Symbol of G' by Z2;
n' ==> roots s' by Z1,01,LANG1:def 1;
hence thesis by DTCONSTR:def 4;
end;
A3: for t being DecoratedTree of the carrier of G
st t in TS(G) holds P[t]
from DTCONSTR:sch 7(A1,A2);
let x be set; assume
A4: x in TS G; then
reconsider t = x as Element of FinTrees(the carrier of G);
P[t] by A3,A4;
hence thesis;
end;
theorem LemX:
for S being ManySortedSign
for X,Y being ManySortedSet of the carrier of S st X c= Y
holds X is with_missing_variables implies Y is with_missing_variables
proof
let S be ManySortedSign;
let X,Y be ManySortedSet of the carrier of S such that
Z0: X c= Y and
Z1: X"{{}} c= rng the ResultSort of S;
let x be set; assume x in Y"{{}}; then
A0: x in dom Y & Y.x in {{}} & dom Y = the carrier of S &
dom X = the carrier of S by FUNCT_1:def 13,PBOOLE:def 3; then
Y.x = {} & X.x c= Y.x by Z0,TARSKI:def 1,PBOOLE:def 5; then
X.x = {} by XBOOLE_1:3; then
X.x in {{}} by TARSKI:def 1; then
x in X"{{}} by A0,FUNCT_1:def 13;
hence thesis by Z1;
end;
theorem LemY0:
for S being set
for X,Y being ManySortedSet of S st X c= Y
holds Union coprod X c= Union coprod Y
proof
let S be set;
let X,Y be ManySortedSet of S such that
Z0: X c= Y;
B0: dom X = S & dom Y = S by PBOOLE:def 3;
let x be set;
assume x in Union coprod X; then
B1: x`2 in dom X & x`1 in X.x`2 & x = [x`1,x`2] by CARD_3:33; then
X.x`2 c= Y.x`2 by Z0,B0,PBOOLE:def 5;
hence thesis by B0,B1,CARD_3:33;
end;
theorem
for S being non void Signature
for X,Y being ManySortedSet of the carrier of S st X c= Y
holds the carrier of DTConMSA X c= the carrier of DTConMSA Y
by LemY0,XBOOLE_1:9;
theorem ThTNT:
for S being non void Signature
for X being ManySortedSet of the carrier of S
st X is with_missing_variables
holds
NonTerminals DTConMSA X = [:the OperSymbols of S,{the carrier of S}:] &
Terminals DTConMSA X = Union coprod X
proof
let S be non void Signature;
let X be ManySortedSet of the carrier of S such that
A0: X is with_missing_variables;
set D = DTConMSA X,
A = [:the OperSymbols of S,{the carrier of S}:] \/
Union (coprod (X qua ManySortedSet of the carrier of S));
A1: Union(coprod X) misses [:the OperSymbols of S,{the carrier of S}:]
by MSAFREE:4;
A2: the carrier of D = (Terminals D) \/ (NonTerminals D) &
(Terminals D) misses (NonTerminals D) by DTCONSTR:8,LANG1:1;
thus NonTerminals DTConMSA X c= [:the OperSymbols of S,{the carrier of S}:]
by MSAFREE:6;
thus
A10:[:the OperSymbols of S,{the carrier of S}:] c= NonTerminals D
proof
let o,x2 be set; assume
A11: [o,x2] in [:the OperSymbols of S,{the carrier of S}:]; then
A12: o in the OperSymbols of S & x2 in {the carrier of S} by ZFMISC_1:106;then
reconsider o as OperSymbol of S;
A13: the carrier of S = x2 by A12,TARSKI:def 1; then
reconsider xa = [o,the carrier of S]
as Element of (the carrier of D) by A11,XBOOLE_0:def 2;
set O = the_arity_of o;
defpred P[set,set] means
$2 in A &
(X.(O.$1) <> {} implies $2 in coprod(O.$1,X)) &
(X.(O.$1) = {} implies ex o being OperSymbol of S st
$2 = [o,the carrier of S] & the_result_sort_of o = O.$1);
A14: for a be set st a in Seg len O ex b be set st P[a,b]
proof
let a be set; assume
a in Seg len O; then
A18: a in dom O by FINSEQ_1:def 3; then
A15: O.a in rng O & rng O c= the carrier of S by FUNCT_1:def 5; then
reconsider s = O.a as SortSymbol of S;
per cases;
suppose X.(O.a) is non empty;
then consider x be set such that
A16: x in X.(O.a) by XBOOLE_0:def 1;
take y = [x,O.a];
A19: y in coprod(O.a,X) by A15,A16,MSAFREE:def 2;
A20: O.a in rng O & rng O c= the carrier of S by A18,FUNCT_1:def 5;
dom coprod(X) = the carrier of S by PBOOLE:def 3;
then (coprod(X)).(O.a) in rng coprod(X) by A20,FUNCT_1:def 5;
then coprod(O.a,X) in rng coprod(X) by A20,MSAFREE:def 3;
then y in Union coprod(X) by A19,TARSKI:def 4;
hence thesis by A15,A16,MSAFREE:def 2,XBOOLE_0:def 2;
end;
suppose
AA: X.(O.a) = {}; then
consider o being OperSymbol of S such that
A3: the_result_sort_of o = s by A0,LemMV;
take y = [o,the carrier of S];
the carrier of S in {the carrier of S} by TARSKI:def 1; then
y in [:the OperSymbols of S,{the carrier of S}:] by ZFMISC_1:106;
hence thesis by AA,A3,XBOOLE_0:def 2;
end;
end;
consider b be Function such that
A17: dom b = Seg len O &
for a be set st a in Seg len O holds P[a,b.a] from CLASSES1:sch 1(A14);
reconsider b as FinSequence by A17,FINSEQ_1:def 2;
rng b c= A
proof let a be set; assume a in rng b;
then ex c being set st c in dom b & b.c = a by FUNCT_1:def 5;
hence a in A by A17;
end;
then reconsider b as FinSequence of A by FINSEQ_1:def 4;
reconsider b as Element of A* by FINSEQ_1:def 11;
A21: len b = len O by A17,FINSEQ_1:def 3;
now let c be set;
assume A22: c in dom b;
then A23: P[c,b.c] by A17;
dom O = Seg len O by FINSEQ_1:def 3;
then A24: O.c in rng O & rng O c= the carrier of S
by A17,A22,FUNCT_1:def 5;
dom coprod(X) = the carrier of S by PBOOLE:def 3;
then (coprod(X)).(O.c) in rng coprod(X) by A24,FUNCT_1:def 5;
then coprod(O.c,X) in rng coprod(X) by A24,MSAFREE:def 3; then
AB: X.(O.c) <> {} implies b.c in Union coprod(X) by A23,TARSKI:def 4;
thus b.c in [:the OperSymbols of S,{the carrier of S}:] implies
for o1 being OperSymbol of S st [o1,the carrier of S] = b.c
holds the_result_sort_of o1 = O.c
by A23,A1,AB,XBOOLE_0:3,ZFMISC_1:33;
assume
B1: b.c in Union (coprod X);
now assume X.(O.c) = {}; then
consider o being OperSymbol of S such that
B2: b.c = [o,the carrier of S] & the_result_sort_of o = O.c by A17,A22;
the carrier of S in {the carrier of S} by TARSKI:def 1; then
b.c in [:the OperSymbols of S,{the carrier of S}:]
by B2,ZFMISC_1:106;
hence contradiction by B1,A1,XBOOLE_0:3;
end;
hence b.c in coprod(O.c,X) by A17,A22;
end;
then [xa,b] in REL(X) by A21,MSAFREE:5;
then xa ==> b by LANG1:def 1;
hence thesis by A13;
end;
thus Terminals D c= Union coprod X
proof
let x be set; assume
A25: x in Terminals D; then
not x in [:the OperSymbols of S,{the carrier of S}:]
by A2,A10,XBOOLE_0:3;
hence thesis by A25,XBOOLE_0:def 2;
end;
thus Union coprod X c= Terminals DTConMSA X by MSAFREE:6;
end;
theorem
for S being non void Signature
for X,Y being ManySortedSet of the carrier of S
st X c= Y & X is with_missing_variables
holds
Terminals DTConMSA X c= Terminals DTConMSA Y &
the Rules of DTConMSA X c= the Rules of DTConMSA Y &
TS DTConMSA X c= TS DTConMSA Y
proof
let S be non void Signature;
let X,Y be ManySortedSet of the carrier of S such that
Z0: X c= Y and
Z1: X is with_missing_variables;
Z2: Y is with_missing_variables by Z0,Z1,LemX;
set G = DTConMSA X, G' = DTConMSA Y;
A1: the carrier of G c= the carrier of G' by Z0,LemY0,XBOOLE_1:9;
Terminals G = Union coprod X & Terminals G' = Union coprod Y
by Z1,Z2,ThTNT;
hence
A2: Terminals G c= Terminals G' by Z0,LemY0;
A3: (the carrier of G)* c= (the carrier of G')* by A1,FINSEQ_1:83;
thus the Rules of G c= the Rules of G'
proof
let a,b be set; assume
C1: [a,b] in the Rules of G; then
C2: a in [:the OperSymbols of S,{the carrier of S}:] &
b in ([:the OperSymbols of S,{the carrier of S}:] \/ Union coprod X)*
by MSAFREE1:2; then
consider a1,a2 being set such that
C3: a1 in the OperSymbols of S & a2 in {the carrier of S} & a = [a1,a2]
by ZFMISC_1:def 2;
reconsider a1 as OperSymbol of S by C3;
reconsider a as Element of [:the OperSymbols of S,{the carrier of S}:]
\/ Union coprod X by C2,XBOOLE_0:def 2;
reconsider a' = a as
Element of [:the OperSymbols of S,{the carrier of S}:]
\/ Union coprod Y by C2,XBOOLE_0:def 2;
reconsider b as Element of
([:the OperSymbols of S,{the carrier of S}:] \/ Union coprod X)* by C2;
reconsider b' = b as Element of
([:the OperSymbols of S,{the carrier of S}:] \/ Union coprod Y)*
by C2,A3;
now let o be OperSymbol of S; assume
C4: [o,the carrier of S] = a';
hence
CC: len b' = len (the_arity_of o) by C1,MSAFREE:def 9;
let x be set; assume
C5: x in dom b';
hence b'.x in [:the OperSymbols of S,{the carrier of S}:] implies
for o1 be OperSymbol of S st [o1,the carrier of S] = b.x
holds the_result_sort_of o1 = (the_arity_of o).x
by C1,C4,MSAFREE:def 9;
C6: Union coprod X misses [:the OperSymbols of S,{the carrier of S}:] &
Union coprod Y misses [:the OperSymbols of S,{the carrier of S}:]
by MSAFREE:4;
C7: b.x in [:the OperSymbols of S,{the carrier of S}:] \/ Union coprod X
by C5,DTCONSTR:2;
dom b' = Seg len b' & dom the_arity_of o = Seg len b'
by CC,FINSEQ_1:def 3; then
C9: (the_arity_of o).x in the carrier of S by C5,DTCONSTR:2;
assume b'.x in Union coprod Y; then
(b.x in [:the OperSymbols of S,{the carrier of S}:] or
b.x in Union coprod X) &
b.x nin [:the OperSymbols of S,{the carrier of S}:]
by C6,C7,XBOOLE_0:3,def 2; then
b.x in coprod((the_arity_of o).x,X) by C1,C4,C5,MSAFREE:def 9; then
consider a being set such that
C8: a in X.((the_arity_of o).x) & b.x = [a, (the_arity_of o).x]
by C9,MSAFREE:def 2;
X.((the_arity_of o).x) c= Y.((the_arity_of o).x)
by Z0,C9,PBOOLE:def 5;
hence b'.x in coprod((the_arity_of o).x,Y) by C8,C9,MSAFREE:def 2;
end;
hence thesis by C2,MSAFREE:def 9;
end;
hence thesis by A2,LemTS0;
end;
theorem LemTerm:
for t being set holds
t in Terminals DTConMSA MSVars C iff
ex x being variable st t = [x,a_Term C]
proof
let t be set;
set X = MSVars C;
A0: Terminals DTConMSA X = Union coprod X by ThTNT;
A1: dom X = the carrier of C by PBOOLE:def 3;
A2: the carrier of C = {a_Type, an_Adj, a_Term} by CONSTRSIGN;
A3: X.a_Type = {} & X.an_Adj = {} & X.a_Term = Vars by MSVARS;
hereby assume
t in Terminals DTConMSA X; then
A4: t`2 in dom X & t`1 in X.t`2 & t = [t`1,t`2] by A0,CARD_3:33; then
A5: t`2 = a_Type or t`2 = an_Adj or t`2 = a_Term
by A1,A2,ENUMSET1:def 1; then
reconsider x = t`1 as variable by A3,A4;
take x;
thus t = [x,a_Term C] by A3,A4,A5;
end;
given x being variable such that
A6: t = [x,a_Term C];
t`1 = x & t`2 = a_Term by A6,MCART_1:7;
hence t in Terminals DTConMSA MSVars C by A0,A1,A3,A6,CARD_3:33;
end;
theorem LemNTerm:
for t being set holds
t in NonTerminals DTConMSA MSVars C iff
t = [ast C, the carrier of C] or
t = [non_op C, the carrier of C] or
ex c being constructor OperSymbol of C st t = [c, the carrier of C]
proof
let t be set;
set X = MSVars C;
A0: NonTerminals DTConMSA X = [:the OperSymbols of C,{the carrier of C}:]
by ThTNT;
hereby assume t in NonTerminals DTConMSA MSVars C; then
consider a,b being set such that
A1: a in the OperSymbols of C & b in {the carrier of C} & t = [a,b]
by A0,ZFMISC_1:def 2;
reconsider a as OperSymbol of C by A1;
b = the carrier of C & (a is constructor or a is not constructor)
by A1,TARSKI:def 1;
hence t = [ast C, the carrier of C] or
t = [non_op C, the carrier of C] or
ex c being constructor OperSymbol of C st t = [c, the carrier of C]
by A1,CNSTR2;
end;
the carrier of C in {the carrier of C} by TARSKI:def 1;
hence thesis by A0,ZFMISC_1:106;
end;
theorem LemFT:
for S being non void Signature
for X being with_missing_variables ManySortedSet of the carrier of S
for t being set st t in Union the Sorts of Free(S,X)
holds t is Term of S, X \/ ((the carrier of S)-->{0})
proof
let S be non void Signature;
let X be with_missing_variables ManySortedSet of the carrier of S;
set V = X \/ ((the carrier of S)-->{0});
set A = Free(S, X);
set U = the Sorts of A;
A1: U = S-Terms(X, V) by MSAFREE3:25;
let t be set; assume
t in Union U; then
consider s being set such that
Z1: s in dom U & t in U.s by CARD_5:10;
reconsider s as SortSymbol of S by PBOOLE:def 3,Z1;
U.s = {r where r is Term of S,V: the_sort_of r = s & variables_in r c= X}
by A1,MSAFREE3:def 6; then
ex r being Term of S,V st t = r & the_sort_of r = s & variables_in r c= X
by Z1;
hence thesis;
end;
theorem
for S being non void Signature
for X being with_missing_variables ManySortedSet of the carrier of S
for t being Term of S, X \/ ((the carrier of S)-->{0})
st t in Union the Sorts of Free(S,X)
holds t in (the Sorts of Free(S,X)).the_sort_of t
proof
let S be non void Signature;
let X be with_missing_variables ManySortedSet of the carrier of S;
set V = X \/ ((the carrier of S)-->{0});
set A = Free(S, X);
set U = the Sorts of A;
A1: U = S-Terms(X, V) by MSAFREE3:25;
let t be Term of S, X \/ ((the carrier of S)-->{0}); assume
t in Union U; then
consider s being set such that
Z1: s in dom U & t in U.s by CARD_5:10;
reconsider s as SortSymbol of S by PBOOLE:def 3,Z1;
U.s = {r where r is Term of S,V: the_sort_of r = s & variables_in r c= X}
by A1,MSAFREE3:def 6; then
ex r being Term of S,V st t = r & the_sort_of r = s & variables_in r c= X
by Z1;
hence thesis by Z1;
end;
theorem
for G being non empty DTConstrStr
for s being Element of G
for p being FinSequence st s ==> p
holds p is FinSequence of the carrier of G
proof
let G be non empty DTConstrStr;
let s be Element of G;
let p be FinSequence;
assume s ==> p; then
[s,p] in the Rules of G by LANG1:def 1; then
p in (the carrier of G)* by ZFMISC_1:106;
hence p is FinSequence of the carrier of G by FINSEQ_1:def 11;
end;
theorem LemArr:
for S being non void Signature
for X,Y being ManySortedSet of the carrier of S
for g1 being Symbol of DTConMSA X
for g2 being Symbol of DTConMSA Y
for p1 being FinSequence of the carrier of DTConMSA X
for p2 being FinSequence of the carrier of DTConMSA Y
st g1 = g2 & p1 = p2 & g1 ==> p1
holds g2 ==> p2
proof
let S be non void Signature;
let X,Y be ManySortedSet of the carrier of S;
A1: dom X = the carrier of S & dom Y = the carrier of S by PBOOLE:def 3;
set G1 = DTConMSA X;
set G2 = DTConMSA Y;
let g1 be Symbol of G1;
let g2 be Symbol of G2;
let p1 be FinSequence of the carrier of G1;
let p2 be FinSequence of the carrier of G2; assume
A0: g1 = g2 & p1 = p2 & g1 ==> p1; then
Y4: [g1, p1] in REL X by LANG1:def 1; then
Y5: g1 in [:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X) &
p1 in ([:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X))*
by ZFMISC_1:106; then
Y6: g1 in [:the OperSymbols of S,{the carrier of S}:] by Y4,MSAFREE:def 9;
Y9: p2 in ([:the OperSymbols of S, {the carrier of S}:] \/
Union (coprod Y))* by FINSEQ_1:def 11;
now let o' be OperSymbol of S;
assume
Y7: [o',the carrier of S] = g2;
hence
Z4: len p2 = len the_arity_of o' by A0,Y4,Y5,MSAFREE:def 9;
let x be set; assume
Y8: x in dom p2;
hence p2.x in [:the OperSymbols of S,{the carrier of S}:]
implies
for o1 be OperSymbol of S st [o1,the carrier of S] = p2.x
holds the_result_sort_of o1 = (the_arity_of o').x
by A0,Y4,Y5,Y7,MSAFREE:def 9;
x in dom the_arity_of o' by Z4,Y8,FINSEQ_3:31; then
(the_arity_of o').x in rng the_arity_of o' by FUNCT_1:def 5; then
reconsider i = (the_arity_of o').x as SortSymbol of S;
assume p2.x in Union coprod Y; then
B1: (p2.x)`2 in dom Y & (p2.x)`1 in Y.(p2.x)`2 & p2.x = [(p2.x)`1,(p2.x)`2]
by CARD_3:33;
p2.x in rng p1 by A0,Y8,FUNCT_1:def 5; then
the carrier of S nin the carrier of S &
p2.x in [:the OperSymbols of S,{the carrier of S}:] or
p2.x in Union coprod X by XBOOLE_0:def 2; then
p2.x in coprod(i,X)
by A0,Y4,Y5,Y7,Y8,A1,B1,ZFMISC_1:129,MSAFREE:def 9; then
consider a being set such that
Z3: a in X.i & p2.x = [a,i] by MSAFREE:def 2;
i = (p2.x)`2 by B1,Z3,ZFMISC_1:33;
hence p2.x in coprod((the_arity_of o').x,Y) by B1,MSAFREE:def 2;
end; then
[g2, p2] in REL Y by A0,Y6,Y9,MSAFREE:def 9;
hence thesis by LANG1:def 1;
end;
theorem LemTS:
for S being non void Signature
for X being with_missing_variables ManySortedSet of the carrier of S holds
Union the Sorts of Free(S, X) = TS DTConMSA X
proof
let S be non void Signature;
let X be with_missing_variables ManySortedSet of the carrier of S;
set V = X \/ ((the carrier of S)-->{0});
set A = Free(S, X);
set U = the Sorts of A;
set G = DTConMSA X;
A1: U = S-Terms(X, V) by MSAFREE3:25;
A2: dom U = the carrier of S by PBOOLE:def 3;
defpred P[set] means $1 in Union U implies $1 in TS G;
T1: for s being SortSymbol of S, v being Element of V.s
holds P[root-tree [v,s]]
proof
let s be SortSymbol of S;
let v be Element of V.s;
assume root-tree [v,s] in Union U; then
consider s1 being set such that
Z1: s1 in dom U & root-tree [v,s] in U.s1 by CARD_5:10;
reconsider s1 as SortSymbol of S by Z1,PBOOLE:def 3;
U.s1={t where t is Term of S,V: the_sort_of t = s1 & variables_in t c= X}
by A1,MSAFREE3:def 6; then
consider t being Term of S,V such that
Z2: root-tree [v,s] = t & the_sort_of t = s1 & variables_in t c= X by Z1;
s1 = s & (variables_in t).s = {v} by Z2,MSATERM:14,MSAFREE3:11; then
{v} c= X.s by Z2,PBOOLE:def 5; then
v in X.s by ZFMISC_1:37; then
[v,s] in Terminals G by MSAFREE:7;
hence root-tree [v,s] in TS G by DTCONSTR:def 4;
end;
T2: for o being OperSymbol of S,
p being ArgumentSeq of Sym(o,V) st
for t being Term of S,V st t in rng p holds P[t]
holds P[[o,the carrier of S]-tree p]
proof
let o be OperSymbol of S;
let p be ArgumentSeq of Sym(o,V) such that
Y0: for t being Term of S,V st t in rng p holds P[t] and
Y1: [o,the carrier of S]-tree p in Union U;
consider s being set such that
Z1: s in dom U & [o,the carrier of S]-tree p in U.s by Y1,CARD_5:10;
reconsider s as SortSymbol of S by Z1,PBOOLE:def 3;
U.s={t where t is Term of S,V: the_sort_of t = s & variables_in t c= X}
by A1,MSAFREE3:def 6; then
consider t being Term of S,V such that
Z2: [o,the carrier of S]-tree p = t & the_sort_of t = s &
variables_in t c= X by Z1;
t.{} = [o,the carrier of S] by Z2,TREES_4:def 4; then
the_result_sort_of o = s by Z2,MSATERM:17; then
Y2: rng p c= Union U by A1,Z1,MSAFREE3:20;
rng p c= TS G
proof let x be set; assume
Y3: x in rng p; then
x is Term of S,V by Y2,LemFT;
hence x in TS G by Y0,Y2,Y3;
end; then
reconsider q = p as FinSequence of TS G by FINSEQ_1:def 4;
NonTerminals G = [:the OperSymbols of S,{the carrier of S}:]
by ThTNT; then
[o,the carrier of S] in NonTerminals G by ZFMISC_1:129; then
reconsider oo = [o,the carrier of S] as Symbol of G;
Sym(o,V) ==> roots p by MSATERM:21; then
oo ==> roots q by LemArr;
hence [o,the carrier of S]-tree p in TS G by DTCONSTR:def 4;
end;
TT: for t being Term of S,V holds P[t] from MSATERM:sch 1(T1,T2);
A4: NonTerminals DTConMSA X = [:the OperSymbols of S,{the carrier of S}:] &
Terminals DTConMSA X = Union coprod X by ThTNT;
defpred Q[set] means $1 in Union U;
D1: for s being Symbol of G st s in Terminals G holds Q[root-tree s]
proof let s be Symbol of G;
assume s in Terminals G; then
B1: s`2 in dom X & s`1 in X.s`2 & s = [s`1,s`2] by A4,CARD_3:33;
B2: dom X = the carrier of S & dom U = the carrier of S by PBOOLE:def 3; then
root-tree s in (the Sorts of Free(S,X)).s`2 by B1,MSAFREE3:5;
hence Q[root-tree s] by B1,B2,CARD_5:10;
end;
D2: for nt being Symbol of G, ts being FinSequence of TS G st nt ==> roots ts &
for t being DecoratedTree of the carrier of G st t in rng ts holds Q[t]
holds Q[nt-tree ts]
proof let nt be Symbol of G;
let ts be FinSequence of TS G such that
Z1: nt ==> roots ts and
Z2: for t being DecoratedTree of the carrier of G st t in rng ts holds Q[t];
nt in NonTerminals G by Z1; then
consider o,z being set such that
Z3: o in the OperSymbols of S & z in {the carrier of S} & nt = [o,z]
by A4,ZFMISC_1:def 2;
reconsider o as OperSymbol of S by Z3;
Z5: rng ts c= Union U
proof
let a be set; assume
Z6: a in rng ts;
a is DecoratedTree of the carrier of G by Z6,TREES_3:def 6;
hence thesis by Z2,Z6;
end;
rng ts c= TS DTConMSA V
proof let a be set; assume
a in rng ts; then
a is Element of S-TermsV & S-TermsV = TS DTConMSA V
by Z5,LemFT,MSATERM:def 1;
hence thesis;
end; then
reconsider p = ts as FinSequence of TS DTConMSA V by FINSEQ_1:def 4;
reconsider q = p as FinSequence of S-TermsV by MSATERM:def 1;
Z4: z = the carrier of S by Z3,TARSKI:def 1; then
Sym(o, V) ==> roots p by Z1,Z3,LemArr; then
reconsider q as ArgumentSeq of Sym(o, V) by MSATERM:21;
set t = Sym(o, V)-tree q;
t in U.the_result_sort_of o by A1,Z5,MSAFREE3:20;
hence Q[nt-tree ts] by A2,Z3,Z4,CARD_5:10;
end;
DD: for t being DecoratedTree of the carrier of G
st t in TS G holds Q[t] from DTCONSTR:sch 7(D1,D2);
thus Union U c= TS DTConMSA X
proof let x be set;
assume
B1: x in Union U; then
consider s being set such that
B2: s in dom U & x in U.s by CARD_5:10;
reconsider s as SortSymbol of S by PBOOLE:def 3,B2;
x in U.s by B2; then
x is Term of S,V by A1,MSAFREE3:17;
hence thesis by B1,TT;
end;
let x be set;
assume
C0: x in TS G; then
reconsider TG = TS G as non empty Subset of FinTrees(the carrier of G);
x is Element of TG by C0;
hence thesis by DD;
end;
definition
let S be non void Signature;
let X be ManySortedSet of the carrier of S;
mode term-transformation of S,X -> UnOp of Union the Sorts of Free(S,X) means
:TT:
for s being SortSymbol of S holds
it.:((the Sorts of Free(S,X)).s) c= (the Sorts of Free(S,X)).s;
existence
proof
set f = id Union the Sorts of Free(S,X);
dom f = Union the Sorts of Free(S,X) & rng f = Union the Sorts of Free(S,X)
by RELAT_1:71; then
reconsider f as UnOp of Union the Sorts of Free(S,X) by FUNCT_2:4;
:: Zamiast RELAT_1:71 i FUNCT_2:4 powinna byc mozliwosc odwolania
:: sie do redefinicji PARTFUN1:func 6
take f;
thus thesis by Lem'id;
end;
end;
theorem ThTr:
for S being non void Signature
for X being non empty ManySortedSet of the carrier of S
for f being UnOp of Union the Sorts of Free(S,X)
holds f is term-transformation of S,X iff
for s being SortSymbol of S
for a being set st a in (the Sorts of Free(S,X)).s
holds f.a in (the Sorts of Free(S,X)).s
proof
let S be non void Signature;
let X be non empty ManySortedSet of the carrier of S;
A0: dom the Sorts of Free(S,X) = the carrier of S by PBOOLE:def 3;
let f be UnOp of Union the Sorts of Free(S,X);
A1: dom f = Union the Sorts of Free(S,X) by FUNCT_2:67;
hereby assume
Z0: f is term-transformation of S,X;
let s be SortSymbol of S;
Z1: f.:((the Sorts of Free(S,X)).s) c= (the Sorts of Free(S,X)).s by TT,Z0;
(the Sorts of Free(S,X)).s in rng the Sorts of Free(S,X)
by A0,FUNCT_1:def 5; then
Z2: (the Sorts of Free(S,X)).s c= Union the Sorts of Free(S,X)
by ZFMISC_1:92;
let a be set;
assume a in (the Sorts of Free(S,X)).s; then
f.a in f.:((the Sorts of Free(S,X)).s) by A1,Z2,FUNCT_1:def 12;
hence f.a in (the Sorts of Free(S,X)).s by Z1;
end;
assume
A2: for s being SortSymbol of S
for a being set st a in (the Sorts of Free(S,X)).s
holds f.a in (the Sorts of Free(S,X)).s;
let s be SortSymbol of S;
let x be set; assume
x in f.:((the Sorts of Free(S,X)).s); then
ex a being set st a in dom f & a in (the Sorts of Free(S,X)).s & x = f.a
by FUNCT_1:def 12;
hence x in (the Sorts of Free(S,X)).s by A2;
end;
theorem ThTr2:
for S being non void Signature
for X being non empty ManySortedSet of the carrier of S
for f being term-transformation of S,X
for s being SortSymbol of S
for p being FinSequence of (the Sorts of Free(S,X)).s
holds f*p is FinSequence of (the Sorts of Free(S,X)).s &
Card (f*p qua set) = len p
proof
let S be non void Signature;
let X be non empty ManySortedSet of the carrier of S;
set A = Free(S,X);
let f be term-transformation of S,X;
let s be SortSymbol of S;
let p be FinSequence of (the Sorts of A).s;
Union the Sorts of A = {} or Union the Sorts of A <> {}; then
Z1: dom the Sorts of A = the carrier of S & dom f = Union the Sorts of A
by PBOOLE:def 3,FUNCT_2:def 1;
(the Sorts of A).s in rng the Sorts of A by Z1,FUNCT_1:def 5; then
(the Sorts of A).s c= Union the Sorts of A by ZFMISC_1:92; then
rng p c= dom f by Z1,XBOOLE_1:1; then
Z7: dom (f*p) = dom p by RELAT_1:46;
dom p = Seg len p by FINSEQ_1:def 3; then
Z2: f*p is FinSequence by Z7,FINSEQ_1:def 2;
rng(f*p) c= (the Sorts of A).s
proof let z be set; assume
z in rng(f*p); then
consider i being set such that
V1: i in dom(f*p) & z = (f*p).i by FUNCT_1:def 5;
p.i in rng p by Z7,V1,FUNCT_1:def 5; then
f.(p.i) in (the Sorts of A).s by ThTr;
hence thesis by V1,FUNCT_1:22;
end;
hence f*p is FinSequence of (the Sorts of Free(S,X)).s
by Z2,FINSEQ_1:def 4; then
reconsider q = f*p as FinSequence of (the Sorts of A).s;
thus Card (f*p qua set) = len q .= len p by Z7,FINSEQ_3:31;
end;
definition
let S be non void Signature;
let X be ManySortedSet of the carrier of S;
let t be term-transformation of S,X;
attr t is substitution means
for o being OperSymbol of S
for p,q being FinSequence of Free(S,X)
st [o, the carrier of S]-tree p in Union the Sorts of Free(S,X) & q = t*p
holds t.([o, the carrier of S]-tree p) = [o, the carrier of S]-tree q;
end;
scheme StructDef
{C() -> initialized ConstructorSignature,
V,N(set) -> (expression of C()),
F,A(set,set) -> (expression of C())}:
ex f being term-transformation of C(), MSVars C() st
(for x being variable holds f.(x-term C()) = V(x)) &
(for c being constructor OperSymbol of C()
for p,q being FinSequence of QuasiTerms C()
st len p = len the_arity_of c & q = f*p
holds f.(c-trm p) = F(c, q)) &
(for a being expression of C(), an_Adj C()
holds f.((non_op C())term a) = N(f.a)) &
(for a being expression of C(), an_Adj C()
for t being expression of C(), a_Type C()
holds f.((ast C())term(a,t)) = A(f.a, f.t))
provided
A1: for x being variable holds V(x) is quasi-term of C() and
A2: for c being constructor OperSymbol of C()
for p being FinSequence of QuasiTerms C()
st len p = len the_arity_of c
holds F(c, p) is expression of C(), the_result_sort_of c and
A3: for a being expression of C(), an_Adj C()
holds N(a) is expression of C(), an_Adj C() and
A4: for a being expression of C(), an_Adj C()
for t being expression of C(), a_Type C()
holds A(a,t) is expression of C(), a_Type C()
proof
set V = MSVars C();
set X = V\/((the carrier of C())-->{0});
set A = Free(C(), V);
set U = the Sorts of A;
set D = Union U;
set G = DTConMSA V;
deffunc TermVal(Symbol of G) = V($1`1);
deffunc NTermVal(Symbol of G, FinSequence, Function) =
IFEQ($1`1,*, A($3.1,$3.2), IFEQ($1`1,non_op, N($3.1), F($1`1,$3)));
consider f being Function of TS G, D such that
A6: for t being Symbol of G st t in Terminals G
holds f.(root-tree t) = TermVal(t) and
A7: for nt being Symbol of G, ts being FinSequence of TS G st nt ==> roots ts
holds f.(nt-tree ts) = NTermVal(nt, roots ts, f * ts)
from DTCONSTR:sch 8;
A5: D = TS G by LemTS; then
reconsider f as Function of D,D;
f is term-transformation of C(), V
proof
let s be SortSymbol of C();
let x be set; assume x in f.:((the Sorts of A).s); then
consider a being Element of D such that
B1: a in (the Sorts of A).s & x = f.a by FUNCT_2:116;
defpred P[expression of C()] means
for s being SortSymbol of C() st $1 in (the Sorts of A).s
holds f.$1 in (the Sorts of A).s;
W1: for x being variable holds P[x-term C()]
proof
let y be variable;
set a = y-term C();
let s be SortSymbol of C(); assume
C1: a in (the Sorts of A).s;
C2: [y,a_Term C()] in Terminals G by LemTerm; then
reconsider t = [y,a_Term C()] as Symbol of G;
f.a = TermVal(t) by A6,C2 .= V(y) by MCART_1:7; then
C3: f.a is quasi-term of C() & a is expression of C(), s
by A1,C1,ELEMENT; then
s = a_Term C() by Th90A;
hence thesis by C3,ELEMENT;
end;
W2: for c being constructor OperSymbol of C()
for p being FinSequence of QuasiTerms C()
st len p = len the_arity_of c &
for t being quasi-term of C() st t in rng p holds P[t]
holds P[c-trm p]
proof
let c be constructor OperSymbol of C();
let p be FinSequence of QuasiTerms C();
assume that
Z0: len p = len the_arity_of c and
Z1: for t being quasi-term of C() st t in rng p holds P[t];
set a = c-trm p;
set nt = [c, the carrier of C()];
let s be SortSymbol of C() such that
00: a in (the Sorts of A).s;
nt in NonTerminals G by LemNTerm; then
reconsider nt as Symbol of G;
reconsider ts = p as FinSequence of TS G by A5;
Z3: a = nt-tree ts by Z0,TERM;
reconsider aa = a as Term of C(), X by MSAFREE3:9;
the Sorts of A = C()-Terms(V,X) by MSAFREE3:25; then
the Sorts of A c= the Sorts of FreeMSA X by PBOOLE:def 23; then
(the Sorts of A).s c= (the Sorts of FreeMSA X).s by PBOOLE:def 5; then
aa in (FreeSort X).s by 00; then
aa in FreeSort(X,s) by MSAFREE:def 13; then
01: the_sort_of aa = s by MSATERM:def 5;
Z4: nt`1 = c & c <> * & c <> non_op by CNSTR2,MCART_1:7;
Z5: rng p c= QuasiTerms C() by FINSEQ_1:def 4;
dom f = D by FUNCT_2:def 1; then
Z7: rng p c= dom f;
rng(f*p) c= QuasiTerms C()
proof let z be set; assume
z in rng(f*p); then
consider i being set such that
V1: i in dom(f*p) & z = (f*p).i by FUNCT_1:def 5;
i in dom p by V1,Z7,RELAT_1:46; then
V2: p.i in rng p by FUNCT_1:def 5; then
reconsider pi = p.i as quasi-term of C() by Z5,Th42;
pi in (the Sorts of A).a_Term C() &
P[pi] by Z1,V2,Th42; then
f.pi in (the Sorts of A).a_Term C();
hence thesis by V1,FUNCT_1:22;
end; then
reconsider q = f*p as FinSequence of QuasiTerms C() by FINSEQ_1:def 4;
rng p c= C()-Terms X
proof
let z be set; assume z in rng p; then
z is Element of C()-TermsX by MSAFREE3:9;
hence thesis;
end; then
reconsider r = p as FinSequence of C()-Terms X by FINSEQ_1:def 4;
Z6: len q = len p by Z7,FINSEQ_2:33;
a is Term of C(), X by MSAFREE3:9; then
r is ArgumentSeq of Sym(c, X) by Z3,MSATERM:1; then
02: the_result_sort_of c = s &
Sym(c, X) ==> roots r by 01,Z3,MSATERM:20,21; then
nt ==> roots ts by LemArr; then
f.a = NTermVal(nt, roots ts, f * ts) by A7,Z3
.= IFEQ(c,non_op, N((f * ts).1), F(c, f * ts)) by Z4,FUNCOP_1:def 8
.= F(c, f * ts) by Z4,FUNCOP_1:def 8; then
f.a is expression of C(), the_result_sort_of c by Z0,Z6,A2;
hence f.a in (the Sorts of A).s by 02,ELEMENT;
end;
W3: for a being expression of C(), an_Adj C() st P[a]
holds P[(non_op C())term a]
proof
let v be expression of C(), an_Adj C() such that
Z1: P[v];
Y1: v in U.an_Adj C() by ELEMENT; then
Y2: f.v in U.an_Adj C() by Z1; then
reconsider fv = f.v as expression of C(), an_Adj C() by ELEMENT;
let s be SortSymbol of C(); assume
00: (non_op C())term v in U.s; then
(non_op C())term v is expression of C(), an_Adj C() &
(non_op C())term v is expression of C(), s by ELEMENT,ThNon; then
03: s = an_Adj C() by Th90A;
set QA = U.an_Adj C();
rng <*v*> = {v} by FINSEQ_1:55; then
rng <*v*> c= QA by Y1,ZFMISC_1:37; then
reconsider p = <*v*> as FinSequence of QA by FINSEQ_1:def 4;
set c = non_op C();
set a = (non_op C())term v;
set nt = [c, the carrier of C()];
nt in NonTerminals G by LemNTerm; then
reconsider nt as Symbol of G;
reconsider ts = p as FinSequence of TS G by A5;
Z3: a = nt-tree ts by ThNon;
reconsider aa = a as Term of C(), X by MSAFREE3:9;
the Sorts of A = C()-Terms(V,X) by MSAFREE3:25; then
the Sorts of A c= the Sorts of FreeMSA X by PBOOLE:def 23; then
(the Sorts of A).s c= (the Sorts of FreeMSA X).s by PBOOLE:def 5; then
aa in (FreeSort X).s by 00; then
aa in FreeSort(X,s) by MSAFREE:def 13; then
01: the_sort_of aa = s by MSATERM:def 5;
Z4: nt`1 = c & c <> * by MCART_1:7;
dom f = D by FUNCT_2:def 1; then
08: f*p = <*fv*> by BAGORDER:3;
rng <*fv*> = {fv} by FINSEQ_1:55; then
rng <*fv*> c= QA by Y2,ZFMISC_1:37; then
reconsider q = f*p as FinSequence of QA by 08,FINSEQ_1:def 4;
rng p c= C()-Terms X
proof
let z be set; assume z in rng p; then
z is expression of C(), an_Adj C() by Th42; then
z is Element of C()-TermsX by MSAFREE3:9;
hence thesis;
end; then
reconsider r = p as FinSequence of C()-Terms X by FINSEQ_1:def 4;
a is Term of C(), X by MSAFREE3:9; then
r is ArgumentSeq of Sym(c, X) by Z3,MSATERM:1; then
the_result_sort_of c = s &
Sym(c, X) ==> roots r by 01,Z3,MSATERM:20,21; then
nt ==> roots ts by LemArr; then
f.a = NTermVal(nt, roots ts, f * ts) by A7,Z3
.= IFEQ(c,non_op, N((f * ts).1), F(c, f * ts)) by Z4,FUNCOP_1:def 8
.= N((f*ts).1) by FUNCOP_1:def 8
.= N(fv) by 08,FINSEQ_1:57; then
f.a is expression of C(), an_Adj C() by A3;
hence f.a in (the Sorts of A).s by 03,ELEMENT;
end;
W4: for a being expression of C(), an_Adj C() st P[a]
for t being expression of C(), a_Type C() st P[t]
holds P[(ast C())term(a,t)]
proof
let v be expression of C(), an_Adj C() such that
Z0: P[v];
let t be expression of C(), a_Type C() such that
Z1: P[t];
v in U.an_Adj C() & t in U.a_Type C() by ELEMENT; then
Y2: f.v in U.an_Adj C() & f.t in U.a_Type C() by Z0,Z1; then
reconsider fv = f.v as expression of C(), an_Adj C() by ELEMENT;
reconsider ft = f.t as expression of C(), a_Type C() by Y2,ELEMENT;
let s be SortSymbol of C(); assume
00: (ast C())term(v,t) in U.s; then
(ast C())term(v,t) is expression of C(), a_Type C() &
(ast C())term(v,t) is expression of C(), s by ELEMENT,ThAst; then
03: s = a_Type C() by Th90A;
set QA = U.a_Type C();
reconsider p = <*v,t*> as FinSequence of D;
set c = ast C();
set a = (ast C())term(v,t);
set nt = [c, the carrier of C()];
nt in NonTerminals G by LemNTerm; then
reconsider nt as Symbol of G;
reconsider ts = p as FinSequence of TS G by A5;
Z3: a = nt-tree ts by ThAst;
reconsider aa = a as Term of C(), X by MSAFREE3:9;
the Sorts of A = C()-Terms(V,X) by MSAFREE3:25; then
the Sorts of A c= the Sorts of FreeMSA X by PBOOLE:def 23; then
(the Sorts of A).s c= (the Sorts of FreeMSA X).s by PBOOLE:def 5; then
aa in (FreeSort X).s by 00; then
aa in FreeSort(X,s) by MSAFREE:def 13; then
01: the_sort_of aa = s by MSATERM:def 5;
Z4: nt`1 = c & c <> non_op by MCART_1:7;
08: f*p = <*fv,ft*> by FINSEQ_2:40;
reconsider q = f*p as FinSequence of D;
rng p c= C()-Terms X
proof
let z be set; assume z in rng p; then
z is Element of C()-TermsX by MSAFREE3:9;
hence thesis;
end; then
reconsider r = p as FinSequence of C()-Terms X by FINSEQ_1:def 4;
a is Term of C(), X by MSAFREE3:9; then
r is ArgumentSeq of Sym(c, X) by Z3,MSATERM:1; then
the_result_sort_of c = s &
Sym(c, X) ==> roots r by 01,Z3,MSATERM:20,21; then
nt ==> roots ts by LemArr; then
f.a = NTermVal(nt, roots ts, f * ts) by A7,Z3
.= A((f*ts).1,(f*ts).2) by Z4,FUNCOP_1:def 8
.= A(fv,(f*ts).2) by 08,FINSEQ_1:61
.= A(fv,ft) by 08,FINSEQ_1:61; then
f.a is expression of C(), a_Type C() by A4;
hence f.a in (the Sorts of A).s by 03,ELEMENT;
end;
P[a] from StructInd(W1,W2,W3,W4);
hence thesis by B1;
end; then
reconsider f as term-transformation of C(), MSVars C();
take f;
hereby let x be variable;
x in Vars; then
00: x in V.a_Term C() by MSVARS; then
reconsider x' = x as Element of V.a_Term C();
reconsider xx = [x',a_Term C()] as Symbol of G by 00,MSAFREE3:3;
x-term C() = root-tree xx & xx in Terminals G by 00,MSAFREE:7;
hence f.(x-term C()) = V(xx`1) by A6 .= V(x) by MCART_1:7;
end;
hereby let c be constructor OperSymbol of C();
the carrier of C() in {the carrier of C()} by TARSKI:def 1; then
[c, the carrier of C()]in[:the OperSymbols of C(),{the carrier of C()}:]
by ZFMISC_1:106; then
reconsider cc = [c,the carrier of C()] as Symbol of G
by XBOOLE_0:def 2;
let p,q be FinSequence of QuasiTerms C();
assume
Z0: len p = len the_arity_of c & q = f*p;
set a = c-trm p;
set nt = [c, the carrier of C()];
nt in NonTerminals G by LemNTerm; then
reconsider nt as Symbol of G;
reconsider ts = p as FinSequence of TS G by A5;
Z3: a = nt-tree ts by Z0,TERM;
reconsider aa = a as Term of C(), X by MSAFREE3:9;
Z4: nt`1 = c & c <> * & c <> non_op by CNSTR2,MCART_1:7;
rng p c= C()-Terms X
proof
let z be set; assume z in rng p; then
z is Element of C()-TermsX by MSAFREE3:9;
hence thesis;
end; then
reconsider r = p as FinSequence of C()-Terms X by FINSEQ_1:def 4;
a is Term of C(), X by MSAFREE3:9; then
r is ArgumentSeq of Sym(c, X) by Z3,MSATERM:1; then
Sym(c, X) ==> roots r by MSATERM:21; then
nt ==> roots ts by LemArr; then
f.a = NTermVal(nt, roots ts, f * ts) by A7,Z3
.= IFEQ(c,non_op, N((f * ts).1), F(c, f * ts)) by Z4,FUNCOP_1:def 8
.= F(c, f * ts) by Z4,FUNCOP_1:def 8;
hence f.(c-trm p) = F(c, q) by Z0;
end;
hereby
let v be expression of C(), an_Adj C();
Y1: v in U.an_Adj C() by ELEMENT; then
Y2: f.v in U.an_Adj C() by ThTr; then
reconsider fv = f.v as expression of C(), an_Adj C() by ELEMENT;
set QA = U.an_Adj C();
rng <*v*> = {v} by FINSEQ_1:55; then
rng <*v*> c= QA by Y1,ZFMISC_1:37; then
reconsider p = <*v*> as FinSequence of QA by FINSEQ_1:def 4;
set c = non_op C();
set a = (non_op C())term v;
set nt = [c, the carrier of C()];
nt in NonTerminals G by LemNTerm; then
reconsider nt as Symbol of G;
reconsider ts = p as FinSequence of TS G by A5;
Z3: a = nt-tree ts by ThNon;
reconsider aa = a as Term of C(), X by MSAFREE3:9;
Z4: nt`1 = c & c <> * by MCART_1:7;
dom f = D by FUNCT_2:def 1; then
08: f*p = <*fv*> by BAGORDER:3;
rng <*fv*> = {fv} by FINSEQ_1:55; then
rng <*fv*> c= QA by Y2,ZFMISC_1:37; then
reconsider q = f*p as FinSequence of QA by 08,FINSEQ_1:def 4;
rng p c= C()-Terms X
proof
let z be set; assume z in rng p; then
z is expression of C(), an_Adj C() by Th42; then
z is Element of C()-TermsX by MSAFREE3:9;
hence thesis;
end; then
reconsider r = p as FinSequence of C()-Terms X by FINSEQ_1:def 4;
a is Term of C(), X by MSAFREE3:9; then
r is ArgumentSeq of Sym(c, X) by Z3,MSATERM:1; then
Sym(c, X) ==> roots r by MSATERM:21; then
nt ==> roots ts by LemArr; then
f.a = NTermVal(nt, roots ts, f * ts) by A7,Z3
.= IFEQ(c,non_op, N((f * ts).1), F(c, f * ts)) by Z4,FUNCOP_1:def 8
.= N((f*ts).1) by FUNCOP_1:def 8;
hence f.((non_op C())term v) = N(f.v) by 08,FINSEQ_1:57;
end;
let v be expression of C(), an_Adj C();
let t be expression of C(), a_Type C();
v in U.an_Adj C() & t in U.a_Type C() by ELEMENT; then
Y2: f.v in U.an_Adj C() & f.t in U.a_Type C() by ThTr; then
reconsider fv = f.v as expression of C(), an_Adj C() by ELEMENT;
reconsider ft = f.t as expression of C(), a_Type C() by Y2,ELEMENT;
reconsider p = <*v,t*> as FinSequence of D;
set c = ast C();
set a = (ast C())term(v,t);
set nt = [c, the carrier of C()];
nt in NonTerminals G by LemNTerm; then
reconsider nt as Symbol of G;
reconsider ts = p as FinSequence of TS G by A5;
Z3: a = nt-tree ts by ThAst;
reconsider aa = a as Term of C(), X by MSAFREE3:9;
Z4: nt`1 = c & c <> non_op by MCART_1:7;
08: f*p = <*fv,ft*> by FINSEQ_2:40;
reconsider q = f*p as FinSequence of D;
rng p c= C()-Terms X
proof
let z be set; assume z in rng p; then
z is Element of C()-TermsX by MSAFREE3:9;
hence thesis;
end; then
reconsider r = p as FinSequence of C()-Terms X by FINSEQ_1:def 4;
a is Term of C(), X by MSAFREE3:9; then
r is ArgumentSeq of Sym(c, X) by Z3,MSATERM:1; then
Sym(c, X) ==> roots r by MSATERM:21; then
nt ==> roots ts by LemArr; then
f.a = NTermVal(nt, roots ts, f * ts) by A7,Z3
.= A((f*ts).1,(f*ts).2) by Z4,FUNCOP_1:def 8
.= A(fv,(f*ts).2) by 08,FINSEQ_1:61;
hence thesis by 08,FINSEQ_1:61;
end;
begin :: Substitution
definition
let A be set;
let x,y be set;
let a,b be Element of A;
redefine func IFIN(x,y,a,b) -> Element of A;
coherence by MATRIX_7:def 1;
end;
definition
let C be initialized ConstructorSignature;
mode valuation of C is PartFunc of Vars, QuasiTerms C;
end;
definition
let C be initialized ConstructorSignature;
let f be valuation of C;
attr f is irrelevant means:
IRR:
for x being variable st x in dom f
ex y being variable st f.x = y-term C;
end;
notation
let C be initialized ConstructorSignature;
let f be valuation of C;
antonym f is relevant for f is irrelevant;
end;
registration
let X,Y be set;
cluster empty PartFunc of X,Y;
existence
proof
dom {} = {}; then
{} is PartFunc of X,Y by PARTFUN1:55;
hence thesis;
end;
end;
registration
let C be initialized ConstructorSignature;
cluster empty -> irrelevant valuation of C;
coherence
proof
let f be valuation of C; assume
f is empty; then
reconsider f as empty valuation of C;
let x be variable;
dom f = {};
hence thesis;
end;
end;
registration
let C be initialized ConstructorSignature;
cluster empty irrelevant one-to-one valuation of C;
existence
proof consider f being empty valuation of C;
take f;
thus thesis;
end;
end;
definition
let C be initialized ConstructorSignature;
let X be Subset of Vars;
func C idval X -> valuation of C equals
{[x, x-term C] where x is variable: x in X};
coherence
proof
set f = {[x, x-term C] where x is variable: x in X};
defpred P[variable,set] means $2 = $1-term C;
AA: now let x be variable;
reconsider t = x-term C as Element of QuasiTerms C by ELEMENT;
take t; thus P[x,t];
end;
consider g being Function of Vars, QuasiTerms C such that
A0: for x being variable holds P[x,g.x] from FUNCT_2:sch 3(AA);
A1: f c= g
proof let a be set;
assume a in f; then
consider x being variable such that
A2: a = [x, x-term C] & x in X;
g.x = x-term C & dom g = Vars by A0,FUNCT_2:def 1;
hence thesis by A2,FUNCT_1:8;
end; then
f is Function by GRFUNC_1:6;
hence thesis by A1,PARTFUN1:33;
end;
end;
theorem ThIV:
for X being Subset of Vars
holds dom (C idval X) = X &
for x being variable st x in X holds (C idval X).x = x-term C
proof
let X be Subset of Vars;
set f = C idval X;
thus dom f c= X
proof
let a being set; assume a in dom f; then
[a,f.a] in f by FUNCT_1:def 4; then
ex x being variable st [a,f.a] = [x,x-term C] & x in X;
hence thesis by ZFMISC_1:33;
end;
hereby let x be set; assume
A0: x in X; then
reconsider a = x as variable;
[a,a-term C] in f by A0;
hence x in dom f by FUNCT_1:8;
end;
let x be variable;
assume x in X; then
[x,x-term C] in C idval X;
hence (C idval X).x = x-term C by FUNCT_1:8;
end;
registration
let C be initialized ConstructorSignature;
let X be Subset of Vars;
cluster C idval X -> irrelevant one-to-one;
coherence
proof
set f = C idval X;
A1: dom f = X by ThIV;
hereby let x be variable; assume
A0: x in dom f;
take y = x; thus f.x = y-term C by A0,A1,ThIV;
end;
let x,y be set; assume
A2: x in dom f & y in dom f; then
reconsider x,y as variable;
f.x = x-term C & f.y = y-term C by A1,A2,ThIV;
hence thesis by ThT0;
end;
end;
registration
let C be initialized ConstructorSignature;
let X be empty Subset of Vars;
cluster C idval X -> empty;
coherence
proof
dom (C idval X) = X by ThIV;
hence thesis by RELAT_1:64;
end;
end;
definition
let C;
let f be valuation of C;
func f# -> term-transformation of C, MSVars C means:
SUBST:
(for x being variable holds
(x in dom f implies it.(x-term C) = f.x) &
(not x in dom f implies it.(x-term C) = x-term C)) &
(for c being constructor OperSymbol of C
for p,q being FinSequence of QuasiTerms C
st len p = len the_arity_of c & q = it*p
holds it.(c-trm p) = c-trm q) &
(for a being expression of C, an_Adj C
holds it.((non_op C)term a) = (non_op C)term (it.a)) &
(for a being expression of C, an_Adj C
for t being expression of C, a_Type C
holds it.((ast C)term(a,t)) = (ast C)term(it.a, it.t));
existence
proof
deffunc V(variable) = IFIN($1, dom f,
(f/.$1 qua Element of (QuasiTerms C)
qua non empty Subset of Free(C, MSVars C))
qua (expression of C), $1-term C);
deffunc F(constructor OperSymbol of C,FinSequence of QuasiTerms C) =
$1-trm $2;
deffunc N(expression of C) = (non_op C)term $1;
deffunc A((expression of C), expression of C) = (ast C)term($1,$2);
A1: for x being variable holds V(x) is quasi-term of C
proof
let x be variable;
(x in dom f or not x in dom f) &
f/.x is quasi-term of C & x-term C is quasi-term of C by Th42;
hence V(x) is quasi-term of C by MATRIX_7:def 1;
end;
A2: for c being constructor OperSymbol of C
for p being FinSequence of QuasiTerms C
st len p = len the_arity_of c
holds F(c, p) is expression of C, the_result_sort_of c by Th43c;
A3: for a holds N(a) is expression of C, an_Adj C by ThNon;
A4: for a,t holds A(a,t) is expression of C, a_Type C by ThAst;
consider f' being term-transformation of C, MSVars C such that
A5: (for x being variable holds f'.(x-term C) = V(x)) &
(for c being constructor OperSymbol of C
for p,q being FinSequence of QuasiTerms C
st len p = len the_arity_of c & q = f'*p
holds f'.(c-trm p) = F(c, q)) &
(for a holds f'.((non_op C)term a) = N(f'.a)) &
(for a,t holds f'.((ast C)term(a,t)) = A(f'.a, f'.t))
from StructDef(A1,A2,A3,A4);
take f';
hereby let x be variable;
A6: f'.(x-term C) = V(x) by A5;
x in dom f implies f/.x = f.x by PARTFUN1:def 8;
hence x in dom f implies f'.(x-term C) = f.x by A6,MATRIX_7:def 1;
thus not x in dom f implies f'.(x-term C) = x-term C by A6,MATRIX_7:def 1;
end;
thus thesis by A5;
end;
correctness
proof let f1,f2 be term-transformation of C, MSVars C such that
A1: (for x being variable holds
(x in dom f implies f1.(x-term C) = f.x) &
(not x in dom f implies f1.(x-term C) = x-term C)) &
(for c being constructor OperSymbol of C
for p,q being FinSequence of QuasiTerms C
st len p = len the_arity_of c & q = f1*p
holds f1.(c-trm p) = c-trm q) &
(for a being expression of C, an_Adj C
holds f1.((non_op C)term a) = (non_op C)term (f1.a)) &
(for a being expression of C, an_Adj C
for t being expression of C, a_Type C
holds f1.((ast C)term(a,t)) = (ast C)term(f1.a, f1.t)) and
A2: (for x being variable holds
(x in dom f implies f2.(x-term C) = f.x) &
(not x in dom f implies f2.(x-term C) = x-term C)) &
(for c being constructor OperSymbol of C
for p,q being FinSequence of QuasiTerms C
st len p = len the_arity_of c & q = f2*p
holds f2.(c-trm p) = c-trm q) &
(for a being expression of C, an_Adj C
holds f2.((non_op C)term a) = (non_op C)term (f2.a)) &
(for a being expression of C, an_Adj C
for t being expression of C, a_Type C
holds f2.((ast C)term(a,t)) = (ast C)term(f2.a, f2.t));
set D = Union the Sorts of Free(C, MSVars C);
A3: dom f1 = D & dom f2 = D by FUNCT_2:def 1;
defpred P[expression of C] means f1.$1 = f2.$1;
W1: for x being variable holds P[x-term C]
proof
let x be variable;
x in dom f or x nin dom f; then
x in dom f & f1.(x-term C) = f.x or
x nin dom f & f1.(x-term C) = x-term C by A1;
hence P[x-term C] by A2;
end;
W2: for c being constructor OperSymbol of C
for p being FinSequence of QuasiTerms C
st len p = len the_arity_of c &
for t being quasi-term of C st t in rng p holds P[t]
holds P[c-trm p]
proof
let c be constructor OperSymbol of C;
let p be FinSequence of QuasiTerms C;
assume that
Z0: len p = len the_arity_of c and
Z1: for t being quasi-term of C st t in rng p holds P[t];
Z3: rng p c= QuasiTerms C & rng(f1*p) = f1.:rng p &
rng(f2*p) = f2.:rng p by RELAT_1:160,FINSEQ_1:def 4; then
rng(f1*p) c= f1.:QuasiTerms C & rng(f2*p) c= f2.:QuasiTerms C &
f1.:QuasiTerms C c= QuasiTerms C & f2.:QuasiTerms C c= QuasiTerms C
by TT,RELAT_1:156; then
rng(f1*p) c= QuasiTerms C & rng(f2*p) c= QuasiTerms C by XBOOLE_1:1; then
reconsider q1 = f1*p, q2 = f2*p as FinSequence of QuasiTerms C
by FINSEQ_1:def 4;
rng p c= D; then
Z2: dom q1 = dom p & dom q2 = dom p by A3,RELAT_1:46;
now
let i be Nat;
assume i in dom p; then
00: q1.i = f1.(p.i) & q2.i = f2.(p.i) & p.i in rng p
by FUNCT_1:23,def 5; then
p.i is quasi-term of C by Z3,Th42;
hence q1.i = q2.i by Z1,00;
end; then
q1 = q2 by Z2,FINSEQ_1:17; then
f1.(c-trm p) = c-trm q2 by A1,Z0;
hence P[c-trm p] by A2,Z0;
end;
W3: for a being expression of C, an_Adj C st P[a] holds P[(non_op C)term a]
proof
let a be expression of C, an_Adj C;
assume P[a]; then
f1.((non_op C)term a) = (non_op C)term (f2.a) by A1;
hence P[(non_op C)term a] by A2;
end;
W4: for a being expression of C, an_Adj C st P[a]
for t being expression of C, a_Type C st P[t]
holds P[(ast C)term(a,t)]
proof
let a be expression of C, an_Adj C such that
Y0: P[a];
let t be expression of C, a_Type C;
assume P[t]; then
f1.((ast C)term(a,t)) = (ast C)term(f2.a,f2.t) by A1,Y0;
hence P[(ast C)term(a,t)] by A2;
end;
now let t be expression of C;
thus P[t] from StructInd(W1,W2,W3,W4);
end;
hence thesis by FUNCT_2:113;
end;
end;
registration
let C;
let f be valuation of C;
cluster f# -> substitution;
coherence
proof
let o be OperSymbol of C;
let p,q be FinSequence of Free(C, MSVars C) such that
00: [o, the carrier of C]-tree p in Union the Sorts of Free(C, MSVars C) &
q = f# *p;
0D: dom (f# ) = Union the Sorts of Free(C, MSVars C) by FUNCT_2:def 1;
reconsider t = [o, the carrier of C]-tree p as expression of C by 00;
0R: t.{} = [o, the carrier of C] by TREES_4:def 4;
set V = (MSVars C)\/((the carrier of C)-->{0});
per cases by CNSTR2;
suppose o is constructor; then
reconsider c = o as constructor OperSymbol of C;
t = [c, the carrier of C]-tree p; then
01: len p = len the_arity_of c & p in (QuasiTerms C)* by Th83; then
reconsider p' = p as FinSequence of QuasiTerms C by FINSEQ_1:def 11;
reconsider q' = f# *p' as FinSequence of QuasiTerms C by ThTr2;
02: len q' = len p by ThTr2;
thus f# .([o, the carrier of C]-tree p)
= f# .(c-trm p') by 01,TERM
.= c-trm q' by 01,SUBST
.= [o, the carrier of C]-tree q by 00,01,02,TERM;
end;
suppose
X0: o = *; then
consider a being expression of C, an_Adj C,
s being expression of C, a_Type C such that
X1: t = (ast C)term(a,s) by 0R,ThAst2;
a in (the Sorts of Free(C, MSVars C)).an_Adj C by ELEMENT; then
f#.a in (the Sorts of Free(C, MSVars C)).an_Adj C by ThTr; then
reconsider fa = f#.a as expression of C, an_Adj C by Th42;
s in (the Sorts of Free(C, MSVars C)).a_Type C by ELEMENT; then
f#.s in (the Sorts of Free(C, MSVars C)).a_Type C by ThTr; then
reconsider fs = f#.s as expression of C, a_Type C by Th42;
t = [ast C, the carrier of C]-tree <*a,s*> by X1,ThAst; then
p = <*a,s*> & a in dom (f# ) & s in dom(f# ) by 0D,TREES_4:15; then
q = <*fa, fs*> by 00,FINSEQ_2:145; then
[o, the carrier of C]-tree q = (ast C)term(fa, fs) by X0,ThAst;
hence f# .([o, the carrier of C]-tree p) = [o, the carrier of C]-tree q
by X1,SUBST;
end;
suppose
X0: o = non_op; then
consider a such that
X1: t = (non_op C)term a by 0R,ThNon2;
a in (the Sorts of Free(C, MSVars C)).an_Adj C by ELEMENT; then
f#.a in (the Sorts of Free(C, MSVars C)).an_Adj C by ThTr; then
reconsider fa = f#.a as expression of C, an_Adj C by Th42;
t = [non_op C, the carrier of C]-tree <*a*> by X1,ThNon; then
p = <*a*> & a in dom (f# ) by 0D,TREES_4:15; then
q = <*fa*> by 00,BAGORDER:3; then
[o, the carrier of C]-tree q = (non_op C)term fa by X0,ThNon;
hence f# .([o, the carrier of C]-tree p) = [o, the carrier of C]-tree q
by X1,SUBST;
end;
end;
end;
reserve f for valuation of C;
definition
let C,f,e;
func e at f -> expression of C equals f#.e;
coherence;
end;
definition
let C,f;
let p be FinSequence such that
A: rng p c= Union the Sorts of Free(C, MSVars C);
func p at f -> FinSequence equals:
PF: f# * p;
coherence
proof
set A = Free(C, MSVars C);
dom (f# ) = Union the Sorts of A by FUNCT_2:def 1; then
Z7: dom (f# *p) = dom p by A,RELAT_1:46;
dom p = Seg len p by FINSEQ_1:def 3;
hence f# *p is FinSequence by Z7,FINSEQ_1:def 2;
end;
end;
definition
let C,f;
let p be FinSequence of QuasiTerms C;
redefine func p at f -> FinSequence of QuasiTerms C equals f# * p;
coherence
proof
A1: f# *p is FinSequence of QuasiTerms C by ThTr2;
rng p c= Union the Sorts of Free(C, MSVars C);
hence thesis by A1,PF;
end;
compatibility
proof
rng p c= Union the Sorts of Free(C, MSVars C);
hence thesis by PF;
end;
end;
reserve x for variable;
theorem ::?
not x in dom f implies (x-term C)at f = x-term C by SUBST;
theorem ::?
x in dom f implies (x-term C)at f = f.x by SUBST;
theorem ThS1: ::?
len p = len the_arity_of c implies (c-trm p)at f = c-trm p at f by SUBST;
theorem ::?
((non_op C)term a)at f = (non_op C)term(a at f) by SUBST;
theorem ::?
((ast C)term(a,t))at f = (ast C)term(a at f,t at f) by SUBST;
theorem ThS2':
for X being Subset of Vars
holds e at (C idval X) = e
proof set t = e;
let X be Subset of Vars;
set f = C idval X;
defpred P[expression of C] means $1 at f = $1;
W1: for x being variable holds P[x-term C]
proof let x be variable;
(x in X or x nin X) &
dom f = X & (x in X implies f.x = x-term C) by ThIV;
hence thesis by SUBST;
end;
W2: for c being constructor OperSymbol of C
for p being FinSequence of QuasiTerms C
st len p = len the_arity_of c &
for t being quasi-term of C st t in rng p holds P[t]
holds P[c-trm p]
proof
let c be constructor OperSymbol of C;
let p be FinSequence of QuasiTerms C such that
Z0: len p = len the_arity_of c and
Z1: for t being quasi-term of C st t in rng p holds P[t];
len (p at f) = len p by ThTr2; then
Z2: dom (p at f) = dom p by FINSEQ_3:31;
now
let i be Nat;
assume i in dom p; then
Z3: (p at f).i = f# .(p.i) & p.i in rng p by FUNCT_1:23,def 5;
rng p c= QuasiTerms C by FINSEQ_1:def 4; then
reconsider pi = p.i as quasi-term of C by Z3,Th42;
(p at f).i = pi at f by Z3;
hence (p at f).i = p.i by Z1,Z3;
end; then
p at f = p by Z2,FINSEQ_1:17;
hence P[c-trm p] by Z0,SUBST;
end;
W3: for a being expression of C, an_Adj C st P[a]
holds P[(non_op C)term a] by SUBST;
W4: for a being expression of C, an_Adj C st P[a]
for t being expression of C, a_Type C st P[t]
holds P[(ast C)term(a,t)] by SUBST;
thus P[t] from StructInd(W1,W2,W3,W4);
end;
theorem
for X being Subset of Vars
holds (C idval X)# = id Union the Sorts of Free(C, MSVars C)
proof let X be Subset of Vars;
set f = C idval X;
A0: dom (f# ) = Union the Sorts of Free(C, MSVars C) by FUNCT_2:def 1;
now
let x be set; assume x in Union the Sorts of Free(C, MSVars C); then
reconsider t = x as expression of C;
thus (f# ).x = t at f .= x by ThS2';
end;
hence f# = id Union the Sorts of Free(C, MSVars C) by A0,FUNCT_1:34;
end;
theorem ThS2:
for f being empty valuation of C
holds e at f = e
proof
let f be empty valuation of C;
consider X being empty Subset of Vars;
f = C idval X;
hence thesis by ThS2';
end;
theorem
for f being empty valuation of C
holds f# = id Union the Sorts of Free(C, MSVars C)
proof
let f be empty valuation of C;
A0: dom (f# ) = Union the Sorts of Free(C, MSVars C) by FUNCT_2:def 1;
now
let x be set; assume x in Union the Sorts of Free(C, MSVars C); then
reconsider t = x as expression of C;
thus (f# ).x = t at f .= x by ThS2;
end;
hence f# = id Union the Sorts of Free(C, MSVars C) by A0,FUNCT_1:34;
end;
:: theorem ::?
:: for t being expression of C
:: for f1,f2 being valuation of C
:: holds (t at f1) at f2 = ((f2# )*(f1# )).t by FUNCT_2:21;
definition
let C,f;
let t be quasi-term of C;
redefine func t at f -> quasi-term of C;
coherence
proof
t in QuasiTerms C by ELEMENT; then
t at f in QuasiTerms C by ThTr;
hence thesis by Th42;
end;
end;
definition
let C,f;
let a be expression of C, an_Adj C;
redefine func a at f -> expression of C, an_Adj C;
coherence
proof
a in (the Sorts of Free(C, MSVars C)).an_Adj C by ELEMENT; then
a at f in (the Sorts of Free(C, MSVars C)).an_Adj C by ThTr;
hence thesis by Th42;
end;
end;
registration
let C,f;
let a be positive expression of C, an_Adj C;
cluster a at f -> positive expression of C, an_Adj C;
coherence
proof consider v being constructor OperSymbol of C such that
A0: the_result_sort_of v = an_Adj C and
A1: ex p being FinSequence of QuasiTerms C st
len p = len the_arity_of v & a = v-trm p by ThPos;
consider p being FinSequence of QuasiTerms C such that
A2: len p = len the_arity_of v & a = v-trm p by A1;
len (p at f) = len p & a at f = v-trm(p at f) by A2,ThS1,ThTr2;
hence thesis by A0,A2,ThPos2;
end;
end;
Lemma:
for C be initialized ConstructorSignature,
f be valuation of C,
a be positive expression of C, an_Adj C holds
a at f is positive;
registration
let C,f;
let a be negative expression of C, an_Adj C;
cluster a at f -> negative expression of C, an_Adj C;
coherence
proof
(non_op C)term (Non a) = a by Th44b; then
a at f = (non_op C)term((Non a)at f) by SUBST
.= Non ((Non a)at f) by Th44;
hence thesis;
end;
end;
definition
let C,f;
let a be quasi-adjective of C;
redefine func a at f -> quasi-adjective of C;
coherence
proof
per cases by REG;
suppose a is positive; then
reconsider a as positive quasi-adjective of C;
a at f is positive;
hence thesis;
end;
suppose a is negative; then
reconsider a as negative quasi-adjective of C;
a at f is negative;
hence thesis;
end;
end;
end;
theorem
(Non a) at f = Non (a at f)
proof per cases;
suppose a is positive; then
reconsider b = a as positive expression of C, an_Adj C;
reconsider af = b at f as positive expression of C, an_Adj C by Lemma;
:: Niech madry czlowiek powie czemu jest potrzebna etykieta "Lemma"?!
thus (Non a) at f = ((non_op C)term b) at f by Th44
.= (non_op C)term af by SUBST
.= Non (a at f) by Th44;
end;
suppose a is non positive; then
consider b being expression of C, an_Adj C such that
A0: a = (non_op C)term b & Non a = b by Th45g;
A1: a at f = (non_op C)term(b at f) by A0,SUBST; then
a at f is non positive by POSITIVE; then
ex k being expression of C, an_Adj C st
a at f = (non_op C)term k & Non(a at f) = k by Th45g;
:: b at f = k by A1,A2,ThNon';
hence (Non a)at f = Non (a at f) by A0,A1,ThNon';
end;
end;
definition
let C,f;
let t be expression of C, a_Type C;
redefine func t at f -> expression of C, a_Type C;
coherence
proof
t in (the Sorts of Free(C, MSVars C)).a_Type C by ELEMENT; then
t at f in (the Sorts of Free(C, MSVars C)).a_Type C by ThTr;
hence thesis by Th42;
end;
end;
registration
let C,f;
let t be pure expression of C, a_Type C;
cluster t at f -> pure expression of C, a_Type C;
coherence
proof consider m being constructor OperSymbol of C such that
A0: the_result_sort_of m = a_Type C and
A1: ex p being FinSequence of QuasiTerms C st
len p = len the_arity_of m & t = m-trm p by ThPure;
consider p being FinSequence of QuasiTerms C such that
A2: len p = len the_arity_of m & t = m-trm p by A1;
len (p at f) = len p & t at f = m-trm(p at f) by A2,ThS1,ThTr2;
hence thesis by A0,A2,ThPure2;
end;
end;
theorem
for f being irrelevant one-to-one valuation of C
ex g being irrelevant one-to-one valuation of C
st for x,y being variable holds
x in dom f & f.x = y-term C iff y in dom g & g.y = x-term C
proof
let f be irrelevant one-to-one valuation of C;
set Y = {x where x is variable: x-term C in rng f};
defpred P[set,set] means
ex x being set st x in dom f & f.x = root-tree [ $1, a_Term] &
$2 = root-tree [x, a_Term];
B0: for x,y1,y2 being set st x in Y & P[x,y1] & P[x,y2] holds y1 = y2
by FUNCT_1:def 8;
B1: for x being set st x in Y ex y being set st P[x,y]
proof let x be set;
assume x in Y; then
B2: ex z being variable st x = z & z-term C in rng f; then
reconsider z = x as variable;
consider y being set such that
B3: y in dom f & z-term C = f.y by B2,FUNCT_1:def 5;
reconsider y as variable by B3;
take y-term C;
thus P[x,y-term C] by B3;
end;
consider g being Function such that
A0: dom g = Y and
A1: for y being set st y in Y holds P[y,g.y] from FUNCT_1:sch 2(B0,B1);
A2: Y c= Vars
proof let x be set;
assume x in Y; then
ex z being variable st x = z & z-term C in rng f;
hence thesis;
end;
rng g c= QuasiTerms C
proof let y be set; assume
y in rng g; then
consider x being set such that
C2: x in dom g & y = g.x by FUNCT_1:def 5;
reconsider x as variable by A0,A2,C2;
consider z being set such that
C3: z in dom f & f.z = x-term C & g.x = root-tree [z,a_Term] by A0,A1,C2;
reconsider z as variable by C3;
y = z-term C by C2,C3;
hence thesis by ELEMENT;
end; then
reconsider g as valuation of C by A0,A2,RELSET_1:11;
A3: g is irrelevant
proof
let x be variable; assume x in dom g; then
consider y being set such that
C1: y in dom f & f.y = x-term C & g.x = root-tree [y,a_Term] by A0,A1;
reconsider y as variable by C1;
take y; thus thesis by C1;
end;
g is one-to-one
proof
let z1,z2 be set; assume
C4: z1 in dom g & z2 in dom g & g.z1 = g.z2; then
reconsider z1,z2 as variable;
consider x1 being set such that
C5: x1 in dom f & f.x1 = z1-term C & g.z1 = root-tree[x1,a_Term] by A0,A1,C4;
consider x2 being set such that
C6: x2 in dom f & f.x2 = z2-term C & g.z1 = root-tree[x2,a_Term] by A0,A1,C4;
reconsider x1,x2 as variable by C5,C6;
x1-term C = x2-term C by C5,C6; then
x1 = x2 by ThT0;
hence thesis by C5,C6,ThT0;
end; then
reconsider g as irrelevant one-to-one valuation of C by A3;
take g;
let x,y be variable;
hereby assume
Z0: x in dom f & f.x = y-term C; then
f.x in rng f by FUNCT_1:def 5;
hence y in dom g by A0,Z0; then
P[y,g.y] by A0,A1;
hence g.y = x-term C by Z0,FUNCT_1:def 8;
end;
assume y in dom g & g.y = x-term C; then
consider z being set such that
Z2: z in dom f & f.z = root-tree [y, a_Term] & x-term C = root-tree [z, a_Term]
by A0,A1;
reconsider z as variable by Z2;
x-term C = z-term C by Z2;
hence thesis by Z2,ThT0;
end;
theorem
for f,g being irrelevant one-to-one valuation of C
st for x,y being variable holds
x in dom f & f.x = y-term C implies y in dom g & g.y = x-term C
for e st variables_in e c= dom f
holds e at f at g = e
proof
let f,g be irrelevant one-to-one valuation of C such that
A0: for x,y being variable holds
x in dom f & f.x = y-term C implies y in dom g & g.y = x-term C;
let t be expression of C;
defpred P[expression of C] means
variables_in $1 c= dom f implies $1 at f at g = $1;
W1: for x being variable holds P[x-term C]
proof let x be variable; assume
variables_in (x-term C) c= dom f; then
{x} c= dom f by MSAFREE3:11; then
A2: x in dom f by ZFMISC_1:37; then
consider y being variable such that
A3: f.x = y-term C by IRR;
y in dom g & g.y = x-term C & (x-term C) at f = y-term C
by A0,A2,A3,SUBST;
hence thesis by SUBST;
end;
W2: for c being constructor OperSymbol of C
for p being FinSequence of QuasiTerms C
st len p = len the_arity_of c &
for t being quasi-term of C st t in rng p holds P[t]
holds P[c-trm p]
proof
let c be constructor OperSymbol of C;
let p be FinSequence of QuasiTerms C such that
Z0: len p = len the_arity_of c and
Z1: for t being quasi-term of C st t in rng p holds P[t] and
00: variables_in (c-trm p) c= dom f;
c-trm p = [c, the carrier of C]-tree p by Z0,TERM; then
01: variables_in (c-trm p) = union {variables_in s where
s is quasi-term of C: s in rng p} by Th84;
Z5: len (p at f) = len p & len (p at f at g) = len (p at f) by ThTr2; then
Z2: dom (p at f) = dom p & dom (p at f at g) = dom (p at f) by FINSEQ_3:31;
now
let i be Nat;
assume i in dom p; then
Z3: (p at f).i = f# .(p.i) & (p at f at g).i = g# .((p at f).i) &
p.i in rng p by Z2,FUNCT_1:23,def 5;
rng p c= QuasiTerms C by FINSEQ_1:def 4; then
reconsider pi = p.i as quasi-term of C by Z3,Th42;
variables_in pi in {variables_in s where s is quasi-term of C:
s in rng p} by Z3; then
Z4: variables_in pi c= variables_in (c-trm p) by 01,ZFMISC_1:92;
(p at f at g).i = pi at f at g by Z3;
hence (p at f at g).i = p.i by Z1,Z3,Z4,00,XBOOLE_1:1;
end; then
p at f at g = p & (c-trm p) at f = c-trm (p at f)
by Z0,Z2,SUBST,FINSEQ_1:17;
hence (c-trm p) at f at g = c-trm p by Z0,Z5,SUBST;
end;
W3: for a being expression of C, an_Adj C st P[a]
holds P[(non_op C)term a]
proof
let a be expression of C, an_Adj C such that
A4: P[a] and
A5: variables_in ((non_op C)term a) c= dom f;
A6: (non_op C)term a = [non_op, the carrier of C]-tree <*a*> by ThNon;
thus ((non_op C)term a) at f at g
= ((non_op C)term (a at f)) at g by SUBST
.= (non_op C)term a by A4,A5,A6,Aux1,SUBST;
end;
W4: for a being expression of C, an_Adj C st P[a]
for t being expression of C, a_Type C st P[t]
holds P[(ast C)term(a,t)]
proof
let a be expression of C, an_Adj C such that
A7: P[a];
let t be expression of C, a_Type C such that
A8: P[t] and
A9: variables_in ((ast C)term(a,t)) c= dom f;
(ast C)term(a,t) = [ *, the carrier of C]-tree <*a,t*> by ThAst; then
AA: variables_in ((ast C)term(a,t))
= ((C variables_in a)\/(C variables_in t)).a_Term by Aux2
.= (variables_in a)\/variables_in t by PBOOLE:def 7;
thus ((ast C)term(a,t)) at f at g
= ((ast C)term (a at f, t at f)) at g by SUBST
.= (ast C)term(a,t) by A7,A8,AA,SUBST,A9,XBOOLE_1:11;
end;
thus P[t] from StructInd(W1,W2,W3,W4);
end;
definition
let C,f;
let A be Subset of QuasiAdjs C;
func A at f -> Subset of QuasiAdjs C equals
{a at f where a is quasi-adjective of C: a in A};
coherence
proof set X = {a at f where a is quasi-adjective of C: a in A};
X c= QuasiAdjs C
proof
let x be set; assume x in X; then
ex a being quasi-adjective of C st x = a at f & a in A;
hence thesis;
end;
hence thesis;
end;
end;
theorem ThZ0:
for A being Subset of QuasiAdjs C
for a being quasi-adjective of C st A = {a}
holds A at f = {a at f}
proof
let A be Subset of QuasiAdjs C;
let a be quasi-adjective of C such that
A0: A = {a};
thus A at f c= {a at f}
proof
let x be set; assume x in A at f; then
ex b being quasi-adjective of C st x = b at f & b in A; then
x = a at f by A0,TARSKI:def 1;
hence thesis by TARSKI:def 1;
end;
let x be set; assume x in {a at f}; then
x = a at f & a in A by A0,TARSKI:def 1;
hence thesis;
end;
theorem ThZ1:
for A,B being Subset of QuasiAdjs C
holds (A \/ B) at f = (A at f) \/ (B at f)
proof
let A,B be Subset of QuasiAdjs C;
thus (A \/ B) at f c= (A at f) \/ (B at f)
proof
let x be set; assume x in (A \/ B) at f; then
consider a being quasi-adjective of C such that
A1: x = a at f & a in A \/ B;
a in A or a in B by A1,XBOOLE_0:def 2; then
x in A at f or x in B at f by A1;
hence thesis by XBOOLE_0:def 2;
end;
let x be set; assume x in (A at f) \/ (B at f); then
x in (A at f) or x in (B at f) by XBOOLE_0:def 2; then
A c= A\/B & (ex a being quasi-adjective of C st x = a at f & a in A) or
B c= A\/B & ex a being quasi-adjective of C st x = a at f & a in B
by XBOOLE_1:7;
hence thesis;
end;
theorem
for A,B being Subset of QuasiAdjs C st A c= B
holds A at f c= B at f
proof
let A,B be Subset of QuasiAdjs C;
assume A c= B; then
A\/B = B by XBOOLE_1:12; then
B at f = (A at f)\/(B at f) by ThZ1;
hence A at f c= B at f by XBOOLE_1:7;
end;
registration
let C be initialized ConstructorSignature;
let f be valuation of C;
let A be finite Subset of QuasiAdjs C;
cluster A at f -> finite;
coherence
proof
A0: A is finite;
deffunc F(expression of C) = $1 at f;
A1: { F(w) where w is expression of C: w in A } is finite
from FRAENKEL:sch 21(A0);
A at f c= { F(w) where w is expression of C: w in A }
proof
let x be set; assume x in A at f; then
ex a being quasi-adjective of C st x = a at f & a in A;
hence thesis;
end;
hence thesis by A1,FINSET_1:13;
end;
end;
definition
let C be initialized ConstructorSignature;
let f be valuation of C;
let T be quasi-type of C;
func T at f -> quasi-type of C equals
((adjs T) at f)ast((the_base_of T) at f);
coherence;
end;
theorem ::?
for T being quasi-type of C
holds adjs(T at f) = (adjs T) at f &
the_base_of (T at f) = (the_base_of T) at f by MCART_1:7;
theorem
for T being quasi-type of C
for a being quasi-adjective of C
holds (a ast T) at f = (a at f) ast (T at f)
proof
let T be quasi-type of C;
let a be quasi-adjective of C;
a in QuasiAdjs C; then
reconsider A = {a} as Subset of QuasiAdjs C by ZFMISC_1:37;
thus (a ast T) at f
= [(adjs (a ast T)) at f ,((the_base_of T) at f)] by MCART_1:7
.= [(A\/(adjs T)) at f ,((the_base_of T) at f)] by MCART_1:7
.= [(A at f)\/((adjs T) at f),(the_base_of T) at f] by ThZ1
.= [{a at f}\/((adjs T) at f),(the_base_of T) at f] by ThZ0
.= [{a at f}\/(adjs (T at f)),(the_base_of T) at f] by MCART_1:7
.= (a at f) ast (T at f) by MCART_1:7;
end;
definition
let C be initialized ConstructorSignature;
let f,g be valuation of C;
func f at g -> valuation of C means:
SUBST2:
dom it = (dom f) \/ dom g &
for x being variable st x in dom it
holds it.x = ((x-term C) at f) at g;
existence
proof
deffunc h(set) = ((In($1,Vars)-term C) at f) at g;
consider h being Function such that
A0: dom h = (dom f) \/ dom g and
A1: for x being set st x in (dom f) \/ dom g holds h.x = h(x)
from FUNCT_1:sch 3;
rng h c= QuasiTerms C
proof
let y be set; assume y in rng h; then
consider x being set such that
A2: x in dom h & y = h.x by FUNCT_1:def 5;
y = h(x) by A0,A1,A2;
hence thesis by ELEMENT;
end; then
reconsider h as valuation of C by A0,RELSET_1:11;
take h; thus dom h = (dom f) \/ dom g by A0;
let x be variable;
assume x in dom h; then
h.x = h(x) by A0,A1;
hence thesis by FUNCT_7:def 1;
end;
uniqueness
proof
let h1,h2 be valuation of C such that
A1: dom h1 = (dom f) \/ dom g and
B1: for x being variable st x in dom h1
holds h1.x = ((x-term C) at f) at g and
A2: dom h2 = (dom f) \/ dom g and
B2: for x being variable st x in dom h2
holds h2.x = ((x-term C) at f) at g;
now let x be variable;
assume x in dom h1; then
h1.x = ((x-term C) at f) at g & h2.x = ((x-term C) at f) at g
by A1,A2,B1,B2;
hence h1.x = h2.x;
end;
hence thesis by A1,A2,PARTFUN1:34;
end;
end;
registration
let C be initialized ConstructorSignature;
let f,g be irrelevant valuation of C;
cluster f at g -> irrelevant;
coherence
proof
let x be variable; assume
A0: x in dom (f at g); then
A1: (f at g).x = ((x-term C) at f) at g by SUBST2;
A2: dom (f at g) = dom f \/ dom g by SUBST2;
per cases;
suppose
A3: x in dom f; then
consider y being variable such that
A4: f.x = y-term C by IRR;
(x-term C) at f = y-term C by A3,A4,SUBST; then
(y in dom g implies (f at g).x = g.y) &
(y nin dom g implies (f at g).x = y-term C) by A1,SUBST;
hence thesis by IRR;
end;
suppose x nin dom f; then
A7: (x-term C) at f = x-term C & x in dom g
by A0,A2,SUBST,XBOOLE_0:def 2; then
(f at g).x = g.x by A1,SUBST;
hence thesis by A7,IRR;
end;
end;
end;
theorem ThS3:
for f1,f2 being valuation of C
holds (e at f1) at f2 = e at (f1 at f2)
proof set t = e;
let f1,f2 be valuation of C;
A0: dom (f1 at f2) = (dom f1) \/ dom f2 by SUBST2;
defpred P[expression of C] means ($1 at f1) at f2 = $1 at (f1 at f2);
W1: for x being variable holds P[x-term C]
proof let x be variable;
per cases;
suppose
Z0: x in dom (f1 at f2); then
(x-term C) at (f1 at f2) = (f1 at f2).x by SUBST;
hence thesis by Z0,SUBST2;
end;
suppose
Z0: x nin dom (f1 at f2); then
x nin dom f1 & x nin dom f2 by A0,XBOOLE_0:def 2; then
(x-term C) at f1 = x-term C & (x-term C) at f2 = x-term C by SUBST;
hence thesis by Z0,SUBST;
end;
end;
W2: for c being constructor OperSymbol of C
for p being FinSequence of QuasiTerms C
st len p = len the_arity_of c &
for t being quasi-term of C st t in rng p holds P[t]
holds P[c-trm p]
proof
let c be constructor OperSymbol of C;
let p be FinSequence of QuasiTerms C such that
Z0: len p = len the_arity_of c and
Z1: for t being quasi-term of C st t in rng p holds P[t];
Z5: len (p at f1) = len p & len (p at (f1 at f2)) = len p &
len ((p at f1) at f2) = len (p at f1) by ThTr2; then
Z2: dom (p at f1) = dom p & dom (p at (f1 at f2)) = dom p &
dom ((p at f1) at f2) = dom p by FINSEQ_3:31;
now
let i be Nat;
assume i in dom p; then
Z3: ((p at f1) at f2).i = f2# .((p at f1).i) & (p at f1).i = f1# .(p.i) &
(p at (f1 at f2)).i = (f1 at f2)#.(p.i) & p.i in rng p
by Z2,FUNCT_1:23,def 5;
rng p c= QuasiTerms C by FINSEQ_1:def 4; then
reconsider pi = p.i as quasi-term of C by Z3,Th42;
thus (p at f1 at f2).i = (pi at f1) at f2 by Z3
.= pi at (f1 at f2) by Z1,Z3
.= (p at (f1 at f2)).i by Z3;
end; then
Z4: p at f1 at f2 = p at (f1 at f2) by Z2,FINSEQ_1:17;
thus (c-trm p) at f1 at f2 = (c-trm(p at f1)) at f2 by Z0,SUBST
.= c-trm (p at (f1 at f2)) by Z0,Z5,Z4,SUBST
.= (c-trm p) at (f1 at f2) by Z0,SUBST;
end;
W3: for a being expression of C, an_Adj C st P[a]
holds P[(non_op C)term a]
proof
let a be expression of C, an_Adj C;
assume P[a]; then
((non_op C)term (a at f1)) at f2 = (non_op C)term (a at (f1 at f2))
by SUBST
.= ((non_op C)term a) at (f1 at f2) by SUBST;
hence P[(non_op C)term a] by SUBST;
end;
W4: for a being expression of C, an_Adj C st P[a]
for t being expression of C, a_Type C st P[t]
holds P[(ast C)term(a,t)]
proof
let a be expression of C, an_Adj C such that
Z1: P[a];
let t be expression of C, a_Type C;
assume P[t]; then
((ast C)term (a at f1,t at f1)) at f2
= (ast C)term (a at (f1 at f2),t at (f1 at f2)) by Z1,SUBST
.= ((ast C)term(a,t)) at (f1 at f2) by SUBST;
hence P[(ast C)term(a,t)] by SUBST;
end;
thus P[t] from StructInd(W1,W2,W3,W4);
end;
theorem ThZ3:
for A being Subset of QuasiAdjs C
for f1,f2 being valuation of C
holds (A at f1) at f2 = A at (f1 at f2)
proof
let A be Subset of QuasiAdjs C;
let f1,f2 be valuation of C;
thus (A at f1) at f2 c= A at (f1 at f2)
proof
let x be set; assume x in (A at f1) at f2; then
consider a being quasi-adjective of C such that
A0: x = a at f2 & a in A at f1;
consider b being quasi-adjective of C such that
A1: a = b at f1 & b in A by A0;
x = b at (f1 at f2) by A0,A1,ThS3;
hence thesis by A1;
end;
let x be set; assume x in A at (f1 at f2); then
consider a being quasi-adjective of C such that
A2: x = a at (f1 at f2) & a in A;
x = a at f1 at f2 & a at f1 in A at f1 by A2,ThS3;
hence thesis;
end;
theorem
for T being quasi-type of C
for f1,f2 being valuation of C
holds (T at f1) at f2 = T at (f1 at f2)
proof
let T be quasi-type of C;
let f1,f2 be valuation of C;
thus (T at f1) at f2
= (((adjs T) at f1) at f2)ast((the_base_of (T at f1))at f2) by MCART_1:7
.= ((adjs T) at (f1 at f2))ast((the_base_of (T at f1))at f2) by ThZ3
.= ((adjs T) at (f1 at f2))ast(((the_base_of T) at f1)at f2) by MCART_1:7
.= T at (f1 at f2) by ThS3;
end;