:: Towards the construction of a model of Mizar concepts
:: by Grzegorz Bancerek
::
:: Received April 21, 2008
:: Copyright (c) 2008-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, NAT_1, SUBSET_1, FUNCT_1, TARSKI, CARD_3, RELAT_1,
XBOOLE_0, STRUCT_0, CATALG_1, PBOOLE, MSATERM, FACIRC_1, MSUALG_1,
ZFMISC_1, ZF_MODEL, FUNCOP_1, CARD_1, FINSEQ_1, TREES_3, TREES_4,
MARGREL1, MSAFREE, CLASSES1, SETFAM_1, FINSET_1, QC_LANG3, ARYTM_3,
XXREAL_0, ORDINAL1, MCART_1, FINSEQ_2, ORDINAL4, PARTFUN1, ABCMIZ_0,
FUNCT_2, FUNCT_4, ZF_LANG1, CAT_3, TREES_2, MSUALG_2, MEMBER_1, AOFA_000,
CARD_5, ORDERS_2, YELLOW_1, ARYTM_0, LATTICE3, EQREL_1, LATTICES,
YELLOW_0, ORDINAL2, WAYBEL_0, ASYMPT_0, LANG1, TDGROUP, DTCONSTR,
BINOP_1, MATRIX_7, FUNCT_7, ABCMIZ_1, SETLIM_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, DOMAIN_1,
SETFAM_1, RELAT_1, FUNCT_1, RELSET_1, BINOP_1, PARTFUN1, FACIRC_1,
ENUMSET1, FUNCT_2, PARTIT_2, FUNCT_4, FUNCOP_1, XXREAL_0, ORDINAL1,
XCMPLX_0, NAT_1, MCART_1, FINSET_1, CARD_1, NUMBERS, CARD_3, FINSEQ_1,
FINSEQ_2, TREES_2, TREES_3, TREES_4, FUNCT_7, PBOOLE, MATRIX_7, XXREAL_2,
STRUCT_0, LANG1, CLASSES1, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_0,
YELLOW_1, YELLOW_7, DTCONSTR, MSUALG_1, MSUALG_2, MSAFREE, EQUATION,
MSATERM, CATALG_1, MSAFREE3, AOFA_000, PRE_POLY;
constructors DOMAIN_1, MATRIX_7, MSAFREE1, FUNCT_7, EQUATION, YELLOW_1,
CATALG_1, LATTICE3, WAYBEL_0, FACIRC_1, CLASSES1, MSAFREE3, XXREAL_2,
RELSET_1, PRE_POLY, PARTIT_2, XTUPLE_0, XFAMILY, FINSEQOP;
registrations XBOOLE_0, SUBSET_1, XREAL_0, ORDINAL1, RELSET_1, FUNCT_1,
FINSET_1, STRUCT_0, PBOOLE, MSUALG_1, MSUALG_2, FINSEQ_1, CARD_1,
MSAFREE, FUNCOP_1, TREES_3, MSAFREE1, PARTFUN1, MSATERM, ORDERS_2,
TREES_2, DTCONSTR, WAYBEL_0, YELLOW_1, LATTICE3, MEMBERED, RELAT_1,
INDEX_1, INSTALG1, MSAFREE3, FACIRC_1, XXREAL_2, CLASSES1, FINSEQ_2,
PARTIT_2, XTUPLE_0;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
definitions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, FINSEQ_2, LANG1, PBOOLE,
TREES_3, MSUALG_1, WAYBEL_0, XTUPLE_0;
equalities TARSKI, RELAT_1, FINSEQ_1, LANG1, LATTICE3, MSAFREE, MSAFREE3,
CARD_3, MSUALG_1, ORDINAL1;
expansions TARSKI, FUNCT_1, LANG1, LATTICE3, PBOOLE, TREES_3;
theorems TARSKI, XBOOLE_0, XBOOLE_1, TREES_1, 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, ORDINAL3,
CARD_1, CARD_3, CARD_5, CLASSES1, ORDINAL1, SETFAM_1, MSUALG_2, TREES_4,
FINSEQ_3, FUNCOP_1, MSAFREE, MSATERM, MSAFREE3, PARTFUN1, LATTICE3,
YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_7, DTCONSTR, MSAFREE1, XXREAL_2,
CARD_2, XTUPLE_0;
schemes XBOOLE_0, FUNCT_1, NAT_1, FRAENKEL, 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 Th1:
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:3,def 2;
hence thesis by ZFMISC_1:74;
end;
theorem
for f being Function st Union f = {} holds f.x = {} by Th1,XBOOLE_1:3;
theorem Th3:
for f being Function for x,y being object st f = [x,y] holds x = y
proof
let f be Function, x,y be object;
assume
A1: f = [x,y];
then
A2: {x} in f by TARSKI:def 2;
A3: {x,y} in f by A1,TARSKI:def 2;
consider a,b being object such that
A4: {x} = [a,b] by A2,RELAT_1:def 1;
A5: {a} = {a,b} by A4,ZFMISC_1:5;
A6: x = {a} by A4,ZFMISC_1:4;
consider c,d being object such that
A7: {x,y} = [c,d] by A3,RELAT_1:def 1;
A8: x = {c} & y = {c,d} or x = {c,d} & y = {c} by A7,ZFMISC_1:6;
then c = a by A5,A6,ZFMISC_1:4;
hence thesis by A2,A3,A4,A5,A7,A8,FUNCT_1:def 1;
end;
theorem Th4:
(id X).:Y c= Y
proof
let x be object;
assume x in (id X).:Y;
then ex y being object st [y,x] in id X & y in Y by RELAT_1:def 13;
hence thesis by RELAT_1:def 10;
end;
theorem Th5:
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 object 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 carrier' 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 object st a in the carrier' of S &
b in {the carrier of S} & t.{} = [a,b] by ZFMISC_1:def 2;
then {{}} <> {{}, t.{}} by ZFMISC_1:5;
then
A2: [{}, t.{}] <> {x} by ZFMISC_1:5;
{} in dom t by TREES_1:22;
then [{}, t.{}] in t by FUNCT_1:def 2;
then
A3: [{}, t.{}] = {x,y} by A1,A2,TARSKI:def 2;
x = y by A1,Th3;
hence thesis by A2,A3,ENUMSET1:29;
end;
registration
let S be non void Signature;
let X be non empty-yielding ManySortedSet of the carrier of S;
cluster -> non pair for 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:8;
hence thesis by Th5;
end;
end;
theorem Th6:
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}* and
A2: y in {z}* and
A3: card x = card y;
reconsider x, y as FinSequence of {z} by A1,A2,FINSEQ_1:def 11;
A4: dom x = Seg len x by FINSEQ_1:def 3
.= dom y by A3,FINSEQ_1:def 3;
now
let i be Nat;
assume
A5: i in dom x;
then
A6: x .i in rng x by FUNCT_1:def 3;
A7: y.i in rng y by A4,A5,FUNCT_1:def 3;
thus x .i = z by A6,TARSKI:def 1
.= y.i by A7,TARSKI:def 1;
end;
hence thesis by A4,FINSEQ_1:13;
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 for FinSequence of Free(S,X);
coherence
proof
let p be FinSequence of Free(S,X);
let x be object;
assume x in rng p;
hence thesis;
end;
end;
theorem Th7:
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 t9 = t as Term of S,V by MSAFREE3:8;
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
A2: t is Element of Free(S,X);
{} in dom t by TREES_1:22;
then t.{} in rng t by FUNCT_1:3;
then [v,s] in rng t by TREES_4:3;
then v in X.s by A2,MSAFREE3:35;
hence thesis;
end;
A3: 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 object such that
A4: s in dom the Sorts of Free(S,X) and
A5: t in (the Sorts of Free(S,X)).s by CARD_5:2;
reconsider s as Element of S by A4;
A6: the Sorts of Free(S,X) = S-Terms(X,V) by MSAFREE3:24;
the_sort_of(Sym(o,V)-tree p) = the_result_sort_of o by MSATERM:20;
then s = the_result_sort_of o by A5,A6,MSAFREE3:17;
then rng p c= Union (S-Terms(X,V)) by A5,A6,MSAFREE3:19;
then
A7: p is FinSequence of Free(S,X) by A6,FINSEQ_1:def 4;
len the_arity_of o = len p by MSATERM:22;
hence thesis by A7;
end;
for t being Term of S,V holds P[t] from MSATERM:sch 1(A1,A3);
then P[t9];
hence thesis;
end;
definition
let A be set;
func varcl A -> set means
:
Def1: 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
A2: B1 c= B2;
B2 c= B1 by A1;
hence thesis by A1,A2,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;
A3: A c= Rank the_rank_of A by CLASSES1:def 9;
A4: now
let x,y;
assume
A5: [x,y] in Rank the_rank_of A;
A6: {x} in {{x,y},{x}} by TARSKI:def 2;
A7: {{x,y},{x}} c= Rank the_rank_of A by A5,ORDINAL1:def 2;
A8: x in {x} by TARSKI:def 1;
{x} c= Rank the_rank_of A by A6,A7,ORDINAL1:def 2;
hence x c= Rank the_rank_of A by A8,ORDINAL1:def 2;
end;
Rank the_rank_of A c= Rank the_rank_of A;
then
A9: Rank the_rank_of A in F by A3,A4;
hereby
let x be object;
assume
A10: 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 A10;
end;
hence x in D by A9,SETFAM_1:def 1;
end;
hereby
let x,y;
assume
A11: [x,y] in D;
thus x c= D
proof
let z be object;
assume
A12: z in x;
now
let X;
assume
A13: X in F;
then
A14: [x,y] in X by A11,SETFAM_1:def 1;
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 A13;
then x c= X by A14;
hence z in X by A12;
end;
hence thesis by A9,SETFAM_1:def 1;
end;
end;
let B being set;
assume that
A15: A c= B and
A16: 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;
A17: A c= C by A3,A15,XBOOLE_1:19;
now
let x,y;
assume
A18: [x,y] in C;
then [x,y] in B by XBOOLE_0:def 4;
then
A19: x c= B by A16;
x c= Rank the_rank_of A by A4,A18;
hence x c= C by A19,XBOOLE_1:19;
end;
then C in F by A17;
then
A20: D c= C by SETFAM_1:3;
C c= B by XBOOLE_1:17;
hence thesis by A20;
end;
projectivity;
end;
theorem Th8:
varcl {} = {}
proof
A1: 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 A1,Def1;
end;
theorem Th9:
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 Def1;
then
A2: A c= varcl B by A1;
for x,y st [x,y] in varcl B holds x c= varcl B by Def1;
hence thesis by A2,Def1;
end;
theorem Th10:
for A being set holds
varcl union A = union the set of all varcl a where a is Element of A
proof
let A be set;
set X = the set of all varcl a where a is Element of A;
A1: union A c= union X
proof
let x be object;
assume x in union A;
then consider Y such that
A2: x in Y and
A3: Y in A by TARSKI:def 4;
reconsider Y as Element of A by A3;
A4: Y c= varcl Y by Def1;
varcl Y in X;
hence thesis by A2,A4,TARSKI:def 4;
end;
now
let x,y be set;
assume [x,y] in union X;
then consider Y being set such that
A5: [x,y] in Y and
A6: Y in X by TARSKI:def 4;
ex a being Element of A st ( Y = varcl a) by A6;
then
A7: x c= Y by A5,Def1;
Y c= union X by A6,ZFMISC_1:74;
hence x c= union X by A7;
end;
hence varcl union A c= union X by A1,Def1;
let x be object;
assume x in union X;
then consider Y being set such that
A8: x in Y and
A9: Y in X by TARSKI:def 4;
consider a being Element of A such that
A10: Y = varcl a by A9;
A is empty or A is not empty;
then a in A or a is empty by SUBSET_1:def 1;
then a c= union A by ZFMISC_1:74;
then Y c= varcl union A by A10,Th9;
hence thesis by A8;
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]};
A1: union Z c= union X
proof
let x be object;
assume x in union Z;
then consider Y such that
A2: x in Y and
A3: Y in Z by TARSKI:def 4;
A4: ex z being Element of A() st ( Y = F(z))&( P[z]) by A3;
A5: Y c= varcl Y by Def1;
varcl Y in X by A4;
hence thesis by A2,A5,TARSKI:def 4;
end;
now
let x,y be set;
assume [x,y] in union X;
then consider Y being set such that
A6: [x,y] in Y and
A7: Y in X by TARSKI:def 4;
ex z being Element of A() st ( Y = varcl F(z))&( P[z]) by A7;
then
A8: x c= Y by A6,Def1;
Y c= union X by A7,ZFMISC_1:74;
hence x c= union X by A8;
end;
hence varcl union Z c= union X by A1,Def1;
let x be object;
assume x in union X;
then consider Y being set such that
A9: x in Y and
A10: Y in X by TARSKI:def 4;
consider z being Element of A() such that
A11: Y = varcl F(z) and
A12: P[z] by A10;
F(z) in Z by A12;
then Y c= varcl union Z by A11,Th9,ZFMISC_1:74;
hence thesis by A9;
end;
theorem Th11:
varcl (X \/ Y) = (varcl X) \/ (varcl Y)
proof
set A = the set of all varcl a where a is Element of {X,Y};
X \/ Y = union {X,Y} by ZFMISC_1:75;
then
A1: varcl (X \/ Y) = union A by Th10;
A = {varcl X, varcl Y}
proof
thus
now
let x be object;
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 be object;
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 thesis;
end;
hence thesis by A1,ZFMISC_1:75;
end;
theorem Th12:
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
A3: Y in B;
then
A4: [x,y] in Y by A2,SETFAM_1:def 1;
Y = varcl Y by A1,A3;
hence x c= Y by A4,Def1;
end;
hence x c= A by SETFAM_1:5;
end;
hence varcl A c= A by Def1;
thus thesis by Def1;
end;
theorem Th13:
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
A1: [x,y] in A;
then
A2: [x,y] in varcl X by XBOOLE_0:def 4;
A3: [x,y] in varcl Y by A1,XBOOLE_0:def 4;
A4: x c= varcl X by A2,Def1;
x c= varcl Y by A3,Def1;
hence x c= A by A4,XBOOLE_1:19;
end;
hence varcl ((varcl X) /\ (varcl Y)) c= (varcl X) /\ (varcl Y) by Def1;
thus thesis by Def1;
end;
registration
let A be empty set;
cluster varcl A -> empty;
coherence by Th8;
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 -> set means
:
Def2: ex V being ManySortedSet of NAT st it = Union V &
V.0 = the set of all [{}, i] where i is Element of NAT &
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 = the set of all [{}, i] where i is Element of NAT 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,PARTFUN1:def 2,RELAT_1:def 18;
take Union f, V = f;
thus Union f = Union V;
thus V.0 = the set of all [{}, i] where i is Element of NAT 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
A4: A1 = Union V1 and
A5: V1.0 = the set of all [{}, i] where i is Element of NAT and
A6: for n being Nat holds V1.(n+1) = F(n,V1.n);
given V2 being ManySortedSet of NAT such that
A7: A2 = Union V2 and
A8: V2.0 = the set of all [{}, i] where i is Element of NAT and
A9: for n being Nat holds V2.(n+1) = F(n,V2.n);
A10: dom V1 = NAT by PARTFUN1:def 2;
A11: dom V2 = NAT by PARTFUN1:def 2;
V1 = V2 from NAT_1:sch 15(A10,A5,A6,A11,A8,A9);
hence thesis by A4,A7;
end;
end;
theorem Th14:
for V being ManySortedSet of NAT st
V.0 = the set of all [{}, i] where i is Element of NAT &
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 = the set of all [{}, i] where i is Element of NAT 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;
A3: now
let j;
assume Q[j];
A4: 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 be object;
assume x in V.0;
then
A5: ex i being Element of NAT st x = [{}, i] by A1;
{} c= V.j;
hence thesis by A4,A5,Th8;
end;
end;
defpred P[Nat] means for i st i <= $1 holds V.i c= V.$1;
A6: P[ 0 ] by NAT_1:3;
A7: now
let j be Nat;
assume
A8: P[j];
A9: V.j c= V.(j+1) proof per cases by NAT_1:6;
suppose j = 0;
hence thesis by A3;
end;
suppose ex k being Nat st j = k+1;
then consider k being Nat such that
A10: j = k+1;
reconsider k as Element of NAT by ORDINAL1:def 12;
A11: V.j = {[varcl A, n] where A is Subset of V.k, n is Element of NAT:
A is finite} by A2,A10;
A12: V
.(j+1) = {[varcl A, n] where A is Subset of V.j,n is Element of NAT:
A is finite} by A2;
A13: V.k c= V.j by A8,A10,NAT_1:11;
let x be object;
assume x in V.j;
then consider A being Subset of V.k, n being Element of NAT such that
A14: x = [varcl A, n] and
A15: A is finite by A11;
A c= V.j by A13;
hence thesis by A12,A14,A15;
end;
end;
thus P[j+1]
proof
let i;
assume i <= j+1;
then i = j+1 or V.i c= V.j by A8,NAT_1:8;
hence thesis by A9;
end;
end;
for j being Nat holds P[j] from NAT_1:sch 2(A6,A7);
hence thesis;
end;
theorem Th15:
for V being ManySortedSet of NAT st
V.0 = the set of all [{}, i] where i is Element of NAT &
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 = the set of all [{}, i] where i is Element of NAT 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,Def2;
defpred P[object,object] means $1 in V.$2;
A4: now
let x be object;
assume x in A;
then consider Y such that
A5: x in Y and
A6: Y in rng V by A3,TARSKI:def 4;
consider i being object such that
A7: i in dom V and
A8: Y = V.i by A6,FUNCT_1:def 3;
reconsider i as object;
take i;
thus i in NAT & P[x,i] by A5,A7,A8;
end;
consider f being Function such that
A9: dom f = A & rng f c= NAT and
A10: for x being object st x in A holds P[x,f.x] from FUNCT_1:sch 6(A4);
per cases;
suppose A = {};
then A c= V.0;
hence thesis;
end;
suppose A <> {};
then reconsider B = rng f as finite non empty Subset of NAT
by A9,FINSET_1:8,RELAT_1:42;
reconsider i = max B as Element of NAT by ORDINAL1:def 12;
take i;
let x be object;
assume
A11: x in A;
then
A12: f.x in B by A9,FUNCT_1:def 3;
then reconsider j = f.x as Element of NAT;
j <= i by A12,XXREAL_2:def 8;
then
A13: V.j c= V.i by A1,A2,Th14;
x in V.j by A10,A11;
hence thesis by A13;
end;
end;
theorem Th16:
the set of all [{}, i] where i is Element of NAT c= Vars
proof consider V being ManySortedSet of NAT such that
A1: Vars = Union V and
A2: V.0 = the set of all [{}, i] where i is Element of NAT 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 Def2;
dom V = NAT by PARTFUN1:def 2;
then V.0 in rng V by FUNCT_1:def 3;
hence thesis by A1,A2,ZFMISC_1:74;
end;
theorem Th17:
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
A1: Vars = Union V and
A2: V.0 = the set of all [{}, k] where k is Element of NAT and
A3: 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 Def2;
consider j being Element of NAT such that
A4: A c= V.j by A2,A3,Th15;
A5: V.(j+1) = {[varcl B, k] where B is Subset of V.j, k is Element of NAT: B
is finite} by A3;
i in NAT by ORDINAL1:def 12;
then
A6: [varcl A, i] in V.(j+1) by A4,A5;
dom V = NAT by PARTFUN1:def 2;
hence thesis by A1,A6,CARD_5:2;
end;
theorem Th18:
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 = the set of all [{}, i] where i is Element of NAT 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 Def2;
set X = {[varcl A, j] where A is Subset of Vars, j is Element of NAT:
A is finite};
A4: dom V = NAT by PARTFUN1:def 2;
defpred P[Nat] means V.$1 c= X;
A5: P[ 0]
proof
let x be object;
assume
A6: x in V.0;
A7: {} c= Vars;
ex i being Element of NAT st x = [{}, i] by A2,A6;
hence thesis by A7,Th8;
end;
A8: now
let i be Nat;
assume P[i];
A9: V.(i+1) = {[varcl A, j] where A is Subset of V.i, j is Element of NAT:
A is finite} by A3;
thus P[i+1]
proof
let x be object;
assume x in V.(i+1);
then consider A being Subset of V.i, j being Element of NAT such that
A10: x = [varcl A, j] and
A11: A is finite by A9;
reconsider ii=i as Element of NAT by ORDINAL1:def 12;
V.ii in rng V by A4,FUNCT_1:def 3;
then V.i c= Vars by A1,ZFMISC_1:74;
then A c= Vars;
hence thesis by A10,A11;
end;
end;
A12: for i being Nat holds P[i] from NAT_1:sch 2(A5,A8);
now
let x;
assume x in rng V;
then ex y being object st y in NAT & x = V.y by A4,FUNCT_1:def 3;
hence x c= X by A12;
end;
hence Vars c= X by A1,ZFMISC_1:76;
let x be object;
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 Th17;
end;
theorem Th19:
varcl Vars = Vars proof consider V being ManySortedSet of NAT such that
A1: Vars = Union V and
A2: V.0 = the set of all [{}, i] where i is Element of NAT 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 Def2;
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 XTUPLE_0:1;
hence x c= V.0;
end;
then
A4: varcl (V.0) c= V.0 by Def1;
V.0 c= varcl (V.0) by Def1;
then
A5: P[ 0] by A4,XBOOLE_0:def 10;
A6: now
let i;
assume
A7: P[i];
reconsider i9 = i as Element of NAT by ORDINAL1:def 12;
A8: 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
A9: [x,y] = [varcl A, j] and A is finite by A8;
x = varcl A by A9,XTUPLE_0:1;
then
A10: x c= V.i by A7,Th9;
V.i9 c= V.(i9+1) by A2,A3,Th14,NAT_1:11;
hence x c= V.(i+1) by A10;
end;
then
A11: varcl (V.(i+1)) c= V.(i+1) by Def1;
V.(i+1) c= varcl (V.(i+1)) by Def1;
hence P[i+1] by A11,XBOOLE_0:def 10;
end;
A12: P[i] from NAT_1:sch 2(A5,A6);
A13: varcl
Vars = union the set of all varcl a where a is Element of rng V
by A1,Th10;
thus
now
let x be object;
assume x in varcl Vars;
then consider Y such that
A14: x in Y and
A15: Y in the set of all varcl a where a is Element of rng V
by A13,TARSKI:def 4;
consider a being Element of rng V such that
A16: Y = varcl a by A15;
consider i being object such that
A17: i in dom V and
A18: a = V.i by FUNCT_1:def 3;
reconsider i as Element of NAT by A17;
varcl (V.i) = a by A12,A18;
hence x in Vars by A1,A14,A16,A17,A18,CARD_5:2;
end;
thus thesis by Def1;
end;
theorem Th20:
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:61;
then
A1: Rank the_rank_of X is finite by CARD_2:67;
X c= Rank the_rank_of X by CLASSES1:def 9;
hence thesis by A1;
end;
theorem Th21:
the_rank_of varcl X = the_rank_of X
proof
A1: X c= Rank the_rank_of X by CLASSES1:def 9;
set a = the_rank_of X;
A2: a c= succ a by ORDINAL3:1;
succ a c= succ succ a by ORDINAL3:1;
then a c= succ succ a by A2;
then
A3: Rank a c= Rank succ succ a by CLASSES1:37;
now
let x,y;
assume [x,y] in Rank the_rank_of X;
then x in Rank a by A3,CLASSES1:45;
hence x c= Rank the_rank_of X by ORDINAL1:def 2;
end;
then varcl X c= Rank a by A1,Def1;
hence the_rank_of varcl X c= a by CLASSES1:65;
X c= varcl X by Def1;
hence thesis by CLASSES1:67;
end;
theorem Th22:
for X being finite Subset of Rank omega holds X in Rank omega
proof
let X be finite Subset of Rank omega;
deffunc F(object) = the_rank_of $1;
consider f being Function such that
A1: dom f = X and
A2: for x being object st x in X holds f.x = F(x) from FUNCT_1:sch 3;
A3: rng f c= NAT
proof
let y be object;
assume y in rng f;
then consider x being object such that
A4: x in X and
A5: y = f.x by A1,FUNCT_1:def 3;
the_rank_of x in omega by A4,CLASSES1:66;
hence thesis by A2,A4,A5;
end;
per cases;
suppose X = {};
then the_rank_of X = 0 by CLASSES1:71;
hence thesis by CLASSES1:66;
end;
suppose X <> {};
then reconsider Y = rng f as finite non empty Subset of NAT
by A1,A3,FINSET_1:8,RELAT_1:42;
reconsider mY = max Y as Element of NAT by ORDINAL1:def 12;
set i = 1+mY;
X c= Rank i
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume
A6: x in X;
then
A7: f.x in Y by A1,FUNCT_1:def 3;
A8: f.x = the_rank_of xx by A2,A6;
reconsider j = f.x as Element of NAT by A7;
j <= mY by A7,XXREAL_2:def 8;
then Segm j c= Segm mY by NAT_1:39;
then
A9: j in succ mY by ORDINAL1:22;
succ Segm mY = Segm i by NAT_1:38;
hence thesis by A8,A9,CLASSES1:66;
end;
then the_rank_of X c= i by CLASSES1:65;
then
A10: the_rank_of X in succ i by ORDINAL1:22;
Segm(i+1) = succ Segm i by NAT_1:38;
hence thesis by A10,CLASSES1:66;
end;
end;
theorem Th23:
Vars c= Rank omega proof consider V being ManySortedSet of NAT such that
A1: Vars = Union V and
A2: V.0 = the set of all [{}, i] where i is Element of NAT 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 Def2;
let x be object;
assume x in Vars;
then consider i being object such that
A4: i in dom V and
A5: x in V.i by A1,CARD_5:2;
reconsider i as Element of NAT by A4;
defpred P[Nat] means V.$1 c= Rank omega;
A6: P[ 0]
proof
let x be object;
assume x in V.0;
then consider i being Element of NAT such that
A7: x = [{}, i] by A2;
A8: Segm(i+1) = succ Segm i by NAT_1:38;
A9: {} c= i;
A10: i in i+1 by A8,ORDINAL1:6;
A11: {} in i+1 by A8,A9,ORDINAL1:6,12;
A12: the_rank_of {} = {} by CLASSES1:73;
A13: the_rank_of i = i by CLASSES1:73;
A14: {} in Rank (i+1) by A11,A12,CLASSES1:66;
i in Rank (i+1) by A10,A13,CLASSES1:66;
then
A15: x in Rank succ succ (i+1) by A7,A14,CLASSES1:45;
succ succ (i+1) c= omega;
then Rank succ succ (i+1) c= Rank omega by CLASSES1:37;
hence thesis by A15;
end;
A16: now
let n be Nat such that
A17: P[n];
A18: 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 be object;
assume x in V.(n+1);
then consider a being Subset of V.n, j being Element of NAT such that
A19: x = [varcl a, j] and
A20: a is finite by A18;
a c= Rank omega by A17,XBOOLE_1:1;
then a in Rank omega by A20,Th22;
then reconsider i = the_rank_of a as Element of NAT by CLASSES1:66;
reconsider k = j \/ i as Element of NAT by ORDINAL3:12;
A21: the_rank_of varcl a = i by Th21;
A22: the_rank_of j = j by CLASSES1:73;
A23: k in succ k by ORDINAL1:6;
then
A24: i in succ k by ORDINAL1:12,XBOOLE_1:7;
A25: j in succ k by A23,ORDINAL1:12,XBOOLE_1:7;
A26: succ Segm k = Segm(k+1) by NAT_1:38;
then
A27: varcl a in Rank (k+1) by A21,A24,CLASSES1:66;
j in Rank (k+1) by A22,A25,A26,CLASSES1:66;
then
A28: x in Rank succ succ (k+1) by A19,A27,CLASSES1:45;
succ succ (k+1) c= omega;
then Rank succ succ (k+1) c= Rank omega by CLASSES1:37;
hence thesis by A28;
end;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A6,A16);
then V.i c= Rank omega;
hence thesis by A5;
end;
theorem Th24:
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 Th23;
then A in Rank omega by Th22;
then the_rank_of A in omega by CLASSES1:66;
then the_rank_of varcl A is finite by Th21;
hence thesis by Th9,Th19,Th20;
end;
registration
cluster Vars -> non empty;
correctness
proof
[{},0] in the set of all [{}, i] where i is Element of NAT;
hence thesis by Th16;
end;
end;
definition
mode variable is Element of Vars;
end;
registration
let x be variable;
cluster x`1 -> finite for set;
coherence
proof x in Vars;
then consider A being Subset of Vars, j being Element of NAT such that
A1: x = [varcl A,j] and
A2: A is finite by Th18;
x`1 = varcl A by A1;
hence thesis by A2,Th24;
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; :: redefines vars (ABCMIZ_1, synonym) → `1 (XTUPLE_0, definition)
coherence
proof x in Vars;
then consider A being Subset of Vars, j being Element of NAT such that
A1: x = [varcl A,j] and
A2: A is finite by Th18;
x`1 = varcl A by A1;
hence thesis by A2,Th24;
end;
end;
theorem
[{}, i] in Vars proof i in NAT by ORDINAL1:def 12;
then [{}, i] in the set of all [{}, j];
hence thesis by Th16;
end;
theorem Th26:
for A being Subset of Vars holds
varcl {[varcl A, j]} = (varcl A) \/ {[varcl A, j]}
proof
let A be Subset of Vars;
A1: {[varcl A, j]} c= (varcl A) \/ {[varcl A, j]} by XBOOLE_1:7;
A2: 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 3;
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 Def1,XTUPLE_0:1;
hence x c= (varcl A) \/ {[varcl A, j]} by A2;
end;
hence varcl {[varcl A, j]} c= (varcl A) \/ {[varcl A, j]} by A1,Def1;
A3: {[varcl A, j]} c= varcl {[varcl A, j]} by Def1;
[varcl A, j] in {[varcl A, j]} by TARSKI:def 1;
then varcl A c= varcl {[varcl A, j]} by A3,Def1;
hence thesis by A3,XBOOLE_1:8;
end;
theorem Th27:
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] and A is finite by Th18;
varcl {x} = (varcl A) \/ {x} by A1,Th26;
hence thesis by A1;
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] and A is finite by Th18;
A2: varcl {x} = (varcl A) \/ {x} by A1,Th26;
A3: vars x = varcl A by A1;
i in NAT by ORDINAL1:def 12;
hence thesis by A2,A3,Th18;
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
:Def3: 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[object] 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: for x being object holds x in L iff x in Vars* & P[ x ]
from XBOOLE_0:sch 1;
L is FinSequenceSet of Vars
proof
let x be object;
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
A2: 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
A3: 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 be object;
assume
A4: x in L1;
then reconsider p = x as FinSequence of Vars by FINSEQ_2:def 3;
A5: p is one-to-one by A2,A4;
for i st i in dom p holds (p.i)`1 c= rng (p|(i qua set)) by A2,A4;
hence x in L2 by A3,A5;
end;
let x be object;
assume
A6: x in L2;
then reconsider p = x as FinSequence of Vars by FINSEQ_2:def 3;
A7: p is one-to-one by A3,A6;
for i st i in dom p holds (p.i)`1 c= rng (p|(i qua set)) by A3,A6;
hence thesis by A2,A7;
end;
end;
theorem Th29:
<*>Vars in QuasiLoci
proof
reconsider p = <*>Vars as FinSequence of Vars;
p is one-to-one &
for i st i in dom p holds (p.i)`1 c= rng (p dom i);
hence thesis by Def3;
end;
registration
cluster QuasiLoci -> non empty;
correctness by Th29;
end;
definition
mode quasi-loci is Element of QuasiLoci;
end;
registration
cluster -> one-to-one for quasi-loci;
coherence by Def3;
end;
theorem Th30:
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 and
A3: x = l.i;
let y be variable such that
A4: y in vars x;
vars x c= rng (l|(i qua set)) by A1,A2,A3,Def3;
then consider z being object such that
A5: z in dom (l dom i) and
A6: y = (l dom i).z by A4,FUNCT_1:def 3;
A7: dom (l dom i) = dom l /\ i by RELAT_1:61;
reconsider z as Element of NAT by A5,A7;
reconsider j = z as Nat;
take j;
A8: card Segm z = z;
card Segm i = i;
hence j in dom l & j < i & y = l.j by A5,A6,A7,A8,FUNCT_1:47,NAT_1:41
,XBOOLE_0:def 4;
end;
assume
A9: 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
A10: i in dom l;
then l.i in rng l by FUNCT_1:def 3;
then reconsider x = l.i as variable;
thus (l.i)`1 c= rng (l dom i)
proof
let y be object;
assume y in (l.i)`1;
then
A11: y in vars x;
then reconsider y as variable;
consider j being Nat such that
A12: j in dom l and
A13: j < i and
A14: y = l.j by A9,A10,A11;
A15: card Segm i = i;
card Segm j = j;
then j in i by A13,A15,NAT_1:41;
hence thesis by A12,A14,FUNCT_1:50;
end;
end;
hence thesis by Def3;
end;
theorem Th31:
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:42;
A2: dom (l^<*x*>) = Seg (len l + len <*x*>) by FINSEQ_1:def 7
.= Seg (len l + 1) by FINSEQ_1:39;
1 <= 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
A5: l^<*x*> is quasi-loci;
thus not x in rng l
proof
assume x in rng l;
then consider a being object such that
A6: a in dom l and
A7: x = l.a by FUNCT_1:def 3;
reconsider a as Element of NAT by A6;
A8: (l^<*x*>).a = x by A6,A7,FINSEQ_1:def 7;
A9: a <= len l by A4,A6,FINSEQ_1:1;
A10: len l < 1+len l by NAT_1:13;
dom l c= dom (l^<*x*>) by FINSEQ_1:26;
hence thesis by A1,A3,A5,A6,A8,A9,A10,FUNCT_1:def 4;
end;
thus vars x c= rng l
proof
let a be object;
assume
A11: a in vars x;
then reconsider a as variable;
consider j being Nat such that
A12: j in dom (l^<*x*>) and
A13: j < 1+len l and
A14: a = (l^<*x*>).j by A1,A3,A5,A11,Th30;
reconsider j as Element of NAT by ORDINAL1:def 12;
A15: j <= len l by A13,NAT_1:13;
j >= 1 by A2,A12,FINSEQ_1:1;
then
A16: j in dom l by A4,A15;
then a = l.j by A14,FINSEQ_1:def 7;
hence thesis by A16,FUNCT_1:def 3;
end;
end;
assume that
A17: not x in rng l and
A18: vars x c= rng l;
A19: (l^<*x*>) is one-to-one
proof
let a,b be object;
assume that
A20: a in dom (l^<*x*>) and
A21: b in dom (l^<*x*>) and
A22: (l^<*x*>).a = (l^<*x*>).b;
reconsider a,b as Element of NAT by A20,A21;
A23: a >= 1 by A2,A20,FINSEQ_1:1;
A24: b >= 1 by A2,A21,FINSEQ_1:1;
A25: a <= 1+len l by A2,A20,FINSEQ_1:1;
A26: b <= 1+len l by A2,A21,FINSEQ_1:1;
A27: a <= len l or a = 1+len l by A25,NAT_1:8;
A28: b <= len l or b = 1+len l by A26,NAT_1:8;
A29: a in dom l or a = 1+len l by A4,A23,A27;
A30: b in dom l or b = 1+len l by A4,A24,A28;
A31: a in dom l & l.a = (l^<*x*>).a & l.a in rng l or a = 1+len l by A29,
FINSEQ_1:def 7,FUNCT_1:def 3;
b in dom l & l.b = (l^<*x*>).b & l.b in rng l or b = 1+len l by A30,
FINSEQ_1:def 7,FUNCT_1:def 3;
hence thesis by A17,A22,A31,FINSEQ_1:42,FUNCT_1:def 4;
end;
now
let i be Nat, z be variable;
assume that
A32: i in dom (l^<*x*>) and
A33: z = (l^<*x*>).i;
A34: i >= 1 by A2,A32,FINSEQ_1:1;
i <= 1+len l by A2,A32,FINSEQ_1:1;
then i <= len l or i = 1+len l by NAT_1:8;
then
A35: i in dom l or i = 1+len l & z = x by A4,A33,A34,FINSEQ_1:42;
let y be variable;
assume
A36: 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 A33,A35,FINSEQ_1:def 7;
suppose
A37: i = 1+len l & z = x;
then consider k being object such that
A38: k in dom l and
A39: y = l.k by A18,A36,FUNCT_1:def 3;
reconsider k as Element of NAT by A38;
take k;
A40: dom l c= dom (l^<*x*>) by FINSEQ_1:26;
k <= len l by A4,A38,FINSEQ_1:1;
hence thesis by A37,A38,A39,A40,FINSEQ_1:def 7,NAT_1:13;
end;
suppose i in dom l & z = l.i;
then consider j being Nat such that
A41: j in dom l and
A42: j < i and
A43: y = l.j by A36,Th30;
take j;
dom l c= dom (l^<*x*>) by FINSEQ_1:26;
hence thesis by A41,A42,A43,FINSEQ_1:def 7;
end;
end;
end;
hence thesis by A19,Th30;
end;
theorem Th32:
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:36,FINSEQ_3:91;
now
let i be Nat, x be variable such that
A3: i in dom p and
A4: x = p.i;
let y be variable such that
A5: y in vars x;
A6: dom p c= dom (p^q) by FINSEQ_1:26;
x = (p^q).i by A3,A4,FINSEQ_1:def 7;
then consider j being Nat such that
A7: j in dom (p^q) and
A8: j < i and
A9: y = (p^q).j by A1,A3,A5,A6,Th30;
take j;
A10: dom p = Seg len p by FINSEQ_1:def 3;
dom (p^q) = Seg len (p^q) by FINSEQ_1:def 3;
then
A11: j >= 1 by A7,FINSEQ_1:1;
i <= len p by A3,A10,FINSEQ_1:1;
then j < len p by A8,XXREAL_0:2;
hence j in dom p & j < i by A8,A10,A11;
hence y = p.j by A9,FINSEQ_1:def 7;
end;
hence thesis by A1,A2,Th30,FINSEQ_1:36;
end;
theorem
for l being quasi-loci holds varcl rng l = rng l
proof
let l be quasi-loci;
now
let x,y;
assume
A1: [x,y] in rng l;
then reconsider xy = [x,y] as variable;
consider i being object such that
A2: i in dom l and
A3: xy = l.i by A1,FUNCT_1:def 3;
reconsider i as Nat by A2;
A4: vars xy = x;
thus x c= rng l
proof
let a be object;
assume
A5: a in x;
then reconsider a as variable by A4;
ex j being Nat st j in dom l & j < i & a = l.j by A2,A3,A4,A5,Th30;
hence thesis by FUNCT_1:def 3;
end;
end;
hence varcl rng l c= rng l by Def1;
thus thesis by Def1;
end;
theorem Th34:
for x being variable holds <*x*> is quasi-loci iff vars x = {}
proof
let x be variable;
A1: <*x*> = (<*>Vars)^<*x*> by FINSEQ_1:34;
A2: rng {} = {};
vars x c= {} implies vars x = {};
hence thesis by A1,A2,Th29,Th31;
end;
theorem Th35:
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;
A1: rng <*x*> = {x} by FINSEQ_1:38;
A2: <*x*> is quasi-loci iff vars x = {} by Th34;
y in {x} iff y = x by TARSKI:def 1;
hence thesis by A1,A2,Th31,Th32;
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;
A1: rng <*x,y*> = {x,y} by FINSEQ_2:127;
A2: <*x,y*> is quasi-loci iff vars x = {} & x <> y & vars y c= {x} by Th35;
z in {x,y} iff z = x or z = y by TARSKI:def 2;
hence thesis by A1,A2,Th31,Th32;
end;
definition
let l be quasi-loci;
redefine func l" -> PartFunc of Vars, NAT; :: redefines " (FUNCT_1, definition)
coherence
proof
A1: dom (l") = rng l by FUNCT_1:33;
rng (l") = dom l by FUNCT_1:33;
hence thesis by A1,RELSET_1:4;
end;
end;
begin :: Mizar Constructor Signature
definition
func a_Type -> set equals
0;
coherence;
func an_Adj -> set equals
1;
coherence;
func a_Term -> set equals
2;
coherence;
func * -> set equals
0;
coherence;
func non_op -> set 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
:
Def9: the carrier of C = {a_Type, an_Adj, a_Term} &
{*, non_op} c= the carrier' 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 carrier' of C st o <> * & o <> non_op
holds (the Arity of C).o in {a_Term}*;
end;
registration
cluster constructor -> non empty non void for Signature;
coherence;
end;
definition
func MinConstrSign -> strict Signature means
:
Def10: it is constructor & the carrier' 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;
take C;
thus the carrier of C = {a_Type, an_Adj, a_Term} &
{*, non_op} c= the carrier' of C;
thus (the Arity of C).* = <*an_Adj, a_Type*> by FUNCT_4:63;
thus (the Arity of C).non_op = <*an_Adj*> by FUNCT_4:63;
thus (the ResultSort of C).* = a_Type by FUNCT_4:63;
thus (the ResultSort of C).non_op = an_Adj by FUNCT_4:63;
thus thesis by TARSKI:def 2;
end;
correctness
proof
let C1, C2 be strict Signature such that
A1: C1 is constructor and
A2: the carrier' of C1 = {*, non_op} and
A3: C2 is constructor and
A4: the carrier' of C2 = {*, non_op};
set A = {a_Type, an_Adj, a_Term};
A5: the carrier of C1 = A by A1;
A6: the carrier of C2 = A by A3;
A7: (the Arity of C1).* = <*an_Adj, a_Type*> by A1;
A8: (the Arity of C2).* = <*an_Adj, a_Type*> by A3;
A9: (the Arity of C1).non_op = <*an_Adj*> by A1;
A10: (the Arity of C2).non_op = <*an_Adj*> by A3;
A11: (the ResultSort of C1).* = a_Type by A1;
A12: (the ResultSort of C2).* = a_Type by A3;
A13: (the ResultSort of C1).non_op = an_Adj by A1;
A14: (the ResultSort of C2).non_op = an_Adj by A3;
A15: dom the Arity of C1 = {*, non_op} by A2,FUNCT_2:def 1;
A16: dom the Arity of C2 = {*, non_op} by A4,FUNCT_2:def 1;
A17: the Arity of C1 = (*, non_op) --> (<*an_Adj, a_Type*>, <*an_Adj*>) by A7
,A9,A15,FUNCT_4:66;
A18: the Arity of C2 = (*, non_op) --> (<*an_Adj, a_Type*>, <*an_Adj*>) by A8
,A10,A16,FUNCT_4:66;
A19: dom the ResultSort of C1 = {*, non_op} by A1,A2,FUNCT_2:def 1;
A20: dom the ResultSort of C2 = {*, non_op} by A3,A4,FUNCT_2:def 1;
the ResultSort of C1 = (*, non_op) --> (a_Type, an_Adj) by A11,A13,A19,
FUNCT_4:66;
hence thesis by A2,A4,A5,A6,A12,A14,A17,A18,A20,FUNCT_4:66;
end;
end;
registration
cluster MinConstrSign -> constructor;
coherence by Def10;
end;
registration
cluster constructor strict for 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
:
Def11: 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 <> * and
A2: o <> non_op;
reconsider t = a_Term as Element of {a_Term} by TARSKI:def 1;
A3: len ((len the_arity_of o)|->a_Term) = len the_arity_of o by CARD_1:def 7;
A4: the_arity_of o in {a_Term}* by A1,A2,Def9;
(len the_arity_of o)|->t in {a_Term}* by FINSEQ_1:def 11;
hence thesis by A3,A4,Th6;
end;
definition
let C be non empty non void Signature;
attr C is initialized means
:
Def12: 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 Def9;
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 carrier' of C by Def9;
A3: * in {*, non_op} by TARSKI:def 2;
A4: non_op in {*, non_op} by TARSKI:def 2;
func non_op C -> OperSymbol of C equals
non_op;
coherence by A2,A4;
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 Def9;
definition
func Modes -> set equals
[:{a_Type},[:QuasiLoci,NAT:]:];
correctness;
func Attrs -> set equals
[:{an_Adj},[:QuasiLoci,NAT:]:];
correctness;
func Funcs -> set 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 being object 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 3;
then x in Modes or x in Attrs or x in Funcs by XBOOLE_0:def 3;
then consider Y,Z being set such that
A3: x in [:Y,Z:];
A4: ex y,z being object st ( y in Y)&( z in Z)&( [y,z] = x)
by A3,ZFMISC_1:def 2;
reconsider x as set by TARSKI:1;
x = * or x = non_op by A1,TARSKI:def 2;
then the_rank_of x = 0 or the_rank_of x = 1 by CLASSES1:73;
then the_rank_of x c= 1;
then the_rank_of x in succ succ {} by ORDINAL1:6,12;
then x in Rank succ succ {} by CLASSES1:66;
hence thesis by A4,CLASSES1:29,45;
end;
definition
let x be Element of [:QuasiLoci, NAT:];
redefine func x`1 -> quasi-loci; :: redefines `1 (XTUPLE_0, definition)
coherence by MCART_1:10;
redefine func x`2 -> Element of NAT; :: redefines `2 (XTUPLE_0, definition)
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}; :: redefines kind_of (ABCMIZ_1, synonym) → `1 (XTUPLE_0, definition)
coherence
proof
c in Modes \/ Attrs or c in Funcs by XBOOLE_0:def 3;
then c in Modes or c in Attrs or c in Funcs by XBOOLE_0:def 3;
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;
redefine func c`2 -> Element of [:QuasiLoci, NAT:]; :: redefines `2 (XTUPLE_0, definition)
coherence
proof
c in Modes \/ Attrs or c in Funcs by XBOOLE_0:def 3;
then c in Modes or c in Attrs or c in Funcs by XBOOLE_0:def 3;
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 3;
A2: x in Modes implies x`1 in {a_Type} by MCART_1:10;
A3: x in Attrs implies x`1 in {an_Adj} by MCART_1:10;
x in Funcs implies x`1 in {a_Term} by MCART_1:10;
hence thesis by A1,A2,A3,TARSKI:def 1,XBOOLE_0:def 3;
end;
definition
func MaxConstrSign -> strict ConstructorSignature means
:
Def24: the carrier' 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);
A3: dom (*, non_op)-->(<*a,t*>, aa) = {*, non_op} by FUNCT_4:62;
A4: dom (*, non_op)-->(t, a) = {*, non_op} by FUNCT_4:62;
A5: dom f = Constructors by PARTFUN1:def 2;
A6: dom g = Constructors by PARTFUN1:def 2;
A7: dom A = O by A3,A5,FUNCT_4:def 1;
A8: dom R = O by A4,A6,FUNCT_4:def 1;
rng f c= S*
proof
let y be object;
assume y in rng f;
then consider x being object such that
A9: x in Constructors and
A10: y = f.x by A5,FUNCT_1:def 3;
reconsider x as Element of Constructors by A9;
y = (len loci_of x)|->tr by A1,A10;
hence thesis by FINSEQ_1:def 11;
end;
then
A11: rng f \/ rng (*, non_op)-->(<*a,t*>, aa) c= (S*) \/ (S*) by XBOOLE_1:13;
rng g c= S
proof
let y be object;
assume y in rng g;
then consider x being object such that
A12: x in Constructors and
A13: y = g.x by A6,FUNCT_1:def 3;
reconsider x as Element of Constructors by A12;
y = kind_of x by A2,A13;
hence thesis;
end;
then
A14: 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:17;
then reconsider A as Function of O, S* by A7,A11,FUNCT_2:2,XBOOLE_1:1;
rng R c= rng g \/ rng (*, non_op)-->(t, a) by FUNCT_4:17;
then reconsider R as Function of O, S by A8,A14,FUNCT_2:2,XBOOLE_1:1;
reconsider Max = ManySortedSign(# S, O, A, R #) as
non empty non void strict Signature;
Max is constructor
proof
thus the carrier of Max = {a_Type, an_Adj, a_Term};
thus {*, non_op} c= the carrier' of Max by XBOOLE_1:7;
A15: * in {*, non_op} by TARSKI:def 2;
A16: non_op in {*, non_op} by TARSKI:def 2;
thus (the Arity of Max).* = ((*, non_op)-->(<*a,t*>, aa)).*
by A3,A15,FUNCT_4:13
.= <*an_Adj, a_Type*> by FUNCT_4:63;
thus
(the Arity of Max).non_op = ((*, non_op)-->(<*a,t*>, aa)).non_op
by A3,A16,FUNCT_4:13
.= <*an_Adj*> by FUNCT_4:63;
thus (the ResultSort of Max).* = ((*, non_op)-->(t, a)).*
by A4,A15,FUNCT_4:13
.= a_Type by FUNCT_4:63;
thus (the ResultSort of Max).non_op = ((*, non_op)-->(t, a)).non_op
by A4,A16,FUNCT_4:13
.= an_Adj by FUNCT_4:63;
let o be Element of the carrier' of Max;
assume that
A17: o <> * and
A18: o <> non_op;
A19: not o in {*, non_op} by A17,A18,TARSKI:def 2;
then reconsider c = o as Element of Constructors by XBOOLE_0:def 3;
reconsider tr as Element of {a_Term} by TARSKI:def 1;
(the Arity of Max).o = f.c by A3,A5,A19,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 carrier' of Max = {*, non_op} \/ Constructors;
let o being OperSymbol of Max;
assume that
A20: o <> * and
A21: o <> non_op;
A22: not o in {*, non_op} by A20,A21,TARSKI:def 2;
then reconsider c = o as Element of Constructors by XBOOLE_0:def 3;
thus (the ResultSort of Max).o = g.c by A4,A6,A22,FUNCT_4:def 1
.= o`1
by A2;
thus card ((the Arity of Max).o) = card (f.c) by A3,A5,A22,FUNCT_4:def 1
.= card F(c) by A1
.= card o`2`1 by CARD_1:def 7;
end;
uniqueness
proof
let it1, it2 be strict ConstructorSignature such that
A23: the carrier' of it1 = {*, non_op} \/ Constructors and
A24: 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
A25: the carrier' of it2 = {*, non_op} \/ Constructors and
A26: 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};
A27: the carrier of it1 = S by Def9;
A28: the carrier of it2 = S by Def9;
A29: now
let c be Element of Constructors;
reconsider o1 = c as OperSymbol of it1 by A23,XBOOLE_0:def 3;
reconsider o2 = o1 as OperSymbol of it2 by A23,A25;
assume that
A30: c <> * and
A31: c <> non_op;
A32: o1 is constructor by A30,A31;
A33: o2 is constructor by A30,A31;
A34: card ((the Arity of it1).o1) = card c`2`1 by A24,A32;
A35: card ((the Arity of it2).o2) = card c`2`1 by A26,A33;
A36: (the Arity of it1).o1 in {a_Term}* by A30,A31,Def9;
(the Arity of it2).o2 in {a_Term}* by A30,A31,Def9;
then reconsider p1 = (the Arity of it1).o1, p2 = (the Arity of it2).o2
as FinSequence of {a_Term} by A36,FINSEQ_1:def 11;
A37: dom p1 = Seg len p1 by FINSEQ_1:def 3;
A38: dom p2 = Seg len p2 by FINSEQ_1:def 3;
now
let i be Nat;
assume
A39: i in dom p1;
then
A40: p1.i in rng p1 by FUNCT_1:def 3;
A41: p2.i in rng p2 by A34,A35,A37,A38,A39,FUNCT_1:def 3;
p1.i = a_Term by A40,TARSKI:def 1;
hence p1.i = p2.i by A41,TARSKI:def 1;
end;
hence (the Arity of it1).c = (the Arity of it2).c by A34,A35,A37,A38;
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 A23,TARSKI:def 2,XBOOLE_0:def 3;
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 A29,Def9;
hence (the Arity of it1).o = (the Arity of it2).o;
end;
then
A42: the Arity of it1 = the Arity of it2 by A23,A25,A27,A28,FUNCT_2:63;
now
let o be OperSymbol of it1;
reconsider o9 = o as OperSymbol of it2 by A23,A25;
not o in {*, non_op} or o in {*,non_op};
then o = * or o = non_op or o in Constructors & o is constructor &
o9 is constructor by A23,TARSKI:def 2,XBOOLE_0:def 3;
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 A24,A26,Def9;
hence (the ResultSort of it1).o = (the ResultSort of it2).o;
end;
hence thesis by A23,A25,A27,A28,A42,FUNCT_2:63;
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
A1: the_arity_of m = {} and
the_result_sort_of a = an_Adj and the_arity_of a = {};
the carrier' of MinConstrSign = {*, non_op} by Def10;
then m = * or m = non_op by TARSKI:def 2;
hence contradiction by A1,Def9;
end;
cluster MaxConstrSign -> initialized;
correctness
proof
set m = [a_Type, [{}, 0]], a = [an_Adj, [{}, 0]];
A2: a_Type in {a_Type} by TARSKI:def 1;
A3: an_Adj in {an_Adj} by TARSKI:def 1;
A4: [<*> Vars, 0] in [:QuasiLoci, NAT:] by Th29,ZFMISC_1:def 2;
then
A5: m in Modes by A2,ZFMISC_1:def 2;
A6: a in Attrs by A3,A4,ZFMISC_1:def 2;
A7: m in Modes \/ Attrs by A5,XBOOLE_0:def 3;
A8: a in Modes \/ Attrs by A6,XBOOLE_0:def 3;
A9: m in Constructors by A7,XBOOLE_0:def 3;
A10: a in Constructors by A8,XBOOLE_0:def 3;
the carrier' of MaxConstrSign = {*, non_op} \/ Constructors by Def24;
then reconsider m,a as OperSymbol of MaxConstrSign by A9,A10,XBOOLE_0:def 3
;
A11: m is constructor;
A12: a is constructor;
take m, a;
thus the_result_sort_of m = m`1 by A11,Def24
.= a_Type;
len the_arity_of m = card m`2`1 by A11,Def24
.= card [{}, 0]`1
.= 0;
hence the_arity_of m = {};
thus the_result_sort_of a = a`1 by A12,Def24
.= an_Adj;
len the_arity_of a = card a`2`1 by A12,Def24
.= card [{}, 0]`1
.= 0;
hence thesis;
end;
end;
registration
cluster initialized strict for ConstructorSignature;
correctness
proof
take MaxConstrSign;
thus thesis; end;
end;
registration
let C be initialized ConstructorSignature;
cluster constructor for OperSymbol of C;
existence
proof
consider m, a being OperSymbol of C such that
A1: the_result_sort_of m = a_Type and
A2: the_arity_of m = {} and
the_result_sort_of a = an_Adj and the_arity_of a = {} by Def12;
take m;
thus m <> * by A2,Def9;
thus thesis by A1,Def9;
end;
end;
begin :: Mizar Expressions
definition
let C be ConstructorSignature;
A1: the carrier of C = {a_Type, an_Adj, a_Term} by Def9;
func MSVars C -> ManySortedSet of the carrier of C means
:
Def25: it.a_Type = {} & it.an_Adj = {} & it.a_Term = Vars;
uniqueness
proof
let V1,V2 be ManySortedSet of the carrier of C such that
A2: V1.a_Type = {} and
A3: V1.an_Adj = {} and
A4: V1.a_Term = Vars and
A5: V2.a_Type = {} and
A6: V2.an_Adj = {} and
A7: V2.a_Term = Vars;
now
let x be object;
assume x in the carrier of C;
then x = a_Type or x = an_Adj or x = a_Term by A1,ENUMSET1:def 1;
hence V1.x = V2.x by A2,A3,A4,A5,A6,A7;
end;
hence thesis;
end;
existence
proof
deffunc F(object) = IFEQ($1, a_Term, Vars, {});
consider V being ManySortedSet of the carrier of C such that
A8: for x being object st x in the carrier of C holds V.x = F(x)
from PBOOLE:sch 4;
take V;
A9: IFEQ(a_Type, a_Term, Vars, {}) = {} by FUNCOP_1:def 8;
A10: IFEQ(an_Adj, a_Term, Vars, {}) = {} by FUNCOP_1:def 8;
A11: IFEQ(a_Term, a_Term, Vars, {}) = Vars by FUNCOP_1:def 8;
A12: a_Type in the carrier of C by A1,ENUMSET1:def 1;
A13: an_Adj in the carrier of C by A1,ENUMSET1:def 1;
a_Term in the carrier of C by A1,ENUMSET1:def 1;
hence thesis by A8,A9,A10,A11,A12,A13;
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 Def9;
hence a_Term in the carrier of C by ENUMSET1:def 1;
thus thesis by Def25;
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 and
A2: the_arity_of m = {} and
A3: the_result_sort_of a = an_Adj and
A4: the_arity_of a = {} by Def12;
A5: root-tree [m, the carrier of C] in (the Sorts of Free(C, X)).a_Type
by A1,A2,MSAFREE3:5;
A6: root-tree [a, the carrier of C] in (the Sorts of Free(C, X)).an_Adj
by A3,A4,MSAFREE3:5;
set x = the variable;
A7: a_Term C = a_Term;
(MSVars C).a_Term = Vars by Def25;
then
A8: root-tree [x, a_Term] in (the Sorts of Free(C, X)).a_Term by A7,MSAFREE3:4;
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 object such that
A9: s in dom the Sorts of Free(C, X) and
A10: {} = (the Sorts of Free(C, X)).s by FUNCT_1:def 3;
s in the carrier of C by A9;
then s in {a_Type, an_Adj, a_Term} by Def9;
hence thesis by A5,A6,A8,A10,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
:
Def27: t.{} in [:the carrier' 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
:
Def28: it in (the Sorts of Free(C, MSVars C)).s;
existence
proof set t = the Element of (the Sorts of Free(C, MSVars C)).s;
dom the Sorts of Free(C, MSVars C) = the carrier of C by PARTFUN1:def 2;
then t in Union the Sorts of Free(C, MSVars C) by CARD_5:2;
hence thesis;
end;
end;
theorem Th41:
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 PARTFUN1:def 2;
(the Sorts of Free(C, MSVars C)).s c= Union the Sorts of Free(C, MSVars C)
by A1,CARD_5:2;
hence thesis by Def28;
end;
definition
let C;
let c such that
A1: len the_arity_of c = 0;
func c term -> expression of C equals
[c, the carrier of C]-tree {};
coherence
proof
the_arity_of c = {} by A1;
then
A2: root-tree [c, the carrier of C] in
(the Sorts of Free(C, MSVars C)).the_result_sort_of c
by MSAFREE3:5;
dom the Sorts of Free(C, MSVars C) = the carrier of C by PARTFUN1:def 2;
then
root-tree [c, the carrier of C] in Union (the Sorts of Free(C, MSVars C))
by A2,CARD_5:2;
hence thesis by TREES_4:20;
end;
end;
theorem Th42:
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
A1: 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
A2: s = (the_arity_of o).1 and
A3: a is expression of C, s;
reconsider ta = a as Term of C,Y by MSAFREE3:8;
A4: dom <*ta*> = Seg 1 by FINSEQ_1:38;
A5: dom <*s*> = Seg 1 by FINSEQ_1:38;
A6: the_arity_of o = <*s*> by A1,A2,FINSEQ_1:40;
A7: the Sorts of Free(C, X) = C-Terms(X, Y) by MSAFREE3:24;
now
let i be Nat;
assume i in dom <*ta*>;
then
A8: i = 1 by A4,FINSEQ_1:2,TARSKI:def 1;
let t be Term of C, Y;
assume
A9: t = <*ta*>.i;
A10: the Sorts of Free(C, X) c= the Sorts of FreeMSA Y by A7,PBOOLE:def 18;
A11: t = a by A8,A9;
A12: (the Sorts of Free(C, X)).s c= (the Sorts of FreeMSA Y).s by A10;
t in (the Sorts of Free(C, X)).s by A3,A11,Th41;
hence the_sort_of t = (the_arity_of o).i by A2,A8,A12,MSAFREE3:7;
end;
then reconsider p = <*ta*> as ArgumentSeq of Sym(o, Y) by A4,A5,A6,MSATERM:25
;
A13: variables_in (Sym(o, Y)-tree p) c= X
proof
let s be object;
assume s in the carrier of C;
then reconsider s9 = s as SortSymbol of C;
let x be object;
assume x in (variables_in (Sym(o, Y)-tree p)).s;
then consider t being DecoratedTree such that
A14: t in rng p and
A15: x in (C variables_in t).s9 by MSAFREE3:11;
A16: C variables_in a c= X by MSAFREE3:27;
A17: rng p = {a} by FINSEQ_1:38;
A18: (C variables_in a).s9 c= X.s9 by A16;
t = a by A14,A17,TARSKI:def 1;
hence thesis by A15,A18;
end;
set s9 = the_result_sort_of o;
A19: the_sort_of (Sym(o, Y)-tree p) = the_result_sort_of o by MSATERM:20;
(the Sorts of Free(C, X)).s9 =
{t where t is Term of C,Y: the_sort_of t = s9 & variables_in t c= X}
by A7,MSAFREE3:def 5;
then [o, the carrier of C]-tree <*a*> in (the Sorts of Free(C, X)).s9 by A13
,A19;
hence thesis by Th41;
end;
definition
let C,o such that
A1: len the_arity_of o = 1;
let e be expression of C such that
A2: 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
:
Def30: [o, the carrier of C]-tree<*e*>;
coherence by A1,A2,Th42;
end;
reserve a,b for expression of C, an_Adj C;
theorem Th43:
(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 by Def9;
A2: the_arity_of non_op C = <*an_Adj C*> by Def9;
then
A3: len the_arity_of non_op C = 1 by FINSEQ_1:40;
A4: (the_arity_of non_op C).1 = an_Adj C by A2;
then (non_op C)term a = [non_op, the carrier of C]-tree <*a*> by A3,Def30;
hence thesis by A1,A3,A4,Th42;
end;
theorem Th44:
(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 Th43
.= [non_op, the carrier of C]-tree <*b*> by Th43;
then <*a*> = <*b*> by TREES_4:15;
hence thesis by FINSEQ_1:76;
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 Th43;
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 carrier' of C, {the carrier of C}:]
by ZFMISC_1:106;
end;
end;
registration
let C;
cluster compound for expression of C;
existence
proof
set a = the expression of C, an_Adj C;
(non_op C)term a is compound;
hence thesis;
end;
end;
theorem Th45:
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
A1: 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
A2: s1 = (the_arity_of o).1 and
A3: s2 = (the_arity_of o).2 and
A4: a is expression of C, s1 and
A5: b is expression of C, s2;
reconsider ta = a, tb = b as Term of C,Y by MSAFREE3:8;
A6: dom <*ta,tb*> = Seg 2 by FINSEQ_1:89;
A7: dom <*s1,s2*> = Seg 2 by FINSEQ_1:89;
A8: the_arity_of o = <*s1,s2*> by A1,A2,A3,FINSEQ_1:44;
A9: the Sorts of Free(C, X) = C-Terms(X, Y) by MSAFREE3:24;
now
let i be Nat;
assume i in dom <*ta,tb*>;
then
A10: i = 1 or i = 2 by A6,FINSEQ_1:2,TARSKI:def 2;
let t be Term of C, Y;
assume
A11: t = <*ta,tb*>.i;
A12: the Sorts of Free(C, X) c= the Sorts of FreeMSA Y by A9,PBOOLE:def 18;
A13: i = 1 & t = a or i = 2 & t = b by A10,A11;
A14: (the Sorts of Free(C, X)).s1 c= (the Sorts of FreeMSA Y).s1 by A12;
A15: (the Sorts of Free(C, X)).s2 c= (the Sorts of FreeMSA Y).s2 by A12;
i = 1 & t in (the Sorts of Free(C, X)).s1 or i = 2 & t in (the Sorts
of Free(C, X)).s2 by A4,A5,A13,Th41;
hence the_sort_of t = (the_arity_of o).i by A2,A3,A14,A15,MSAFREE3:7;
end;
then reconsider p = <*ta,tb*> as ArgumentSeq of Sym(o, Y) by A6,A7,A8,
MSATERM:25;
A16: variables_in (Sym(o, Y)-tree p) c= X
proof
let s be object;
assume s in the carrier of C;
then reconsider s9 = s as SortSymbol of C;
let x be object;
assume x in (variables_in (Sym(o, Y)-tree p)).s;
then consider t being DecoratedTree such that
A17: t in rng p and
A18: x in (C variables_in t).s9 by MSAFREE3:11;
A19: C variables_in a c= X by MSAFREE3:27;
A20: C variables_in b c= X by MSAFREE3:27;
A21: rng p = {a,b} by FINSEQ_2:127;
A22: (C variables_in a).s9 c= X.s9 by A19;
A23: (C variables_in b).s9 c= X.s9 by A20;
t = a or t = b by A17,A21,TARSKI:def 2;
hence thesis by A18,A22,A23;
end;
set s9 = the_result_sort_of o;
A24: the_sort_of (Sym(o, Y)-tree p) = the_result_sort_of o by MSATERM:20;
(the Sorts of Free(C, X)).s9 =
{t where t is Term of C,Y: the_sort_of t = s9 & variables_in t c= X}
by A9,MSAFREE3:def 5;
then [o, the carrier of C]-tree <*a,b*> in (the Sorts of Free(C, X)).s9
by A16,A24;
hence thesis by Th41;
end;
definition
let C,o such that
A1: len the_arity_of o = 2;
let e1,e2 be expression of C such that
A2: 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
:
Def31: [o, the carrier of C]-tree<*e1,e2*>;
coherence by A1,A2,Th45;
end;
reserve t, t1,t2 for expression of C, a_Type C;
theorem Th46:
(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 by Def9;
A2: the_arity_of ast C = <*an_Adj C, a_Type C*> by Def9;
then
A3: len the_arity_of ast C = 2 by FINSEQ_1:44;
A4: (the_arity_of ast C).1 = an_Adj C by A2;
A5: (the_arity_of ast C).2 = a_Type C by A2;
then (ast C)term(a,t) = [ *, the carrier of C]-tree <*a,t*> by A3,A4,Def31;
hence thesis by A1,A3,A4,A5,Th45;
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 Th46
.= [ *, the carrier of C]-tree<*b,t2*> by Th46;
then <*a,t1*> = <*b,t2*> by TREES_4:15;
hence thesis by FINSEQ_1:77;
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 Th46;
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 carrier' of C, {the carrier of C}:]
by ZFMISC_1:106;
end;
end;
definition
let S be non void Signature;
let s be SortSymbol of S such that
A1: 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 A1;
end;
definition
let C be ConstructorSignature;
redefine func non_op C -> OperSymbol of an_Adj C; :: redefines non_op (ABCMIZ_1, definition)
coherence
proof
the_result_sort_of non_op C = an_Adj C by Def9;
hence ex o being OperSymbol of C st the_result_sort_of o = an_Adj C;
thus thesis by Def9;
end;
redefine func ast C -> OperSymbol of a_Type C; :: redefines ast (ABCMIZ_1, definition)
coherence
proof
the_result_sort_of ast C = a_Type C by Def9;
hence ex o being OperSymbol of C st the_result_sort_of o = a_Type C;
thus thesis by Def9;
end;
end;
theorem Th48:
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});
A1: ex A being MSSubset of FreeMSA Y st ( Free(C, X) = GenMSAlg
A)&( A = (Reverse Y)""X) by MSAFREE3:def 1;
let s1,s2 be SortSymbol of C;
the Sorts of Free(C, X) is MSSubset of FreeMSA Y by A1,MSUALG_2:def 9;
then
A2: the Sorts of Free(C, X) c= the Sorts of FreeMSA Y by PBOOLE:def 18;
then
A3: (the Sorts of Free(C,X)).s1 c= (the Sorts of FreeMSA Y).s1;
A4: (the Sorts of Free(C,X)).s2 c= (the Sorts of FreeMSA Y).s2 by A2;
assume s1 <> s2;
then
A5: (the Sorts of FreeMSA Y).s1 misses (the Sorts of FreeMSA Y).s2
by PROB_2:def 2;
let t1 be expression of C, s1;
let t2 be expression of C, s2;
A6: t1 in (the Sorts of Free(C,X)).s1 by Def28;
t2 in (the Sorts of Free(C,X)).s2 by Def28;
hence thesis by A3,A4,A5,A6,XBOOLE_0:3;
end;
begin :: Quasi-terms
definition
let C;
A1: (the Sorts of Free(C, MSVars C)).a_Term C c=
Union the Sorts of Free(C, MSVars C)
proof
let x be object;
dom the Sorts of Free(C, MSVars C) = the carrier of C by PARTFUN1:def 2;
hence thesis by CARD_5:2;
end;
func QuasiTerms C -> Subset of Free(C, MSVars C) equals
(the Sorts of Free(C, MSVars C)).a_Term C;
coherence by A1;
end;
registration
let C;
cluster QuasiTerms C -> non empty constituted-DTrees;
coherence;
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 Th41;
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 by Def25;
then root-tree [x, a_Term] in QuasiTerms C by MSAFREE3:4;
hence thesis by Th41;
end;
end;
theorem Th50:
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 thesis by XTUPLE_0:1;
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
A1: a_Term C <> the carrier of C;
A2: (x-term C).{} = [x, a_Term C] by TREES_4:3;
a_Term C nin {the carrier of C} by A1,TARSKI:def 1;
hence (x-term C).{} nin [:the carrier' of C, {the carrier of C}:]
by A2,ZFMISC_1:87;
end;
end;
theorem Th51:
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;
A1: o <> * by Def11;
A2: o <> non_op by Def11;
let p be DTree-yielding FinSequence;
set V = (MSVars C) (\/) ((the carrier of C) --> {0});
A3: the Sorts of Free(C, MSVars C) = C-Terms(MSVars C, V) by MSAFREE3:24;
thus
now
assume
A4: [o, the carrier of C]-tree p is expression of C;
then
A5: [o, the carrier of C]-tree p is Term of C, V by MSAFREE3:8;
then
A6: 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 A5,MSATERM:1;
A7: the_sort_of ((Sym(o,V))-tree q) = the_result_sort_of o by MSATERM:20;
A8: variables_in ((Sym(o,V))-tree q) c= MSVars C by A4,MSAFREE3:27;
(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 5;
then Sym(o,V)-tree p in (C-Terms(MSVars C,V)).the_result_sort_of o
by A7,A8;
then
A9: rng p c= Union (C-Terms(MSVars C,V)) by A6,MSAFREE3:19;
rng p c= QuasiTerms C
proof
let a be object;
assume
A10: a in rng p;
then reconsider ta = a as expression of C by A9,MSAFREE3:24;
consider i being object such that
A11: i in dom p and
A12: a = p.i by A10,FUNCT_1:def 3;
reconsider i as Nat by A11;
reconsider t = p.i as Term of C, V by A6,A11,MSATERM:22;
A13: (the Arity of C).o in {a_Term}* by A1,A2,Def9;
A14: dom p = dom the_arity_of o by A6,MSATERM:22;
A15: the_arity_of o is FinSequence of {a_Term} by A13,FINSEQ_1:def 11;
A16: (the_arity_of o).i in rng the_arity_of o by A11,A14,FUNCT_1:def 3;
rng the_arity_of o c= {a_Term C} by A15,FINSEQ_1:def 4;
then (the_arity_of o).i = a_Term C by A16,TARSKI:def 1;
then
A17: the_sort_of t = a_Term C by A6,A11,MSATERM:23;
t = ta by A12;
then variables_in t c= MSVars C by MSAFREE3:27;
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 A17;
then t in (C-Terms(MSVars C,V)).a_Term C by MSAFREE3:def 5;
hence thesis by A12,MSAFREE3:23;
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
A18: len p = len the_arity_of o;
assume
A19: p in (QuasiTerms C)*;
Free(C, MSVars C) = (FreeMSA V)|(C-Terms(MSVars C, V)) by MSAFREE3:25;
then the Sorts of Free(C, MSVars C) is ManySortedSubset of
the Sorts of FreeMSA V by MSUALG_2:def 9;
then the Sorts of Free(C, MSVars C) c= the Sorts of FreeMSA V
by PBOOLE:def 18;
then
A20: QuasiTerms C c= (the Sorts of FreeMSA V).a_Term C;
A21: p is FinSequence of QuasiTerms C by A19,FINSEQ_1:def 11;
then
A22: rng p c= QuasiTerms C by FINSEQ_1:def 4;
now
let i be Nat;
assume
A23: i in dom p;
then p.i in rng p by FUNCT_1:def 3;
then
A24: p.i in QuasiTerms C by A22;
then reconsider t = p.i as expression of C;
A25: (the Arity of C).o in {a_Term}* by A1,A2,Def9;
A26: dom p = dom the_arity_of o by A18,FINSEQ_3:29;
A27: the_arity_of o is FinSequence of {a_Term} by A25,FINSEQ_1:def 11;
A28: (the_arity_of o).i in rng the_arity_of o by A23,A26,FUNCT_1:def 3;
rng the_arity_of o c= {a_Term C} by A27,FINSEQ_1:def 4;
then
A29: (the_arity_of o).i = a_Term C by A28,TARSKI:def 1;
reconsider T = t as Term of C,V by MSAFREE3:8;
take T;
thus T = p.i;
T in (the Sorts of FreeMSA V).a_Term C by A20,A24;
then T in FreeSort(V, a_Term C) by MSAFREE:def 11;
hence the_sort_of T = (the_arity_of o).i by A29,MSATERM:def 5;
end;
then
A30: p is ArgumentSeq of Sym(o,V) by A18,MSATERM:24;
A31: dom the Sorts of Free(C, MSVars C) = the carrier of C by PARTFUN1:def 2;
rng p c= Union (C-Terms(MSVars C, V)) by A3,A21,FINSEQ_1:def 4;
then Sym(o,V)-tree p in (C-Terms(MSVars C, V)).the_result_sort_of o
by A30,MSAFREE3:19;
hence thesis by A3,A31,CARD_5:2;
end;
reserve p for FinSequence of QuasiTerms C;
definition
let C,c;
let p such that
A1: len p = len the_arity_of c;
A2: p in (QuasiTerms C)* by FINSEQ_1:def 11;
func c-trm p -> compound expression of C equals
:
Def35: [c, the carrier of C]-tree p;
coherence
proof
reconsider t = [c, the carrier of C]-tree p as expression of C by A1,A2
,Th51;
t.{} = [c, the carrier of C] by TREES_4:def 4;
then t.{} in [:the carrier' of C, {the carrier of C}:] by ZFMISC_1:106;
hence thesis by Def27;
end;
end;
theorem Th52:
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
A1: Sym(c,V)-tree p = c-trm p by Def35;
A2: the Sorts of Free(C,X) = C-Terms(X,V) by MSAFREE3:24;
c-trm p is Term of C,V by MSAFREE3:8;
then reconsider q = p as ArgumentSeq of Sym(c,V) by A1,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 A1,A2,MSAFREE3:19;
hence thesis by A2,Def28;
end;
theorem Th53:
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 Th7;
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
A1: t = root-tree [v,s] and
A2: v in X.s;
the carrier of C = {a_Type, an_Adj, a_Term} by Def9;
then
A3: s = a_Term or s = an_Adj or s = a_Type by ENUMSET1:def 1;
then reconsider v as variable by A2,Def25;
t = v-term C by A1,A2,A3,Def25;
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
A4: t = [o, the carrier of C]-tree p and
A5: len p = len the_arity_of o and
p is DTree-yielding and
A6: p is ArgumentSeq of Sym(o,V);
per cases;
suppose
A7: o = *;
then
A8: the_arity_of o = <*an_Adj,a_Type*> by Def9;
A9: dom p = dom the_arity_of o by A6,MSATERM:22;
A10: dom the_arity_of o = Seg 2 by A8,FINSEQ_1:89;
A11: len the_arity_of o = 2 by A8,FINSEQ_1:44;
A12: 1 in Seg 2;
A13: 2 in Seg 2;
A14: p.1 in rng p by A9,A10,A12,FUNCT_1:3;
p.2 in rng p by A9,A10,A13,FUNCT_1:3;
then reconsider p1 = p.1, p2 = p.2 as expression of C by A14;
reconsider t1 = p1, t2 = p2 as Term of C,V by MSAFREE3:8;
A15: C variables_in p1 c= X by MSAFREE3:27;
A16: variables_in t1 = C variables_in t1;
A17: C variables_in p2 c= X by MSAFREE3:27;
A18: variables_in t2 = C variables_in t2;
A19: <*an_Adj,a_Type*>.2 = a_Type C;
A20: <*an_Adj,a_Type*>.1 = an_Adj C;
the_sort_of t1 = (the_arity_of o).1 by A6,A9,A10,A12,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 A8,A15,A16;
then p1 in C-Terms(X,V).an_Adj C by MSAFREE3:def 5;
then p1 in (the Sorts of Free(C,X)).an_Adj C by MSAFREE3:24;
then reconsider a = p1 as expression of C, an_Adj C by Def28;
the_sort_of t2 = (the_arity_of o).2 by A6,A9,A10,A13,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 A8,A17,A18;
then p2 in C-Terms(X,V).a_Type C by MSAFREE3:def 5;
then p2 in (the Sorts of Free(C,X)).a_Type C by MSAFREE3:24;
then reconsider q = p2 as expression of C, a_Type C by Def28;
p = <*a,q*> by A5,A11,FINSEQ_1:44;
then t = (ast C)term(a,q) by A4,A7,A8,A11,A19,A20,Def31;
hence thesis;
end;
suppose
A21: o = non_op;
then
A22: the_arity_of o = <*an_Adj*> by Def9;
A23: dom p = dom the_arity_of o by A6,MSATERM:22;
A24: dom the_arity_of o = Seg 1 by A22,FINSEQ_1:38;
A25: len the_arity_of o = 1 by A22,FINSEQ_1:39;
A26: 1 in Seg 1;
then p.1 in rng p by A23,A24,FUNCT_1:3;
then reconsider p1 = p.1 as expression of C;
reconsider t1 = p1 as Term of C,V by MSAFREE3:8;
A27: C variables_in p1 c= X by MSAFREE3:27;
A28: variables_in t1 = C variables_in t1;
A29: <*an_Adj*>.1 = an_Adj C;
the_sort_of t1 = (the_arity_of o).1 by A6,A23,A24,A26,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 A22,A27,A28;
then p1 in C-Terms(X,V).an_Adj C by MSAFREE3:def 5;
then p1 in (the Sorts of Free(C,X)).an_Adj C by MSAFREE3:24;
then reconsider a = p1 as expression of C, an_Adj C by Def28;
p = <*a*> by A5,A25,FINSEQ_1:40;
then t = (non_op C)term(a) by A4,A21,A22,A25,A29,Def30;
hence thesis;
end;
suppose o is constructor;
then reconsider o as constructor OperSymbol of C;
t = [o, the carrier of C]-tree p by A4;
then p in (QuasiTerms C)* by Th51;
then reconsider p as FinSequence of QuasiTerms C by FINSEQ_1:def 11;
t = o-trm p by A4,A5,Def35;
hence thesis by A5;
end;
end;
end;
theorem Th54:
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 Def35;
then
A1: (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 Th43;
then [c, the carrier of C] = [non_op, the carrier of C] by A1,TREES_4:def 4;
then c = non_op by XTUPLE_0:1;
hence thesis by Def11;
end;
theorem Th55:
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 Def35;
then
A1: (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 Th46;
then [c, the carrier of C] = [ *, the carrier of C] by A1,TREES_4:def 4;
then c = * by XTUPLE_0:1;
hence thesis by Def11;
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 Th46;
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 Th43;
then [non_op, the carrier of C] = [ *, the carrier of C] by TREES_4:def 4;
hence thesis by XTUPLE_0:1;
end;
reserve e for expression of C;
theorem Th57:
e.{} = [non_op, the carrier of C] implies ex a st e = (non_op C)term a
proof
assume
A1: e.{} = [non_op, the carrier of C];
non_op C in the carrier' of C;
then
A2: e.{} in [:the carrier' of C, {the carrier of C}:] by A1,ZFMISC_1:106;
per cases by Th53;
suppose
ex x being variable st e = x-term C;
hence thesis by A2,Def27;
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
A3: len p = len the_arity_of c and
A4: e = c-trm p;
e = [c, the carrier of C]-tree p by A3,A4,Def35;
then e.{} = [c, the carrier of C] by TREES_4:def 4;
then non_op = c by A1,XTUPLE_0:1;
hence thesis by Def11;
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
A5: e = (ast C)term(a,t);
e = [ *, the carrier of C]-tree <*a,t*> by A5,Th46;
then e.{} = [ *, the carrier of C] by TREES_4:def 4;
hence thesis by A1,XTUPLE_0:1;
end;
end;
theorem Th58:
e.{} = [ *, the carrier of C] implies ex a, t st e = (ast C)term(a,t)
proof
assume
A1: e.{} = [ *, the carrier of C];
ast C in the carrier' of C;
then
A2: e.{} in [:the carrier' of C, {the carrier of C}:] by A1,ZFMISC_1:106;
per cases by Th53;
suppose
ex x being variable st e = x-term C;
hence thesis by A2,Def27;
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
A3: len p = len the_arity_of c and
A4: e = c-trm p;
e = [c, the carrier of C]-tree p by A3,A4,Def35;
then e.{} = [c, the carrier of C] by TREES_4:def 4;
then * = c by A1,XTUPLE_0:1;
hence thesis by Def11;
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
A5: e = (non_op C)term a;
e = [non_op, the carrier of C]-tree <*a*> by A5,Th43;
then e.{} = [non_op, the carrier of C] by TREES_4:def 4;
hence thesis by A1,XTUPLE_0:1;
end;
suppose
ex a,t st e = (ast C)term(a,t);
hence thesis;
end;
end;
begin :: Quasi-adjectives
reserve a,a9 for expression of C, an_Adj C;
definition
let C,a;
func Non a -> expression of C, an_Adj C equals
:
Def36: a|<* 0 *> if ex a9 st a = (non_op C)term a9
otherwise (non_op C)term a;
coherence
proof
thus
now
given a9 being expression of C, an_Adj C such that
A1: a = (non_op C)term a9;
A2: a = [non_op, the carrier of C]-tree <*a9*> by A1,Th43;
len <*a9*> = 1 by FINSEQ_1:40;
then a|<* 0*> = <*a9*>.(0+1) by A2,TREES_4:def 4;
hence a|<* 0*> is expression of C, an_Adj C;
end;
thus thesis by Th43;
end;
consistency;
end;
definition
let C,a;
attr a is positive means
:
Def37: not ex a9 st a = (non_op C)term a9;
end;
registration
let C;
cluster positive for expression of C, an_Adj C;
existence
proof consider m, a being OperSymbol of C such that
the_result_sort_of m = a_Type and the_arity_of m = {} and
A1: the_result_sort_of a = an_Adj and
A2: the_arity_of a = {} by Def12;
set X = MSVars C;
root-tree [a, the carrier of C] in (the Sorts of Free(C, X)).an_Adj by A1
,A2,MSAFREE3:5;
then reconsider
v = root-tree [a, the carrier of C] as expression of C, an_Adj C
by Th41;
take v;
given a9 being expression of C, an_Adj C such that
A3: v = (non_op C)term a9;
v = [non_op, the carrier of C]-tree<*a9*> by A3,Th43;
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 XTUPLE_0:1;
hence contradiction by A2,Def9;
end;
end;
theorem Th59:
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 a9 being expression of C, an_Adj C st a = (non_op C)term a9 by Def37;
hence thesis by Def36;
end;
definition
let C,a;
attr a is negative means
:
Def38: ex a9 st a9 is positive & a = (non_op C)term a9;
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 Th59; end;
take a;
thus thesis by Th59;
end;
end;
registration
let C;
cluster negative non positive for expression of C, an_Adj C;
existence
proof set a = the positive expression of C, an_Adj C;
take Non a;
thus thesis;
end;
end;
theorem Th60:
for a being non positive expression of C, an_Adj C
ex a9 being expression of C, an_Adj C
st a = (non_op C)term a9 & Non a = a9
proof
let a be non positive expression of C, an_Adj C;
consider a9 being expression of C, an_Adj C such that
A1: a = (non_op C)term a9 by Def37;
A2: a = [non_op, the carrier of C]-tree<*a9*> by A1,Th43;
take a9;
len <*a9*> = 1 by FINSEQ_1:40;
then a|<* 0*> = <*a9*>.(0+1) by A2,TREES_4:def 4
.= a9;
hence thesis by A1,Def36;
end;
theorem Th61:
for a being negative expression of C, an_Adj C
ex a9 being positive expression of C, an_Adj C
st a = (non_op C)term a9 & Non a = a9
proof
let a be negative expression of C, an_Adj C;
consider a9 being expression of C, an_Adj C such that
A1: a9 is positive and
A2: a = (non_op C)term a9 by Def38;
A3: a = [non_op, the carrier of C]-tree<*a9*> by A2,Th43;
reconsider a9 as positive expression of C, an_Adj C by A1;
take a9;
len <*a9*> = 1 by FINSEQ_1:40;
then a|<* 0*> = <*a9*>.(0+1) by A3,TREES_4:def 4
.= a9;
hence thesis by A2,Def36;
end;
theorem Th62:
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;
ex a9 being expression of C, an_Adj C st ( a = (non_op C)
term a9)&( Non a = a9) by Th60;
hence thesis;
end;
registration
let C;
let a be negative expression of C, an_Adj C;
cluster Non a -> positive;
coherence
proof
ex a9 being positive expression of C, an_Adj C st
a = (non_op C)term a9 & Non a = a9 by Th61;
hence thesis;
end;
end;
definition
let C,a;
attr a is regular means
:
Def39: a is positive or a is negative;
end;
registration
let C;
cluster positive -> regular non negative for expression of C, an_Adj C;
coherence;
cluster negative -> regular non positive for expression of C, an_Adj C;
coherence;
end;
registration
let C;
cluster regular for expression of C, an_Adj C;
existence
proof
set a = the positive expression of C, an_Adj C;
take a;
thus thesis;
end;
end;
definition
let C;
set X = {a: a is regular};
A1: X c= Union the Sorts of Free(C, MSVars C)
proof
let x be object;
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 A1;
end;
registration
let C;
cluster QuasiAdjs C -> non empty constituted-DTrees;
coherence
proof set v = the positive expression of C, an_Adj C;
v in {a: a is regular};
hence QuasiAdjs C is non empty;
let x be object;
assume x in QuasiAdjs C;
hence thesis;
end;
end;
definition
let C;
mode quasi-adjective of C is regular expression of C, an_Adj C;
end;
theorem Th63:
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 Def39;
registration
let C;
cluster non positive -> negative for quasi-adjective of C;
coherence by Def39;
cluster non negative -> positive for quasi-adjective of C;
coherence;
end;
registration
let C;
cluster positive for quasi-adjective of C;
existence
proof set a = the positive expression of C, an_Adj C;
a is quasi-adjective of C;
hence thesis;
end;
cluster negative for quasi-adjective of C;
existence
proof set a = the negative expression of C, an_Adj C;
a is quasi-adjective of C;
hence thesis;
end;
end;
theorem Th65:
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 Th53;
suppose
ex x being variable st e = x-term C;
hence thesis by Th48;
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
A1: len p = len the_arity_of c and
A2: e = c-trm p;
take c;
e is expression of C, the_result_sort_of c by A1,A2,Th52;
hence the_result_sort_of c = an_Adj C by Th48;
take p;
thus thesis by A1,A2;
end;
suppose
ex a st e = (non_op C)term a;
hence thesis by Def37;
end;
suppose
ex a,t st e = (ast C)term(a,t);
then e is expression of C, a_Type C by Th46;
hence thesis by Th48;
end;
end;
theorem Th66:
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
A1: the_result_sort_of v = an_Adj C;
assume
A2: len p = len the_arity_of v;
then reconsider a = v-trm p as expression of C, an_Adj C by A1,Th52;
a is positive
by A2,Th54;
hence thesis;
end;
registration
let C;
let a be quasi-adjective of C;
cluster Non a -> regular;
coherence
proof per cases;
suppose a is positive;
then reconsider a9 = a as positive expression of C, an_Adj C;
Non a9 is negative;
hence thesis;
end;
suppose a is negative;
then reconsider a9 = a as negative expression of C, an_Adj C;
Non a9 is positive;
hence thesis;
end;
end;
end;
theorem Th67:
for a being quasi-adjective of C holds Non Non a = a
proof
let a be quasi-adjective of C;
per cases;
suppose a is positive;
then reconsider a9 = a as positive expression of C, an_Adj C;
A1: ex b being positive expression of C, an_Adj C st ( Non a9 =
(non_op C)term b)&( Non Non a9 = b) by Th61;
Non a9 = (non_op C)term a by Th59;
hence thesis by A1,Th44;
end;
suppose a is negative;
then reconsider a9 = a as negative expression of C, an_Adj C;
ex b being positive expression of C, an_Adj C st
a9 = (non_op C)term b & Non a9 = b by Th61;
hence thesis by Th59;
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 by Th67;
hence thesis by Th67;
end;
theorem
for a being quasi-adjective of C holds Non a <> a
proof
let a be quasi-adjective of C;
per cases;
suppose a is positive;
then reconsider a9 = a as positive quasi-adjective of C;
Non a9 is negative quasi-adjective of C;
hence thesis;
end;
suppose a is negative;
then reconsider a9 = a as negative quasi-adjective of C;
Non a9 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
:
Def41: not ex a, t st q = (ast C)term(a,t);
end;
theorem Th70:
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
A1: the_result_sort_of m = a_Type and
A2: the_arity_of m = {};
set X = MSVars C;
root-tree [m, the carrier of C] in (the Sorts of Free(C, X)).a_Type by A1,A2,
MSAFREE3:5;
then reconsider
T = root-tree [m, the carrier of C] as expression of C, a_Type C
by Th41;
take T;
thus T = root-tree [m, the carrier of C];
given a,t such that
A3: T = (ast C)term(a,t);
T = [ *, the carrier of C]-tree<*a,t*> by A3,Th46;
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 XTUPLE_0:1;
hence contradiction by A2,Def9;
end;
theorem Th71:
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
A1: the_result_sort_of m = an_Adj and
A2: 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 A1,A2,MSAFREE3:5;
then reconsider
T = root-tree [m, the carrier of C] as expression of C, an_Adj C
by Th41;
take T;
thus T = root-tree [m, the carrier of C];
given a being expression of C, an_Adj C such that
A3: T = (non_op C)term a;
T = [non_op, the carrier of C]-tree<*a*> by A3,Th43;
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 XTUPLE_0:1;
hence contradiction by A2,Def9;
end;
registration
let C;
cluster pure for 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 and
A2: the_arity_of m = {} and
the_result_sort_of a = an_Adj and the_arity_of a = {} by Def12;
ex t being expression of C, a_Type C st
t = root-tree [m, the carrier of C] & t is pure by A1,A2,Th70;
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 -> set equals
{[A,t]: t is pure};
coherence;
end;
registration
let C;
cluster QuasiTypes C -> non empty;
coherence
proof set q = the pure expression of C, a_Type C;
{} 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 -> set means
:
Def43: it in QuasiTypes C;
existence
proof set T = the Element of QuasiTypes C;
take T;
thus thesis;
end;
end;
theorem Th72:
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 Def43;
end;
theorem Th73:
[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 ex A,q st ( [x,y] = [A,q]) by Th72;
hence x is finite Subset of QuasiAdjs C &
y is pure expression of C, a_Type C by XTUPLE_0:1;
end;
thus thesis by Th72;
end;
reserve T for quasi-type of C;
registration
let C;
cluster -> pair for quasi-type of C;
coherence
proof
let x be quasi-type of C;
ex A,q st x = [A,q] by Th72;
hence thesis;
end;
end;
theorem Th74:
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 Th53;
suppose
ex x being variable st e = x-term C;
hence thesis by Th48;
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
A1: len p = len the_arity_of c and
A2: e = c-trm p;
take c;
e is expression of C, the_result_sort_of c by A1,A2,Th52;
hence the_result_sort_of c = a_Type C by Th48;
take p;
thus thesis by A1,A2;
end;
suppose
ex a st e = (non_op C)term a;
then e is expression of C, an_Adj C by Th43;
hence thesis by Th48;
end;
suppose
ex a st ex q being expression of C, a_Type C st e = (ast C)term(a,q);
hence thesis by Def41;
end;
end;
theorem Th75:
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
A1: the_result_sort_of v = a_Type C;
assume
A2: len p = len the_arity_of v;
then reconsider a = v-trm p as expression of C, a_Type C by A1,Th52;
a is pure
by A2,Th55;
hence thesis;
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});
ex A being MSSubset of FreeMSA Y st ( Free(C, X) = GenMSAlg
A)&( A = (Reverse Y)""X) by MSAFREE3:def 1;
then the Sorts of Free(C, X) is MSSubset of FreeMSA Y by MSUALG_2:def 9;
then
A1: the Sorts of Free(C, X) c= the Sorts of FreeMSA Y by PBOOLE:def 18;
then
A2: QuasiTerms C c= (the Sorts of FreeMSA Y).a_Term C;
A3: (the Sorts of Free(C,X)).an_Adj C c= (the Sorts of FreeMSA Y).an_Adj C
by A1;
QuasiAdjs C c= (the Sorts of Free(C,X)).an_Adj C
proof
let x be object;
assume x in QuasiAdjs C;
then ex a st x = a & a is regular;
hence thesis by Def28;
end;
then
A4: QuasiAdjs C c= (the Sorts of FreeMSA Y).an_Adj C by A3;
(the Sorts of FreeMSA Y).a_Term C misses (the Sorts of FreeMSA Y).an_Adj C
by PROB_2:def 2;
hence QuasiTerms C misses QuasiAdjs C by A2,A4,XBOOLE_1:64;
now
let x be object;
assume that
A5: x in QuasiTerms C and
A6: x in QuasiTypes C;
x is quasi-type of C by A6,Def43;
hence contradiction by A5;
end;
hence QuasiTerms C misses QuasiTypes C by XBOOLE_0:3;
now
let x be object;
assume that
A7: x in QuasiAdjs C and
A8: x in QuasiTypes C;
x is quasi-type of C by A8,Def43;
hence contradiction by A7;
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 Th48;
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; :: redefines ast (ABCMIZ_1, synonym) → [ (TARSKI, definition)
coherence by Th73;
end;
registration
let C,T;
cluster T`1 -> finite for set;
coherence
proof
ex A,q st T = [A,q] by Th72;
hence thesis;
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; :: redefines adjs (ABCMIZ_1, synonym) → `1 (XTUPLE_0, definition)
coherence
proof
ex A,q st T = [A,q] by Th72;
hence thesis;
end;
redefine func the_base_of T -> pure expression of C, a_Type C; :: redefines the_base_of (ABCMIZ_1, synonym) → `2 (XTUPLE_0, definition)
coherence
proof
ex A,q st T = [A,q] by Th72;
hence thesis;
end;
end;
theorem
adjs (A ast q) = A & the_base_of (A ast q) = q;
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 XTUPLE_0:1;
theorem Th80:
T = (adjs T) ast the_base_of T;
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;
hence thesis by Th80;
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:31;
then {a} \/ adjs T is Subset of QuasiAdjs C by XBOOLE_1:8;
hence thesis by Th73;
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;
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)]
.= [{a} \/ {a} \/ adjs T, the_base_of (a ast T)] by XBOOLE_1:4
.= a ast T;
end;
theorem
for a,b being quasi-adjective of C holds a ast (b ast T) = b ast (a ast T)
by XBOOLE_1:4;
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:10;
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
A3: 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};
A4: rng p is finite;
A5: A is finite from FRAENKEL:sch 21(A4);
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 A3;
end;
then
A6: union A is finite by A5,FINSET_1:7;
(S variables_in ([o,the carrier of S]-tree p)).s c= union A
proof
let x be object;
assume x in (S variables_in ([o,the carrier of S]-tree p)).s;
then consider t being DecoratedTree such that
A7: t in rng p and
A8: x in (S variables_in t).s by MSAFREE3:11;
consider i being object such that
A9: i in dom p and
A10: t = p.i by A7,FUNCT_1:def 3;
reconsider i as Nat by A9;
reconsider t = p.i as Term of S,X by A9,MSATERM:22;
(S variables_in t).s in A by A7,A10;
hence thesis by A8,A10,TARSKI:def 4;
end;
hence thesis by A6;
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:8;
(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
:
Def45: 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:63;
end;
existence
proof
defpred P[object,object] means
ex t being Element of Free(S,X) st t = $1 & $2 = (S variables_in t).s;
A3: now
let x be object;
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:27;
then (S variables_in t).s c= X.s;
hence ex y being object 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 being object st x in Union the Sorts of Free(S,X) holds P[x, f.x]
from FUNCT_1:sch 6(A3);
reconsider f as Function of Union the Sorts of Free(S,X), bool (X.s)
by A4,FUNCT_2:2;
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
A1: (MSVars C).a_Term C = Vars by Def25;
C variables_in e c= MSVars C by MSAFREE3:27;
hence thesis by A1;
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 Th24;
end;
theorem
varcl vars e = vars e;
theorem
for x being variable holds variables_in (x-term C) = {x} by MSAFREE3:10;
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:10
.= {x} \/ vars x by Th27;
end;
theorem Th88:
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
A1: e = [c, the carrier of C]-tree p;
then p in (QuasiTerms C)* by Th51;
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 object;
assume a in variables_in e;
then consider t being DecoratedTree such that
A3: t in rng p and
A4: a in (C variables_in t).a_Term C by A1,MSAFREE3:11;
reconsider t as quasi-term of C by A2,A3,Th41;
variables_in t in X by A3;
hence thesis by A4,TARSKI:def 4;
end;
let a be object;
assume a in union X;
then consider Y being set such that
A5: a in Y and
A6: Y in X by TARSKI:def 4;
ex t being quasi-term of C st Y = variables_in t & t in rng p by A6;
hence thesis by A1,A5,MSAFREE3:11;
end;
theorem Th89:
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
A2: A = {};
set b = the Element of B;
now
assume B <> {};
then b in B;
then consider t being quasi-term of C such that
b = vars t and
A3: t in rng p;
variables_in t in A by A3;
hence contradiction by A2;
end;
hence thesis by A1,A2,Th8,Th88,ZFMISC_1:2;
end;
suppose A <> {};
then reconsider A as non empty set;
set D = the set of all varcl s where s is Element of A;
A4: B c= D
proof
let a be object;
assume a in B;
then consider t being quasi-term of C such that
A5: a = vars t and
A6: t in rng p;
variables_in t in A by A6;
then reconsider s = variables_in t as Element of A;
a = varcl s by A5;
hence thesis;
end;
A7: D c= B
proof
let a be object;
assume a in D;
then consider s being Element of A such that
A8: a = varcl s;
s in A;
then consider t being quasi-term of C such that
A9: s = variables_in t and
A10: t in rng p;
vars t = a by A8,A9;
hence thesis by A10;
end;
thus vars e = varcl union A by A1,Th88
.= union D by Th10
.= union B by A4,A7,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 Def35;
hence thesis by Th88;
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 Def35;
hence thesis by Th89;
end;
theorem
for S being ManySortedSign, o being set holds
S variables_in ([o, the carrier of S]-tree {}) = EmptyMS the carrier of S
proof
let S be ManySortedSign, o be set;
now
let s be object;
assume
A1: s in the carrier of S;
now
let x be object;
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:11;
hence x in (S variables_in ([o, the carrier of S]-tree {})).s iff
x in (EmptyMS the carrier of S).s;
end;
hence (S variables_in ([o, the carrier of S]-tree {})).s =
(EmptyMS the carrier of S).s by TARSKI:2;
end;
hence thesis;
end;
theorem Th93:
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 object;
assume
A1: s in the carrier of S;
A2: t in {t} by TARSKI:def 1;
now
let x be object;
rng <*t*> = {t} by FINSEQ_1:39;
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:11;
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;
end;
theorem Th94:
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 Th43;
hence thesis by Th93;
end;
theorem
vars ((non_op C)term a) = vars a by Th94;
theorem Th96:
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 object;
assume
A1: s in the carrier of S;
A2: t1 in {t1,t2} by TARSKI:def 2;
A3: t2 in {t1,t2} by TARSKI:def 2;
now
let x be object;
rng <*t1,t2*> = {t1,t2} by FINSEQ_2:127;
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:11;
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,A3,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 3;
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 4;
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;
end;
theorem Th97:
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 Th46;
then variables_in ((ast C)term(a,t))
= ((C variables_in a)(\/)(C variables_in t)).a_Term by Th96;
hence thesis by PBOOLE:def 4;
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 Th97
.= (vars a)\/(vars t) by Th11;
end;
theorem Th99:
variables_in Non a = variables_in a proof per cases;
suppose a is non positive;
then consider a9 being expression of C, an_Adj C such that
A1: a = (non_op C)term a9 and
A2: Non a = a9 by Th60;
[non_op C, the carrier of C]-tree<*a9*> = a by A1,Th43;
hence thesis by A2,Th93;
end;
suppose a is positive;
then Non a = (non_op C)term a by Th59
.= [non_op, the carrier of C]-tree <*a*> by Th43;
hence thesis by Th93;
end;
end;
theorem
vars Non a = vars a by Th99;
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
A1: ((MSVars C, a_Term C) variables_in).:adjs T is Subset of bool Vars by Def25
;
union bool Vars = Vars by ZFMISC_1:81;
then (union (((MSVars C, a_Term C) variables_in).:adjs T)) c= Vars
by A1,ZFMISC_1:77;
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 object such that
A1: x in Union the Sorts of Free(C, MSVars C) and x in adjs T and
A2: A = ((MSVars C, a_Term C) variables_in).x by FUNCT_2:64;
reconsider x as expression of C by A1;
A = (C variables_in x).a_Term C by A2,Def45;
hence A is finite;
end;
then union (((MSVars C, a_Term C) variables_in).:adjs T) is finite
by FINSET_1:7;
hence thesis;
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 Th24;
end;
theorem
for T being quasi-type of C holds varcl vars T = vars T;
theorem Th102:
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
.= (union (((MSVars C, a_Term C) variables_in).:({a} \/ adjs T)))
\/ variables_in the_base_of T
.= (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:120
.= (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:78
.= (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:59
.= (((MSVars C, a_Term C) variables_in).a) \/
variables_in T by ZFMISC_1:25
.= (variables_in a) \/ variables_in T by Def45;
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 Th102
.= (vars a) \/ vars T by Th11;
end;
theorem Th104:
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 object;
assume z in X;
then consider a being object such that
a in dom ((MSVars C, a_Term C) variables_in) and
A2: a in A and
A3: z = ((MSVars C, a_Term C) variables_in).a by FUNCT_1:def 6;
reconsider a as quasi-adjective of C by A2,Th63;
z = variables_in a by A3,Def45;
hence thesis by A2;
end;
A4: Y c= X
proof
let z be object;
assume z in Y;
then consider a being quasi-adjective of C such that
A5: z = variables_in a and
A6: a in A;
A7: z = ((MSVars C, a_Term C) variables_in).a by A5,Def45;
dom ((MSVars C, a_Term C) variables_in) = Union the Sorts of Free(C,
MSVars C) by FUNCT_2:def 1;
hence thesis by A6,A7,FUNCT_1:def 6;
end;
thus variables_in (A ast q)
= (union (((MSVars C, a_Term C) variables_in).:adjs(A ast q)))
\/ variables_in q
.= (union (((MSVars C, a_Term C) variables_in).:A))
\/ variables_in q
.= (union {variables_in a where a is quasi-adjective of C: a in A})
\/ (variables_in q) by A1,A4,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 object;
assume x in union X;
then consider Z being set such that
A2: x in Z and
A3: Z in X by TARSKI:def 4;
consider a being quasi-adjective of C such that
A4: Z = variables_in a and
A5: a in A by A3;
A6: Z c= vars a by A4,Def1;
vars a in Y by A5;
hence thesis by A2,A6,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
A7: [x,y] in Z and
A8: Z in Y by TARSKI:def 4;
ex a being quasi-adjective of C st ( Z = vars a)&( a in A) by A8;
then
A9: x c= Z by A7,Def1;
Z c= union Y by A8,ZFMISC_1:74;
hence thesis by A9;
end;
then
A10: varcl union X c= union Y by A1,Def1;
A11: union Y c= varcl union X
proof
let x be object;
assume x in union Y;
then consider Z being set such that
A12: x in Z and
A13: Z in Y by TARSKI:def 4;
consider a being quasi-adjective of C such that
A14: Z = vars a and
A15: a in A by A13;
variables_in a in X by A15;
then vars a c= varcl union X by Th9,ZFMISC_1:74;
hence thesis by A12,A14;
end;
thus vars (A ast q) = varcl((union X) \/ (variables_in q)) by Th104
.= (varcl union X) \/ (vars q) by Th11
.= (union Y) \/ (vars q) by A10,A11,XBOOLE_0:def 10;
end;
theorem Th106:
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 be object;
assume x in AA;
then ex a being quasi-adjective of C st x = variables_in a & a in A;
hence thesis;
end;
then
A1: AA = {};
variables_in (A ast q) = (union AA) \/ (variables_in q) by Th104;
hence thesis by A1,ZFMISC_1:2;
end;
theorem Th107:
e is ground iff variables_in e = {}
proof
thus e is ground implies variables_in e = {}
by Th1,XBOOLE_1:3;
assume that
A1: variables_in e = {} and
A2: Union (C variables_in e) <> {};
set x = the Element of Union (C variables_in e);
A3: ex y being object st ( y in dom (C variables_in e))&( x in (C
variables_in e).y) by A2,CARD_5:2;
A4: dom (C variables_in e) = the carrier of C by PARTFUN1:def 2
.= {a_Type, an_Adj, a_Term} by Def9;
A5: C variables_in e c= MSVars C by MSAFREE3:27;
A6: (MSVars C).an_Adj = {} by Def25;
A7: (MSVars C).a_Type = {} by Def25;
A8: (C variables_in e).an_Adj C c= {} by A5,A6;
(C variables_in e).a_Type C c= {} by A5,A7;
hence thesis by A1,A3,A4,A8,ENUMSET1:def 1;
end;
definition
let C;
let T be quasi-type of C;
attr T is ground means
:
Def50: variables_in T = {};
end;
registration
let C;
cluster ground pure for 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 and
A2: the_arity_of m = {} and
the_result_sort_of a = an_Adj and the_arity_of a = {} by Def12;
root-tree [m, the carrier of C] in
(the Sorts of Free(C,MSVars C)).a_Type C by A1,A2,MSAFREE3:5;
then reconsider
mm = root-tree [m, the carrier of C] as expression of C, a_Type C
by Th41;
take mm;
set p = <*>Union the Sorts of Free(C, MSVars C);
A3: mm = [m, the carrier of C]-tree p by TREES_4:20;
A4: m <> * by A2,Def9;
m <> non_op by A1,Def9;
then
A5: m is constructor by A4;
variables_in mm c= {}
proof
let x be object;
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 A3,A5,Th88;
then consider Y such that
x in Y and
A6: 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 A6;
hence thesis;
end;
then variables_in mm = {};
hence mm is ground by Th107;
ex t being expression of C, a_Type C st
t = root-tree [m, the carrier of C] & t is pure by A1,A2,Th70;
hence thesis;
end;
cluster ground for quasi-adjective of C;
existence
proof
consider m, a being OperSymbol of C such that
the_result_sort_of m = a_Type and the_arity_of m = {} and
A7: the_result_sort_of a = an_Adj and
A8: the_arity_of a = {} by Def12;
consider mm being expression of C, an_Adj C such that
A9: mm = root-tree [a, the carrier of C] and
A10: mm is positive by A7,A8,Th71;
reconsider mm as quasi-adjective of C by A10;
take mm;
set p = <*>Union the Sorts of Free(C, MSVars C);
A11: mm = [a, the carrier of C]-tree p by A9,TREES_4:20;
A12: a <> * by A7,Def9;
a <> non_op by A8,Def9;
then
A13: a is constructor by A12;
variables_in mm c= {}
proof
let x be object;
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 A11,A13,Th88;
then consider Y such that
x in Y and
A14: 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 A14;
hence thesis;
end;
then variables_in mm = {};
hence thesis by Th107;
end;
end;
theorem Th108:
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 Th106
.= {} by Th107;
end;
registration
let C;
let t be ground pure expression of C, a_Type C;
cluster ({} QuasiAdjs C) ast t -> ground for quasi-type of C;
coherence by Th108;
end;
registration
let C;
cluster ground for quasi-type of C;
existence
proof
set t = the 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 Th102
.= {}\/variables_in T by Th107
.= {} by Def50;
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 the set of all varcl A where A is finite Subset of Vars)opp;
coherence
proof set A0 = the finite Subset of Vars;
set V = the set of all varcl A where A is finite Subset of Vars;
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 Th109:
for x, y being Element of VarPoset holds x <= y iff y c= x
proof
let x, y be Element of VarPoset;
set V = the set of all varcl A where A is finite Subset of Vars;
set A0 = the 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 Th110:
for x holds
x is Element of VarPoset iff x is finite Subset of Vars & varcl x = x
proof
let x;
set V = the set of all varcl A where A is finite Subset of Vars;
set A0 = the finite Subset of Vars;
varcl A0 in V;
then reconsider V as non empty set;
the carrier of InclPoset V = V by YELLOW_1:1;
then x is Element of VarPoset iff x in V;
then x is Element of VarPoset iff
ex A being finite Subset of Vars st x = varcl A;
hence thesis by Th24;
end;
registration
cluster VarPoset -> with_infima with_suprema;
coherence
proof
set V = the set of all varcl A where A is finite Subset of Vars;
set A0 = the 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
A1: x = varcl A1;
assume y in V;
then consider A2 being finite Subset of Vars such that
A2: y = varcl A2;
x \/ y = varcl (A1 \/ A2) by A1,A2,Th11;
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
A3: x = varcl A1;
assume y in V;
then consider A2 being finite Subset of Vars such that
A4: y = varcl A2;
reconsider V1 = varcl A1, V2 = varcl A2 as finite Subset of Vars by Th24;
x /\ y = varcl (V1 /\ V2) by A3,A4,Th13;
hence x /\ y in V;
end;
then InclPoset V is with_infima by YELLOW_1:12;
hence thesis by YELLOW_7:16;
end;
end;
theorem Th111:
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 = the set of all varcl A where A is finite Subset of Vars;
set A0 = the 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
A3: V1 = varcl A1;
V2 in V by A2;
then consider A2 being finite Subset of Vars such that
A4: V2 = varcl A2;
A5: a1~ = v1;
A6: 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 A3,A4,Th24;
V1 /\ V2 = varcl (x1 /\ x2) by A3,A4,Th13;
then V1 /\ V2 in V;
then a1 "/\" a2 = V1 /\ V2 by YELLOW_1:9;
hence V1 "\/" V2 = V1 /\ V2 by A5,A6,A7,YELLOW_7:21;
V1 \/ V2 = varcl (A1 \/ A2) by A3,A4,Th11;
then a1 \/ a2 in V;
then a1 "\/" a2 = V1 \/ V2 by YELLOW_1:8;
hence thesis by A5,A6,A7,YELLOW_7:23;
end;
registration
let V1,V2 be Element of VarPoset;
identify V1 "\/" V2 with V1 /\ V2;
compatibility by Th111;
identify V1 "/\" V2 with V1 \/ V2;
compatibility by Th111;
end;
theorem Th112:
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;
set a = the Element of X;
A1: meet X c= a by SETFAM_1:3;
A2: a is finite Subset of Vars by Th110;
then
A3: meet X c= Vars by A1,XBOOLE_1:1;
for a being Element of X holds varcl a = a by Th110;
then varcl meet X = meet X by Th12;
then reconsider m = meet X as Element of VarPoset by A1,A2,A3,Th110;
A4: now
thus X is_<=_than m
by SETFAM_1:3,Th109;
let b be Element of VarPoset;
assume
A5: X is_<=_than b;
for Y st Y in X holds b c= Y by Th109,A5;
then b c= m by SETFAM_1:5;
hence m <= b by Th109;
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 Th112;
hence thesis by WAYBEL_0:75;
end;
end;
theorem
Top VarPoset = {}
proof
set V = the set of all varcl A where A is finite Subset of Vars;
A1: {} Vars in V by Th8;
A2: VarPoset opp is lower-bounded by YELLOW_7:31;
(Bottom InclPoset V)~ = {} by A1,YELLOW_1:13;
hence thesis by A2,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 Def43;
thus f1.T = vars t by A1
.= f2.T by A2;
end;
hence thesis by FUNCT_2:63;
end;
existence
proof
defpred P[object,object] means
ex T being quasi-type of C st $1 = T & $2 = vars T;
A3: for x being object st x in QuasiTypes C
ex y being object st P[x,y]
proof
let x be object;
assume x in QuasiTypes C;
then reconsider T = x as quasi-type of C by Def43;
take vars T, T;
thus thesis;
end;
consider f being Function such that
A4: dom f = QuasiTypes C and
A5: for x being object st x in QuasiTypes C holds P[x,f.x]
from CLASSES1:sch 1(A3);
rng f c= the carrier of VarPoset
proof
let y be object;
assume y in rng f;
then consider x being object such that
A6: x in dom f and
A7: y = f.x by FUNCT_1:def 3;
consider T being quasi-type of C such that
x = T and
A8: y = vars T by A4,A5,A6,A7;
varcl vars T = vars T;
then y is Element of VarPoset by A8,Th110;
hence thesis;
end;
then reconsider f as Function of QuasiTypes C, the carrier of VarPoset
by A4,FUNCT_2:2;
take f;
let x be quasi-type of C;
x in QuasiTypes C by Def43;
then ex T being quasi-type of C st x = T & f.x = vars T by A5;
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}#);
A1: T in QuasiTypes C by Def43;
then {T} c= QuasiTypes C by ZFMISC_1:31;
then reconsider f = (vars-function C)|{T} as Function of L, VarPoset
by FUNCT_2:32;
take C, f;
thus the carrier of L c= QuasiTypes C by A1,ZFMISC_1:31;
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 by TARSKI:def 1;
y = T by TARSKI:def 1;
then
A3: F = {T} by A2,ENUMSET1:29;
dom f = {T} by FUNCT_2:def 1;
then
A4: Im(f,T) = {f.x} by A2,FUNCT_1:59;
hence ex_sup_of f.:F, VarPoset by A3,YELLOW_0:38;
thus sup (f.:F) = f.x by A3,A4,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
A1: for x being variable holds P[x-term 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 &
for t being quasi-term of C() st t in rng p holds P[t]
holds P[c-trm p] and
A3: for a being expression of C(), an_Adj C() st P[a]
holds P[(non_op C())term a] and
A4: 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();
A5: t() is Term of S,V by MSAFREE3:8;
A6: 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
A7: t is expression of S;
A8: t.{} = [v,s] by TREES_4:3;
A9: s in the carrier of C;
A10: (t.{})`2 = s by A8;
A11: s <> the carrier of C by A9;
per cases by A7,Th53;
suppose ex x being variable st t = x-term C;
hence thesis by A1;
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
A12: len p = len the_arity_of c and
A13: t = c-trm p;
t = [c, the carrier of C]-tree p by A12,A13,Def35;
then t.{} = [c, the carrier of C] by TREES_4:def 4;
hence thesis by A10,A11;
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
A14: t = (non_op C)term a;
A15: the_arity_of non_op C = <*an_Adj C*> by Def9;
A16: <*an_Adj C*>.1 = an_Adj C;
len <*an_Adj C*> = 1 by FINSEQ_1:40;
then t = [non_op C, the carrier of C]-tree<*a*> by A14,A15,A16,Def30;
then t.{} = [non_op C, the carrier of C] by TREES_4:def 4;
hence thesis by A10,A11;
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
A17: t = (ast C)term(a,q);
A18: the_arity_of ast C = <*an_Adj C,a_Type C*> by Def9;
A19: <*an_Adj C,a_Type C*>.1 = an_Adj C;
A20: <*an_Adj C,a_Type C*>.2 = a_Type C;
len <*an_Adj C,a_Type C*> = 2 by FINSEQ_1:44;
then t = [ast C, the carrier of C]-tree<*a,q*> by A17,A18,A19,A20,Def31;
then t.{} = [ast C, the carrier of C] by TREES_4:def 4;
hence thesis by A10,A11;
end;
end;
A21: 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
A22: 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
A23: t is expression of S;
per cases by A23,Th53;
suppose ex x being variable st t = x-term C;
hence thesis by A1;
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
A24: len q = len the_arity_of c and
A25: t = c-trm q;
t = [c, the carrier of C]-tree q by A24,A25,Def35;
then
A26: p = q by TREES_4:15;
now
let t be quasi-term of C;
t is Term of S,V by MSAFREE3:8;
hence t in rng q implies P[t] by A22,A26;
end;
hence thesis by A2,A24,A25;
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
A27: t = (non_op C)term a;
A28: the_arity_of non_op C = <*an_Adj C*> by Def9;
A29: <*an_Adj C*>.1 = an_Adj C;
len <*an_Adj C*> = 1 by FINSEQ_1:40;
then t = [non_op C, the carrier of C]-tree<*a*> by A27,A28,A29,Def30;
then
A30: p = <*a*> by TREES_4:15;
A31: rng <*a*> = {a} by FINSEQ_1:39;
A32: a in {a} by TARSKI:def 1;
a is Term of S,V by MSAFREE3:8;
hence thesis by A3,A22,A27,A30,A31,A32;
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
A33: t = (ast C)term(a,q);
A34: the_arity_of ast C = <*an_Adj C,a_Type C*> by Def9;
A35: <*an_Adj C,a_Type C*>.1 = an_Adj C;
A36: <*an_Adj C,a_Type C*>.2 = a_Type C;
len <*an_Adj C,a_Type C*> = 2 by FINSEQ_1:44;
then t = [ast C, the carrier of C]-tree<*a,q*> by A33,A34,A35,A36,Def31;
then
A37: p = <*a,q*> by TREES_4:15;
A38: rng <*a,q*> = {a,q} by FINSEQ_2:127;
A39: a in {a,q} by TARSKI:def 2;
A40: q in {a,q} by TARSKI:def 2;
A41: a is Term of S,V by MSAFREE3:8;
A42: q is Term of S,V by MSAFREE3:8;
P[a] by A22,A37,A38,A39,A41;
hence thesis by A4,A22,A33,A37,A38,A40,A42;
end;
end;
for t being Term of S,V holds Q[t] from MSATERM:sch 1(A6,A21);
hence thesis by A5;
end;
definition
let S be ManySortedSign;
attr S is with_an_operation_for_each_sort means
:
Def54: 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
X"{{}} c= rng the ResultSort of S;
end;
theorem Th114:
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;
A1: dom X = the carrier of S by PARTFUN1:def 2;
hereby
assume X is with_missing_variables;
then
A2: X"{{}} c= rng the ResultSort of S;
let s be SortSymbol of S;
assume X.s = {};
then X.s in {{}} by TARSKI:def 1;
then s in X"{{}} by A1,FUNCT_1:def 7;
then consider o being object such that
A3: o in the carrier' of S and
A4: (the ResultSort of S).o = s by A2,FUNCT_2:11;
reconsider o as OperSymbol of S by A3;
take o;
thus the_result_sort_of o = s by A4;
end;
assume
A5: 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 object;
assume
A6: x in X"{{}};
then
A7: X.x in {{}} by FUNCT_1:def 7;
reconsider x as SortSymbol of S by A1,A6,FUNCT_1:def 7;
X.x = {} by A7,TARSKI:def 1;
then ex o being OperSymbol of S st the_result_sort_of o = x by A5;
hence thesis by FUNCT_2:4;
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]];
A1: a_Type in {a_Type} by TARSKI:def 1;
A2: an_Adj in {an_Adj} by TARSKI:def 1;
A3: a_Term in {a_Term} by TARSKI:def 1;
A4: [<*> Vars, 0] in [:QuasiLoci, NAT:] by Th29,ZFMISC_1:def 2;
then
A5: m in Modes by A1,ZFMISC_1:def 2;
A6: a in Attrs by A2,A4,ZFMISC_1:def 2;
A7: f in Funcs by A3,A4,ZFMISC_1:def 2;
A8: m in Modes \/ Attrs by A5,XBOOLE_0:def 3;
A9: a in Modes \/ Attrs by A6,XBOOLE_0:def 3;
A10: m in Constructors by A8,XBOOLE_0:def 3;
A11: a in Constructors by A9,XBOOLE_0:def 3;
A12: f in Constructors by A7,XBOOLE_0:def 3;
the carrier' of MaxConstrSign = {*, non_op} \/ Constructors by Def24;
then reconsider m,a,f as OperSymbol of MaxConstrSign by A10,A11,A12,
XBOOLE_0:def 3;
A13: m is constructor;
A14: a is constructor;
A15: f is constructor;
A16: (the ResultSort of C).m = m`1 by A13,Def24;
A17: (the ResultSort of C).a = a`1 by A14,Def24;
A18: (the ResultSort of C).f = f`1 by A15,Def24;
A19: (the ResultSort of C).m = a_Type by A16;
A20: (the ResultSort of C).a = an_Adj by A17;
A21: (the ResultSort of C).f = a_Term by A18;
A22: the carrier of C = {a_Type, an_Adj, a_Term} by Def9;
let x be object;
assume x in the carrier of C;
then x = a_Type or x = an_Adj or x = a_Term by A22,ENUMSET1:def 1;
hence thesis by A19,A20,A21,FUNCT_2:4;
end;
let C be ConstructorSignature;
cluster MSVars C -> with_missing_variables;
coherence
proof
set X = MSVars C;
let x be object;
assume
A23: x in X"{{}};
then
A24: x in dom X by FUNCT_1:def 7;
A25: X.x in {{}} by A23,FUNCT_1:def 7;
x in the carrier of C by A24;
then x in {a_Type, an_Adj, a_Term} by Def9;
then
A26: x = a_Type or x = an_Adj or x = a_Term by ENUMSET1:def 1;
A27: X.x = {} by A25,TARSKI:def 1;
A28: (the ResultSort of C).(ast C) = a_Type by Def9;
(the ResultSort of C).(non_op C) = an_Adj by Def9;
hence thesis by A26,A27,A28,Def25,FUNCT_2:4;
end;
end;
registration
let S be ManySortedSign;
cluster non-empty -> with_missing_variables
for ManySortedSet of the carrier of S;
coherence
proof
let X be ManySortedSet of the carrier of S such that
A1: X is non-empty;
let x be object;
assume
A2: x in X"{{}};
then
A3: x in dom X by FUNCT_1:def 7;
A4: X.x in {{}} by A2,FUNCT_1:def 7;
A5: X.x in rng X by A3,FUNCT_1:def 3;
X.x = {} by A4,TARSKI:def 1;
hence thesis by A1,A5;
end;
end;
registration
let S be ManySortedSign;
cluster with_missing_variables for ManySortedSet of the carrier of S;
existence
proof
set A = the non-empty ManySortedSet of the carrier of S;
take A;
thus thesis;
end;
end;
registration
cluster initialized with_an_operation_for_each_sort
strict for ConstructorSignature;
existence
proof
take MaxConstrSign;
thus thesis;
end;
end;
registration
let C be with_an_operation_for_each_sort ManySortedSign;
cluster -> with_missing_variables for 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:132;
A2: dom X = the carrier of C by PARTFUN1:def 2;
the carrier of C c= rng the ResultSort of C by Def54;
hence X"{{}} c= rng the ResultSort of C by A1,A2;
end;
end;
definition
let G be non empty DTConstrStr;
redefine func Terminals G -> Subset of G; :: redefines Terminals (LANG1, definition)
coherence
proof
the carrier of G = Terminals G \/NonTerminals G by LANG1:1;
hence thesis by XBOOLE_1:7;
end;
redefine func NonTerminals G -> Subset of G; :: redefines NonTerminals (LANG1, definition)
coherence
proof
the carrier of G = Terminals G \/NonTerminals G by LANG1:1;
hence thesis by XBOOLE_1:7;
end;
end;
theorem Th115:
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
A1: the Rules of D1 c= the Rules of D2;
thus
A2: NonTerminals D1 c= NonTerminals D2
proof
let x be object;
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
A3: x = s and
A4: s ==> n;
A5: [s,n] in the Rules of D1 by A4;
then [s,n] in the Rules of D2 by A1;
then reconsider s9 = s as Symbol of D2 by ZFMISC_1:87;
s9 ==> n by A1,A5;
hence thesis by A3;
end;
hereby
let x be object;
assume
A6: x in (the carrier of D1) /\ Terminals D2;
then
A7: x in Terminals D2 by XBOOLE_0:def 4;
reconsider s9 = x as Symbol of D1 by A6,XBOOLE_0:def 4;
reconsider s = x as Symbol of D2 by A6;
assume not x in Terminals D1;
then consider n being FinSequence such that
A8: s9 ==> n;
[s9,n] in the Rules of D1 by A8;
then s ==> n by A1;
then not ex s being Symbol of D2 st x = s &
not ex n being FinSequence st s ==> n;
hence contradiction by A7;
end;
assume Terminals D1 c= Terminals D2;
then Terminals D1 \/ NonTerminals D1 c= Terminals D2 \/ NonTerminals D2
by A2,XBOOLE_1:13;
then Terminals D1 \/ NonTerminals D1 c= the carrier of D2 by LANG1:1;
hence thesis by LANG1:1;
end;
theorem Th116:
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,G9 be non empty DTConstrStr such that
A1: Terminals G c= Terminals G9 and
A2: the Rules of G c= the Rules of G9;
A3: the carrier of G9 = (Terminals G9) \/ NonTerminals G9 by LANG1:1;
A4: the carrier of G c= the carrier of G9 by A1,A2,Th115;
defpred P[set] means $1 in TS G9;
A5: for s being Symbol of G st s in Terminals G holds P[root-tree s]
proof
let s be Symbol of G;
assume
A6: s in Terminals G;
then reconsider s9 = s as Symbol of G9 by A1,A3,XBOOLE_0:def 3;
root-tree s = root-tree s9;
hence thesis by A1,A6,DTCONSTR:def 1;
end;
A7: 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
A8: [n, roots s] in the Rules of G and
A9: for t being DecoratedTree of the carrier of G st t in rng s holds P[t];
rng s c= TS G9
by A9;
then reconsider s9 = s as FinSequence of TS G9 by FINSEQ_1:def 4;
reconsider n9 = n as Symbol of G9 by A4;
n9 ==> roots s9 by A2,A8;
hence thesis by DTCONSTR:def 1;
end;
A10: for t being DecoratedTree of the carrier of G st t in TS(G) holds P[t]
from DTCONSTR:sch 7(A5,A7);
let x be object;
assume
A11: x in TS G;
then reconsider t = x as Element of FinTrees(the carrier of G);
P[t] by A10,A11;
hence thesis;
end;
theorem Th117:
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
A1: X c= Y and
A2: X"{{}} c= rng the ResultSort of S;
let x be object;
assume
A3: x in Y"{{}};
then
A4: x in dom Y by FUNCT_1:def 7;
A5: Y.x in {{}} by A3,FUNCT_1:def 7;
A6: dom X = the carrier of S by PARTFUN1:def 2;
A7: Y.x = {} by A5,TARSKI:def 1;
X.x c= Y.x by A1,A4;
then X.x = {} by A7;
then X.x in {{}} by TARSKI:def 1;
then x in X"{{}} by A4,A6,FUNCT_1:def 7;
hence thesis by A2;
end;
theorem Th118:
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
A1: X c= Y;
A2: dom Y = S by PARTFUN1:def 2;
let x be object;
assume
A3: x in Union coprod X;
then
A4: x`2 in dom X by CARD_3:22;
A5: x`1 in X.x`2 by A3,CARD_3:22;
A6: x = [x`1,x`2] by A3,CARD_3:22;
X.x`2 c= Y.x`2 by A1,A4;
hence thesis by A2,A4,A5,A6,CARD_3:22;
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 Th118,XBOOLE_1:9;
theorem Th120:
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 carrier' 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
A1: X is with_missing_variables;
set D = DTConMSA X,
A = [:the carrier' of S,{the carrier of S}:] \/
Union (coprod (X qua ManySortedSet of the carrier of S));
A2: Union(coprod X) misses [:the carrier' of S,{the carrier of S}:]
by MSAFREE:4;
A3: (Terminals D) misses (NonTerminals D) by DTCONSTR:8;
thus
NonTerminals DTConMSA X c= [:the carrier' of S,{the carrier of S}:]
by MSAFREE:6;
thus
A4: [:the carrier' of S,{the carrier of S}:] c= NonTerminals D
proof
let o,x2 be object;
assume
A5: [o,x2] in [:the carrier' of S,{the carrier of S}:];
then
A6: x2 in {the carrier of S} by ZFMISC_1:87;
reconsider o as OperSymbol of S by A5,ZFMISC_1:87;
A7: the carrier of S = x2 by A6,TARSKI:def 1;
then reconsider xa = [o,the carrier of S]
as Element of (the carrier of D) by A5,XBOOLE_0:def 3;
set O = the_arity_of o;
defpred P[object,object] 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);
A8: for a be object st a in Seg len O ex b be object st P[a,b]
proof
let a be object;
assume a in Seg len O;
then
A9: a in dom O by FINSEQ_1:def 3;
then
A10: O.a in rng O by FUNCT_1:def 3;
then reconsider s = O.a as SortSymbol of S;
per cases;
suppose X.(O.a) is non empty;
then consider x be object such that
A11: x in X.(O.a) by XBOOLE_0:def 1;
take y = [x,O.a];
A12: y in coprod(O.a,X) by A10,A11,MSAFREE:def 2;
A13: O.a in rng O by A9,FUNCT_1:def 3;
dom coprod(X) = the carrier of S by PARTFUN1:def 2;
then (coprod(X)).(O.a) in rng coprod(X) by A13,FUNCT_1:def 3;
then coprod(O.a,X) in rng coprod(X) by A13,MSAFREE:def 3;
then y in Union coprod(X) by A12,TARSKI:def 4;
hence thesis by A10,A11,MSAFREE:def 2,XBOOLE_0:def 3;
end;
suppose
A14: X.(O.a) = {};
then consider o being OperSymbol of S such that
A15: the_result_sort_of o = s by A1,Th114;
take y = [o,the carrier of S];
the carrier of S in {the carrier of S} by TARSKI:def 1;
then y in [:the carrier' of S,{the carrier of S}:] by ZFMISC_1:87;
hence thesis by A14,A15,XBOOLE_0:def 3;
end;
end;
consider b be Function such that
A16: dom b = Seg len O &
for a be object st a in Seg len O holds P[a,b.a]
from CLASSES1:sch 1(A8);
reconsider b as FinSequence by A16,FINSEQ_1:def 2;
rng b c= A
proof
let a be object;
assume a in rng b;
then ex c being object st c in dom b & b.c = a by FUNCT_1:def 3;
hence thesis by A16;
end;
then reconsider b as FinSequence of A by FINSEQ_1:def 4;
reconsider b as Element of A* by FINSEQ_1:def 11;
A17: len b = len O by A16,FINSEQ_1:def 3;
now
let c be set;
assume
A18: c in dom b;
then
A19: P[c,b.c] by A16;
dom O = Seg len O by FINSEQ_1:def 3;
then
A20: O.c in rng O by A16,A18,FUNCT_1:def 3;
dom coprod(X) = the carrier of S by PARTFUN1:def 2;
then (coprod(X)).(O.c) in rng coprod(X) by A20,FUNCT_1:def 3;
then coprod(O.c,X) in rng coprod(X) by A20,MSAFREE:def 3;
then X.(O.c) <> {} implies b.c in Union coprod(X) by A19,TARSKI:def 4;
hence b.c in [:the carrier' 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 A2,A19,XBOOLE_0:3,XTUPLE_0:1;
assume
A21: b.c in Union (coprod X);
now
assume X.(O.c) = {};
then
A22: ex o being OperSymbol of S st ( b.c = [o,the carrier of S])
&( the_result_sort_of o = O.c) by A16,A18;
the carrier of S in {the carrier of S} by TARSKI:def 1;
then b.c in [:the carrier' of S,{the carrier of S}:]
by A22,ZFMISC_1:87;
hence contradiction by A2,A21,XBOOLE_0:3;
end;
hence b.c in coprod(O.c,X) by A16,A18;
end;
then [xa,b] in REL(X) by A17,MSAFREE:5;
then xa ==> b;
hence thesis by A7;
end;
thus Terminals D c= Union coprod X
proof
let x be object;
assume
A23: x in Terminals D;
then not x in [:the carrier' of S,{the carrier of S}:] by A3,A4,XBOOLE_0:3;
hence thesis by A23,XBOOLE_0:def 3;
end;
thus thesis 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
A1: X c= Y and
A2: X is with_missing_variables;
A3: Y is with_missing_variables by A1,A2,Th117;
set G = DTConMSA X, G9 = DTConMSA Y;
A4: the carrier of G c= the carrier of G9 by A1,Th118,XBOOLE_1:9;
A5: Terminals G = Union coprod X by A2,Th120;
A6: Terminals G9 = Union coprod Y by A3,Th120;
hence
Terminals G c= Terminals G9 by A1,A5,Th118;
A7: (the carrier of G)* c= (the carrier of G9)* by A4,FINSEQ_1:62;
thus the Rules of G c= the Rules of G9
proof
let a,b be object;
assume
A8: [a,b] in the Rules of G;
then
A9: a in [:the carrier' of S,{the carrier of S}:] by MSAFREE1:2;
reconsider a as Element of [:the carrier' of S,{the carrier of S}:]
\/ Union coprod X by A9,XBOOLE_0:def 3;
reconsider a9 = a as
Element of [:the carrier' of S,{the carrier of S}:]
\/ Union coprod Y by A9,XBOOLE_0:def 3;
reconsider b as Element of
([:the carrier' of S,{the carrier of S}:] \/ Union coprod X)* by A8,
MSAFREE1:2;
reconsider b9 = b as Element of
([:the carrier' of S,{the carrier of S}:] \/ Union coprod Y)*
by A7;
now
let o be OperSymbol of S;
assume
A10: [o,the carrier of S] = a9;
hence
A11: len b9 = len (the_arity_of o) by A8,MSAFREE:def 7;
let x be set;
assume
A12: x in dom b9;
hence b9.x in [:the carrier' 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 A8,A10,MSAFREE:def 7;
A13: Union coprod Y misses [:the carrier' of S,{the carrier of S}:] by
MSAFREE:4;
A14: b.x in [:the carrier' of S,{the carrier of S}:] \/ Union coprod X
by A12,DTCONSTR:2;
A15: dom b9 = Seg len b9 by FINSEQ_1:def 3;
dom the_arity_of o = Seg len b9 by A11,FINSEQ_1:def 3;
then
A16: (the_arity_of o).x in the carrier of S by A12,A15,DTCONSTR:2;
assume
A17: b9.x in Union coprod Y;
b.x in [:the carrier' of S,{the carrier of S}:] or b.x in Union coprod
X by A14,XBOOLE_0:def 3;
then b.x in coprod((the_arity_of o).x,X) by A8,A10,A12,A13,A17,
MSAFREE:def 7,XBOOLE_0:3;
then
A18: ex a being set st ( a in X.((the_arity_of o).x))&( b.x = [a
, (the_arity_of o).x]) by A16,MSAFREE:def 2;
X.((the_arity_of o).x) c= Y.((the_arity_of o).x) by A1,A16;
hence b9.x in coprod((the_arity_of o).x,Y) by A16,A18,MSAFREE:def 2;
end;
hence thesis by A9,MSAFREE:def 7;
end;
hence thesis by A1,A5,A6,Th116,Th118;
end;
theorem Th122:
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;
A1: Terminals DTConMSA X = Union coprod X by Th120;
A2: dom X = the carrier of C by PARTFUN1:def 2;
A3: the carrier of C = {a_Type, an_Adj, a_Term} by Def9;
A4: X.a_Type = {} by Def25;
A5: X.an_Adj = {} by Def25;
A6: X.a_Term = Vars by Def25;
hereby
assume
A7: t in Terminals DTConMSA X;
then
A8: t`2 in dom X by A1,CARD_3:22;
A9: t`1 in X.t`2 by A1,A7,CARD_3:22;
A10: t`2 = a_Type or t`2 = an_Adj or t`2 = a_Term by A3,A8,ENUMSET1:def 1;
reconsider x = t`1 as variable by A3,A4,A5,A6,A8,A9,ENUMSET1:def 1;
take x;
thus t = [x,a_Term C] by A1,A4,A5,A7,A10,CARD_3:22;
end;
given x being variable such that
A11: t = [x,a_Term C];
A12: t`1 = x by A11;
t`2 = a_Term by A11;
hence thesis by A1,A2,A6,A11,A12,CARD_3:22;
end;
theorem Th123:
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;
A1: NonTerminals DTConMSA X = [:the carrier' of C,{the carrier of C}:]
by Th120;
hereby
assume t in NonTerminals DTConMSA MSVars C;
then consider a,b being object such that
A2: a in the carrier' of C and
A3: b in {the carrier of C} and
A4: t = [a,b] by A1,ZFMISC_1:def 2;
reconsider a as OperSymbol of C by A2;
A5: b = the carrier of C by A3,TARSKI:def 1;
a is constructor or a is not constructor;
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 A4,A5;
end;
the carrier of C in {the carrier of C} by TARSKI:def 1;
hence thesis by A1,ZFMISC_1:87;
end;
theorem Th124:
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:24;
let t be set;
assume t in Union U;
then consider s being object such that
A2: s in dom U and
A3: t in U.s by CARD_5:2;
reconsider s as SortSymbol of S by A2;
U.s = {r where r is Term of S,V: the_sort_of r = s & variables_in r c= X}
by A1,MSAFREE3:def 5;
then
ex r being Term of S,V st t = r & the_sort_of r = s & variables_in r c= X
by A3;
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:24;
let t be Term of S, X (\/) ((the carrier of S)-->{0});
assume t in Union U;
then consider s being object such that
A2: s in dom U and
A3: t in U.s by CARD_5:2;
reconsider s as SortSymbol of S by A2;
U.s = {r where r is Term of S,V: the_sort_of r = s & variables_in r c= X}
by A1,MSAFREE3:def 5;
then
ex r being Term of S,V st t = r & the_sort_of r = s & variables_in r c= X
by A3;
hence thesis by A3;
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;
then p in (the carrier of G)* by ZFMISC_1:87;
hence thesis by FINSEQ_1:def 11;
end;
theorem Th127:
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 Y = the carrier of S by PARTFUN1:def 2;
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 that
A2: g1 = g2 and
A3: p1 = p2 and
A4: g1 ==> p1;
A5: [g1, p1] in REL X by A4;
then
A6: p1 in ([:the carrier' of S,{the carrier of S}:] \/ Union (coprod X))*
by ZFMISC_1:87;
then
A7: g1 in [:the carrier' of S,{the carrier of S}:] by A5,MSAFREE:def 7;
A8: p2 in ([:the carrier' of S, {the carrier of S}:] \/
Union (coprod Y))* by FINSEQ_1:def 11;
now
let o9 be OperSymbol of S;
assume
A9: [o9,the carrier of S] = g2;
hence
A10: len p2 = len the_arity_of o9 by A2,A3,A5,A6,MSAFREE:def 7;
let x be set;
assume
A11: x in dom p2;
hence p2.x in [:the carrier' 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 o9).x
by A2,A3,A5,A6,A9,MSAFREE:def 7;
x in dom the_arity_of o9 by A10,A11,FINSEQ_3:29;
then (the_arity_of o9).x in rng the_arity_of o9 by FUNCT_1:def 3;
then reconsider i = (the_arity_of o9).x as SortSymbol of S;
assume
A12: p2.x in Union coprod Y;
then
A13: (p2.x)`2 in dom Y by CARD_3:22;
A14: (p2.x)`1 in Y.(p2.x)`2 by A12,CARD_3:22;
A15: p2.x = [(p2.x)`1,(p2.x)`2] by A12,CARD_3:22;
reconsider nn = the carrier of S as set;
A: not nn in nn;
p2.x in rng p1 by A3,A11,FUNCT_1:def 3;
then the carrier of S nin the carrier of S &
p2.x in [:the carrier' of S,{the carrier of S}:] or
p2.x in Union coprod X by XBOOLE_0:def 3,A;
then p2.x in coprod(i,X)
by A1,A2,A3,A5,A6,A9,A11,A13,A15,MSAFREE:def 7,ZFMISC_1:106;
then ex a being set st ( a in X.i)&( p2.x = [a,i]) by MSAFREE:def 2;
then i = (p2.x)`2;
hence p2.x in coprod((the_arity_of o9).x,Y) by A14,A15,MSAFREE:def 2;
end;
then [g2, p2] in REL Y by A2,A7,A8,MSAFREE:def 7;
hence thesis;
end;
theorem Th128:
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:24;
A2: dom U = the carrier of S by PARTFUN1:def 2;
defpred P[set] means $1 in Union U implies $1 in TS G;
A3: 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 object such that
A4: s1 in dom U and
A5: root-tree [v,s] in U.s1 by CARD_5:2;
reconsider s1 as SortSymbol of S by A4;
U.s1={t where t is Term of S,V: the_sort_of t = s1 & variables_in t c= X}
by A1,MSAFREE3:def 5;
then consider t being Term of S,V such that
A6: root-tree [v,s] = t and the_sort_of t = s1 and
A7: variables_in t c= X by A5;
(variables_in t).s = {v} by A6,MSAFREE3:10;
then {v} c= X.s by A7;
then v in X.s by ZFMISC_1:31;
then [v,s] in Terminals G by MSAFREE:7;
hence thesis by DTCONSTR:def 1;
end;
A8: 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
A9: for t being Term of S,V st t in rng p holds P[t] and
A10: [o,the carrier of S]-tree p in Union U;
consider s being object such that
A11: s in dom U and
A12: [o,the carrier of S]-tree p in U.s by A10,CARD_5:2;
reconsider s as SortSymbol of S by A11;
U.s={t where t is Term of S,V: the_sort_of t = s & variables_in t c= X}
by A1,MSAFREE3:def 5;
then consider t being Term of S,V such that
A13: [o,the carrier of S]-tree p = t and
A14: the_sort_of t = s and variables_in t c= X by A12;
t.{} = [o,the carrier of S] by A13,TREES_4:def 4;
then the_result_sort_of o = s by A14,MSATERM:17;
then
A15: rng p c= Union U by A1,A12,MSAFREE3:19;
rng p c= TS G
proof
let x be object;
assume
A16: x in rng p;
then x is Term of S,V by A15,Th124;
hence thesis by A9,A15,A16;
end;
then reconsider q = p as FinSequence of TS G by FINSEQ_1:def 4;
NonTerminals G = [:the carrier' of S,{the carrier of S}:] by Th120;
then [o,the carrier of S] in NonTerminals G by ZFMISC_1:106;
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 Th127;
hence thesis by DTCONSTR:def 1;
end;
A17: for t being Term of S,V holds P[t] from MSATERM:sch 1(A3,A8);
A18: NonTerminals DTConMSA X = [:the carrier' of S,{the carrier of S}:] by
Th120;
A19: Terminals DTConMSA X = Union coprod X by Th120;
defpred Q[set] means $1 in Union U;
A20: for s being Symbol of G st s in Terminals G holds Q[root-tree s]
proof
let s be Symbol of G;
assume
A21: s in Terminals G;
then
A22: s`2 in dom X by A19,CARD_3:22;
A23: s`1 in X.s`2 by A19,A21,CARD_3:22;
A24: s = [s`1,s`2] by A19,A21,CARD_3:22;
A25: dom U = the carrier of S by PARTFUN1:def 2;
root-tree s in (the Sorts of Free(S,X)).s`2 by A22,A23,A24,MSAFREE3:4;
hence thesis by A22,A25,CARD_5:2;
end;
A26: 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
A27: nt ==> roots ts and
A28: for
t being DecoratedTree of the carrier of G st t in rng ts holds Q[t];
nt in NonTerminals G by A27;
then consider o,z being object such that
A29: o in the carrier' of S and
A30: z in {the carrier of S} and
A31: nt = [o,z] by A18,ZFMISC_1:def 2;
reconsider o as OperSymbol of S by A29;
A32: rng ts c= Union U
by A28;
rng ts c= TS DTConMSA V
proof
let a be object;
assume a in rng ts;
then
A33: a is Element of S-TermsV by A32,Th124;
S-TermsV = TS DTConMSA V by MSATERM:def 1;
hence thesis by A33;
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;
A34: z = the carrier of S by A30,TARSKI:def 1;
then Sym(o, V) ==> roots p by A27,A31,Th127;
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,A32,MSAFREE3:19;
hence thesis by A2,A31,A34,CARD_5:2;
end;
A35: for t being DecoratedTree of the carrier of G
st t in TS G holds Q[t] from DTCONSTR:sch 7(A20,A26);
thus Union U c= TS DTConMSA X
proof
let x be object;
assume
A36: x in Union U;
then consider s being object such that
A37: s in dom U and
A38: x in U.s by CARD_5:2;
reconsider s as SortSymbol of S by A37;
x in U.s by A38;
then x is Term of S,V by A1,MSAFREE3:16;
hence thesis by A17,A36;
end;
let x be object;
assume
A39: 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 A39;
hence thesis by A35;
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
:Def56:
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);
A1: dom f = Union the Sorts of Free(S,X);
rng f = Union the Sorts of Free(S,X);
then reconsider f as UnOp of Union the Sorts of Free(S,X) by A1,FUNCT_2:2;
take f;
thus thesis by Th4;
end;
end;
theorem Th129:
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;
A1: dom the Sorts of Free(S,X) = the carrier of S by PARTFUN1:def 2;
let f be UnOp of Union the Sorts of Free(S,X);
A2: dom f = Union the Sorts of Free(S,X) by FUNCT_2:52;
hereby
assume
A3: f is term-transformation of S,X;
let s be SortSymbol of S;
A4: f.:((the Sorts of Free(S,X)).s) c= (the Sorts of Free(S,X)).s by A3,Def56;
(the Sorts of Free(S,X)).s in rng the Sorts of Free(S,X)
by A1,FUNCT_1:def 3;
then
A5: (the Sorts of Free(S,X)).s c= Union the Sorts of Free(S,X) by ZFMISC_1:74;
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 A2,A5,FUNCT_1:def 6;
hence f.a in (the Sorts of Free(S,X)).s by A4;
end;
assume
A6: 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 object;
assume x in f.:((the Sorts of Free(S,X)).s);
then
ex a being object
st a in dom f & a in (the Sorts of Free(S,X)).s & x = f.a
by FUNCT_1:def 6;
hence thesis by A6;
end;
theorem Th130:
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) = 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;
A1: Union the Sorts of A = {} or Union the Sorts of A <> {};
A2: dom the Sorts of A = the carrier of S by PARTFUN1:def 2;
A3: dom f = Union the Sorts of A by A1,FUNCT_2:def 1;
(the Sorts of A).s in rng the Sorts of A by A2,FUNCT_1:def 3;
then (the Sorts of A).s c= Union the Sorts of A by ZFMISC_1:74;
then rng p c= dom f by A3;
then
A4: dom (f*p) = dom p by RELAT_1:27;
dom p = Seg len p by FINSEQ_1:def 3;
then
A5: f*p is FinSequence by A4,FINSEQ_1:def 2;
A6: rng(f*p) c= (the Sorts of A).s
proof
let z be object;
assume z in rng(f*p);
then consider i being object such that
A7: i in dom(f*p) and
A8: z = (f*p).i by FUNCT_1:def 3;
p.i in rng p by A4,A7,FUNCT_1:def 3;
then f.(p.i) in (the Sorts of A).s by Th129;
hence thesis by A7,A8,FUNCT_1:12;
end;
hence f*p is FinSequence of (the Sorts of Free(S,X)).s by A5,FINSEQ_1:def 4;
reconsider q = f*p as FinSequence of (the Sorts of A).s by A5,A6,
FINSEQ_1:def 4;
thus card(f*p) = len q .= len p by A4,FINSEQ_3:29;
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
A5: for t being Symbol of G st t in Terminals G
holds f.(root-tree t) = TermVal(t) and
A6: 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;
D = TS G by Th128;
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 object;
assume x in f.:((the Sorts of A).s);
then consider a being Element of D such that
A7: a in (the Sorts of A).s and
A8: x = f.a by FUNCT_2:65;
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;
A9: 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
A10: a in (the Sorts of A).s;
A11: [y,a_Term C()] in Terminals G by Th122;
then reconsider t = [y,a_Term C()] as Symbol of G;
f.a = TermVal(t) by A5,A11
.= V(y);
then
A12: f.a is quasi-term of C() by A1;
a is expression of C(), s by A10,Def28;
then s = a_Term C() by Th48;
hence thesis by A12,Def28;
end;
A13: 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
A14: len p = len the_arity_of c and
A15: 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
A16: a in (the Sorts of A).s;
nt in NonTerminals G by Th123;
then reconsider nt as Symbol of G;
reconsider ts = p as FinSequence of TS G by Th128;
A17: a = nt-tree ts by A14,Def35;
reconsider aa = a as Term of C(), X by MSAFREE3:8;
the Sorts of A = C()-Terms(V,X) by MSAFREE3:24;
then the Sorts of A c= the Sorts of FreeMSA X by PBOOLE:def 18;
then (the Sorts of A).s c= (the Sorts of FreeMSA X).s;
then aa in (FreeSort X).s by A16;
then aa in FreeSort(X,s) by MSAFREE:def 11;
then
A18: the_sort_of aa = s by MSATERM:def 5;
A19: c <> * by Def11;
A20: c <> non_op by Def11;
A21: rng p c= QuasiTerms C() by FINSEQ_1:def 4;
dom f = D by FUNCT_2:def 1;
then
A22: rng p c= dom f;
rng(f*p) c= QuasiTerms C()
proof
let z be object;
assume z in rng(f*p);
then consider i being object such that
A23: i in dom(f*p) and
A24: z = (f*p).i by FUNCT_1:def 3;
i in dom p by A22,A23,RELAT_1:27;
then
A25: p.i in rng p by FUNCT_1:def 3;
then reconsider pi1 = p.i as quasi-term of C() by A21,Th41;
pi1 in (the Sorts of A).a_Term C() by Th41;
then f.pi1 in (the Sorts of A).a_Term C() by A15,A25;
hence thesis by A23,A24,FUNCT_1:12;
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 object;
assume z in rng p;
then z is Element of C()-TermsX by MSAFREE3:8;
hence thesis;
end;
then reconsider r = p as FinSequence of C()-Terms X by FINSEQ_1:def 4;
A26: len q = len p by A22,FINSEQ_2:29;
a is Term of C(), X by MSAFREE3:8;
then
A27: r is ArgumentSeq of Sym(c, X) by A17,MSATERM:1;
then
A28: the_result_sort_of c = s by A17,A18,MSATERM:20;
Sym(c, X) ==> roots r by A27,MSATERM:21;
then nt ==> roots ts by Th127;
then f.a = NTermVal(nt, roots ts, f * ts) by A6,A17
.= IFEQ(c,non_op, N((f * ts).1), F(c, f * ts)) by A19,
FUNCOP_1:def 8
.= F(c, f * ts) by A20,FUNCOP_1:def 8;
then f.a is expression of C(), the_result_sort_of c by A2,A14,A26;
hence thesis by A28,Def28;
end;
A29: 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
A30: P[v];
A31: v in U.an_Adj C() by Def28;
then f.v in U.an_Adj C() by A30;
then reconsider fv = f.v as expression of C(), an_Adj C() by Def28;
let s be SortSymbol of C();
assume
A32: (non_op C())term v in U.s;
A33: (non_op C())term v is expression of C(), an_Adj C() by Th43;
(non_op C())term v is expression of C(), s by A32,Def28;
then
A34: s = an_Adj C() by A33,Th48;
set QA = U.an_Adj C();
rng <*v*> = {v} by FINSEQ_1:38;
then rng <*v*> c= QA by A31,ZFMISC_1:31;
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 Th123;
then reconsider nt as Symbol of G;
reconsider ts = p as FinSequence of TS G by Th128;
A35: a = nt-tree ts by Th43;
dom f = D by FUNCT_2:def 1;
then
A36: f*p = <*fv*> by FINSEQ_2:34;
rng p c= C()-Terms X
proof
let z be object;
assume z in rng p;
then z is expression of C(), an_Adj C() by Th41;
then z is Element of C()-TermsX by MSAFREE3:8;
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:8;
then r is ArgumentSeq of Sym(c, X) by A35,MSATERM:1;
then Sym(c, X) ==> roots r by MSATERM:21;
then nt ==> roots ts by Th127;
then f.a = NTermVal(nt, roots ts, f * ts) by A6,A35
.= IFEQ(c,non_op, N((f * ts).1), F(c, f * ts)) by FUNCOP_1:def 8
.= N((f*ts).1) by FUNCOP_1:def 8
.= N(fv) by A36;
then f.a is expression of C(), an_Adj C() by A3;
hence thesis by A34,Def28;
end;
A37: 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
A38: P[v];
let t be expression of C(), a_Type C() such that
A39: P[t];
A40: v in U.an_Adj C() by Def28;
A41: t in U.a_Type C() by Def28;
A42: f.v in U.an_Adj C() by A38,A40;
A43: f.t in U.a_Type C() by A39,A41;
reconsider fv = f.v as expression of C(), an_Adj C() by A42,Def28;
reconsider ft = f.t as expression of C(), a_Type C() by A43,Def28;
let s be SortSymbol of C();
assume
A44: (ast C())term(v,t) in U.s;
A45: (ast C())term(v,t) is expression of C(), a_Type C() by Th46;
(ast C())term(v,t) is expression of C(), s by A44,Def28;
then
A46: s = a_Type C() by A45,Th48;
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 Th123;
then reconsider nt as Symbol of G;
reconsider ts = p as FinSequence of TS G by Th128;
A47: a = nt-tree ts by Th46;
A48: f*p = <*fv,ft*> by FINSEQ_2:36;
rng p c= C()-Terms X
proof
let z be object;
assume z in rng p;
then z is Element of C()-TermsX by MSAFREE3:8;
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:8;
then r is ArgumentSeq of Sym(c, X) by A47,MSATERM:1;
then Sym(c, X) ==> roots r by MSATERM:21;
then nt ==> roots ts by Th127;
then f.a = NTermVal(nt, roots ts, f * ts) by A6,A47
.= A((f*ts).1,(f*ts).2) by FUNCOP_1:def 8
.= A(fv,(f*ts).2) by A48
.= A(fv,ft) by A48;
then f.a is expression of C(), a_Type C() by A4;
hence thesis by A46,Def28;
end;
P[a] from StructInd(A9,A13,A29,A37);
hence thesis by A7,A8;
end;
then reconsider f as term-transformation of C(), MSVars C();
take f;
hereby
let x be variable;
x in Vars;
then
A49: x in V.a_Term C() by Def25;
reconsider x9 = x as Element of V.a_Term C() by Def25;
reconsider xx = [x9,a_Term C()] as Symbol of G by A49,MSAFREE3:2;
xx in Terminals G by A49,MSAFREE:7;
hence f.(x-term C()) = V(xx`1) by A5
.= V(x);
end;
hereby
let c be constructor OperSymbol of C();
let p,q be FinSequence of QuasiTerms C();
assume that
A50: len p = len the_arity_of c and
A51: q = f*p;
set a = c-trm p;
set nt = [c, the carrier of C()];
nt in NonTerminals G by Th123;
then reconsider nt as Symbol of G;
reconsider ts = p as FinSequence of TS G by Th128;
A52: a = nt-tree ts by A50,Def35;
A53: c <> * by Def11;
A54: c <> non_op by Def11;
rng p c= C()-Terms X
proof
let z be object;
assume z in rng p;
then z is Element of C()-TermsX by MSAFREE3:8;
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:8;
then r is ArgumentSeq of Sym(c, X) by A52,MSATERM:1;
then Sym(c, X) ==> roots r by MSATERM:21;
then nt ==> roots ts by Th127;
then f.a = NTermVal(nt, roots ts, f * ts) by A6,A52
.= IFEQ(c,non_op, N((f * ts).1), F(c, f * ts)) by A53,FUNCOP_1:def 8
.= F(c, f * ts) by A54,FUNCOP_1:def 8;
hence f.(c-trm p) = F(c, q) by A51;
end;
hereby
let v be expression of C(), an_Adj C();
A55: v in U.an_Adj C() by Def28;
then f.v in U.an_Adj C() by Th129;
then reconsider fv = f.v as expression of C(), an_Adj C() by Def28;
set QA = U.an_Adj C();
rng <*v*> = {v} by FINSEQ_1:38;
then rng <*v*> c= QA by A55,ZFMISC_1:31;
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 Th123;
then reconsider nt as Symbol of G;
reconsider ts = p as FinSequence of TS G by Th128;
A56: a = nt-tree ts by Th43;
dom f = D by FUNCT_2:def 1;
then
A57: f*p = <*fv*> by FINSEQ_2:34;
rng p c= C()-Terms X
proof
let z be object;
assume z in rng p;
then z is expression of C(), an_Adj C() by Th41;
then z is Element of C()-TermsX by MSAFREE3:8;
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:8;
then r is ArgumentSeq of Sym(c, X) by A56,MSATERM:1;
then Sym(c, X) ==> roots r by MSATERM:21;
then nt ==> roots ts by Th127;
then f.a = NTermVal(nt, roots ts, f * ts) by A6,A56
.= IFEQ(c,non_op, N((f * ts).1), F(c, f * ts)) by FUNCOP_1:def 8
.= N((f*ts).1) by FUNCOP_1:def 8;
hence f.((non_op C())term v) = N(f.v) by A57;
end;
let v be expression of C(), an_Adj C();
let t be expression of C(), a_Type C();
A58: v in U.an_Adj C() by Def28;
A59: t in U.a_Type C() by Def28;
A60: f.v in U.an_Adj C() by A58,Th129;
A61: f.t in U.a_Type C() by A59,Th129;
reconsider fv = f.v as expression of C(), an_Adj C() by A60,Def28;
reconsider ft = f.t as expression of C(), a_Type C() by A61,Def28;
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 Th123;
then reconsider nt as Symbol of G;
reconsider ts = p as FinSequence of TS G by Th128;
A62: a = nt-tree ts by Th46;
A63: f*p = <*fv,ft*> by FINSEQ_2:36;
rng p c= C()-Terms X
proof
let z be object;
assume z in rng p;
then z is Element of C()-TermsX by MSAFREE3:8;
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:8;
then r is ArgumentSeq of Sym(c, X) by A62,MSATERM:1;
then Sym(c, X) ==> roots r by MSATERM:21;
then nt ==> roots ts by Th127;
then f.a = NTermVal(nt, roots ts, f * ts) by A6,A62
.= A((f*ts).1,(f*ts).2) by FUNCOP_1:def 8
.= A(fv,(f*ts).2) by A63;
hence thesis by A63;
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; :: redefines IFIN (MATRIX_7, definition)
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
:
Def58: 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 C be initialized ConstructorSignature;
cluster empty -> irrelevant for valuation of C;
coherence;
end;
registration
let C be initialized ConstructorSignature;
cluster empty for valuation of C;
existence
proof
take {}(Vars, QuasiTerms C);
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;
A1: now
let x be variable;
reconsider t = x-term C as Element of QuasiTerms C by Def28;
take t;
thus P[x,t];
end;
consider g being Function of Vars, QuasiTerms C such that
A2: for x being variable holds P[x,g.x] from FUNCT_2:sch 3(A1);
f c= g
proof
let a be object;
assume a in f;
then consider x being variable such that
A3: a = [x, x-term C] and x in X;
A4: g.x = x-term C by A2;
dom g = Vars by FUNCT_2:def 1;
hence thesis by A3,A4,FUNCT_1:1;
end;
hence thesis by RELSET_1:1;
end;
end;
theorem Th131:
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 object;
assume a in dom f;
then [a,f.a] in f by FUNCT_1:def 2;
then ex x being variable st [a,f.a] = [x,x-term C] & x in X;
hence thesis by XTUPLE_0:1;
end;
hereby
let x be object;
assume
A1: x in X;
then reconsider a = x as variable;
[a,a-term C] in f by A1;
hence x in dom f by FUNCT_1:1;
end;
let x be variable;
assume x in X;
then [x,x-term C] in C idval X;
hence thesis by FUNCT_1:1;
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 Th131;
hereby
let x be variable;
assume
A2: x in dom f;
take y = x;
thus f.x = y-term C by A1,A2,Th131;
end;
let x,y be object;
assume that
A3: x in dom f and
A4: y in dom f;
reconsider x,y as variable by A3,A4;
A5: f.x = x-term C by A1,A3,Th131;
f.y = y-term C by A1,A4,Th131;
hence thesis by A5,Th50;
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 Th131;
hence thesis;
end;
end;
definition
let C;
let f be valuation of C;
func f# -> term-transformation of C, MSVars C means
:
Def60: (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;
f/.x is quasi-term of C by Th41;
hence thesis 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 Th52;
A3: for a holds N(a) is expression of C, an_Adj C by Th43;
A4: for a,t holds A(a,t) is expression of C, a_Type C by Th46;
consider f9 being term-transformation of C, MSVars C such that
A5: (for x being variable holds f9.(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 = f9*p
holds f9.(c-trm p) = F(c, q)) &
(for a holds f9.((non_op C)term a) = N(f9.a)) &
for a,t holds f9.((ast C)term(a,t)) = A(f9.a, f9.t)
from StructDef(A1,A2,A3,A4);
take f9;
hereby
let x be variable;
A6: f9.(x-term C) = V(x) by A5;
x in dom f implies f/.x = f.x by PARTFUN1:def 6;
hence x in dom f implies f9.(x-term C) = f.x by A6,MATRIX_7:def 1;
thus not x in dom f implies f9.(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
A7: 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) and
A8: 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 and
A9: for a being expression of C, an_Adj C holds f1.((non_op C)term a)
= (non_op C)term (f1.a) and
A10: 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
A11: 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) and
A12: 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 and
A13: for a being expression of C, an_Adj C holds f2.((non_op C)term a)
= (non_op C)term (f2.a) and
A14: 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);
A15: dom f1 = D by FUNCT_2:def 1;
A16: dom f2 = D by FUNCT_2:def 1;
defpred P[expression of C] means f1.$1 = f2.$1;
A17: for x being variable holds P[x-term C]
proof
let x be variable;
x in dom f & f1.(x-term C) = f.x or
x nin dom f & f1.(x-term C) = x-term C by A7;
hence thesis by A11;
end;
A18: 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
A19: len p = len the_arity_of c and
A20: for t being quasi-term of C st t in rng p holds P[t];
A21: rng p c= QuasiTerms C by FINSEQ_1:def 4;
A22: rng(f1*p) = f1.:rng p by RELAT_1:127;
A23: rng(f2*p) = f2.:rng p by RELAT_1:127;
A24: rng(f1*p) c= f1.:QuasiTerms C by A21,A22,RELAT_1:123;
A25: rng(f2*p) c= f2.:QuasiTerms C by A21,A23,RELAT_1:123;
A26: f1.:QuasiTerms C c= QuasiTerms C by Def56;
A27: f2.:QuasiTerms C c= QuasiTerms C by Def56;
A28: rng(f1*p) c= QuasiTerms C by A24,A26;
rng(f2*p) c= QuasiTerms C by A25,A27;
then reconsider q1 = f1*p, q2 = f2*p as FinSequence of QuasiTerms C
by A28,FINSEQ_1:def 4;
A29: rng p c= D;
then
A30: dom q1 = dom p by A15,RELAT_1:27;
A31: dom q2 = dom p by A16,A29,RELAT_1:27;
now
let i be Nat;
assume
A32: i in dom p;
then
A33: q1.i = f1.(p.i) by FUNCT_1:13;
A34: q2.i = f2.(p.i) by A32,FUNCT_1:13;
A35: p.i in rng p by A32,FUNCT_1:def 3;
then p.i is quasi-term of C by A21,Th41;
hence q1.i = q2.i by A20,A33,A34,A35;
end;
then f1.(c-trm p) = c-trm q2 by A8,A19,A30,A31,FINSEQ_1:13;
hence thesis by A12,A19;
end;
A36: 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 A9;
hence thesis by A13;
end;
A37: 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
A38: 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 A10,A38;
hence thesis by A14;
end;
now
let t be expression of C;
thus P[t] from StructInd(A17,A18,A36,A37);
end;
hence thesis by FUNCT_2:63;
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
A1: [o, the carrier of C]-tree p in Union the Sorts of Free(C, MSVars C) and
A2: q = f# *p;
A3: 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 A1;
A4: t.{} = [o, the carrier of C] by TREES_4:def 4;
per cases;
suppose o is constructor;
then reconsider c = o as constructor OperSymbol of C;
A5: t = [c, the carrier of C]-tree p;
then
A6: len p = len the_arity_of c by Th51;
p in (QuasiTerms C)* by A5,Th51;
then reconsider p9 = p as FinSequence of QuasiTerms C by FINSEQ_1:def 11;
reconsider q9 = f# *p9 as FinSequence of QuasiTerms C by Th130;
A7: len q9 = len p by Th130;
thus f# .([o, the carrier of C]-tree p) = f# .(c-trm p9) by A6,Def35
.= c-trm q9 by A6,Def60
.= [o, the carrier of C]-tree q by A2,A6,A7,Def35;
end;
suppose
A8: o = *;
then consider a being expression of C, an_Adj C,
s being expression of C, a_Type C such that
A9: t = (ast C)term(a,s) by A4,Th58;
a in (the Sorts of Free(C, MSVars C)).an_Adj C by Def28;
then f#.a in (the Sorts of Free(C, MSVars C)).an_Adj C by Th129;
then reconsider fa = f#.a as expression of C, an_Adj C by Th41;
s in (the Sorts of Free(C, MSVars C)).a_Type C by Def28;
then f#.s in (the Sorts of Free(C, MSVars C)).a_Type C by Th129;
then reconsider fs = f#.s as expression of C, a_Type C by Th41;
t = [ast C, the carrier of C]-tree <*a,s*> by A9,Th46;
then p = <*a,s*> by TREES_4:15;
then q = <*fa, fs*> by A2,A3,FINSEQ_2:125;
then [o, the carrier of C]-tree q = (ast C)term(fa, fs) by A8,Th46;
hence thesis by A9,Def60;
end;
suppose
A10: o = non_op;
then consider a such that
A11: t = (non_op C)term a by A4,Th57;
a in (the Sorts of Free(C, MSVars C)).an_Adj C by Def28;
then f#.a in (the Sorts of Free(C, MSVars C)).an_Adj C by Th129;
then reconsider fa = f#.a as expression of C, an_Adj C by Th41;
t = [non_op C, the carrier of C]-tree <*a*> by A11,Th43;
then p = <*a*> by TREES_4:15;
then q = <*fa*> by A2,A3,FINSEQ_2:34;
then [o, the carrier of C]-tree q = (non_op C)term fa by A10,Th43;
hence thesis by A11,Def60;
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
A1: rng p c= Union the Sorts of Free(C, MSVars C);
func p at f -> FinSequence equals
:
Def62: f# * p;
coherence
proof
set A = Free(C, MSVars C);
dom (f# ) = Union the Sorts of A by FUNCT_2:def 1;
then
A2: dom (f# *p) = dom p by A1,RELAT_1:27;
dom p = Seg len p by FINSEQ_1:def 3;
hence thesis by A2,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 :: redefines at (ABCMIZ_1, definition)
f# * p;
coherence
proof
A1: f# *p is FinSequence of QuasiTerms C by Th130;
rng p c= Union the Sorts of Free(C, MSVars C);
hence thesis by A1,Def62;
end;
compatibility
proof
rng p c= Union the Sorts of Free(C, MSVars C);
hence thesis by Def62;
end;
end;
reserve x for variable;
theorem
not x in dom f implies (x-term C)at f = x-term C by Def60;
theorem
x in dom f implies (x-term C)at f = f.x by Def60;
theorem
len p = len the_arity_of c implies (c-trm p)at f = c-trm p at f by Def60;
theorem
((non_op C)term a)at f = (non_op C)term(a at f) by Def60;
theorem
((ast C)term(a,t))at f = (ast C)term(a at f,t at f) by Def60;
theorem Th137:
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;
A1: for x being variable holds P[x-term C]
proof
let x be variable;
A2: x in X or x nin X;
A3: dom f = X by Th131;
x in X implies f.x = x-term C by Th131;
hence thesis by A2,A3,Def60;
end;
A4: 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
A5: len p = len the_arity_of c and
A6: for t being quasi-term of C st t in rng p holds P[t];
len (p at f) = len p by Th130;
then
A7: dom (p at f) = dom p by FINSEQ_3:29;
now
let i be Nat;
assume
A8: i in dom p;
then
A9: p.i in rng p by FUNCT_1:def 3;
rng p c= QuasiTerms C by FINSEQ_1:def 4;
then reconsider pi1 = p.i as quasi-term of C by A9,Th41;
(p at f).i = pi1 at f by A8,FUNCT_1:13;
hence (p at f).i = p.i by A6,A9;
end;
then p at f = p by A7;
hence thesis by A5,Def60;
end;
A10: for a being expression of C, an_Adj C st P[a]
holds P[(non_op C)term a] by Def60;
A11: 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 Def60;
thus P[t] from StructInd(A1,A4,A10,A11);
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;
A1: dom (f# ) = Union the Sorts of Free(C, MSVars C) by FUNCT_2:def 1;
now
let x be object;
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 Th137;
end;
hence thesis by A1,FUNCT_1:17;
end;
theorem Th139:
for f being empty valuation of C holds e at f = e
proof
let f be empty valuation of C;
f = C idval {}Vars;
hence thesis by Th137;
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;
A1: dom (f# ) = Union the Sorts of Free(C, MSVars C) by FUNCT_2:def 1;
now
let x be object;
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 Th139;
end;
hence thesis by A1,FUNCT_1:17;
end;
definition
let C,f;
let t be quasi-term of C;
redefine func t at f -> quasi-term of C; :: redefines at (ABCMIZ_1, definition)
coherence
proof
t in QuasiTerms C by Def28;
then t at f in QuasiTerms C by Th129;
hence thesis by Th41;
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; :: redefines at (ABCMIZ_1, definition)
coherence
proof
a in (the Sorts of Free(C, MSVars C)).an_Adj C by Def28;
then a at f in (the Sorts of Free(C, MSVars C)).an_Adj C by Th129;
hence thesis by Th41;
end;
end;
registration
let C,f;
let a be positive expression of C, an_Adj C;
cluster a at f -> positive for expression of C, an_Adj C;
coherence
proof consider v being constructor OperSymbol of C such that
A1: the_result_sort_of v = an_Adj C and
A2: ex p being FinSequence of QuasiTerms C st
len p = len the_arity_of v & a = v-trm p by Th65;
consider p being FinSequence of QuasiTerms C such that
A3: len p = len the_arity_of v and
A4: a = v-trm p by A2;
A5: len (p at f) = len p by Th130;
a at f = v-trm(p at f) by A3,A4,Def60;
hence thesis by A1,A3,A5,Th66;
end;
end;
registration
let C,f;
let a be negative expression of C, an_Adj C;
cluster a at f -> negative for expression of C, an_Adj C;
coherence
proof
(non_op C)term (Non a) = a by Th62;
then a at f = (non_op C)term((Non a)at f) by Def60
.= Non ((Non a)at f) by Th59;
hence thesis;
end;
end;
definition
let C,f;
let a be quasi-adjective of C;
redefine func a at f -> quasi-adjective of C; :: redefines at (ABCMIZ_1, definition)
coherence
proof
per cases;
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;
thus (Non a) at f = ((non_op C)term b) at f by Th59
.= (non_op C)term af by Def60
.= Non (a at f) by Th59;
end;
suppose a is non positive;
then consider b being expression of C, an_Adj C such that
A1: a = (non_op C)term b and
A2: Non a = b by Th60;
A3: a at f = (non_op C)term(b at f) by A1,Def60;
then a at f is non 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 Th60;
hence thesis by A2,A3,Th44;
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; :: redefines at (ABCMIZ_1, definition)
coherence
proof
t in (the Sorts of Free(C, MSVars C)).a_Type C by Def28;
then t at f in (the Sorts of Free(C, MSVars C)).a_Type C by Th129;
hence thesis by Th41;
end;
end;
registration
let C,f;
let t be pure expression of C, a_Type C;
cluster t at f -> pure for expression of C, a_Type C;
coherence
proof consider m being constructor OperSymbol of C such that
A1: the_result_sort_of m = a_Type C and
A2: ex p being FinSequence of QuasiTerms C st
len p = len the_arity_of m & t = m-trm p by Th74;
consider p being FinSequence of QuasiTerms C such that
A3: len p = len the_arity_of m and
A4: t = m-trm p by A2;
A5: len (p at f) = len p by Th130;
t at f = m-trm(p at f) by A3,A4,Def60;
hence thesis by A1,A3,A5,Th75;
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[object,object] means
ex x being set st x in dom f & f.x = root-tree [ $1, a_Term] &
$2 = root-tree [x, a_Term];
A1: for x being object st x in Y ex y being object st P[x,y]
proof
let x be object;
assume x in Y;
then
A2: ex z being variable st x = z & z-term C in rng f;
then reconsider z = x as variable;
consider y being object such that
A3: y in dom f and
A4: z-term C = f.y by A2,FUNCT_1:def 3;
reconsider y as variable by A3;
take y-term C;
thus thesis by A3,A4;
end;
consider g being Function such that
A5: dom g = Y and
A6: for y being object st y in Y holds P[y,g.y]
from CLASSES1:sch 1(A1);
A7: Y c= Vars
proof
let x be object;
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 object;
assume y in rng g;
then consider x being object such that
A8: x in dom g and
A9: y = g.x by FUNCT_1:def 3;
reconsider x as variable by A5,A7,A8;
consider z being set such that
A10: z in dom f and f.z = x-term C and
A11: g.x = root-tree [z,a_Term] by A5,A6,A8;
reconsider z as variable by A10;
y = z-term C by A9,A11;
hence thesis by Def28;
end;
then reconsider g as valuation of C by A5,A7,RELSET_1:4;
A12: g is irrelevant
proof
let x be variable;
assume x in dom g;
then consider y being set such that
A13: y in dom f and f.y = x-term C and
A14: g.x = root-tree [y,a_Term] by A5,A6;
reconsider y as variable by A13;
take y;
thus thesis by A14;
end;
g is one-to-one
proof
let z1,z2 be object;
assume that
A15: z1 in dom g and
A16: z2 in dom g and
A17: g.z1 = g.z2;
reconsider z1,z2 as variable by A15,A16;
consider x1 being set such that
A18: x1 in dom f and
A19: f.x1 = z1-term C and
A20: g.z1 = root-tree[x1,a_Term] by A5,A6,A15;
consider x2 being set such that
A21: x2 in dom f and
A22: f.x2 = z2-term C and
A23: g.z1 = root-tree[x2,a_Term] by A5,A6,A16,A17;
reconsider x1,x2 as variable by A18,A21;
x1-term C = x2-term C by A20,A23;
then x1 = x2 by Th50;
hence thesis by A19,A22,Th50;
end;
then reconsider g as irrelevant one-to-one valuation of C by A12;
take g;
let x,y be variable;
hereby
assume that
A24: x in dom f and
A25: f.x = y-term C;
f.x in rng f by A24,FUNCT_1:def 3;
hence y in dom g by A5,A25;
then P[y,g.y] by A5,A6;
hence g.y = x-term C by A24,A25,FUNCT_1:def 4;
end;
assume that
A26: y in dom g and
A27: g.y = x-term C;
consider z being set such that
A28: z in dom f and
A29: f.z = root-tree [y, a_Term] and
A30: x-term C = root-tree [z, a_Term] by A5,A6,A26,A27;
reconsider z as variable by A28;
x-term C = z-term C by A30;
hence thesis by A28,A29,Th50;
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
A1: 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;
A2: 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:10;
then
A3: x in dom f by ZFMISC_1:31;
then consider y being variable such that
A4: f.x = y-term C by Def58;
A5: y in dom g by A1,A3,A4;
A6: g.y = x-term C by A1,A3,A4;
(x-term C) at f = y-term C by A3,A4,Def60;
hence thesis by A5,A6,Def60;
end;
A7: 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
A8: len p = len the_arity_of c and
A9: for t being quasi-term of C st t in rng p holds P[t] and
A10: variables_in (c-trm p) c= dom f;
c-trm p = [c, the carrier of C]-tree p by A8,Def35;
then
A11: variables_in (c-trm p) = union {variables_in s where
s is quasi-term of C: s in rng p} by Th88;
A12: len (p at f) = len p by Th130;
A13: len (p at f at g) = len (p at f) by Th130;
A14: dom (p at f) = dom p by A12,FINSEQ_3:29;
A15: dom (p at f at g) = dom (p at f) by A13,FINSEQ_3:29;
now
let i be Nat;
assume
A16: i in dom p;
then
A17: (p at f).i = f# .(p.i) by FUNCT_1:13;
A18: p.i in rng p by A16,FUNCT_1:def 3;
rng p c= QuasiTerms C by FINSEQ_1:def 4;
then reconsider pi1 = p.i as quasi-term of C by A18,Th41;
variables_in pi1 in {variables_in s where s is quasi-term of C:
s in rng p} by A18;
then
A19: variables_in pi1 c= variables_in (c-trm p) by A11,ZFMISC_1:74;
(p at f at g).i = pi1 at f at g by A14,A16,A17,FUNCT_1:13;
hence (p at f at g).i = p.i by A9,A10,A18,A19,XBOOLE_1:1;
end;
then
A20: p at f at g = p by A14,A15;
(c-trm p) at f = c-trm (p at f) by A8,Def60;
hence thesis by A8,A12,A20,Def60;
end;
A21: 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
A22: P[a] and
A23: variables_in ((non_op C)term a) c= dom f;
A24: (non_op C)term a = [non_op, the carrier of C]-tree <*a*> by Th43;
thus ((non_op C)term a) at f at g = ((non_op C)term (a at f)) at g by Def60
.= (non_op C)term a by A22,A23,A24,Def60,Th93;
end;
A25: 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
A26: P[a];
let t be expression of C, a_Type C such that
A27: P[t] and
A28: variables_in ((ast C)term(a,t)) c= dom f;
(ast C)term(a,t) = [ *, the carrier of C]-tree <*a,t*> by Th46;
then
A29: variables_in ((ast C)term(a,t))
= ((C variables_in a)(\/)(C variables_in t)).a_Term by Th96
.= (variables_in a)\/variables_in t by PBOOLE:def 4;
thus ((ast C)term(a,t)) at f at g
= ((ast C)term (a at f, t at f)) at g by Def60
.= (ast C)term(a,t) by A26,A27,A28,A29,Def60,XBOOLE_1:11;
end;
thus P[t] from StructInd(A2,A7,A21,A25);
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 object;
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 Th144:
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
A1: A = {a};
thus A at f c= {a at f}
proof
let x be object;
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 A1,TARSKI:def 1;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {a at f};
then
A2: x = a at f by TARSKI:def 1;
a in A by A1,TARSKI:def 1;
hence thesis by A2;
end;
theorem Th145:
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 object;
assume x in (A \/ B) at f;
then consider a being quasi-adjective of C such that
A1: x = a at f and
A2: a in A \/ B;
a in A or a in B by A2,XBOOLE_0:def 3;
then x in A at f or x in B at f by A1;
hence thesis by XBOOLE_0:def 3;
end;
let x be object;
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 3;
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 Th145;
hence thesis 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
A1: A is finite;
deffunc F(expression of C) = $1 at f;
A2: { F(w) where w is expression of C: w in A } is finite
from FRAENKEL:sch 21(A1);
A at f c= { F(w) where w is expression of C: w in A }
proof
let x be object;
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 A2;
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;
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:31;
thus (a ast T) at f
= [(adjs (a ast T)) at f,((the_base_of T) at f)]
.= [(A\/(adjs T)) at f,((the_base_of T) at f)]
.= [(A at f)\/((adjs T) at f),(the_base_of T) at f] by Th145
.= [{a at f}\/((adjs T) at f),(the_base_of T) at f] by Th144
.= [{a at f}\/(adjs (T at f)),(the_base_of T) at f]
.= (a at f) ast (T at f);
end;
definition
let C be initialized ConstructorSignature;
let f,g be valuation of C;
func f at g -> valuation of C means
:
Def66: 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(object) = ((In($1,Vars)-term C) at f) at g;
consider h being Function such that
A1: dom h = (dom f) \/ dom g and
A2: for x being object 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 object;
assume y in rng h;
then consider x being object such that
A3: x in dom h and
A4: y = h.x by FUNCT_1:def 3;
y = h(x) by A1,A2,A3,A4;
hence thesis by Def28;
end;
then reconsider h as valuation of C by A1,RELSET_1:4;
take h;
thus dom h = (dom f) \/ dom g by A1;
let x be variable;
assume x in dom h;
then h.x = h(x) by A1,A2;
hence thesis;
end;
uniqueness
proof
let h1,h2 be valuation of C such that
A5: dom h1 = (dom f) \/ dom g and
A6: for x being variable st x in dom h1 holds h1.x = ((x-term C) at f) at g and
A7: dom h2 = (dom f) \/ dom g and
A8: 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
A9: x in dom h1;
then h1.x = ((x-term C) at f) at g by A6;
hence h1.x = h2.x by A5,A7,A8,A9;
end;
hence thesis by A5,A7;
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
A1: x in dom (f at g);
then
A2: (f at g).x = ((x-term C) at f) at g by Def66;
A3: dom (f at g) = dom f \/ dom g by Def66;
per cases;
suppose
A4: x in dom f;
then consider y being variable such that
A5: f.x = y-term C by Def58;
A6: (x-term C) at f = y-term C by A4,A5,Def60;
then
A7: y in dom g implies (f at g).x = g.y by A2,Def60;
y nin dom g implies (f at g).x = y-term C by A2,A6,Def60;
hence thesis by A7,Def58;
end;
suppose
A8: x nin dom f;
then
A9: (x-term C) at f = x-term C by Def60;
A10: x in dom g by A1,A3,A8,XBOOLE_0:def 3;
then (f at g).x = g.x by A2,A9,Def60;
hence thesis by A10,Def58;
end;
end;
end;
theorem Th149:
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;
A1: dom (f1 at f2) = (dom f1) \/ dom f2 by Def66;
defpred P[expression of C] means ($1 at f1) at f2 = $1 at (f1 at f2);
A2: for x being variable holds P[x-term C]
proof
let x be variable;
per cases;
suppose
A3: x in dom (f1 at f2);
then (x-term C) at (f1 at f2) = (f1 at f2).x by Def60;
hence thesis by A3,Def66;
end;
suppose
A4: x nin dom (f1 at f2);
then
A5: x nin dom f1 by A1,XBOOLE_0:def 3;
A6: x nin dom f2 by A1,A4,XBOOLE_0:def 3;
A7: (x-term C) at f1 = x-term C by A5,Def60;
(x-term C) at f2 = x-term C by A6,Def60;
hence thesis by A4,A7,Def60;
end;
end;
A8: 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
A9: len p = len the_arity_of c and
A10: for t being quasi-term of C st t in rng p holds P[t];
A11: len (p at f1) = len p by Th130;
A12: len (p at (f1 at f2)) = len p by Th130;
A13: len ((p at f1) at f2) = len (p at f1) by Th130;
A14: dom (p at f1) = dom p by A11,FINSEQ_3:29;
A15: dom (p at (f1 at f2)) = dom p by A12,FINSEQ_3:29;
A16: dom ((p at f1) at f2) = dom p by A11,A13,FINSEQ_3:29;
now
let i be Nat;
assume
A17: i in dom p;
then
A18: ((p at f1) at f2).i = f2# .((p at f1).i) by A14,FUNCT_1:13;
A19: p.i in rng p by A17,FUNCT_1:def 3;
rng p c= QuasiTerms C by FINSEQ_1:def 4;
then reconsider pi1 = p.i as quasi-term of C by A19,Th41;
thus (p at f1 at f2).i = (pi1 at f1) at f2 by A17,A18,FUNCT_1:13
.= pi1 at (f1 at f2) by A10,A19
.= (p at (f1 at f2)).i by A17,FUNCT_1:13;
end;
then
A20: p at f1 at f2 = p at (f1 at f2) by A15,A16;
thus (c-trm p) at f1 at f2 = (c-trm(p at f1)) at f2 by A9,Def60
.= c-trm (p at (f1 at f2)) by A9,A11,A20,Def60
.= (c-trm p) at (f1 at f2) by A9,Def60;
end;
A21: 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 Def60
.= ((non_op C)term a) at (f1 at f2) by Def60;
hence thesis by Def60;
end;
A22: 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
A23: 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 A23,Def60
.= ((ast C)term(a,t)) at (f1 at f2) by Def60;
hence thesis by Def60;
end;
thus P[t] from StructInd(A2,A8,A21,A22);
end;
theorem Th150:
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 object;
assume x in (A at f1) at f2;
then consider a being quasi-adjective of C such that
A1: x = a at f2 and
A2: a in A at f1;
consider b being quasi-adjective of C such that
A3: a = b at f1 and
A4: b in A by A2;
x = b at (f1 at f2) by A1,A3,Th149;
hence thesis by A4;
end;
let x be object;
assume x in A at (f1 at f2);
then consider a being quasi-adjective of C such that
A5: x = a at (f1 at f2) and
A6: a in A;
A7: x = a at f1 at f2 by A5,Th149;
a at f1 in A at f1 by A6;
hence thesis by A7;
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)
.= ((adjs T) at (f1 at f2))ast((the_base_of (T at f1))at f2) by Th150
.= ((adjs T) at (f1 at f2))ast(((the_base_of T) at f1)at f2)
.= T at (f1 at f2) by Th149;
end;