Copyright (c) 2002 Association of Mizar Users
environ
vocabulary FUNCT_1, PBOOLE, TDGROUP, CARD_3, RELAT_1, MSUALG_2, PRALG_1,
REALSET1, BOOLE, ZF_REFLE, PROB_1, TARSKI, AMI_1, MSUALG_1, ALG_1,
FINSEQ_1, QC_LANG1, LANG1, DTCONSTR, TREES_4, TREES_2, TREES_3, FUNCT_6,
MCART_1, UNIALG_2, GROUP_6, MSUALG_3, MSAFREE, MSUALG_4, NATTRA_1,
FINSEQ_4, OSALG_1, SEQM_3, YELLOW18, COH_SP, EQREL_1, RELAT_2, FUNCT_5,
CARD_LAR, CARD_5, OSALG_2, OSALG_4, OSAFREE, PARTFUN1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XREAL_0, NAT_1, RELAT_1,
RELSET_1, STRUCT_0, FUNCT_1, MCART_1, PARTFUN1, FUNCT_2, FINSEQ_1,
FINSEQ_2, RELAT_2, TREES_2, PROB_1, CARD_3, EQREL_1, FINSEQ_4, LANG1,
TREES_3, FUNCT_6, TREES_4, FUNCT_5, DTCONSTR, ORDERS_1, ORDERS_3, PBOOLE,
PRALG_1, MSUALG_1, MSUALG_2, MSUALG_3, MSUALG_4, OSALG_1, OSALG_2,
OSALG_3, OSALG_4, MSAFREE, YELLOW18;
constructors NAT_1, MSUALG_3, FINSOP_1, FINSEQ_4, FINSEQOP, ORDERS_3, OSALG_2,
OSALG_3, OSALG_4, MSAFREE3, MEMBERED, YELLOW18;
clusters SUBSET_1, PBOOLE, TREES_3, TREES_4, DTCONSTR, PRALG_1, MSUALG_1,
RELSET_1, STRUCT_0, XBOOLE_0, MSUALG_4, MSUALG_9, OSALG_1, OSALG_4,
MSAFREE, NAT_1, MEMBERED, PARTFUN1, NUMBERS, ORDINAL2;
requirements NUMERALS, BOOLE, SUBSET;
definitions TARSKI, XBOOLE_0, PBOOLE, MSUALG_3, STRUCT_0, OSALG_1, OSALG_3,
OSALG_4;
theorems TARSKI, FUNCT_1, FUNCT_2, MCART_1, ZFMISC_1, PBOOLE, CARD_3,
MSUALG_1, MSUALG_2, MSUALG_3, PRALG_1, RELAT_1, LANG1, DTCONSTR,
FINSEQ_1, TREES_4, FINSEQ_4, TREES_1, TREES_2, ALG_1, DOMAIN_1, PROB_1,
RELSET_1, XBOOLE_0, XBOOLE_1, OSALG_1, OSALG_2, OSALG_3, OSALG_4,
MSAFREE, MSUALG_6, MSAFREE2, CARD_5, FINSEQ_2, FINSEQ_3, MSUALG_9,
MSUALG_4, EQREL_1, FUNCT_5, ORDERS_1, RELAT_2, PARTFUN1;
schemes ZFREFLE1, FUNCT_1, RELSET_1, MSUALG_2, DTCONSTR, COMPTS_1, XBOOLE_0,
FUNCT_2, MSUALG_1;
begin
reserve S for OrderSortedSign;
:: REVISE: should rather be attribute
:: changing to MSSubset and its OSCl, to make free algebras easier
:: no good way how to retypeOSCL into OSSubset now?
definition
let S be OrderSortedSign,
U0 be OSAlgebra of S;
mode OSGeneratorSet of U0 -> MSSubset of U0 means :Def1:
for O being OSSubset of U0 st O = OSCl it holds
the Sorts of GenOSAlg(O) = the Sorts of U0;
existence
proof
set A = the Sorts of U0;
reconsider A as MSSubset of U0 by MSUALG_2:def 1;
A1: A is OrderSortedSet of S by OSALG_1:17;
then reconsider A as OSSubset of U0 by OSALG_2:def 2;
take A;
A2: A = OSCl A by A1,OSALG_2:14;
set G = GenOSAlg(A);
A is OSSubset of G by OSALG_2:def 13;
then A3: A c= the Sorts of G by MSUALG_2:def 1;
the Sorts of G is MSSubset of U0 by MSUALG_2:def 10;
then the Sorts of G c= A by MSUALG_2:def 1;
hence thesis by A2,A3,PBOOLE:def 13;
end;
end;
theorem
for S be OrderSortedSign,
U0 be strict non-empty OSAlgebra of S,
A be MSSubset of U0 holds
A is OSGeneratorSet of U0 iff
for O being OSSubset of U0 st O = OSCl A holds GenOSAlg(O) = U0
proof
let S be OrderSortedSign,
U0 be strict non-empty OSAlgebra of S,
A be MSSubset of U0;
thus A is OSGeneratorSet of U0 implies
for O being OSSubset of U0 st O = OSCl A holds GenOSAlg(O) = U0
proof
assume A1: A is OSGeneratorSet of U0;
let O be OSSubset of U0 such that A2: O = OSCl A;
reconsider U1 = U0 as MSSubAlgebra of U0 by MSUALG_2:6;
the Sorts of GenOSAlg(O) = the Sorts of U1 by A1,A2,Def1;
hence thesis by MSUALG_2:10;
end;
assume A3: for O being OSSubset of U0 st O = OSCl A holds GenOSAlg(O) = U0;
let O be OSSubset of U0 such that A4: O = OSCl A;
thus the Sorts of GenOSAlg(O) = the Sorts of U0 by A3,A4;
end;
:: renaming to osfree - if OSGeneratorSet and GeneratorSet become
:: attributes, Mizar would be puzzled
:: we do this for monotone osas only, though more general approach is possible
definition
let S; let U0 be monotone OSAlgebra of S;
let IT be OSGeneratorSet of U0;
attr IT is osfree means
for U1 be monotone non-empty OSAlgebra of S
for f be ManySortedFunction of IT,the Sorts of U1
ex h be ManySortedFunction of U0,U1
st h is_homomorphism U0,U1 & h is order-sorted & h || IT = f;
end;
definition
let S be OrderSortedSign;
let IT be monotone OSAlgebra of S;
attr IT is osfree means
ex G being OSGeneratorSet of IT st G is osfree;
end;
begin
::
:: Construction of Free Order Sorted Algebras for Given Signature
::
definition
let S be OrderSortedSign,
X be ManySortedSet of S;
func OSREL(X) -> Relation of
([:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X)),
(([:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X))*) means
:Def4:
for a be Element of
[:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X),
b be Element of
([:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X))*
holds
[a,b] in it iff
a in [:the OperSymbols of S,{the carrier of S}:] &
for o be OperSymbol of S st [o,the carrier of S] = a holds
len b = len (the_arity_of o) &
for x be set st x in dom b holds
(b.x in [:the OperSymbols of S,{the carrier of S}:] implies
for o1 be OperSymbol of S st [o1,the carrier of S] = b.x
holds (the_result_sort_of o1) <= (the_arity_of o)/.x) &
(b.x in Union (coprod X) implies
ex i being Element of S st
i <= (the_arity_of o)/.x &
b.x in coprod(i,X));
existence
proof
set O = [:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X);
defpred P[Element of O, Element of O*] means
$1 in [:the OperSymbols of S,{the carrier of S}:] &
for o be OperSymbol of S st [o,the carrier of S] = $1 holds
len $2 = len (the_arity_of o) &
for x be set st x in dom $2 holds
($2.x in [:the OperSymbols of S,{the carrier of S}:] implies
for o1 be OperSymbol of S st [o1,the carrier of S] = $2.x
holds the_result_sort_of o1 <= (the_arity_of o)/.x) &
($2.x in Union (coprod X) implies
ex i being Element of S st
i <= (the_arity_of o)/.x &
$2.x in coprod(i,X));
consider R be Relation of O,O* such that
A1: for a be Element of O, b be Element of O* holds [a,b] in R iff
P[a,b] from Rel_On_Dom_Ex;
take R;
let a be Element of O, b be Element of O*;
thus [a,b] in R implies a in [:the OperSymbols of S,{the carrier of S}:] &
for o be OperSymbol of S st [o,the carrier of S] = a holds
len b = len (the_arity_of o) &
for x be set st x in dom b holds
(b.x in [:the OperSymbols of S,{the carrier of S}:] implies
for o1 be OperSymbol of S st [o1,the carrier of S] = b.x
holds the_result_sort_of o1 <= (the_arity_of o)/.x) &
(b.x in Union (coprod X) implies
ex i being Element of S st
i <= (the_arity_of o)/.x &
b.x in coprod(i,X)) by A1;
assume a in [:the OperSymbols of S,{the carrier of S}:] &
for o be OperSymbol of S st [o,the carrier of S] = a holds
len b = len (the_arity_of o) &
for x be set st x in dom b holds
(b.x in [:the OperSymbols of S,{the carrier of S}:] implies
for o1 be OperSymbol of S st [o1,the carrier of S] = b.x
holds the_result_sort_of o1 <= (the_arity_of o)/.x) &
(b.x in Union (coprod X) implies
ex i being Element of S st
i <= (the_arity_of o)/.x &
b.x in coprod(i,X));
hence thesis by A1;
end;
uniqueness
proof
set O = [:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X);
let R,P be Relation of O,O*;
assume that
A2: for a be Element of O, b be Element of O* holds [a,b] in R iff
a in [:the OperSymbols of S,{the carrier of S}:] &
for o be OperSymbol of S st [o,the carrier of S] = a holds
len b = len (the_arity_of o) &
for x be set st x in dom b holds
(b.x in [:the OperSymbols of S,{the carrier of S}:] implies
for o1 be OperSymbol of S st [o1,the carrier of S] = b.x
holds the_result_sort_of o1 <= (the_arity_of o)/.x) &
(b.x in Union (coprod X) implies
ex i being Element of S st
i <= (the_arity_of o)/.x &
b.x in coprod(i,X)) and
A3: for a be Element of O, b be Element of O* holds [a,b] in P iff
a in [:the OperSymbols of S,{the carrier of S}:] &
for o be OperSymbol of S st [o,the carrier of S] = a holds
len b = len (the_arity_of o) &
for x be set st x in dom b holds
(b.x in [:the OperSymbols of S,{the carrier of S}:] implies
for o1 be OperSymbol of S st [o1,the carrier of S] = b.x
holds the_result_sort_of o1 <= (the_arity_of o)/.x) &
(b.x in Union (coprod X) implies
ex i being Element of S st
i <= (the_arity_of o)/.x &
b.x in coprod(i,X));
for x,y be set holds [x,y] in R iff [x,y] in P
proof
let x,y be set;
thus [x,y] in R implies [x,y] in P
proof
assume A4: [x,y] in R;
then reconsider a = x as Element of O by ZFMISC_1:106;
reconsider b = y as Element of O* by A4,ZFMISC_1:106;
[a,b] in R by A4;
then a in [:the OperSymbols of S,{the carrier of S}:] &
for o be OperSymbol of S st [o,the carrier of S] = a holds
len b = len (the_arity_of o) &
for x be set st x in dom b holds
(b.x in [:the OperSymbols of S,{the carrier of S}:] implies
for o1 be OperSymbol of S st [o1,the carrier of S] = b.x
holds the_result_sort_of o1 <= (the_arity_of o)/.x) &
(b.x in Union (coprod X) implies
ex i being Element of S st
i <= (the_arity_of o)/.x &
b.x in coprod(i,X)) by A2;
hence thesis by A3;
end;
assume A5: [x,y] in P;
then reconsider a = x as Element of O by ZFMISC_1:106;
reconsider b = y as Element of O* by A5,ZFMISC_1:106;
[a,b] in P by A5;
then a in [:the OperSymbols of S,{the carrier of S}:] &
for o be OperSymbol of S st [o,the carrier of S] = a holds
len b = len (the_arity_of o) &
for x be set st x in dom b holds
(b.x in [:the OperSymbols of S,{the carrier of S}:] implies
for o1 be OperSymbol of S st [o1,the carrier of S] = b.x
holds the_result_sort_of o1 <= (the_arity_of o)/.x) &
(b.x in Union (coprod X) implies
ex i being Element of S st
i <= (the_arity_of o)/.x &
b.x in coprod(i,X)) by A3;
hence thesis by A2;
end;
hence thesis by RELAT_1:def 2;
end;
end;
reserve S for OrderSortedSign,
X for ManySortedSet of S,
o for OperSymbol of S,
b for Element of
([:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X))*;
theorem Th2:
[[o,the carrier of S],b] in OSREL(X)
iff
len b = len (the_arity_of o) &
for x be set st x in dom b holds
(b.x in [:the OperSymbols of S,{the carrier of S}:] implies
for o1 be OperSymbol of S st [o1,the carrier of S] = b.x
holds (the_result_sort_of o1) <= (the_arity_of o)/.x) &
(b.x in Union (coprod X) implies
ex i being Element of S st
i <= (the_arity_of o)/.x &
b.x in coprod(i,X))
proof
defpred
P[OperSymbol of S,Element of
([:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X))*]
means len $2 = len (the_arity_of $1) &
for x be set st x in dom $2 holds
($2.x in [:the OperSymbols of S,{the carrier of S}:] implies
for o1 be OperSymbol of S st [o1,the carrier of S] = $2.x
holds the_result_sort_of o1 <= (the_arity_of $1)/.x) &
($2.x in Union (coprod X) implies
ex i being Element of S st
i <= (the_arity_of $1)/.x &
b.x in coprod(i,X));
set a = [o,the carrier of S];
the carrier of S in {the carrier of S} by TARSKI:def 1;
then A1: a in [:the OperSymbols of S,{the carrier of S}:] by ZFMISC_1:106;
then reconsider a as Element of
[:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X)
by XBOOLE_0:def 2;
thus [[o,the carrier of S],b] in OSREL(X) implies P[o,b]
proof
assume [[o,the carrier of S],b] in OSREL(X);
then for o1 be OperSymbol of S st [o1,the carrier of S] = a
holds P[o1,b] by Def4;
hence thesis;
end;
assume
A2: P[o,b];
now let o1 be OperSymbol of S;
assume [o1,the carrier of S] = a;
then o1 = o by ZFMISC_1:33;
hence P[o1,b] by A2;
end;
hence thesis by A1,Def4;
end;
definition
let S be OrderSortedSign,
X be ManySortedSet of S;
func DTConOSA(X) -> DTConstrStr equals :Def5:
DTConstrStr (# [:the OperSymbols of S,{the carrier of S}:]
\/ Union (coprod X), OSREL(X) #);
correctness;
end;
definition
let S be OrderSortedSign,
X be ManySortedSet of S;
cluster DTConOSA(X) -> strict non empty;
coherence
proof
DTConOSA(X) = DTConstrStr (# [:the OperSymbols of S,{the carrier of S}:]
\/ Union (coprod X), OSREL(X) #) by Def5;
hence DTConOSA X is strict & the carrier of DTConOSA(X) is non empty;
end;
end;
theorem Th3:
for S be OrderSortedSign,
X be non-empty ManySortedSet of S holds
NonTerminals(DTConOSA(X)) = [:the OperSymbols of S,{the carrier of S}:]
& Terminals (DTConOSA(X)) = Union (coprod X)
proof
let S be OrderSortedSign,
X be non-empty ManySortedSet of S;
A1: Union(coprod X) misses [:the OperSymbols of S,{the carrier of S}:]
by MSAFREE:4;
set D = DTConOSA(X),
A = [:the OperSymbols of S,{the carrier of S}:] \/
Union (coprod (X qua ManySortedSet of S));
A2: D = DTConstrStr (# A , OSREL(X) #) by Def5;
A3: the carrier of D = (Terminals D) \/ (NonTerminals D) &
(Terminals D) misses (NonTerminals D) by DTCONSTR:8,LANG1:1;
thus
A4: NonTerminals D c= [:the OperSymbols of S,{the carrier of S}:]
proof
let x be set;
assume x in NonTerminals D;
then x in { s where s is Symbol of D: ex n being FinSequence st s ==> n}
by LANG1:def 3;
then consider s be Symbol of D such that
A5: s = x & ex n being FinSequence st s ==> n;
consider n be FinSequence such that
A6: s ==> n by A5;
A7: [s,n] in the Rules of D by A6,LANG1:def 1;
reconsider s as Element of A by A2;
reconsider n as Element of A* by A2,A7,ZFMISC_1:106;
[s,n] in OSREL X by A2,A6,LANG1:def 1;
hence thesis by A5,Def4;
end;
thus
A8: [:the OperSymbols of S,{the carrier of S}:] c= NonTerminals D
proof
let x be set; assume
A9: x in [:the OperSymbols of S,{the carrier of S}:];
then consider o being Element of the OperSymbols of S,
x2 being Element of {the carrier of S}
such that
A10: x = [o,x2] by DOMAIN_1:9;
A11: the carrier of S = x2 by TARSKI:def 1;
then reconsider xa = [o,the carrier of S]
as Element of (the carrier of D) by A2,A9,A10,XBOOLE_0:def 2;
set O = the_arity_of o;
defpred P[set,set] means
ex i being Element of S st
i <= O/.$1 & $2 in coprod(i,X);
A12: for a be set st a in Seg len O ex b be set st P[a,b]
proof
let a be set; assume
a in Seg len O;
then A13: a in dom O by FINSEQ_1:def 3;
then A14: O.a in rng O & rng O c= the carrier of S
by FINSEQ_1:def 4,FUNCT_1:def 5;
then X.(O.a) is non empty by PBOOLE:def 16;
then consider x be set such that
A15: x in X.(O.a) by XBOOLE_0:def 1;
take y = [x,O.a];
A16: y in coprod(O.a,X) by A14,A15,MSAFREE:def 2;
take O/.a;
thus thesis by A13,A16,FINSEQ_4:def 4;
end;
consider b be Function such that
A17: dom b = Seg len O &
for a be set st a in Seg len O holds P[a,b.a] from NonUniqFuncEx(A12);
reconsider b as FinSequence by A17,FINSEQ_1:def 2;
rng b c= A
proof let a be set; assume a in rng b;
then consider c be set such that
A18: c in dom b & b.c = a by FUNCT_1:def 5;
consider i being Element of S such that
A19: i <= O/.c & a in coprod(i,X) by A17,A18;
dom coprod(X) = the carrier of S by PBOOLE:def 3;
then (coprod(X)).(i) in rng coprod(X) by FUNCT_1:def 5;
then coprod(i,X) in rng coprod(X) by MSAFREE:def 3;
then a in union rng coprod(X) by A19,TARSKI:def 4;
then a in Union coprod(X) by PROB_1:def 3;
hence thesis by XBOOLE_0:def 2;
end;
then reconsider b as FinSequence of A by FINSEQ_1:def 4;
reconsider b as Element of A* by FINSEQ_1:def 11;
A20: len b = len O by A17,FINSEQ_1:def 3;
now let c be set;
assume c in dom b;
then consider i being Element of S such that
A21: i <= O/.c & b.c in coprod(i,X) by A17;
dom coprod(X) = the carrier of S by PBOOLE:def 3;
then (coprod(X)).(i) in rng coprod(X) by FUNCT_1:def 5;
then coprod(i,X) in rng coprod(X) by MSAFREE:def 3;
then b.c in union rng coprod(X) by A21,TARSKI:def 4;
then b.c in Union coprod(X) by PROB_1:def 3;
hence b.c in [:the OperSymbols of S,{the carrier of S}:] implies
for o1 be OperSymbol of S st [o1,the carrier of S] = b.c holds
the_result_sort_of o1 <= O/.c by A1,XBOOLE_0:3;
assume b.c in Union (coprod X);
thus ex i being Element of S st
i <= O/.c &
b.c in coprod(i,X) by A21;
end;
then [xa,b] in OSREL(X) by A20,Th2;
then xa ==> b by A2,LANG1:def 1;
then xa in { t where t is Symbol of D: ex n be FinSequence st t ==> n};
hence thesis by A10,A11,LANG1:def 3;
end;
thus Terminals D c= Union (coprod X)
proof
let x be set; assume A22: x in Terminals D;
then A23: x in A by A2,A3,XBOOLE_0:def 2;
not x in [:the OperSymbols of S,{the carrier of S}:]
by A3,A8,A22,XBOOLE_0:3;
hence thesis by A23,XBOOLE_0:def 2;
end;
let x be set; assume A24: x in Union (coprod X);
then x in A by XBOOLE_0:def 2;
then x in Terminals D or x in NonTerminals D by A2,A3,XBOOLE_0:def 2;
hence thesis by A1,A4,A24,XBOOLE_0:3;
end;
reserve x for set;
definition
let S be OrderSortedSign,
X be non-empty ManySortedSet of S;
cluster DTConOSA(X) -> with_terminals with_nonterminals
with_useful_nonterminals;
coherence
proof
set D = DTConOSA(X),
A = [:the OperSymbols of S,{the carrier of S}:] \/
Union (coprod (X qua ManySortedSet of S));
A1: Union (coprod X) misses [:the OperSymbols of S,{the carrier of S}:]
by MSAFREE:4;
A2: Terminals D = Union (coprod X) &
NonTerminals D = [:the OperSymbols of S,{the carrier of S}:] by Th3;
A3: D = DTConstrStr (# A , OSREL(X) #) by Def5;
for nt being Symbol of D st nt in NonTerminals D
ex p being FinSequence of TS(D) st nt ==> roots p
proof
let nt be Symbol of D;
assume nt in NonTerminals D;
then consider o being Element of the OperSymbols of S,
x2 being Element of {the carrier of S}
such that
A4: nt = [o,x2] by A2,DOMAIN_1:9;
A5: the carrier of S = x2 by TARSKI:def 1;
set O = the_arity_of o;
defpred P[set,set] means
ex i being Element of S st
i <= O/.$1 & $2 in coprod(i,X);
A6: for a be set st a in Seg len O ex b be set st P[a,b]
proof
let a be set; assume
a in Seg len O;
then A7: a in dom O by FINSEQ_1:def 3;
then A8: O.a in
rng O & rng O c= the carrier of S by FINSEQ_1:def 4,FUNCT_1:def 5;
then X.(O.a) is non empty by PBOOLE:def 16;
then consider x be set such that
A9: x in X.(O.a) by XBOOLE_0:def 1;
take y = [x,O.a];
A10: y in coprod(O.a,X) by A8,A9,MSAFREE:def 2;
take O/.a;
thus thesis by A7,A10,FINSEQ_4:def 4;
end;
consider b be Function such that
A11: dom b = Seg len O &
for a be set st a in Seg len O holds P[a,b.a] from NonUniqFuncEx(A6);
reconsider b as FinSequence by A11,FINSEQ_1:def 2;
A12: rng b c= A
proof let a be set; assume a in rng b;
then consider c be set such that
A13: c in dom b & b.c = a by FUNCT_1:def 5;
consider i being Element of S such that
A14: i <= O/.c & a in coprod(i,X) by A11,A13;
dom coprod(X) = the carrier of S by PBOOLE:def 3;
then (coprod(X)).i in rng coprod(X) by FUNCT_1:def 5;
then coprod(i,X) in rng coprod(X) by MSAFREE:def 3;
then a in union rng coprod(X) by A14,TARSKI:def 4;
then a in Union coprod(X) by PROB_1:def 3;
hence thesis by XBOOLE_0:def 2;
end;
then reconsider b as FinSequence of A by FINSEQ_1:def 4;
reconsider b as Element of A* by FINSEQ_1:def 11;
A15: len b = len O by A11,FINSEQ_1:def 3;
now let c be set;
assume c in dom b;
then consider i being Element of S such that
A16: i <= O/.c & b.c in coprod(i,X) by A11;
dom coprod(X) = the carrier of S by PBOOLE:def 3;
then (coprod(X)).i in rng coprod(X) by FUNCT_1:def 5;
then coprod(i,X) in rng coprod(X) by MSAFREE:def 3;
then b.c in union rng coprod(X) by A16,TARSKI:def 4;
then b.c in Union coprod(X) by PROB_1:def 3;
hence b.c in [:the OperSymbols of S,{the carrier of S}:] implies
for o1 be OperSymbol of S st [o1,the carrier of S] = b.c holds
the_result_sort_of o1 <= O/.c by A1,XBOOLE_0:3;
assume b.c in Union (coprod X);
thus ex i being Element of S st
i <= O/.c &
b.c in coprod(i,X) by A16;
end;
then [nt,b] in OSREL(X) by A4,A5,A15,Th2;
then A17: nt ==> b by A3,LANG1:def 1;
deffunc F(set) = root-tree (b.$1);
consider f be Function such that
A18: dom f = dom b & for x st x in dom b holds f.x = F(x)
from Lambda;
reconsider f as FinSequence by A11,A18,FINSEQ_1:def 2;
rng f c= TS(D)
proof
let x;
assume x in rng f;
then consider y be set such that
A19: y in dom f & f.y = x by FUNCT_1:def 5;
A20: x = root-tree(b.y) by A18,A19;
b.y in rng b by A18,A19,FUNCT_1:def 5;
then reconsider a = b.y as Symbol of D by A3,A12;
consider i being Element of S such that
A21: i <= O/.y & b.y in coprod(i,X) by A11,A18,A19;
dom coprod(X) = the carrier of S by PBOOLE:def 3;
then (coprod(X)).(i) in rng coprod(X) by FUNCT_1:def 5;
then coprod(i,X) in rng coprod(X) by MSAFREE:def 3;
then b.y in union rng coprod(X) by A21,TARSKI:def 4;
then a in Terminals D by A2,PROB_1:def 3;
hence thesis by A20,DTCONSTR:def 4;
end;
then reconsider f as FinSequence of TS(D) by FINSEQ_1:def 4;
take f;
A22: dom (roots f) = dom f by DTCONSTR:def 1;
for x st x in dom b holds (roots f).x = b.x
proof
let x;
assume A23: x in dom b;
then A24: f.x = root-tree (b.x) by A18;
reconsider i = x as Nat by A23;
consider T be DecoratedTree such that
A25: T = f.i & (roots f).i = T.{} by A18,A23,DTCONSTR:def 1;
thus thesis by A24,A25,TREES_4:3;
end;
hence thesis by A17,A18,A22,FUNCT_1:9;
end;
hence thesis by A2,DTCONSTR:def 6,def 7,def 8;
end;
end;
theorem Th4:
for S be OrderSortedSign,
X be non-empty ManySortedSet of S,
t be set holds
t in Terminals DTConOSA(X)
iff
ex s be Element of S, x be set st x in X.s & t = [x,s]
proof
let S be OrderSortedSign,
X be non-empty ManySortedSet of S,
t be set;
set D = DTConOSA(X);
A1: Terminals D = Union (coprod X) by Th3
.= union rng (coprod X) by PROB_1:def 3;
thus t in Terminals D implies
ex s be Element of S, x be set st x in X.s & t = [x,s]
proof
assume t in Terminals D;
then consider A be set such that
A2: t in A & A in rng(coprod X) by A1,TARSKI:def 4;
consider s be set such that
A3: s in dom (coprod X) & (coprod X).s = A by A2,FUNCT_1:def 5;
reconsider s as Element of S by A3,PBOOLE:def 3;
take s;
(coprod X).s = coprod(s,X) by MSAFREE:def 3;
then consider x be set such that
A4: x in X.s & t = [x,s] by A2,A3,MSAFREE:def 2;
take x;
thus thesis by A4;
end;
given s be Element of S, x be set such that
A5: x in X.s & t = [x,s];
t in coprod(s,X) by A5,MSAFREE:def 2;
then A6: t in (coprod X).s by MSAFREE:def 3;
dom(coprod X) = the carrier of S by PBOOLE:def 3;
then (coprod X).s in rng (coprod X) by FUNCT_1:def 5;
hence thesis by A1,A6,TARSKI:def 4;
end;
:: have to rename
definition
let S be OrderSortedSign,
X be non-empty ManySortedSet of S,
o be OperSymbol of S;
func OSSym(o,X) ->Symbol of DTConOSA(X) equals :Def6:
[o,the carrier of S];
coherence
proof
the carrier of S in {the carrier of S} by TARSKI:def 1;
then [o,the carrier of S] in [:the OperSymbols of S,{the carrier of S}:]
by ZFMISC_1:106;
then [o,the carrier of S] in NonTerminals (DTConOSA X) by Th3;
hence [o,the carrier of S] is Symbol of DTConOSA(X);
end;
end;
:: originally FreeSort, but it is not a good name in order-sorted context
definition
let S be OrderSortedSign,
X be non-empty ManySortedSet of S,
s be Element of S;
func ParsedTerms(X,s) -> Subset of TS(DTConOSA(X)) equals :Def7:
{a where a is Element of TS(DTConOSA(X)):
(ex s1 being Element of S, x be set st
s1 <= s & x in X.s1 & a = root-tree [x,s1]) or
ex o be OperSymbol of S st [o,the carrier of S] = a.{}
& the_result_sort_of o <= s};
coherence
proof
set A = {a where a is Element of TS(DTConOSA(X)):
(ex s1 being Element of S, x be set st
s1 <= s & x in X.s1 & a = root-tree [x,s1]) or
ex o be OperSymbol of S st [o,the carrier of S] = a.{}
& the_result_sort_of o <= s};
A c= TS(DTConOSA(X))
proof
let x be set;
assume x in A;
then consider a be Element of TS(DTConOSA(X)) such that A1: x = a and
(ex s1 being Element of S, x be set st
s1 <= s & x in X.s1 & a = root-tree [x,s1]) or
ex o be OperSymbol of S st [o,the carrier of S] = a.{}
& the_result_sort_of o <= s;
thus thesis by A1;
end;
hence thesis;
end;
end;
definition
let S be OrderSortedSign,
X be non-empty ManySortedSet of S,
s be Element of S;
cluster ParsedTerms(X,s) -> non empty;
coherence
proof
set A = {a where a is Element of TS(DTConOSA(X)):
(ex s1 being Element of S, x be set st
s1 <= s & x in X.s1 & a = root-tree [x,s1]) or
ex o be OperSymbol of S st [o,the carrier of S] = a.{}
& the_result_sort_of o <= s};
consider x be set such that A1: x in X.s by XBOOLE_0:def 1;
set a = [x,s];
A2: a in coprod(s,X) by A1,MSAFREE:def 2;
A3: (Terminals (DTConOSA(X))) = Union (coprod X) by Th3;
dom coprod(X) = the carrier of S by PBOOLE:def 3;
then (coprod(X)).s in rng coprod(X) by FUNCT_1:def 5;
then coprod(s,X) in rng coprod(X) by MSAFREE:def 3;
then a in union rng coprod(X) by A2,TARSKI:def 4;
then A4: a in Terminals (DTConOSA X) by A3,PROB_1:def 3;
then reconsider a as Symbol of DTConOSA(X);
reconsider b = root-tree a as Element of TS(DTConOSA X)
by A4,DTCONSTR:def 4;
b in A by A1;
hence thesis by Def7;
end;
end;
definition
let S be OrderSortedSign,
X be non-empty ManySortedSet of S;
func ParsedTerms(X) -> OrderSortedSet of S means :Def8:
for s be Element of S holds it.s = ParsedTerms(X,s);
existence
proof
deffunc F(Element of S) = ParsedTerms(X,$1);
consider f be Function such that
A1: dom f = the carrier of S &
for d be Element of S holds f.d = F(d) from LambdaB;
reconsider f as ManySortedSet of S by A1,PBOOLE:def 3;
f is order-sorted
proof
let s1,s2 be Element of S
such that A2: s1 <= s2;
thus f.s1 c= f.s2
proof
let x1 be set such that A3: x1 in f.s1;
x1 in ParsedTerms(X,s1) by A1,A3;
then x1 in {a where a is Element of TS(DTConOSA(X)):
(ex s3 being Element of S, x be set st
s3 <= s1 & x in X.s3 & a = root-tree [x,s3]) or
ex o be OperSymbol of S st [o,the carrier of S] = a.{}
& the_result_sort_of o <= s1} by Def7;
then consider a being Element of TS(DTConOSA(X)) such that
A4: x1 = a and
A5: (ex s3 being Element of S, x be set st
s3 <= s1 & x in X.s3 & a = root-tree [x,s3]) or
ex o be OperSymbol of S st [o,the carrier of S] = a.{}
& the_result_sort_of o <= s1;
(ex s3 being Element of S, x be set st
s3 <= s2 & x in X.s3 & a = root-tree [x,s3]) or
ex o be OperSymbol of S st [o,the carrier of S] = a.{}
& the_result_sort_of o <= s2
proof
per cases by A5;
suppose ex s3 being Element of S, x be set st
s3 <= s1 & x in X.s3 & a = root-tree [x,s3];
then consider s3 being Element of S, x be set such that
A6: s3 <= s1 & x in X.s3 & a = root-tree [x,s3];
reconsider s2_1 = s2 , s3_1 = s3 as Element of S
;
s3_1 <= s2_1 by A2,A6,ORDERS_1:26;
hence thesis by A6;
suppose ex o be OperSymbol of S st [o,the carrier of S] = a.{}
& the_result_sort_of o <= s1;
then consider o be OperSymbol of S such that
A7: [o,the carrier of S] = a.{} & the_result_sort_of o <= s1;
reconsider s2_1 = s2 as Element of S;
the_result_sort_of o <= s2_1 by A2,A7,ORDERS_1:26;
hence thesis by A7;
end;
then x1 in {b where b is Element of TS(DTConOSA(X)):
(ex s3 being Element of S, x be set st
s3 <= s2 & x in X.s3 & b = root-tree [x,s3]) or
ex o be OperSymbol of S st [o,the carrier of S] = b.{}
& the_result_sort_of o <= s2} by A4;
then x1 in ParsedTerms(X,s2) by Def7;
hence thesis by A1;
end;
end;
then reconsider f as OrderSortedSet of S;
take f;
thus thesis by A1;
end;
uniqueness
proof
let A,B be OrderSortedSet of S;
assume that A8: for s be Element of S
holds A.s = ParsedTerms(X,s) and
A9: for s be Element of S holds
B.s = ParsedTerms(X,s);
for i be set st i in the carrier of S holds A.i = B.i
proof
let i be set;
assume i in the carrier of S;
then reconsider s = i as Element of S;
A.s = ParsedTerms(X,s) & B.s = ParsedTerms(X,s) by A8,A9;
hence thesis;
end;
hence thesis by PBOOLE:3;
end;
end;
definition
let S be OrderSortedSign,
X be non-empty ManySortedSet of S;
cluster ParsedTerms(X) -> non-empty;
coherence
proof
let i be set;
assume i in the carrier of S;
then reconsider s = i as Element of S;
(ParsedTerms(X)).s = ParsedTerms(X,s) by Def8;
hence thesis;
end;
end;
theorem Th5:
for S be OrderSortedSign,
X be non-empty ManySortedSet of S, o be OperSymbol of S,
x be set
st x in ((ParsedTerms X)# * (the Arity of S)).o holds
x is FinSequence of TS(DTConOSA(X))
proof
let S be OrderSortedSign,
X be non-empty ManySortedSet of S,
o be OperSymbol of S,
x be set;
assume A1: x in ((ParsedTerms X)# * (the Arity of S)).o;
set D = DTConOSA(X),
ar = the_arity_of o;
(the Arity of S).o = ar by MSUALG_1:def 6;
then x in product ((ParsedTerms X) * ar) by A1,MSAFREE:1;
then consider f be Function such that
A2: x = f & dom f = dom ((ParsedTerms X) * ar) &
for y be set st y in dom ((ParsedTerms X)* ar)
holds f.y in ((ParsedTerms X) * ar).y by CARD_3:def 5;
A3: dom ((ParsedTerms X) * ar) = dom ar by PBOOLE:def 3;
dom ar = Seg len ar by FINSEQ_1:def 3;
then reconsider f as FinSequence by A2,A3,FINSEQ_1:def 2;
rng f c= TS D
proof
let a be set; assume a in rng f;
then consider b be set such that
A4: b in dom f & f.b = a by FUNCT_1:def 5;
A5: a in ((ParsedTerms X) * ar).b by A2,A4;
reconsider b as Nat by A4;
((ParsedTerms X) * ar).b = (ParsedTerms X).(ar.b) by A2,A4,FUNCT_1:22
.= (ParsedTerms X). (ar/.b) by A2,A3,A4,FINSEQ_4:def 4
.= ParsedTerms(X,ar/.b) by Def8
.= { s where s is Element of TS D:
(ex s1 being Element of S, x be set st
s1 <= ar/.b & x in X.(s1) & s = root-tree [x,s1]) or
ex o1 be OperSymbol of S st
[o1,the carrier of S] = s.{} & the_result_sort_of o1 <= ar/.b}
by Def7;
then consider e be Element of TS D such that
A6: a = e and
(ex s1 being Element of S, x be set st
s1 <= ar/.b & x in X.(s1) & e = root-tree [x,s1]) or
ex o be OperSymbol of S st
[o,the carrier of S] = e.{} & the_result_sort_of o <= ar/.b by A5;
thus thesis by A6;
end;
then reconsider f as FinSequence of TS(D) by FINSEQ_1:def 4;
f = x by A2;
hence thesis;
end;
theorem Th6:
for S be OrderSortedSign,
X be non-empty ManySortedSet of S,
o be OperSymbol of S,
p be FinSequence of TS(DTConOSA(X))
holds p in ((ParsedTerms X)# * (the Arity of S)).o iff
dom p = dom (the_arity_of o) &
for n be Nat st n in dom p holds
p.n in ParsedTerms(X,(the_arity_of o)/.n)
proof
let S be OrderSortedSign,
X be non-empty ManySortedSet of S,
o be OperSymbol of S,
p be FinSequence of TS(DTConOSA(X));
set AR = the Arity of S,
ar = the_arity_of o;
thus p in ((ParsedTerms X)# * AR).o implies
dom p = dom (the_arity_of o) &
for n be Nat st n in dom p holds p.n in ParsedTerms(X,(the_arity_of o)/.n)
proof
assume A1: p in ((ParsedTerms X)# * (the Arity of S)).o;
AR.o = ar by MSUALG_1:def 6;
then p in product ((ParsedTerms X) * ar) by A1,MSAFREE:1;
then A2: dom p = dom ((ParsedTerms X) * ar) &
for x be set st x in dom ((ParsedTerms X) * ar)
holds p.x in ((ParsedTerms X) * ar).x by CARD_3:18;
A3: dom ((ParsedTerms X) * ar) = dom ar by PBOOLE:def 3;
thus dom p = dom ar by A2,PBOOLE:def 3;
let n be Nat;
assume A4: n in dom p;
then ((ParsedTerms X) * ar).n = (ParsedTerms X).(ar.n) by A2,FUNCT_1:22
.= (ParsedTerms X). (ar/.n) by A2,A3,A4,FINSEQ_4:def 4
.= ParsedTerms(X,ar/.n) by Def8;
hence thesis by A2,A4;
end;
assume A5: dom p = dom (the_arity_of o) &
for n be Nat st n in dom p holds p.n in ParsedTerms(X,(the_arity_of o)/.n);
AR.o = ar by MSUALG_1:def 6;
then A6: ((ParsedTerms X)# * AR).o = product ((ParsedTerms X) * ar) by
MSAFREE:1;
A7: dom p = dom ((ParsedTerms X) * ar) by A5,PBOOLE:def 3;
for x be set st x in dom((ParsedTerms X) * ar) holds p.x in
((ParsedTerms X) * ar).x
proof
let x be set;
assume A8: x in dom ((ParsedTerms X) * ar);
then reconsider n = x as Nat;
ParsedTerms(X,ar/.n) = (ParsedTerms X). (ar/.n) by Def8
.= (ParsedTerms X).(ar.n) by A5,A7,A8,FINSEQ_4:def 4
.= ((ParsedTerms X) * ar).x by A8,FUNCT_1:22;
hence thesis by A5,A7,A8;
end;
hence thesis by A6,A7,CARD_3:18;
end;
theorem Th7:
for S be OrderSortedSign,
X be non-empty ManySortedSet of S,
o be OperSymbol of S,
p be FinSequence of TS(DTConOSA(X)) holds
OSSym(o,X) ==> roots p iff p in ((ParsedTerms X)# * (the Arity of S)).o
proof
let S be OrderSortedSign,
X be non-empty ManySortedSet of S,
o be OperSymbol of S,
p be FinSequence of TS(DTConOSA(X));
set D = DTConOSA(X),
ar = the_arity_of o;
A1: Union (coprod X) misses [:the OperSymbols of S,{the carrier of S}:]
by MSAFREE:4;
A2: OSSym(o,X) = [o,the carrier of S] by Def6;
A3: D = DTConstrStr (#
[:the OperSymbols of S,{the carrier of S}:] \/
Union (coprod (X qua ManySortedSet of S)), OSREL(X) #) &
(Terminals (DTConOSA(X))) = Union (coprod X) &
NonTerminals(DTConOSA(X)) = [:the OperSymbols of S,{the carrier of S}:]
by Def5,Th3;
thus OSSym(o,X) ==> roots p implies
p in ((ParsedTerms X)# * (the Arity of S)).o
proof
assume OSSym(o,X) ==> roots p;
then A4: [[o,the carrier of S],roots p] in OSREL(X) by A2,A3,LANG1:def 1;
then reconsider r = roots p as
Element of
([:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X))*
by ZFMISC_1:106;
A5: len r = len ar &
for x be set st x in dom r holds
(r.x in [:the OperSymbols of S,{the carrier of S}:] implies
for o1 be OperSymbol of S st [o1,the carrier of S] = r.x holds
the_result_sort_of o1 <= ar/.x) &
(r.x in Union (coprod X) implies
ex i being Element of S st
i <= ar/.x & r.x in coprod(i,X)) by A4,Th2;
A6: dom p = dom r by DTCONSTR:def 1;
A7: dom r = Seg len r & Seg len ar = dom ar by FINSEQ_1:def 3;
for n be Nat st n in dom p holds p.n in ParsedTerms(X,ar/.n)
proof let n be Nat;
set s = ar/.n,
A = {a where a is Element of TS D:
(ex s1 being Element of S, x be set st
s1 <= s & x in X.s1 & a = root-tree [x,s1]) or
ex o be OperSymbol of S st
[o,the carrier of S] = a.{} & the_result_sort_of o <= s};
A8: A = ParsedTerms(X,s) by Def7;
assume A9: n in dom p;
then consider T be DecoratedTree such that
A10: T = p.n & r.n = T.{} by DTCONSTR:def 1;
A11: rng r c=
[:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X)
by FINSEQ_1:def 4;
A12: r.n in rng r by A6,A9,FUNCT_1:def 5;
A13: rng p c= TS D by FINSEQ_1:def 4;
p.n in rng p by A9,FUNCT_1:def 5;
then reconsider T as Element of TS(D) by A10,A13;
per cases by A11,A12,XBOOLE_0:def 2;
suppose
A14: r.n in [:the OperSymbols of S,{the carrier of S}:];
then consider o1 being Element of the OperSymbols of S,
x2 being Element of {the carrier of S} such that
A15: r.n = [o1,x2] by DOMAIN_1:9;
A16: x2 = the carrier of S by TARSKI:def 1;
then the_result_sort_of o1 <= ar/.n by A4,A6,A9,A14,A15,Th2;
then ex o be OperSymbol of S
st [o,the carrier of S] = T.{} & the_result_sort_of o <= s
by A10,A15,A16;
hence thesis by A8,A10;
suppose A17: r.n in Union (coprod X);
then consider i being Element of S such that
A18: i <= ar/.n & r.n in coprod(i,X) by A4,A6,A9,Th2;
consider a be set such that
A19: a in X.i & r.n = [a,i] by A18,MSAFREE:def 2;
reconsider t = r.n as Terminal of D by A17,Th3;
T = root-tree t by A10,DTCONSTR:9;
hence thesis by A8,A10,A18,A19;
end;
hence thesis by A5,A6,A7,Th6;
end;
set r = roots p,
OU = [:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X);
assume A20: p in ((ParsedTerms X)# * (the Arity of S)).o;
then A21: dom p = dom ar &
for n be Nat st n in dom p holds p.n in ParsedTerms(X,ar/.n) by Th6;
A22: dom p = dom r by DTCONSTR:def 1;
A23: dom r = Seg len r & Seg len ar = dom ar by FINSEQ_1:def 3;
rng r c= [:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X)
proof
let x be set;
assume x in rng r;
then consider n be set such that
A24: n in dom r & r.n = x by FUNCT_1:def 5;
reconsider n as Nat by A24;
set s = ar/.n,
A = {a where a is Element of TS D:
(ex s1 being Element of S, x be set st
s1 <= s & x in X.s1 & a = root-tree [x,s1]) or
ex o be OperSymbol of S st [o,the carrier of S] = a.{}
& the_result_sort_of o <= s};
A25: A = ParsedTerms(X,s) by Def7;
p.n in ParsedTerms(X,s) by A20,A22,A24,Th6;
then consider a be Element of TS D such that
A26: a = p.n and
A27: (ex s1 being Element of S, x be set st
s1 <= s & x in X.s1 & a = root-tree [x,s1]) or
ex o be OperSymbol of S st [o,the carrier of S] = a.{} &
the_result_sort_of o <= s by A25;
consider T be DecoratedTree such that
A28: T = p.n & r.n = T.{} by A22,A24,DTCONSTR:def 1;
per cases by A27;
suppose ex s1 being Element of S, x be set st
s1 <= s & x in X.s1 & a = root-tree [x,s1];
then consider s1 being Element of S, y be set such that
A29: s1 <= s & y in X.s1 & a = root-tree [y,s1];
A30: a.{} = [y,s1] by A29,TREES_4:3;
A31: [y,s1] in coprod(s1,X) by A29,MSAFREE:def 2;
dom coprod(X) = the carrier of S by PBOOLE:def 3;
then (coprod(X)).s1 in rng coprod(X) by FUNCT_1:def 5;
then coprod(s1,X) in rng coprod(X) by MSAFREE:def 3;
then [y,s1] in union rng coprod(X) by A31,TARSKI:def 4;
then [y,s1] in Union (coprod X) by PROB_1:def 3;
hence thesis by A24,A26,A28,A30,XBOOLE_0:def 2;
suppose ex o be OperSymbol of S st [o,the carrier of S] = a.{}
& the_result_sort_of o <= s;
then consider o1 be OperSymbol of S such that
A32: [o1,the carrier of S] = a.{} & the_result_sort_of o1 <= s;
the carrier of S in {the carrier of S} by TARSKI:def 1;
then [o1,the carrier of S] in [:the OperSymbols of S,{the carrier of S}
:]
by ZFMISC_1:106;
hence thesis by A24,A26,A28,A32,XBOOLE_0:def 2;
end;
then reconsider r as FinSequence of OU by FINSEQ_1:def 4;
reconsider r as Element of OU* by FINSEQ_1:def 11;
A33: len r = len ar by A21,A22,A23,FINSEQ_1:8;
for x be set st x in dom r holds
(r.x in [:the OperSymbols of S,{the carrier of S}:] implies
for o1 be OperSymbol of S st [o1,the carrier of S] = r.x
holds the_result_sort_of o1 <= ar/.x) &
(r.x in Union (coprod X) implies
ex i being Element of S st
i <= ar/.x &
r.x in coprod(i,X))
proof
let x be set;
assume A34: x in dom r;
then reconsider n = x as Nat;
set s = ar/.n,
A = {a where a is Element of TS D:
(ex s1 being Element of S, x be set st
s1 <= s & x in X.s1 & a = root-tree [x,s1]) or
ex o be OperSymbol of S st
[o,the carrier of S] = a.{} & the_result_sort_of o <= s};
A35: A = ParsedTerms(X,s) by Def7;
p.n in ParsedTerms(X,s) by A20,A22,A34,Th6;
then consider a be Element of TS D such that
A36: a = p.n and
A37: (ex s1 being Element of S, x be set st
s1 <= s & x in X.s1 & a = root-tree [x,s1]) or
ex o be OperSymbol of S st [o,the carrier of S] = a.{}
& the_result_sort_of o <= s by A35;
consider T be DecoratedTree such that
A38: T = p.n & r.n = T.{} by A22,A34,DTCONSTR:def 1;
thus r.x in [:the OperSymbols of S,{the carrier of S}:] implies
for o1 be OperSymbol of S st [o1,the carrier of S] = r.x holds
the_result_sort_of o1 <= ar/.x
proof
assume A39: r.x in [:the OperSymbols of S,{the carrier of S}:];
let o1 be OperSymbol of S;
assume A40: [o1,the carrier of S] = r.x;
now given s1 being Element of S, y be set such that
A41: s1 <= s & y in X.s1 & a = root-tree [y,s1];
A42: r.x = [y,s1] by A36,A38,A41,TREES_4:3;
A43: [y,s1] in coprod(s1,X) by A41,MSAFREE:def 2;
dom coprod(X) = the carrier of S by PBOOLE:def 3;
then (coprod(X)).s1 in rng coprod(X) by FUNCT_1:def 5;
then coprod(s1,X) in rng coprod(X) by MSAFREE:def 3;
then r.x in union rng coprod(X) by A42,A43,TARSKI:def 4;
then r.x in Union (coprod X) by PROB_1:def 3;
hence contradiction by A1,A39,XBOOLE_0:3;
end;
then consider o2 be OperSymbol of S such that
A44: [o2,the carrier of S] = a.{} & the_result_sort_of o2 <= s by A37;
thus thesis by A36,A38,A40,A44,ZFMISC_1:33;
end;
assume A45: r.x in Union (coprod X);
now given o1 be OperSymbol of S such that
A46: [o1,the carrier of S] = a.{} & the_result_sort_of o1 <= s;
the carrier of S in {the carrier of S} by TARSKI:def 1;
then [o1,the carrier of S] in [:the OperSymbols of S,{the carrier of
S}:]
by ZFMISC_1:106;
hence contradiction by A1,A36,A38,A45,A46,XBOOLE_0:3;
end;
then consider s1 being Element of S, y be set such that
A47: s1 <= s & y in X.s1 & a = root-tree [y,s1] by A37;
A48: r.x = [y,s1] by A36,A38,A47,TREES_4:3;
take s1;
thus thesis by A47,A48,MSAFREE:def 2;
end;
then [[o,the carrier of S],r] in OSREL X by A33,Th2;
hence thesis by A2,A3,LANG1:def 1;
end;
theorem Th8:
for S be OrderSortedSign,
X be non-empty ManySortedSet of S holds
union rng (ParsedTerms X) = TS (DTConOSA(X))
proof
let S be OrderSortedSign,
X be non-empty ManySortedSet of S;
set D = DTConOSA(X);
A1: dom (ParsedTerms X) = the carrier of S &
dom (coprod X) = the carrier of S by PBOOLE:def 3;
thus union rng (ParsedTerms X) c= TS D
proof
let x; assume x in union rng (ParsedTerms X);
then consider A be set such that
A2: x in A & A in rng (ParsedTerms X) by TARSKI:def 4;
consider s be set such that
A3: s in dom (ParsedTerms X) & (ParsedTerms X).s = A by A2,FUNCT_1:def 5;
reconsider s as Element of S by A3,PBOOLE:def 3;
A = ParsedTerms(X,s) by A3,Def8
.= {a where a is Element of TS(D):
(ex s1 being Element of S, x be set st
s1 <= s & x in X.s1 & a = root-tree [x,s1]) or
ex o1 be OperSymbol of S st
[o1,the carrier of S] = a.{} & the_result_sort_of o1 <= s}
by Def7;
then consider a be Element of TS(D) such that
A4: a = x and
(ex s1 being Element of S, x be set st
s1 <= s & x in X.s1 & a = root-tree [x,s1]) or
ex o1 be OperSymbol of S st
[o1,the carrier of S]=a.{} & the_result_sort_of o1 <= s by A2;
thus thesis by A4;
end;
let x;
assume x in TS D;
then reconsider t = x as Element of TS(D);
A5: rng t c= the carrier of D by TREES_2:def 9;
{} in dom t by TREES_1:47;
then A6: t.{} in rng t by FUNCT_1:def 5;
A7: the carrier of D = (Terminals D) \/ (NonTerminals D) by LANG1:1;
A8: Terminals D = Union (coprod X) &
NonTerminals D = [:the OperSymbols of S,{the carrier of S}:] by Th3;
per cases by A5,A6,A7,XBOOLE_0:def 2;
suppose A9: t.{} in Terminals D;
then reconsider a = t.{} as Terminal of D;
A10: t = root-tree a by DTCONSTR:9;
a in union rng(coprod X) by A8,A9,PROB_1:def 3;
then consider A be set such that
A11: a in A & A in rng(coprod X) by TARSKI:def 4;
consider s be set such that
A12: s in dom(coprod X) & (coprod X).s = A by A11,FUNCT_1:def 5;
reconsider s as Element of S by A12,PBOOLE:def 3;
A = coprod(s,X) by A12,MSAFREE:def 3;
then consider b be set such that
A13: b in X.s & a = [b,s] by A11,MSAFREE:def 2;
t in {aa where aa is Element of TS(D):
(ex s1 being Element of S, x be set st
s1 <= s & x in X.s1 & aa = root-tree [x,s1]) or
ex o1 be OperSymbol of S st
[o1,the carrier of S] =aa.{} & the_result_sort_of o1 <= s} by A10,A13
;
then t in ParsedTerms(X,s) by Def7;
then A14: t in (ParsedTerms X).s by Def8;
(ParsedTerms X).s in rng (ParsedTerms X) by A1,FUNCT_1:def 5;
hence thesis by A14,TARSKI:def 4;
suppose t.{} in NonTerminals D;
then reconsider a = t.{} as NonTerminal of D;
consider o being Element of the OperSymbols of S,
x2 being Element of {the carrier of S} such that
A15: a = [o,x2] by A8,DOMAIN_1:9;
A16: x2 = the carrier of S by TARSKI:def 1;
set rs = the_result_sort_of o;
t in {aa where aa is Element of TS(D):
(ex s1 being Element of S, x be set st
s1 <= rs & x in X.s1 & aa = root-tree [x,s1]) or
ex o1 be OperSymbol of S st
[o1,the carrier of S] =aa.{} & the_result_sort_of o1 <= rs}
by A15,A16;
then t in ParsedTerms(X,rs) by Def7;
then A17: t in (ParsedTerms X).rs by Def8;
(ParsedTerms X).rs in rng (ParsedTerms X) by A1,FUNCT_1:def 5;
hence thesis by A17,TARSKI:def 4;
end;
definition
let S be OrderSortedSign,
X be non-empty ManySortedSet of S,
o be OperSymbol of S;
func PTDenOp(o,X) ->
Function of ((ParsedTerms X)# * (the Arity of S)).o,
((ParsedTerms X) * (the ResultSort of S)).o means:Def9:
for p be FinSequence of TS(DTConOSA(X)) st OSSym(o,X) ==> roots p holds
it.p = (OSSym(o,X))-tree p;
existence
proof
set AL = ((ParsedTerms X)# * (the Arity of S)).o,
AX = ((ParsedTerms X) * (the ResultSort of S)).o,
D = DTConOSA(X),
O = the OperSymbols of S,
rs = the_result_sort_of o,
RS = the ResultSort of S;
defpred P[set,set] means
for p be FinSequence of TS D st p = $1 holds $2 = (OSSym(o,X))-tree p;
A1: for x be set st x in AL ex y be set st y in AX & P[x,y]
proof
let x be set;
assume A2: x in AL;
then reconsider p = x as FinSequence of TS(D) by Th5;
take y = (OSSym(o,X))-tree p;
o in O;
then o in dom ((ParsedTerms X) * RS) by PBOOLE:def 3;
then A3: AX =(ParsedTerms X).(RS.o) by FUNCT_1:22
.= (ParsedTerms X).rs by MSUALG_1:def 7
.= ParsedTerms(X,rs) by Def8;
set A = {a where a is Element of TS(D):
(ex s1 being Element of S, x be set st
s1 <= rs & x in X.s1 & a = root-tree [x,s1]) or
ex o1 be OperSymbol of S st
[o1,the carrier of S] = a.{} & the_result_sort_of o1 <= rs};
A4: A = AX by A3,Def7;
OSSym(o,X) ==> roots p by A2,Th7;
then reconsider a = (OSSym(o,X))-tree p as Element of TS D by DTCONSTR:def
4;
(ex q being DTree-yielding FinSequence st p = q & dom a = tree doms q) &
a.{} = OSSym(o,X) & for n be Nat st n < len p holds a|<*n*> = p.(n+1)
by TREES_4:def 4;
then consider q being DTree-yielding FinSequence such that
A5: p = q & dom a = tree doms q &
a.{} = OSSym(o,X) &
for n be Nat st n < len p holds a|<*n*> = p.(n+1);
OSSym(o,X) = [o,the carrier of S] by Def6;
hence y in AX by A4,A5;
thus P[x,y];
end;
consider f be Function such that
A6: dom f = AL & rng f c= AX &
for x be set st x in AL holds P[x,f.x] from NonUniqBoundFuncEx(A1);
reconsider g = f as Function of AL,rng f by A6,FUNCT_2:3;
reconsider g as Function of AL,AX by A6,FUNCT_2:4;
take g;
let p be FinSequence of TS D;
assume OSSym(o,X) ==> roots p;
then p in AL by Th7;
hence thesis by A6;
end;
uniqueness
proof
set AL = ((ParsedTerms X)# * (the Arity of S)).o,
AX = ((ParsedTerms X) * (the ResultSort of S)).o,
D = DTConOSA(X);
let f,g be Function of AL, AX; assume that
A7: for p be FinSequence of TS D st OSSym(o,X) ==> roots p holds
f.p = (OSSym(o,X))-tree p and
A8: for p be FinSequence of TS D st OSSym(o,X) ==> roots p holds
g.p = (OSSym(o,X))-tree p;
A9: dom f = AL & dom g = AL by FUNCT_2:def 1;
for x be set st x in AL holds f.x = g.x
proof
let x be set;
assume A10: x in AL;
then reconsider p = x as FinSequence of TS(D) by Th5;
OSSym(o,X) ==> roots p by A10,Th7;
then f.p = (OSSym(o,X))-tree p & g.p = (OSSym(o,X))-tree p by A7,A8;
hence thesis;
end;
hence thesis by A9,FUNCT_1:9;
end;
end;
definition
let S be OrderSortedSign,
X be non-empty ManySortedSet of S;
func PTOper(X) ->
ManySortedFunction of (ParsedTerms X)# * (the Arity of S),
(ParsedTerms X) * (the ResultSort of S) means :Def10:
for o be OperSymbol of S holds it.o = PTDenOp(o,X);
existence
proof
set Y = the OperSymbols of S;
defpred P[set,set] means
for o be OperSymbol of S st $1 = o holds $2 = PTDenOp(o,X);
A1: for x be set st x in Y ex y be set st P[x,y]
proof
let x be set;
assume x in Y;
then reconsider o = x as OperSymbol of S;
take PTDenOp(o,X);
thus thesis;
end;
consider f be Function such that
A2: dom f = Y & for x be set st x in
Y holds P[x,f.x] from NonUniqFuncEx(A1);
reconsider f as ManySortedSet of Y by A2,PBOOLE:def 3;
for x be set st x in dom f holds f.x is Function
proof
let x be set;
assume x in dom f;
then reconsider o = x as OperSymbol of S by A2;
f.o = PTDenOp(o,X) by A2;
hence thesis;
end;
then reconsider f as ManySortedFunction of Y by PRALG_1:def 15;
for x be set st x in Y holds f.x is Function of
((ParsedTerms X)# * (the Arity of S)).x,
((ParsedTerms X) * (the ResultSort of S)).x
proof
let x be set;
assume x in Y;
then reconsider o = x as OperSymbol of S;
f.o = PTDenOp(o,X) by A2;
hence thesis;
end;
then reconsider f as ManySortedFunction of (ParsedTerms X)# * (the Arity of
S),
(ParsedTerms X) * (the ResultSort of S) by MSUALG_1:def 2;
take f;
let o be OperSymbol of S;
thus thesis by A2;
end;
uniqueness
proof
let A,B be ManySortedFunction of
(ParsedTerms X)# * (the Arity of S),
(ParsedTerms X) * (the ResultSort of S);
assume that A3: for o be OperSymbol of S holds A.o = PTDenOp(o,X) and
A4: for o be OperSymbol of S holds B.o = PTDenOp(o,X);
for i be set st i in the OperSymbols of S holds A.i = B.i
proof
let i be set;
assume i in the OperSymbols of S;
then reconsider s = i as OperSymbol of S;
A.s = PTDenOp(s,X) & B.s = PTDenOp(s,X) by A3,A4;
hence thesis;
end;
hence thesis by PBOOLE:3;
end;
end;
definition
let S be OrderSortedSign,
X be non-empty ManySortedSet of S;
func ParsedTermsOSA(X) -> OSAlgebra of S equals :Def11:
MSAlgebra (# ParsedTerms(X), PTOper(X) #);
coherence by OSALG_1:17;
end;
definition
let S be OrderSortedSign,
X be non-empty ManySortedSet of S;
cluster ParsedTermsOSA(X) -> strict non-empty;
coherence
proof
MSAlgebra (# ParsedTerms(X), PTOper(X) #) = ParsedTermsOSA X by Def11;
hence thesis by MSUALG_1:def 8;
end;
end;
definition
let S be OrderSortedSign;
let X be non-empty ManySortedSet of S;
let o be OperSymbol of S;
redefine func OSSym(o, X) -> NonTerminal of DTConOSA X;
coherence
proof
A1: OSSym(o, X) = [o,the carrier of S] &
NonTerminals DTConOSA X = [:the OperSymbols of S,{the carrier of S}:]
by Def6,Th3;
the carrier of S in { the carrier of S } by TARSKI:def 1;
hence thesis by A1,ZFMISC_1:106;
end;
end;
theorem Th9:
for S being OrderSortedSign,
X being non-empty ManySortedSet of S,
s being Element of S holds
(the Sorts of ParsedTermsOSA(X)).s =
{a where a is Element of TS(DTConOSA(X)):
(ex s1 being Element of S, x be set st
s1 <= s & x in X.s1 & a = root-tree [x,s1]) or
ex o be OperSymbol of S st [o,the carrier of S] = a.{}
& the_result_sort_of o <= s}
proof
let S being OrderSortedSign,
X being non-empty ManySortedSet of S,
s being Element of S;
set PTA = ParsedTermsOSA(X);
A1: PTA = MSAlgebra (# ParsedTerms(X), PTOper(X) #) by Def11;
{a where a is Element of TS(DTConOSA(X)):
(ex s1 being Element of S, x be set st
s1 <= s & x in X.s1 & a = root-tree [x,s1]) or
ex o be OperSymbol of S st [o,the carrier of S] = a.{}
& the_result_sort_of o <= s}
= ParsedTerms(X,s) by Def7 .= (the Sorts of PTA).s by A1,Def8;
hence thesis;
end;
theorem Th10:
for S being OrderSortedSign,
X being non-empty ManySortedSet of S,
s,s1 being Element of S,
x being set st x in X.s holds
root-tree [x,s] is Element of TS DTConOSA(X) &
( for z being set holds
[z,the carrier of S] <> (root-tree [x,s]).{} ) &
( root-tree [x,s] in (the Sorts of ParsedTermsOSA(X)).s1
iff s <= s1 )
proof
let S be OrderSortedSign,
X be non-empty ManySortedSet of S,
s,s1 be Element of S,
x be set such that A1: x in X.s;
set PTA = ParsedTermsOSA(X),
D = DTConOSA(X);
reconsider s0 = s, s1_1 = s1 as Element of S;
reconsider SPTA = the Sorts of PTA as OrderSortedSet of S by OSALG_1:17;
reconsider t = [x,s] as Terminal of D by A1,Th4;
root-tree t is Element of TS D;
hence root-tree [x,s] is Element of TS D;
root-tree t in {a where a is Element of TS(DTConOSA(X)):
(ex s1 being Element of S, x be set st
s1 <= s & x in X.s1 & a = root-tree [x,s1]) or
ex o be OperSymbol of S st [o,the carrier of S] = a.{}
& the_result_sort_of o <= s} by A1;
then A2: root-tree [x,s] in SPTA.s0 by Th9;
thus A3: for z being set holds
[z,the carrier of S] <> (root-tree [x,s]).{}
proof let z be set;
A4: (root-tree [x,s]).{} = [x,s] by TREES_4:3;
assume [z,the carrier of S] = (root-tree [x,s]).{};
then s = the carrier of S by A4,ZFMISC_1:33;
then s in s;
hence contradiction;
end;
hereby
assume root-tree [x,s] in (the Sorts of PTA).s1;
then root-tree [x,s] in {a where a is Element of TS(DTConOSA(X)):
(ex s2 being Element of S, x be set st
s2 <= s1 & x in X.s2 & a = root-tree [x,s2]) or
ex o be OperSymbol of S st [o,the carrier of S] = a.{}
& the_result_sort_of o <= s1} by Th9;
then consider a being Element of TS D such that
A5: a = root-tree [x,s] and
A6: (ex s2 being Element of S, x be set st
s2 <= s1 & x in X.s2 & a = root-tree [x,s2]) or
ex o be OperSymbol of S st [o,the carrier of S] = a.{}
& the_result_sort_of o <= s1;
consider s2 being Element of S,x1 be set such that
A7: s2 <= s1 & x1 in X.s2 & a = root-tree [x1,s2] by A3,A5,A6;
[x1,s2] = [x,s] by A5,A7,TREES_4:4;
hence s <= s1 by A7,ZFMISC_1:33;
end;
assume s <= s1;
then SPTA.s0 c= SPTA.s1_1 by OSALG_1:def 18;
hence thesis by A2;
end;
theorem Th11:
for S being OrderSortedSign,
X being non-empty ManySortedSet of S,
t being Element of TS (DTConOSA X),
o being OperSymbol of S st t.{} = [o,the carrier of S] holds
(ex p being SubtreeSeq of OSSym(o,X) st
t = OSSym(o,X)-tree p & OSSym(o,X) ==> roots p &
p in Args(o,ParsedTermsOSA(X)) &
t = Den(o,ParsedTermsOSA(X)).p ) &
( for s2 being Element of S, x being set holds
t <> root-tree [x,s2] ) &
for s1 being Element of S holds
t in (the Sorts of ParsedTermsOSA(X)).s1
iff the_result_sort_of o <= s1
proof
let S be OrderSortedSign,
X be non-empty ManySortedSet of S,
t be Element of TS (DTConOSA X),
o be OperSymbol of S such that
A1: t.{} = [o,the carrier of S];
set G = DTConOSA X, PTA = ParsedTermsOSA(X);
A2: PTA = MSAlgebra (# ParsedTerms(X), PTOper(X) #) by Def11;
reconsider SPTA = the Sorts of PTA as OrderSortedSet of S by OSALG_1:17;
[o,the carrier of S] = OSSym(o, X) by Def6;
then consider p being FinSequence of TS G such that
A3: t = OSSym(o,X)-tree p & OSSym(o,X) ==> roots p by A1,DTCONSTR:10;
reconsider p as SubtreeSeq of OSSym(o,X) by A3,DTCONSTR:def 9;
p in ((ParsedTerms X)# * (the Arity of S)).o by A3,Th7;
then A4: p in Args(o,ParsedTermsOSA(X)) by A2,MSUALG_1:def 9;
Den(o,PTA).p = ((the Charact of PTA).o).p
by MSUALG_1:def 11
.= PTDenOp(o,X).p by A2,Def10
.= t by A3,Def9;
hence ex p being SubtreeSeq of OSSym(o,X) st
t = OSSym(o,X)-tree p & OSSym(o,X) ==> roots p &
p in Args(o,ParsedTermsOSA(X)) &
t = Den(o,ParsedTermsOSA(X)).p by A3,A4;
set s = the_result_sort_of o;
t in {a where a is Element of TS(DTConOSA(X)):
(ex s1 being Element of S, x be set st
s1 <= s & x in X.s1 & a = root-tree [x,s1]) or
ex o be OperSymbol of S st [o,the carrier of S] = a.{}
& the_result_sort_of o <= s} by A1;
then A5: t in SPTA.s by Th9;
thus A6: for s2 being Element of S, x being set
holds t <> root-tree [x,s2]
proof let s2 be Element of S, x be set;
assume t = root-tree [x,s2];
then [x,s2] = [o, the carrier of S] by A1,TREES_4:3;
then s2 = the carrier of S by ZFMISC_1:33;
then s2 in s2;
hence contradiction;
end;
let s1 be Element of S;
reconsider s0 = s, s1_1 = s1 as Element of S;
hereby
assume t in (the Sorts of PTA).s1;
then t in {a where a is Element of TS(DTConOSA(X)):
(ex s2 being Element of S, x be set st
s2 <= s1 & x in X.s2 & a = root-tree [x,s2]) or
ex o be OperSymbol of S st [o,the carrier of S] = a.{}
& the_result_sort_of o <= s1} by Th9;
then consider a being Element of TS DTConOSA(X) such that
A7: a = t and
A8: (ex s2 being Element of S, x be set st
s2 <= s1 & x in X.s2 & a = root-tree [x,s2]) or
ex o be OperSymbol of S st [o,the carrier of S] = a.{}
& the_result_sort_of o <= s1;
consider o1 being OperSymbol of S such that
A9: [o1,the carrier of S] = a.{}
& the_result_sort_of o1 <= s1 by A6,A7,A8;
thus s <= s1 by A1,A7,A9,ZFMISC_1:33;
end;
assume the_result_sort_of o <= s1;
then SPTA.s0 c= SPTA.s1_1 by OSALG_1:def 18;
hence thesis by A5;
end;
theorem Th12:
for S being OrderSortedSign,
X being non-empty ManySortedSet of S,
nt being Symbol of DTConOSA(X),
ts being FinSequence of TS(DTConOSA(X)) st
nt ==> roots ts holds
nt in NonTerminals DTConOSA(X) &
nt-tree ts in TS DTConOSA(X) &
ex o being OperSymbol of S st nt = [o,the carrier of S] &
ts in Args(o,ParsedTermsOSA(X)) &
nt-tree ts = Den(o,ParsedTermsOSA(X)).ts &
for s1 being Element of S holds
nt-tree ts in (the Sorts of ParsedTermsOSA(X)).s1
iff the_result_sort_of o <= s1
proof
let S be OrderSortedSign,
X be non-empty ManySortedSet of S,
nt be Symbol of DTConOSA(X),
ts be FinSequence of TS(DTConOSA(X)) such that
A1: nt ==> roots ts;
set D = DTConOSA(X),
PTA = ParsedTermsOSA(X);
A2: nt in { s where s is Symbol of D:
ex n being FinSequence st s ==> n} by A1;
hence nt in NonTerminals D by LANG1:def 3;
then nt in [:the OperSymbols of S,{the carrier of S}:] by Th3;
then consider o1,b1 being set such that
A3: o1 in the OperSymbols of S &
b1 in {the carrier of S} & nt = [o1,b1] by ZFMISC_1:def 2;
reconsider o1 as OperSymbol of S by A3;
reconsider nt1 = nt as NonTerminal of D by A2,LANG1:def 3;
reconsider ts1 = ts as SubtreeSeq of nt1 by A1,DTCONSTR:def 9;
nt1-tree ts1 in TS D;
hence nt-tree ts in TS DTConOSA(X);
A4: b1 = the carrier of S by A3,TARSKI:def 1;
take o1;
thus nt = [o1,the carrier of S] by A3,TARSKI:def 1;
A5: (nt1-tree ts).{} = [o1,the carrier of S] by A3,A4,TREES_4:def 4;
then consider p being SubtreeSeq of OSSym(o1,X) such that
A6: (nt1-tree ts1) = OSSym(o1,X)-tree p &
OSSym(o1,X) ==> roots p &
p in Args(o1,PTA) &
(nt1-tree ts1) = Den(o1,PTA).p by Th11;
thus thesis by A5,A6,Th11,TREES_4:15;
end;
:: Element of Args is FinSequence (if clusters MSUALG_9)
theorem Th13:
for S being OrderSortedSign,
X being non-empty ManySortedSet of S, o be OperSymbol of S,
x being FinSequence holds
x in Args(o,ParsedTermsOSA(X)) iff
x is FinSequence of TS(DTConOSA(X)) &
OSSym(o,X) ==> roots x
proof
let S be OrderSortedSign,
X be non-empty ManySortedSet of S, o be OperSymbol of S,
x be FinSequence;
set PTA = ParsedTermsOSA(X);
A1: PTA = MSAlgebra(# ParsedTerms(X), PTOper(X) #) by Def11;
hereby assume A2: x in Args(o,PTA);
then A3: x in ((the Sorts of PTA)# * the Arity of S).o by MSUALG_1:def 9;
A4: x in ((ParsedTerms X)# * (the Arity of S)).o by A1,A2,MSUALG_1:def 9;
thus x is FinSequence of TS(DTConOSA(X)) by A1,A3,Th5;
reconsider x1 = x as FinSequence of TS(DTConOSA(X)) by A4,Th5;
OSSym(o,X) ==> roots x1 by A1,A3,Th7;
hence OSSym(o,X) ==> roots x;
end;
assume A5: x is FinSequence of TS(DTConOSA(X)) &
OSSym(o,X) ==> roots x;
then reconsider x1 = x as FinSequence of TS(DTConOSA(X));
x1 in ((ParsedTerms X)# * (the Arity of S)).o by A5,Th7;
hence thesis by A1,MSUALG_1:def 9;
end;
theorem Th14:
for S be OrderSortedSign,
X be non-empty ManySortedSet of S,
t be Element of TS DTConOSA(X)
ex s being SortSymbol of S st
t in (the Sorts of ParsedTermsOSA(X)).s &
for s1 being Element of S st
t in (the Sorts of ParsedTermsOSA(X)).s1 holds
s <= s1
proof
let S be OrderSortedSign,
X be non-empty ManySortedSet of S,
t be Element of TS DTConOSA(X);
set D = DTConOSA(X);
defpred P[set] means
ex s being SortSymbol of S st
$1 in (the Sorts of ParsedTermsOSA(X)).s &
for s1 being Element of S st
$1 in (the Sorts of ParsedTermsOSA(X)).s1 holds
s <= s1;
A1: for s being Symbol of D st s in Terminals D holds P[root-tree s]
proof
let sy be Symbol of D such that A2: sy in Terminals D;
consider s being Element of S, x being set
such that A3: x in X.s & sy = [x,s] by A2,Th4;
reconsider s as SortSymbol of S;
take s;
thus thesis by A3,Th10;
end;
A4: for nt being Symbol of D,
ts being FinSequence of TS(D) st nt ==> roots ts &
for t being DecoratedTree of the carrier of D st t in rng ts
holds P[t]
holds P[nt-tree ts]
proof
let nt be Symbol of D,
ts be FinSequence of TS(D) such that
A5: nt ==> roots ts and
for t being DecoratedTree of the carrier of D
st t in rng ts holds P[t];
consider o being OperSymbol of S such that
nt = [o,the carrier of S] &
ts in Args(o,ParsedTermsOSA(X)) &
nt-tree ts = Den(o,ParsedTermsOSA(X)).ts and
A6: for s1 being Element of S holds
nt-tree ts in (the Sorts of ParsedTermsOSA(X)).s1
iff the_result_sort_of o <= s1 by A5,Th12;
reconsider s = the_result_sort_of o as SortSymbol of S;
take s;
thus thesis by A6;
end;
for t being DecoratedTree of the carrier of D
st t in TS(D) holds P[t] from DTConstrInd(A1,A4);
hence thesis;
end;
:: this should be done more generally for leastsorted osas (and
:: then remove the LeastSorts func), however, it is better here
:: to have it defined for terms (and not Elements of osa)
definition
let S be OrderSortedSign,
X be non-empty ManySortedSet of S,
t be Element of TS DTConOSA(X);
func LeastSort t -> SortSymbol of S means
:Def12: t in (the Sorts of ParsedTermsOSA(X)).it &
for s1 being Element of S st
t in (the Sorts of ParsedTermsOSA(X)).s1 holds
it <= s1;
existence by Th14;
uniqueness
proof
let s2,s3 be SortSymbol of S such that
A1: t in (the Sorts of ParsedTermsOSA(X)).s2 &
for s1 being Element of S st
t in (the Sorts of ParsedTermsOSA(X)).s1 holds
s2 <= s1 and
A2: t in (the Sorts of ParsedTermsOSA(X)).s3 &
for s1 being Element of S st
t in (the Sorts of ParsedTermsOSA(X)).s1 holds
s3 <= s1;
s3 <= s2 & s2 <= s3 by A1,A2;
hence s2 = s3 by ORDERS_1:25;
end;
end;
:: REVISE: the clusters needed to make the def from MSAFREE3 work
:: are too demanding, make it more easily accessible (or include
:: the clusters if it is too hard)
definition
let S be non empty non void ManySortedSign;
let A be non-empty MSAlgebra over S;
mode Element of A is Element of Union the Sorts of A;
canceled;
end;
theorem Th15:
for S being OrderSortedSign,
X being non-empty ManySortedSet of S,
x being set holds
x is Element of ParsedTermsOSA(X) iff
x is Element of TS DTConOSA(X)
proof
let S being OrderSortedSign,
X being non-empty ManySortedSet of S,
x being set;
A1: ParsedTermsOSA(X) = MSAlgebra (# ParsedTerms(X), PTOper(X) #)
by Def11;
TS DTConOSA X = union rng (ParsedTerms X) by Th8
.= Union (the Sorts of ParsedTermsOSA(X)) by A1,PROB_1:def 3;
hence thesis;
end;
theorem Th16:
for S being OrderSortedSign,
X being non-empty ManySortedSet of S,
s be Element of S,
x being set st x in (the Sorts of ParsedTermsOSA(X)).s
holds x is Element of TS DTConOSA(X)
proof
let S being OrderSortedSign,
X being non-empty ManySortedSet of S,
s be Element of S,
x being set such that
A1: x in (the Sorts of ParsedTermsOSA(X)).s;
set PTA = ParsedTermsOSA(X), SPTA = the Sorts of PTA;
s in the carrier of S;
then s in dom SPTA by PBOOLE:def 3;
then SPTA.s in rng SPTA by FUNCT_1:def 5;
then x in union rng SPTA by A1,TARSKI:def 4;
then reconsider x1=x as Element of Union SPTA by PROB_1:def 3;
x1 is Element of PTA;
hence x is Element of TS DTConOSA(X) by Th15;
end;
theorem
for S being OrderSortedSign,
X being non-empty ManySortedSet of S,
s being Element of S,
x being set st x in X.s
for t being Element of TS DTConOSA(X) st t = root-tree [x,s]
holds LeastSort t = s
proof
let S being OrderSortedSign,
X being non-empty ManySortedSet of S,
s being Element of S,
x being set such that A1: x in X.s;
reconsider s2 = s as Element of S;
let t being Element of TS DTConOSA(X) such that
A2: t = root-tree [x,s];
A3: t in (the Sorts of ParsedTermsOSA(X)).s2 by A1,A2,Th10;
for s1 being Element of S st
t in (the Sorts of ParsedTermsOSA(X)).s1 holds s2 <= s1 by A1,A2,Th10;
hence thesis by A3,Def12;
end;
theorem Th18:
for S being OrderSortedSign,
X being non-empty ManySortedSet of S, o be OperSymbol of S,
x being Element of Args(o,ParsedTermsOSA(X)) holds
for t being Element of TS DTConOSA(X)
st t = Den(o,ParsedTermsOSA(X)).x
holds LeastSort t = the_result_sort_of o
proof
let S being OrderSortedSign,
X being non-empty ManySortedSet of S, o be OperSymbol of S,
x being Element of Args(o,ParsedTermsOSA(X));
set PTA = ParsedTermsOSA(X);
A1: OSSym(o,X) = [o,the carrier of S] by Def6;
let t being Element of TS DTConOSA(X) such that
A2: t = Den(o,ParsedTermsOSA(X)).x;
A3: x is FinSequence of TS(DTConOSA(X)) &
OSSym(o,X) ==> roots x by Th13;
reconsider x1 = x as FinSequence of TS(DTConOSA(X)) by Th13;
consider o1 being OperSymbol of S such that
A4: OSSym(o,X) = [o1,the carrier of S] &
x1 in Args(o1,ParsedTermsOSA(X)) &
OSSym(o,X)-tree x1 = Den(o1,ParsedTermsOSA(X)).x1 &
for s1 being Element of S holds
OSSym(o,X)-tree x1 in (the Sorts of ParsedTermsOSA(X)).s1
iff the_result_sort_of o1 <= s1 by A3,Th12;
A5: o = o1 by A1,A4,ZFMISC_1:33;
then t in (the Sorts of PTA).(the_result_sort_of o) by A2,A4;
hence LeastSort t = the_result_sort_of o by A2,A4,A5,Def12;
end;
:: WHY is this necessary??? bug?
definition
let S be OrderSortedSign,
X be non-empty ManySortedSet of S;
let o2 be OperSymbol of S;
cluster Args(o2,ParsedTermsOSA(X)) -> non empty;
coherence;
end;
:: REVISE: was probably needed for casting, but try if
:: LeastSort * x does the work and if so, remove this
definition
let S be locally_directed OrderSortedSign,
X be non-empty ManySortedSet of S,
x be FinSequence of TS DTConOSA(X);
func LeastSorts x -> Element of (the carrier of S)* means
:Def14: dom it = dom x &
for y being Nat st y in dom x holds
ex t being Element of TS DTConOSA(X) st t = x.y &
it.y = LeastSort t;
existence
proof
set D = DTConOSA(X);
defpred P[set,set] means ex t being Element of TS D
st t = $1 & LeastSort t = $2;
A1: for x being set st x in TS D ex y being set st
y in the carrier of S & P[x,y]
proof
let x being set such that A2: x in TS D;
reconsider t = x as Element of TS D by A2;
take LeastSort t;
thus LeastSort t in the carrier of S;
take t;
thus thesis;
end;
consider f being Function of TS D,(the carrier of S) such that
A3: for x being set st x in TS D holds
P[x,f.x] from FuncEx1(A1);
take f*x;
thus dom (f*x) = dom x by ALG_1:1;
A4: rng x c= TS D by FINSEQ_1:def 4;
let y being Nat such that A5: y in dom x;
A6: y in dom (f*x) by A5,ALG_1:1;
x.y in rng x by A5,FUNCT_1:12;
then reconsider t1 = x.y as Element of TS D by A4;
take t1;
thus t1 = x.y;
consider t2 being Element of TS D such that
A7: t2 = t1 & LeastSort t2 = f.t1 by A3;
thus (f*x).y = LeastSort t1 by A6,A7,ALG_1:1;
end;
uniqueness
proof
set D = DTConOSA(X);
let f1,f2 be Element of (the carrier of S)* such that
A8: dom f1 = dom x &
for y being Nat st y in dom x holds
ex t being Element of TS DTConOSA(X) st t = x.y &
f1.y = LeastSort t and
A9: dom f2 = dom x &
for y being Nat st y in dom x holds
ex t being Element of TS DTConOSA(X) st t = x.y &
f2.y = LeastSort t;
for k being Nat st k in dom f1 holds f1.k = f2.k
proof let k be Nat such that A10: k in dom f1;
consider t1 being Element of TS D such that
A11: t1 = x.k & f1.k = LeastSort t1 by A8,A10;
consider t2 being Element of TS D such that
A12: t2 = x.k & f2.k = LeastSort t2 by A8,A9,A10;
thus f1.k = f2.k by A11,A12;
end;
hence f1 = f2 by A8,A9,FINSEQ_1:17;
end;
end;
:: all these should be generalized to any leastsorted osa
theorem Th19:
for S be locally_directed OrderSortedSign,
X be non-empty ManySortedSet of S,
o be OperSymbol of S,
x be FinSequence of TS DTConOSA(X) holds
LeastSorts x <= the_arity_of o iff x in Args(o,ParsedTermsOSA(X))
proof
let S be locally_directed OrderSortedSign,
X be non-empty ManySortedSet of S,
o be OperSymbol of S,
x be FinSequence of TS DTConOSA(X);
set PTA = ParsedTermsOSA(X), D = DTConOSA(X), w = the_arity_of o,
LSx = LeastSorts x;
A1: dom LSx = dom x &
for y being Nat st y in dom x holds
ex t being Element of TS DTConOSA(X) st t = x.y &
LSx.y = LeastSort t by Def14;
reconsider SPTA = the Sorts of PTA as OrderSortedSet of S by OSALG_1:17;
hereby
assume A2: LeastSorts x <= w;
then len LSx = len w &
for i being set st i in dom LSx
for s1,s2 being Element of S st s1 = LSx.i & s2 = w.i
holds s1 <= s2 by OSALG_1:def 7;
then A3: dom LSx = dom w & len x = len w by A1,FINSEQ_3:31;
for k be Nat st k in dom x holds
x.k in (the Sorts of PTA).(w/.k)
proof
let k be Nat such that A4: k in dom x;
A5: (w/.k) = w.k by A1,A3,A4,FINSEQ_4:def 4;
reconsider wk = (w/.k) as Element of S;
consider t2 being Element of TS DTConOSA(X) such that
A6: t2 = x.k & LSx.k = LeastSort t2 by A4,Def14;
A7: t2 in (the Sorts of PTA).(LeastSort t2) by Def12;
LeastSort t2 <= wk by A1,A2,A4,A5,A6,OSALG_1:def 7;
then SPTA.(LeastSort t2) c= SPTA.wk by OSALG_1:def 18;
hence x.k in (the Sorts of PTA).(w/.k) by A6,A7;
end;
hence x in Args(o,PTA) by A3,MSAFREE2:7;
end;
assume A8: x in Args(o,PTA);
then A9: dom x = dom w &
for i being Nat st i in dom w
holds x.i in (the Sorts of PTA).(w/.i) by MSUALG_6:2;
hence len LSx = len w by A1,FINSEQ_3:31;
let i be set such that A10: i in dom LSx;
A11: i in dom w & i in dom x by A9,A10,Def14;
reconsider k = i as Nat by A10;
let s1,s2 be Element of S such that
A12: s1 = LSx.i & s2 = w.i;
consider t2 being Element of TS D such that
A13: t2 = x.k & LSx.k = LeastSort t2 by A11,Def14;
A14: w/.k = w.k by A1,A9,A10,FINSEQ_4:def 4;
x.k in (the Sorts of PTA).(w/.k) by A8,A11,MSUALG_6:2;
hence s1 <= s2 by A12,A13,A14,Def12;
end;
definition
cluster locally_directed regular (monotone OrderSortedSign);
existence
proof consider S1 being discrete op-discrete OrderSortedSign;
take S1;
thus thesis;
end;
end;
:: just casting funcs necessary for the usage of schemes,
definition
let S be locally_directed regular (monotone OrderSortedSign),
X be non-empty ManySortedSet of S,
o be OperSymbol of S,
x be FinSequence of TS DTConOSA(X);
assume A1: OSSym(LBound(o,LeastSorts x),X) ==> roots x;
func pi(o,x) -> Element of TS DTConOSA(X) equals
:Def15: OSSym(LBound(o,LeastSorts x),X)-tree x;
correctness by A1,Th12;
end;
definition
let S be locally_directed OrderSortedSign,
X be non-empty ManySortedSet of S,
t be Symbol of DTConOSA(X);
assume A1: ex p be FinSequence st t ==> p;
func @(X,t) -> OperSymbol of S means:Def16:
[it,the carrier of S] = t;
existence
proof
set D = DTConOSA(X),
OU = [:the OperSymbols of S,{the carrier of S}:] \/
Union (coprod (X qua ManySortedSet of S));
consider p be FinSequence such that
A2: t ==> p by A1;
A3: [t,p] in the Rules of D by A2,LANG1:def 1;
A4: D = DTConstrStr (# OU, OSREL(X) #) by Def5;
then reconsider a = t as Element of OU;
reconsider p as Element of OU* by A3,A4,ZFMISC_1:106;
[a,p] in OSREL(X) by A2,A4,LANG1:def 1;
then a in [:the OperSymbols of S,{the carrier of S}:] by Def4;
then consider o being Element of the OperSymbols of S,
x2 being Element of {the carrier of S} such that
A5: a = [o,x2] by DOMAIN_1:9;
take o;
thus thesis by A5,TARSKI:def 1;
end;
uniqueness by ZFMISC_1:33;
end;
definition
let S be OrderSortedSign,
X be non-empty ManySortedSet of S;
let t be Symbol of DTConOSA(X);
assume A1: t in Terminals DTConOSA(X);
func pi t -> Element of TS(DTConOSA(X)) equals
:Def17: root-tree t;
correctness by A1,DTCONSTR:def 4;
end;
:: the least monotone OSCongruence
definition
let S be locally_directed OrderSortedSign,
X be non-empty ManySortedSet of S;
func LCongruence X -> monotone OSCongruence of ParsedTermsOSA(X) means:Def18:
for R be monotone OSCongruence of ParsedTermsOSA(X) holds
it c= R;
existence
proof
:: I could do the equivalence using MSUALG_8:11, but preparing all
:: seems too painful
set PTA = ParsedTermsOSA(X), D = DTConOSA(X), SPTA=the Sorts of PTA;
defpred MC[set,set,set] means
for R being monotone OSCongruence of PTA holds [$1,$2] in R.$3;
deffunc F(set) = {[x,y] where x,y is Element of TS D:
x in SPTA.$1 & y in SPTA.$1 &
for R being monotone OSCongruence of PTA holds [x,y] in R.$1};
consider f being ManySortedSet of the carrier of S such that
A1: for i being set st i in the carrier of S holds
f.i = F(i) from MSSLambda;
A2: for i be set st i in the carrier of S
holds f.i is Equivalence_Relation of SPTA.i
proof
let i be set such that A3: i in the carrier of S;
reconsider s = i as Element of S by A3;
A4: f.i = {[x,y] where x,y is Element of TS D:
x in SPTA.i & y in SPTA.i &
for R being monotone OSCongruence of PTA holds [x,y] in R.i}
by A1,A3;
now let z be set such that A5: z in f.i;
consider x,y being Element of TS D such that
A6: z = [x,y] & x in SPTA.i & y in SPTA.i & MC[x,y,i]
by A4,A5;
thus z in [:SPTA.i,SPTA.i:] by A6,ZFMISC_1:106;
end;
then f.i c= [:SPTA.i,SPTA.i:] by TARSKI:def 3;
then reconsider fi = f.i as Relation of SPTA.i by RELSET_1:def 1;
now let x be set such that A7: x in SPTA.s;
thus [x,x] in fi
proof
reconsider t1 = x as Element of TS D by A7,Th16;
now let R be monotone OSCongruence of PTA;
field(R.s) = SPTA.s by ORDERS_1:97;
then R.s is_reflexive_in SPTA.s by RELAT_2:def 9;
hence [t1,t1] in R.s by A7,RELAT_2:def 1;
end;
hence thesis by A4,A7;
end;
end;
then fi is_reflexive_in SPTA.s by RELAT_2:def 1;
then
A8: dom fi = SPTA.s & field fi = SPTA.s by ORDERS_1:98;
then
A9: fi is total by PARTFUN1:def 4;
now let x,y be set such that
A10: x in SPTA.s & y in SPTA.s & [x,y] in fi;
thus [y,x] in fi
proof reconsider t1=x,t2=y as Element of TS D by A10,Th16;
consider t3,t4 being Element of TS D such that
A11: [t1,t2] = [t3,t4] &
t3 in SPTA.i & t4 in SPTA.i & MC[t3,t4,i] by A4,A10;
now let R be monotone OSCongruence of PTA;
A12: [t1,t2] in R.s by A11;
field(R.s) = SPTA.s by ORDERS_1:97;
then R.s is_symmetric_in SPTA.s by RELAT_2:def 11;
hence [t2,t1] in R.s by A10,A12,RELAT_2:def 3;
end;
hence thesis by A4,A10;
end;
end;
then A13: fi is_symmetric_in SPTA.s by RELAT_2:def 3;
now let x,y,z be set such that
A14: x in SPTA.s & y in SPTA.s & z in SPTA.s &
[x,y] in fi & [y,z] in fi;
thus [x,z] in fi
proof
reconsider t1=x,t2=y,t3=z as Element of TS D by A14,Th16;
consider t4,t5 being Element of TS D such that
A15: [t1,t2] = [t4,t5] &
t4 in SPTA.i & t5 in SPTA.i & MC[t4,t5,i]
by A4,A14;
consider t6,t7 being Element of TS D such that
A16: [t2,t3] = [t6,t7] &
t6 in SPTA.i & t7 in SPTA.i & MC[t6,t7,i]
by A4,A14;
now let R be monotone OSCongruence of PTA;
A17: [t1,t2] in R.s & [t2,t3] in R.s
by A15,A16;
field(R.s) = SPTA.s by ORDERS_1:97;
then R.s is_transitive_in SPTA.s by RELAT_2:def 16;
hence [t1,t3] in R.s by A14,A17,RELAT_2:def 8;
end;
hence thesis by A4,A14;
end;
end;
then fi is_transitive_in SPTA.s by RELAT_2:def 8;
hence f.i is Equivalence_Relation of SPTA.i
by A8,A9,A13,RELAT_2:def 11,def 16;
end;
then for i be set st i in the carrier of S
holds f.i is Relation of SPTA.i,SPTA.i;
then reconsider f as ManySortedRelation of the Sorts of PTA
by MSUALG_4:def 2;
reconsider f as ManySortedRelation of PTA;
for i be set, R be Relation of SPTA.i st
i in the carrier of S & f.i = R holds
R is Equivalence_Relation of SPTA.i by A2;
then f is MSEquivalence_Relation-like by MSUALG_4:def 3;
then reconsider f as MSEquivalence-like ManySortedRelation of PTA
by MSUALG_4:def 5;
f is os-compatible
proof
let s1,s2 being Element of S such that
A18: s1 <= s2;
A19: f.s1 = {[x,y] where x,y is Element of TS D:
x in SPTA.s1 & y in SPTA.s1 & MC[x,y,s1]} by A1;
A20: f.s2 = {[x,y] where x,y is Element of TS D:
x in SPTA.s2 & y in SPTA.s2 & MC[x,y,s2]} by A1;
let x,y being set such that
A21: x in SPTA.s1 & y in SPTA.s1;
hereby assume [x,y] in f.s1;
then consider t1,t2 being Element of TS D such that
A22: [x,y]=[t1,t2] & t1 in SPTA.s1 & t2 in SPTA.s1
& MC[t1,t2,s1] by A19;
now let R be monotone OSCongruence of PTA;
A23: R is os-compatible by OSALG_4:def 3;
[t1,t2] in R.s1 by A22;
then [t1,t2] in R.s2 by A18,A22,A23,OSALG_4:def 1;
hence t1 in SPTA.s2 & t2 in SPTA.s2 & [t1,t2] in R.s2
by ZFMISC_1:106;
end;
hence [x,y] in f.s2 by A20,A22;
end;
assume [x,y] in f.s2;
then consider t1,t2 being Element of TS D such that
A24: [x,y]=[t1,t2] & t1 in SPTA.s2 & t2 in SPTA.s2
& MC[t1,t2,s2] by A20;
A25: x = t1 & y = t2 by A24,ZFMISC_1:33;
now let R be monotone OSCongruence of PTA;
A26: R is os-compatible by OSALG_4:def 3;
[t1,t2] in R.s2 by A24;
hence [t1,t2] in R.s1 by A18,A21,A24,A26,OSALG_4:def 1;
end;
hence [x,y] in f.s1 by A19,A21,A25;
end;
then reconsider f as MSEquivalence-like OrderSortedRelation of PTA
by OSALG_4:def 3;
f is monotone
proof
let o1,o2 being OperSymbol of S such that
A27: o1 <= o2;
set w2 = the_arity_of o2,
rs2 = the_result_sort_of o2;
let x1 being Element of Args(o1,PTA),
x2 being Element of Args(o2,PTA) such that
A28: for y being Nat st y in dom x1 holds
[x1.y,x2.y] in f.(w2/.y);
A29: f.rs2 = {[x,y] where x,y is Element of TS D:
x in SPTA.rs2 & y in SPTA.rs2 & MC[x,y,rs2]} by A1;
set D1 = Den(o1,PTA).x1, D2 = Den(o2,PTA).x2;
now let R be monotone OSCongruence of PTA;
now let y being Nat such that A30: y in dom x1;
A31: f.(w2/.y) = {[x,z] where x,z is Element of TS D:
x in SPTA.(w2/.y) & z in SPTA.(w2/.y) & MC[x,z,w2/.y]} by A1;
[x1.y,x2.y] in f.(w2/.y) by A28,A30;
then consider x,z being Element of TS D such that
A32: [x1.y,x2.y] = [x,z] & x in SPTA.(w2/.y)
& z in SPTA.(w2/.y) & MC[x,z,w2/.y] by A31;
thus [x1.y,x2.y] in R.(w2/.y) by A32;
end;
then [D1,D2] in R.rs2 by A27,OSALG_4:def 28;
then D1 in SPTA.rs2 & D2 in SPTA.rs2 & [D1,D2] in R.rs2
by ZFMISC_1:106;
hence D1 in SPTA.rs2 & D2 in SPTA.rs2 & [D1,D2] in R.rs2
& D1 is Element of TS D & D2 is Element of TS D by Th16;
end;
hence [D1,D2] in f.rs2 by A29;
end;
then reconsider f as monotone (MSEquivalence-like OrderSortedRelation of PTA)
;
take f;
let R be monotone OSCongruence of PTA;
let i be set such that A33: i in the carrier of S;
reconsider s = i as Element of S by A33;
A34: f.s = {[x,y] where x,y is Element of TS D:
x in SPTA.s & y in SPTA.s & MC[x,y,s]} by A1;
let z be set such that A35: z in f.i;
consider x,y being Element of TS D such that
A36: z = [x,y] & x in SPTA.s & y in SPTA.s & MC[x,y,s] by A34,A35;
thus thesis by A36;
end;
uniqueness
proof
set PTA = ParsedTermsOSA(X);
let L1,L2 be monotone OSCongruence of PTA such that
A37: for R be monotone OSCongruence of ParsedTermsOSA(X) holds
L1 c= R and
A38: for R be monotone OSCongruence of ParsedTermsOSA(X) holds
L2 c= R;
L1 c= L2 & L2 c= L1 by A37,A38;
hence thesis by PBOOLE:def 13;
end;
end;
definition
let S be locally_directed OrderSortedSign,
X be non-empty ManySortedSet of S;
func FreeOSA(X) -> strict non-empty monotone OSAlgebra of S equals
:Def19: QuotOSAlg(ParsedTermsOSA(X),LCongruence(X));
correctness;
end;
:: now we need an explicit description of a sufficiently small
:: monotone OSCongruence on PTA; the PTCongruence turns out to
:: be LCongruence on regular signatures, and is also used to describe
:: minimal terms there
:: just casting funcs necessary for the usage of schemes,
:: remove when Frankel behaves better
definition
let S be OrderSortedSign,
X be non-empty ManySortedSet of S;
let t be Symbol of DTConOSA(X);
func @ t -> Subset of [:TS(DTConOSA(X)), the carrier of S:] equals:Def20:
{[root-tree t,s1] where s1 is Element of S:
ex s be Element of S, x be set st
x in X.s & t = [x,s] & s <= s1};
correctness
proof
set RT = {[root-tree t,s1] where s1 is Element of S:
ex s be Element of S, x be set st
x in X.s & t = [x,s] & s <= s1};
RT c= [:TS(DTConOSA(X)), the carrier of S:]
proof
let y be set such that A1: y in RT;
consider s1 being Element of S such that
A2: y = [root-tree t,s1] and
A3: ex s be Element of S, x be set st
x in X.s & t = [x,s] & s <= s1 by A1;
consider s being Element of S, x be set such that
A4: x in X.s & t = [x,s] & s <= s1 by A3;
root-tree [x,s] is Element of TS DTConOSA(X) by A4,Th10;
hence y in [:TS(DTConOSA(X)), the carrier of S:]
by A2,A4,ZFMISC_1:def 2;
end;
hence thesis;
end;
end;
definition
let S be OrderSortedSign,
X be non-empty ManySortedSet of S;
let nt be Symbol of DTConOSA(X),
x be FinSequence of bool [:TS(DTConOSA(X)), the carrier of S:];
func @ (nt,x) -> Subset of [:TS(DTConOSA(X)), the carrier of S:]
equals :Def21:
{[Den(o2,ParsedTermsOSA(X)).x2,s3] where
o2 is OperSymbol of S,
x2 is Element of Args(o2,ParsedTermsOSA(X)),
s3 is Element of S :
( ex o1 being OperSymbol of S st nt = [o1,the carrier of S] &
o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 &
the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3) &
ex w3 being Element of (the carrier of S)* st
dom w3 = dom x &
for y being Nat st y in dom x holds
[x2.y,w3/.y] in x.y
};
correctness
proof
set NT = {[Den(o2,ParsedTermsOSA(X)).x2,s3] where
o2 is OperSymbol of S,
x2 is Element of Args(o2,ParsedTermsOSA(X)),
s3 is Element of S :
( ex o1 being OperSymbol of S st nt = [o1,the carrier of S] &
o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 &
the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3) &
ex w3 being Element of (the carrier of S)* st
dom w3 = dom x &
for y being Nat st y in dom x holds
[x2.y,w3/.y] in x.y
};
NT c= [:TS(DTConOSA(X)), the carrier of S:]
proof
let y be set such that A1: y in NT;
consider o2 being OperSymbol of S,
x2 being Element of Args(o2,ParsedTermsOSA(X)),
s3 being Element of S such that
A2: y = [Den(o2,ParsedTermsOSA(X)).x2,s3] and
( ex o1 being OperSymbol of S st nt = [o1,the carrier of S] &
o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 &
the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3) &
ex w3 being Element of (the carrier of S)* st
dom w3 = dom x &
for y being Nat st y in dom x holds
[x2.y,w3/.y] in x.y
by A1;
A3: x2 is FinSequence of TS(DTConOSA(X)) &
OSSym(o2,X) ==> roots x2 by Th13;
then A4: OSSym(o2,X)-tree x2 in TS DTConOSA(X) by Th12;
consider o being OperSymbol of S such that
A5: OSSym(o2,X) = [o,the carrier of S] &
x2 in Args(o,ParsedTermsOSA(X)) &
OSSym(o2,X)-tree x2 = Den(o,ParsedTermsOSA(X)).x2 &
for s1 being Element of S holds
OSSym(o2,X)-tree x2 in (the Sorts of ParsedTermsOSA(X)).s1
iff the_result_sort_of o <= s1 by A3,Th12;
[o2,the carrier of S] = [o,the carrier of S] by A5,Def6;
then o2 = o by ZFMISC_1:33;
hence y in [:TS(DTConOSA(X)), the carrier of S:]
by A2,A4,A5,ZFMISC_1:def 2;
end;
hence thesis;
end;
end;
:: a bit technical, to create the PTCongruence
definition
let S be locally_directed OrderSortedSign,
X be non-empty ManySortedSet of S;
func PTClasses X -> Function of TS(DTConOSA(X)),
bool [:TS(DTConOSA(X)), the carrier of S:] means
:Def22:
(for t being Symbol of DTConOSA(X) st t in Terminals DTConOSA(X)
holds it.(root-tree t) = @(t) ) &
(for nt being Symbol of DTConOSA(X),
ts being FinSequence of TS(DTConOSA(X)) st nt ==> roots ts
holds it.(nt-tree ts) = @(nt,it * ts) );
existence
proof
set G = DTConOSA(X),
D = bool [:TS(DTConOSA(X)), the carrier of S:];
deffunc TermVal(Symbol of G) = @ $1;
deffunc NTermVal(Symbol of G,FinSequence of TS(G),
FinSequence of D) = @($1,$3);
thus ex f being Function of TS(G), D st
(for t being Symbol of G st t in Terminals G
holds f.(root-tree t) = TermVal(t)) &
(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 DTConstrIndDef;
end;
uniqueness
proof
set G = DTConOSA(X),
D = bool [:TS(DTConOSA(X)), the carrier of S:];
deffunc TermVal(Symbol of G) = @ $1;
deffunc NTermVal(Symbol of G,FinSequence of TS(G),
FinSequence of D) = @($1,$3);
let f1,f2 be Function of TS(DTConOSA(X)),
bool [:TS(DTConOSA(X)), the carrier of S:] such that
A1: (for t being Symbol of DTConOSA(X) st t in Terminals DTConOSA(X)
holds f1.(root-tree t) = TermVal(t) ) &
(for nt being Symbol of DTConOSA(X),
ts being FinSequence of TS(DTConOSA(X)) st nt ==> roots ts
holds f1.(nt-tree ts) = NTermVal(nt, roots ts, f1*ts) ) and
A2: (for t being Symbol of DTConOSA(X) st t in Terminals DTConOSA(X)
holds f2.(root-tree t) = TermVal(t) ) &
(for nt being Symbol of DTConOSA(X),
ts being FinSequence of TS(DTConOSA(X)) st nt ==> roots ts
holds f2.(nt-tree ts) = NTermVal(nt, roots ts, f2 * ts) );
thus f1 = f2 from DTConstrUniqDef(A1,A2);
end;
end;
theorem Th20:
for S be locally_directed OrderSortedSign,
X be non-empty ManySortedSet of S,
t being Element of TS DTConOSA(X)
holds
( for s being Element of S holds
t in (the Sorts of ParsedTermsOSA(X)).s iff
[t,s] in (PTClasses X).t ) &
( for s being Element of S,
y being Element of TS(DTConOSA X) holds
[y,s] in (PTClasses X).t implies [t,s] in (PTClasses X).y )
proof
let S be locally_directed OrderSortedSign,
X be non-empty ManySortedSet of S,
t be Element of TS DTConOSA(X);
set PTA = ParsedTermsOSA(X),
SPTA = the Sorts of PTA,
D = DTConOSA(X),
C = bool [:TS(D), the carrier of S:],
F = PTClasses X;
defpred R1[set] means
for s being Element of S holds
$1 in SPTA.s iff [$1,s] in F.$1;
:: switched to have easier prooving
defpred R2[set] means
for s being Element of S,
y being Element of TS(D) holds
[y,s] in F.$1 implies [$1,s] in F.y;
reconsider SPTA1 = SPTA as OrderSortedSet of S by OSALG_1:17;
A1: for s1,s2 being Element of S st
s1 <= s2 holds SPTA.s1 c= SPTA.s2
proof
let s1,s2 be Element of S such that
A2: s1 <= s2;
reconsider s11 = s1, s21= s2 as Element of S;
SPTA1.s11 c= SPTA1.s21 by A2,OSALG_1:def 18;
hence SPTA.s1 c= SPTA.s2;
end;
defpred P[DecoratedTree of the carrier of D] means R1[$1] & R2[$1];
A3: for s being Symbol of D st s in Terminals D holds
P[root-tree s]
proof let sy be Symbol of D such that A4: sy in Terminals D;
reconsider sy1 = sy as Terminal of D by A4;
consider s being Element of S, x being set
such that A5: x in X.s & sy = [x,s] by A4,Th4;
root-tree sy1 in
{a where a is Element of TS(DTConOSA(X)):
(ex s1 being Element of S, x be set st
s1 <= s & x in X.s1 & a = root-tree [x,s1]) or
ex o be OperSymbol of S st [o,the carrier of S] = a.{}
& the_result_sort_of o <= s} by A5;
then A6: root-tree sy1 in SPTA.s by Th9;
A7: F.(root-tree sy) = @(sy) by A4,Def22 .=
{[root-tree sy,s1] where s1 is Element of S:
ex s2 be Element of S, x be set st
x in X.s2 & sy = [x,s2] & s2 <= s1} by Def20;
thus R1[root-tree sy]
proof
let s1 be Element of S;
hereby
assume root-tree sy in SPTA.s1;
then s <= s1 by A5,Th10;
hence [root-tree sy,s1] in F.(root-tree sy) by A5,A7;
end;
assume [root-tree sy,s1] in F.(root-tree sy);
then consider s3 being Element of S such that
A8: [root-tree sy,s1] = [root-tree sy,s3] and
A9: ex s2 be Element of S, x be set st
x in X.s2 & sy = [x,s2] & s2 <= s3 by A7;
A10: s1 = s3 by A8,ZFMISC_1:33;
consider s2 be Element of S, x2 be set
such that A11: x2 in X.s2 & sy = [x2,s2] & s2 <= s3 by A9;
x2 = x & s2 = s by A5,A11,ZFMISC_1:33;
then SPTA.s c= SPTA.s1 by A1,A10,A11;
hence root-tree sy in SPTA.s1 by A6;
end;
thus R2[root-tree sy]
proof
let s1 be Element of S,
y be Element of TS(D);
assume A12: [y,s1] in F.(root-tree sy);
then consider s2 being Element of S such that
A13: [y,s1] = [root-tree sy,s2] and
ex s3 be Element of S, x be set st
x in X.s3 & sy = [x,s3] & s3 <= s2 by A7;
y = root-tree sy & s1 = s2 by A13,ZFMISC_1:33;
hence [root-tree sy,s1] in F.y by A12;
end;
end;
A14: for nt being Symbol of D,
ts being FinSequence of TS(D) st nt ==> roots ts &
for t being DecoratedTree of the carrier of D st
t in rng ts holds P[t]
holds P[nt-tree ts]
proof
let nt be Symbol of D,
ts be FinSequence of TS(D) such that
A15: nt ==> roots ts and
A16: for t being DecoratedTree of the carrier of D st
t in rng ts holds R1[t] & R2[t];
consider o being OperSymbol of S such that
A17: nt = [o,the carrier of S] &
ts in Args(o,PTA) & nt-tree ts = Den(o,PTA).ts &
for s1 being Element of S holds
nt-tree ts in (the Sorts of PTA).s1 iff
the_result_sort_of o <= s1 by A15,Th12;
reconsider ts1 = ts as Element of Args(o,PTA) by A17;
set w = the_arity_of o;
reconsider x = F * ts as FinSequence of C;
A18: rng ts c= TS D & dom F = TS D by FINSEQ_1:def 4,FUNCT_2:def 1;
then len x = len ts by FINSEQ_2:33;
then A19: dom x = dom ts & dom w = dom ts by A17,FINSEQ_3:31,MSUALG_3:6;
A20: for y being Nat st y in dom x holds
[ts1.y,w/.y] in x.y
proof let y being Nat such that A21: y in dom x;
A22: ts1.y in rng ts1 by A19,A21,FUNCT_1:12;
then reconsider t1 = ts1.y as Element of TS D by A18;
ts1.y in SPTA.(w/.y) by A19,A21,MSUALG_6:2;
then [t1,w/.y] in F.t1 by A16,A22;
hence [ts1.y,w/.y] in x.y by A19,A21,FUNCT_1:23;
end;
A23: F.(nt-tree ts) = @(nt,x) by A15,Def22
.= {[Den(o2,ParsedTermsOSA(X)).x2,s3] where
o2 is OperSymbol of S,
x2 is Element of Args(o2,ParsedTermsOSA(X)),
s3 is Element of S :
( ex o1 being OperSymbol of S st nt = [o1,the carrier of S] &
o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 &
the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) &
ex w3 being Element of (the carrier of S)* st
dom w3 = dom x &
for y being Nat st y in dom x holds
[x2.y,w3/.y] in x.y} by Def21;
thus R1[nt-tree ts]
proof
let s1 be Element of S;
hereby
assume nt-tree ts in SPTA.s1;
then o ~= o & len the_arity_of o = len the_arity_of o &
the_result_sort_of o <= s1 & the_result_sort_of o <= s1 by A17;
hence [nt-tree ts,s1] in F.(nt-tree ts) by A17,A19,A20,A23;
end;
assume [nt-tree ts,s1] in F.(nt-tree ts);
then consider o2 being OperSymbol of S,
x2 being Element of Args(o2,PTA),
s3 being Element of S such that
A24: [nt-tree ts,s1] = [Den(o2,PTA).x2,s3] and
A25: ( ex o1 being OperSymbol of S st nt = [o1,the carrier of S] &
o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 &
the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) &
ex w3 being Element of (the carrier of S)* st
dom w3 = dom x &
for y being Nat st y in dom x holds
[x2.y,w3/.y] in x.y by A23;
A26: nt-tree ts = Den(o2,PTA).x2 & s1 = s3 by A24,ZFMISC_1:33;
consider o1 being OperSymbol of S such that
A27: nt = [o1,the carrier of S] &
o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 &
the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3
by A25;
A28: Den(o2,PTA).x2 in SPTA.(the_result_sort_of o2)
by MSUALG_9:19;
SPTA.(the_result_sort_of o2) c= SPTA.s1 by A1,A26,A27;
hence nt-tree ts in SPTA.s1 by A26,A28;
end;
thus R2[nt-tree ts]
proof
let s1 be Element of S,
y be Element of TS(D);
assume [y,s1] in F.(nt-tree ts);
then consider o2 being OperSymbol of S,
x2 being Element of Args(o2,PTA),
s3 being Element of S such that
A29: [y,s1] = [Den(o2,PTA).x2,s3] and
A30: ( ex o1 being OperSymbol of S st nt = [o1,the carrier of S] &
o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 &
the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) &
ex w3 being Element of (the carrier of S)* st
dom w3 = dom x &
for y being Nat st y in dom x holds
[x2.y,w3/.y] in x.y by A23;
A31: y = Den(o2,PTA).x2 & s1 = s3 by A29,ZFMISC_1:33;
consider o1 being OperSymbol of S such that
A32: nt = [o1,the carrier of S] &
o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 &
the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 by A30;
A33: o1 = o by A17,A32,ZFMISC_1:33;
A34: x2 is FinSequence of TS D &
OSSym(o2,X) ==> roots x2 by Th13;
reconsider x3 = x2 as FinSequence of TS D by Th13;
consider o3 being OperSymbol of S such that
A35: OSSym(o2,X) = [o3,the carrier of S] & x3 in Args(o3,PTA) &
OSSym(o2,X)-tree x3 = Den(o3,PTA).x3 &
for s2 being Element of S holds
OSSym(o2,X)-tree x3 in (the Sorts of PTA).s2
iff the_result_sort_of o3 <= s2 by A34,Th12;
[o2,the carrier of S] = [o3,the carrier of S] by A35,Def6;
then A36: o2 = o3 by ZFMISC_1:33;
A37: dom the_arity_of o2 = dom the_arity_of o
by A32,A33,FINSEQ_3:31;
consider w3 being Element of (the carrier of S)* such that
A38: dom w3 = dom x &
for y being Nat st y in dom x holds
[x2.y,w3/.y] in x.y by A30;
reconsider xy = F * x3 as FinSequence of C;
A39: rng x3 c= TS D by FINSEQ_1:def 4;
then rng x3 c= dom F by FUNCT_2:def 1;
then len xy = len x3 by FINSEQ_2:33;
then A40: dom x3 = dom xy by FINSEQ_3:31;
A41: dom x2 = dom x by A19,A37,MSUALG_3:6;
A42: dom w3 = dom xy & dom xy = dom x3 by A19,A37,A38,A40,MSUALG_3:6;
A43: for y being Nat st y in dom xy holds
[ts1.y,w3/.y] in xy.y
proof let y be Nat such that A44: y in dom xy;
A45: ts1.y in rng ts1 & x2.y in rng x3
by A19,A38,A42,A44,FUNCT_1:12;
then reconsider t1 = ts1.y,t2 = x2.y as Element of TS D
by A18,A39;
[x2.y,w3/.y] in x.y by A38,A40,A41,A44;
then [x2.y,w3/.y] in F.(ts1.y) by A19,A38,A42,A44,FUNCT_1:23;
then [t1,w3/.y] in F.(t2) by A16,A45;
hence [ts1.y,w3/.y] in xy.y by A44,FUNCT_1:22;
end;
A46: F.y = @(OSSym(o2,X),xy) by A31,A34,A35,A36,Def22
.= {[Den(o4,PTA).x4,s4] where
o4 is OperSymbol of S,
x4 is Element of Args(o4,PTA),
s4 is Element of S :
( ex o1 being OperSymbol of S st OSSym(o2,X) =
[o1,the carrier of S] &
o1 ~= o4 & len the_arity_of o1 = len the_arity_of o4 &
the_result_sort_of o1 <= s4 & the_result_sort_of o4 <= s4 ) &
ex w4 being Element of (the carrier of S)* st
dom w4 = dom xy &
for y being Nat st y in dom xy holds
[x4.y,w4/.y] in xy.y} by Def21;
OSSym(o2,X) = [o2,the carrier of S] &
o2 ~= o & len the_arity_of o2 = len the_arity_of o &
the_result_sort_of o2 <= s1 & the_result_sort_of o <= s1
by A29,A32,A33,Def6,ZFMISC_1:33;
hence [nt-tree ts,s1] in F.y by A17,A42,A43,A46;
end;
end;
for t being DecoratedTree of the carrier of D
st t in TS(D) holds P[t]
from DTConstrInd(A3,A14);
hence thesis;
end;
theorem Th21:
for S be locally_directed OrderSortedSign,
X be non-empty ManySortedSet of S,
t being Element of TS DTConOSA(X),
s being Element of S holds
( ex y being Element of TS(DTConOSA X)
st [y,s] in (PTClasses X).t )
implies [t,s] in (PTClasses X).t
proof
let S be locally_directed OrderSortedSign,
X be non-empty ManySortedSet of S;
set D = DTConOSA(X), PTA = ParsedTermsOSA(X),
C = bool [:TS(D), the carrier of S:],
SPTA = the Sorts of PTA,
F = PTClasses X;
defpred R3[set] means
for s being Element of S holds
( ex y being Element of TS(DTConOSA X)
st [y,s] in (PTClasses X).$1 ) implies
[$1,s] in (PTClasses X).$1;
A1: for s being Symbol of D st s in Terminals D holds
R3[root-tree s]
proof
let sy be Symbol of D such that A2: sy in Terminals D;
A3: F.(root-tree sy) = @(sy) by A2,Def22 .=
{[root-tree sy,s1] where s1 is Element of S:
ex s2 be Element of S, x be set st
x in X.s2 & sy = [x,s2] & s2 <= s1} by Def20;
let s1 be Element of S;
assume ex y being Element of TS(DTConOSA X)
st [y,s1] in F.(root-tree sy);
then consider y being Element of TS(DTConOSA X) such that
A4: [y,s1] in F.(root-tree sy);
consider s3 being Element of S such that
A5: [y,s1] = [root-tree sy,s3] and
ex s2 be Element of S, x be set st
x in X.s2 & sy = [x,s2] & s2 <= s3 by A3,A4;
thus [root-tree sy,s1] in (PTClasses X).(root-tree sy) by A4,A5,ZFMISC_1:33
;
end;
A6: for nt being Symbol of D,
ts being FinSequence of TS(D) st nt ==> roots ts &
for t being DecoratedTree of the carrier of D st
t in rng ts holds R3[t]
holds R3[nt-tree ts]
proof
let nt be Symbol of D,
ts be FinSequence of TS(D) such that
A7: nt ==> roots ts and
for t being DecoratedTree of the carrier of D st
t in rng ts holds R3[t];
consider o being OperSymbol of S such that
A8: nt = [o,the carrier of S] &
ts in Args(o,PTA) & nt-tree ts = Den(o,PTA).ts &
for s1 being Element of S holds
nt-tree ts in (the Sorts of PTA).s1 iff
the_result_sort_of o <= s1 by A7,Th12;
reconsider ts1 = ts as Element of Args(o,PTA) by A8;
set w = the_arity_of o;
reconsider x = F * ts as FinSequence of C;
A9: rng ts c= TS D & dom F = TS D by FINSEQ_1:def 4,FUNCT_2:def 1;
then len x = len ts by FINSEQ_2:33;
then A10: dom x = dom ts & dom w = dom ts by A8,FINSEQ_3:31,MSUALG_3:6;
A11: for y being Nat st y in dom x holds
[ts1.y,w/.y] in x.y
proof let y being Nat such that A12: y in dom x;
ts1.y in rng ts1 by A10,A12,FUNCT_1:12;
then reconsider t1 = ts1.y as Element of TS D by A9;
ts1.y in SPTA.(w/.y) by A10,A12,MSUALG_6:2;
then [t1,w/.y] in F.t1 by Th20;
hence [ts1.y,w/.y] in x.y by A10,A12,FUNCT_1:23;
end;
A13: F.(nt-tree ts) = @(nt,x) by A7,Def22
.= {[Den(o2,ParsedTermsOSA(X)).x2,s3] where
o2 is OperSymbol of S,
x2 is Element of Args(o2,ParsedTermsOSA(X)),
s3 is Element of S :
( ex o1 being OperSymbol of S st nt = [o1,the carrier of S] &
o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 &
the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) &
ex w3 being Element of (the carrier of S)* st
dom w3 = dom x &
for y being Nat st y in dom x holds
[x2.y,w3/.y] in x.y} by Def21;
let s1 be Element of S;
assume ex y being Element of TS(DTConOSA X)
st [y,s1] in F.(nt-tree ts);
then consider y being Element of TS(DTConOSA X) such that
A14: [y,s1] in F.(nt-tree ts);
consider o2 being OperSymbol of S,
x2 being Element of Args(o2,PTA),
s3 being Element of S such that
A15: [y,s1] = [Den(o2,PTA).x2,s3] and
A16: ( ex o1 being OperSymbol of S st nt = [o1,the carrier of S] &
o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 &
the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) &
ex w3 being Element of (the carrier of S)* st
dom w3 = dom x &
for y being Nat st y in dom x holds
[x2.y,w3/.y] in x.y by A13,A14;
A17: y = Den(o2,PTA).x2 & s1 = s3 by A15,ZFMISC_1:33;
consider o1 being OperSymbol of S such that
A18: nt = [o1,the carrier of S] &
o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 &
the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3
by A16;
o ~= o & len the_arity_of o = len the_arity_of o &
the_result_sort_of o <= s3 & the_result_sort_of o <= s3
by A8,A18,ZFMISC_1:33;
hence [nt-tree ts,s1] in F.(nt-tree ts) by A8,A10,A11,A13,A17;
end;
for t being DecoratedTree of the carrier of D
st t in TS(D) holds R3[t] from DTConstrInd(A1,A6);
hence thesis;
end;
theorem Th22:
for S be locally_directed OrderSortedSign,
X be non-empty ManySortedSet of S,
x,y being Element of TS DTConOSA(X),
s1,s2 being Element of S
st s1 <= s2 & x in (the Sorts of ParsedTermsOSA(X)).s1
& y in (the Sorts of ParsedTermsOSA(X)).s1 holds
[y,s1] in (PTClasses X).x iff [y,s2] in (PTClasses X).x
proof
let S be locally_directed OrderSortedSign,
X be non-empty ManySortedSet of S;
set D = DTConOSA(X), PTA = ParsedTermsOSA(X),
C = bool [:TS(D), the carrier of S:],
SPTA = the Sorts of PTA,
F = PTClasses X;
defpred R3[set] means
for s1,s2 being Element of S,
y being Element of TS(DTConOSA X)
st s1 <= s2 & $1 in SPTA.s1 & y in SPTA.s1 holds
([y,s1] in (PTClasses X).$1 iff [y,s2] in (PTClasses X).$1);
reconsider SPTA1 = SPTA as OrderSortedSet of S by OSALG_1:17;
A1: for s1,s2 being Element of S st
s1 <= s2 holds SPTA.s1 c= SPTA.s2
proof
let s1,s2 be Element of S such that
A2: s1 <= s2;
reconsider s11 = s1, s21= s2 as Element of S;
SPTA1.s11 c= SPTA1.s21 by A2,OSALG_1:def 18;
hence SPTA.s1 c= SPTA.s2;
end;
A3: for s being Symbol of D st s in Terminals D holds
R3[root-tree s]
proof
let sy be Symbol of D such that A4: sy in Terminals D;
reconsider sy1 = sy as Terminal of D by A4;
A5: F.(root-tree sy) = @(sy) by A4,Def22 .=
{[root-tree sy,s1] where s1 is Element of S:
ex s2 be Element of S, x be set st
x in X.s2 & sy = [x,s2] & s2 <= s1} by Def20;
let s1,s2 be Element of S,
y be Element of TS D such that
A6: s1 <= s2 & root-tree sy in SPTA.s1 & y in SPTA.s1;
A7: [root-tree sy1,s1] in F.(root-tree sy) by A6,Th20;
SPTA.s1 c= SPTA.s2 by A1,A6;
then A8: [root-tree sy1,s2] in F.(root-tree sy) by A6,Th20;
hereby assume [y,s1] in F.(root-tree sy);
then consider s3 being Element of S such that
A9: [y,s1] = [root-tree sy,s3] and
ex s2 be Element of S, x be set st
x in X.s2 & sy = [x,s2] & s2 <= s3 by A5;
thus [y,s2] in F.(root-tree sy) by A8,A9,ZFMISC_1:33;
end;
assume [y,s2] in F.(root-tree sy);
then consider s3 being Element of S such that
A10: [y,s2] = [root-tree sy,s3] and
ex s4 be Element of S, x be set st
x in X.s4 & sy = [x,s4] & s4 <= s3 by A5;
thus [y,s1] in F.(root-tree sy) by A7,A10,ZFMISC_1:33;
end;
A11: for nt being Symbol of D,
ts being FinSequence of TS(D) st nt ==> roots ts &
for t being DecoratedTree of the carrier of D st
t in rng ts holds R3[t]
holds R3[nt-tree ts]
proof
let nt be Symbol of D,
ts be FinSequence of TS(D) such that
A12: nt ==> roots ts and
for t being DecoratedTree of the carrier of D st
t in rng ts holds R3[t];
consider o being OperSymbol of S such that
A13: nt = [o,the carrier of S] &
ts in Args(o,PTA) & nt-tree ts = Den(o,PTA).ts &
for s1 being Element of S holds
nt-tree ts in (the Sorts of PTA).s1 iff
the_result_sort_of o <= s1 by A12,Th12;
reconsider x = F * ts as FinSequence of C;
A14: F.(nt-tree ts) = @(nt,x) by A12,Def22
.= {[Den(o2,ParsedTermsOSA(X)).x2,s3] where
o2 is OperSymbol of S,
x2 is Element of Args(o2,ParsedTermsOSA(X)),
s3 is Element of S :
( ex o1 being OperSymbol of S st nt = [o1,the carrier of S] &
o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 &
the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) &
ex w3 being Element of (the carrier of S)* st
dom w3 = dom x &
for y being Nat st y in dom x holds
[x2.y,w3/.y] in x.y} by Def21;
let s1,s2 be Element of S,
y be Element of TS D such that
A15: s1 <= s2 & nt-tree ts in SPTA.s1 & y in SPTA.s1;
A16: the_result_sort_of o <= s1 by A13,A15;
hereby assume [y,s1] in F.(nt-tree ts);
then consider o2 being OperSymbol of S,
x2 being Element of Args(o2,PTA),
s3 being Element of S such that
A17: [y,s1] = [Den(o2,PTA).x2,s3] and
A18: ( ex o1 being OperSymbol of S st nt = [o1,the carrier of S] &
o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 &
the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) &
ex w3 being Element of (the carrier of S)* st
dom w3 = dom x &
for y being Nat st y in dom x holds
[x2.y,w3/.y] in x.y by A14;
A19: y = Den(o2,PTA).x2 & s1 = s3 by A17,ZFMISC_1:33;
consider o1 being OperSymbol of S such that
A20: nt = [o1,the carrier of S] &
o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 &
the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3
by A18;
reconsider s21 = s2 as Element of S;
the_result_sort_of o1 <= s21 &
the_result_sort_of o2 <= s21 by A15,A19,A20,ORDERS_1:26;
hence [y,s2] in F.(nt-tree ts) by A14,A18,A19,A20;
end;
assume [y,s2] in F.(nt-tree ts);
then consider o2 being OperSymbol of S,
x2 being Element of Args(o2,PTA),
s3 being Element of S such that
A21: [y,s2] = [Den(o2,PTA).x2,s3] and
A22: ( ex o1 being OperSymbol of S st nt = [o1,the carrier of S] &
o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 &
the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) &
ex w3 being Element of (the carrier of S)* st
dom w3 = dom x &
for y being Nat st y in dom x holds
[x2.y,w3/.y] in x.y by A14;
A23: y = Den(o2,PTA).x2 & s2 = s3 by A21,ZFMISC_1:33;
consider o1 being OperSymbol of S such that
A24: nt = [o1,the carrier of S] &
o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 &
the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3
by A22;
A25: the_result_sort_of o1 <= s1 by A13,A16,A24,ZFMISC_1:33;
A26: x2 is FinSequence of TS D &
OSSym(o2,X) ==> roots x2 by Th13;
reconsider x3 = x2 as FinSequence of TS D by Th13;
consider o3 being OperSymbol of S such that
A27: OSSym(o2,X) = [o3,the carrier of S] & x3 in Args(o3,PTA) &
OSSym(o2,X)-tree x3 = Den(o3,PTA).x3 &
for s2 being Element of S holds
OSSym(o2,X)-tree x3 in (the Sorts of PTA).s2
iff the_result_sort_of o3 <= s2 by A26,Th12;
[o2,the carrier of S] = [o3,the carrier of S] by A27,Def6;
then o2 = o3 by ZFMISC_1:33;
then the_result_sort_of o2 <= s1 by A15,A23,A27;
hence [y,s1] in F.(nt-tree ts) by A14,A22,A23,A24,A25;
end;
for t being DecoratedTree of the carrier of D
st t in TS(D) holds R3[t] from DTConstrInd(A3,A11);
hence thesis;
end;
theorem Th23:
for S be locally_directed OrderSortedSign,
X be non-empty ManySortedSet of S,
x,y,z being Element of TS DTConOSA(X),
s being Element of S holds
[y,s] in (PTClasses X).x & [z,s] in (PTClasses X).y implies
[x,s] in (PTClasses X).z
proof
let S be locally_directed OrderSortedSign,
X be non-empty ManySortedSet of S;
set D = DTConOSA(X), PTA = ParsedTermsOSA(X),
C = bool [:TS(D), the carrier of S:],
SPTA = the Sorts of PTA,
F = PTClasses X;
defpred R3[set] means
for s being Element of S,
y,z being Element of TS(D) holds
[y,s] in F.$1 & [z,s] in F.y implies [$1,s] in F.z;
A1: for s being Symbol of D st s in Terminals D holds
R3[root-tree s]
proof let sy be Symbol of D such that A2: sy in Terminals D;
A3: F.(root-tree sy) = @(sy) by A2,Def22 .=
{[root-tree sy,s1] where s1 is Element of S:
ex s2 be Element of S, x be set st
x in X.s2 & sy = [x,s2] & s2 <= s1} by Def20;
thus R3[root-tree sy]
proof
let s1 be Element of S,
y,z be Element of TS(D);
assume A4: [y,s1] in F.(root-tree sy) & [z,s1] in F.y;
then consider s2 being Element of S such that
A5: [y,s1] = [root-tree sy,s2] and
ex s0 be Element of S, x be set st
x in X.s0 & sy = [x,s0] & s0 <= s2 by A3;
A6: y = root-tree sy & s1 = s2 by A5,ZFMISC_1:33;
then consider s3 being Element of S such that
A7: [z,s1] = [root-tree sy,s3] and
ex s0 be Element of S, x be set st
x in X.s0 & sy = [x,s0] & s0 <= s3 by A3,A4;
thus [root-tree sy,s1] in F.z by A4,A6,A7,ZFMISC_1:33;
end;
end;
A8: for nt being Symbol of D,
ts being FinSequence of TS(D) st nt ==> roots ts &
for t being DecoratedTree of the carrier of D st
t in rng ts holds R3[t]
holds R3[nt-tree ts]
proof
let nt be Symbol of D,
ts be FinSequence of TS(D) such that
A9: nt ==> roots ts and
A10: for t being DecoratedTree of the carrier of D st
t in rng ts holds R3[t];
consider o being OperSymbol of S such that
A11: nt = [o,the carrier of S] &
ts in Args(o,PTA) & nt-tree ts = Den(o,PTA).ts &
for s1 being Element of S holds
nt-tree ts in (the Sorts of PTA).s1 iff
the_result_sort_of o <= s1 by A9,Th12;
reconsider ts1 = ts as Element of Args(o,PTA) by A11;
set w = the_arity_of o;
reconsider x = F * ts as FinSequence of C;
A12: rng ts c= TS D & dom F = TS D by FINSEQ_1:def 4,FUNCT_2:def 1;
then len x = len ts by FINSEQ_2:33;
then A13: dom x = dom ts & dom w = dom ts by A11,FINSEQ_3:31,MSUALG_3:6;
A14: F.(nt-tree ts) = @(nt,x) by A9,Def22
.= {[Den(o2,ParsedTermsOSA(X)).x2,s3] where
o2 is OperSymbol of S,
x2 is Element of Args(o2,ParsedTermsOSA(X)),
s3 is Element of S :
( ex o1 being OperSymbol of S st nt = [o1,the carrier of S] &
o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 &
the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) &
ex w3 being Element of (the carrier of S)* st
dom w3 = dom x &
for y being Nat st y in dom x holds
[x2.y,w3/.y] in x.y} by Def21;
thus R3[nt-tree ts]
proof
let s1 be Element of S,
y,z be Element of TS(D);
assume A15: [y,s1] in F.(nt-tree ts) & [z,s1] in F.y;
then consider o2 being OperSymbol of S,
x2 being Element of Args(o2,PTA),
s3 being Element of S such that
A16: [y,s1] = [Den(o2,PTA).x2,s3] and
A17: ( ex o1 being OperSymbol of S st nt = [o1,the carrier of S] &
o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 &
the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) &
ex w3 being Element of (the carrier of S)* st
dom w3 = dom x &
for y being Nat st y in dom x holds
[x2.y,w3/.y] in x.y by A14;
A18: y = Den(o2,PTA).x2 & s1 = s3 by A16,ZFMISC_1:33;
consider o1 being OperSymbol of S such that
A19: nt = [o1,the carrier of S] &
o1 ~= o2 & len the_arity_of o1 = len the_arity_of o2 &
the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 by A17;
A20: o1 = o by A11,A19,ZFMISC_1:33;
A21: x2 is FinSequence of TS D &
OSSym(o2,X) ==> roots x2 by Th13;
reconsider x3 = x2 as FinSequence of TS D by Th13;
consider o3 being OperSymbol of S such that
A22: OSSym(o2,X) = [o3,the carrier of S] & x3 in Args(o3,PTA) &
OSSym(o2,X)-tree x3 = Den(o3,PTA).x3 &
for s2 being Element of S holds
OSSym(o2,X)-tree x3 in (the Sorts of PTA).s2
iff the_result_sort_of o3 <= s2 by A21,Th12;
[o2,the carrier of S] = [o3,the carrier of S] by A22,Def6;
then A23: o2 = o3 by ZFMISC_1:33;
A24: dom the_arity_of o2 = dom the_arity_of o
by A19,A20,FINSEQ_3:31;
consider w3 being Element of (the carrier of S)* such that
A25: dom w3 = dom x &
for y being Nat st y in dom x holds
[x2.y,w3/.y] in x.y by A17;
reconsider xy = F * x3 as FinSequence of C;
rng x3 c= TS D by FINSEQ_1:def 4;
then rng x3 c= dom F by FUNCT_2:def 1;
then len xy = len x3 by FINSEQ_2:33;
then A26: dom x3 = dom xy by FINSEQ_3:31;
A27: dom x2 = dom x by A13,A24,MSUALG_3:6;
A28: F.y = @(OSSym(o2,X),xy) by A18,A21,A22,A23,Def22
.= {[Den(o4,PTA).x4,s4] where
o4 is OperSymbol of S,
x4 is Element of Args(o4,PTA),
s4 is Element of S :
( ex o1 being OperSymbol of S st OSSym(o2,X) =
[o1,the carrier of S] &
o1 ~= o4 & len the_arity_of o1 = len the_arity_of o4 &
the_result_sort_of o1 <= s4 & the_result_sort_of o4 <= s4 ) &
ex w4 being Element of (the carrier of S)* st
dom w4 = dom xy &
for y being Nat st y in dom xy holds
[x4.y,w4/.y] in xy.y} by Def21;
A29: OSSym(o2,X) = [o2,the carrier of S] by Def6;
consider o5 being OperSymbol of S,
x5 being Element of Args(o5,PTA),
s5 being Element of S such that
A30: [z,s1] = [Den(o5,PTA).x5,s5] and
A31: ( ex o1 being OperSymbol of S st
OSSym(o2,X) = [o1,the carrier of S] &
o1 ~= o5 & len the_arity_of o1 = len the_arity_of o5 &
the_result_sort_of o1 <= s5 & the_result_sort_of o5 <= s5 ) &
ex w3 being Element of (the carrier of S)* st
dom w3 = dom xy &
for y being Nat st y in dom xy holds
[x5.y,w3/.y] in xy.y by A15,A28;
A32: z = Den(o5,PTA).x5 & s1 = s5 by A30,ZFMISC_1:33;
consider o6 being OperSymbol of S such that
A33: OSSym(o2,X) = [o6,the carrier of S] &
o6 ~= o5 & len the_arity_of o6 = len the_arity_of o5 &
the_result_sort_of o6 <= s5 & the_result_sort_of o5 <= s5 by A31;
A34: o6 = o2 by A29,A33,ZFMISC_1:33;
A35: x5 is FinSequence of TS D &
OSSym(o5,X) ==> roots x5 by Th13;
reconsider x6 = x5 as FinSequence of TS D by Th13;
consider o7 being OperSymbol of S such that
A36: OSSym(o5,X) = [o7,the carrier of S] & x6 in Args(o7,PTA) &
OSSym(o5,X)-tree x6 = Den(o7,PTA).x6 &
for s2 being Element of S holds
OSSym(o5,X)-tree x6 in (the Sorts of PTA).s2
iff the_result_sort_of o7 <= s2 by A35,Th12;
[o5,the carrier of S] = [o7,the carrier of S] by A36,Def6;
then A37: o5 = o7 by ZFMISC_1:33;
A38: dom the_arity_of o5 = dom the_arity_of o2
by A33,A34,FINSEQ_3:31;
consider w5 being Element of (the carrier of S)* such that
A39: dom w5 = dom xy &
for y being Nat st y in dom xy holds
[x5.y,w5/.y] in xy.y by A31;
reconsider xz = F * x6 as FinSequence of C;
A40: rng x6 c= TS D & rng x3 c= TS D by FINSEQ_1:def 4;
then rng x6 c= dom F by FUNCT_2:def 1;
then len xz = len x6 by FINSEQ_2:33;
then A41: dom x6 = dom xz by FINSEQ_3:31;
A42: dom x5 = dom (the_arity_of o2) by A38,MSUALG_3:6
.= dom xy by A26,MSUALG_3:6;
defpred P[set,set] means
[ts1.$1,$2] in xz.$1;
A43: for y being set st y in dom xz ex
sy being set st sy in the carrier of S & P[y,sy]
proof let y be set such that A44: y in dom xz;
A45: y in dom ts1 & y in dom x5 &
y in dom x2 & y in dom x
by A13,A24,A26,A41,A42,A44,MSUALG_3:6;
A46: ts1.y in rng ts1 & x5.y in rng x6 & x2.y in rng x3
by A13,A26,A27,A41,A42,A44,FUNCT_1:12;
then reconsider t1 = ts1.y,t2 = x3.y,t3 = x5.y as Element of TS D
by A12,A40;
[x5.y,w5/.y] in xy.y by A39,A41,A42,A44;
then A47: [t3,w5/.y] in F.(t2) by A26,A41,A42,A44,FUNCT_1:23;
then A48: [t2,w5/.y] in F.(t2) &
[t2,w5/.y] in F.t3 by Th20,Th21;
then [t3,w5/.y] in F.t3 by Th21;
then A49: t2 in SPTA.(w5/.y) &
t3 in SPTA.(w5/.y) by A48,Th20;
then A50: LeastSort t2 <= w5/.y by Def12;
A51: [x2.y,w3/.y] in x.y by A25,A26,A27,A41,A42,A44;
then A52: [x2.y,w3/.y] in F.(ts1.y) by A13,A26,A27,A41,A42,A44,FUNCT_1
:23;
[t2,w3/.y] in F.(t1) by A45,A51,FUNCT_1:23;
then A53: [t1,w3/.y] in F.t2 & [t1,w3/.y] in F.t1
by Th20,Th21;
then [t2,w3/.y] in F.t2 by Th21;
then A54: t2 in SPTA.(w3/.y) & t1 in SPTA.(w3/.y)
by A53,Th20;
then LeastSort t2 <= w3/.y by Def12;
then consider s7 being Element of S such that
A55: w5/.y <= s7 & w3/.y <= s7 by A50,OSALG_4:12;
A56: [t2,s7] in F.t1 by A52,A54,A55,Th22;
[t3,s7] in F.t2 by A47,A49,A55,Th22;
then A57: [t1,s7] in F.t3 by A10,A46,A56;
take s7;
thus s7 in the carrier of S;
thus [ts1.y,s7] in xz.y by A44,A57,FUNCT_1:22;
end;
consider f being Function of dom xz,(the carrier of S)
such that A58: for y being set st y in dom xz
holds P[y,f.y] from FuncEx1(A43);
A59: dom f = dom xz by FUNCT_2:def 1;
then ex n being Nat st dom f = Seg n by FINSEQ_1:def 2;
then reconsider f1 = f as FinSequence by FINSEQ_1:def 2;
rng f c= the carrier of S by RELSET_1:12;
then f1 is FinSequence of the carrier of S by FINSEQ_1:def 4;
then reconsider f as Element of (the carrier of S)* by FINSEQ_1:def 11;
A60: dom f = dom xz &
for y being Nat st y in dom xz
holds [ts1.y,f/.y] in xz.y
proof
thus dom f = dom xz by FUNCT_2:def 1;
let y be Nat such that A61: y in dom xz;
[ts1.y,f.y] in xz.y by A58,A61;
hence [ts1.y,f/.y] in xz.y by A59,A61,FINSEQ_4:def 4;
end;
A62: F.z = @(OSSym(o5,X),xz) by A32,A35,A36,A37,Def22
.= {[Den(o4,PTA).x4,s4] where
o4 is OperSymbol of S,
x4 is Element of Args(o4,PTA),
s4 is Element of S :
( ex o1 being OperSymbol of S st OSSym(o5,X) =
[o1,the carrier of S] &
o1 ~= o4 & len the_arity_of o1 = len the_arity_of o4 &
the_result_sort_of o1 <= s4 & the_result_sort_of o4 <= s4 ) &
ex w4 being Element of (the carrier of S)* st
dom w4 = dom xz &
for y being Nat st y in dom xz holds
[x4.y,w4/.y] in xz.y} by Def21;
OSSym(o5,X) = [o5,the carrier of S] &
o5 ~= o & len the_arity_of o5 = len the_arity_of o &
the_result_sort_of o5 <= s1 & the_result_sort_of o <= s1
by A16,A19,A20,A30,A33,A34,Def6,OSALG_1:2,ZFMISC_1:33;
hence [nt-tree ts,s1] in F.z by A11,A60,A62;
end;
end;
for t being DecoratedTree of the carrier of D
st t in TS(D) holds R3[t] from DTConstrInd(A1,A8);
hence thesis;
end;
definition
let S be locally_directed OrderSortedSign,
X be non-empty ManySortedSet of S;
func PTCongruence(X) -> MSEquivalence-like OrderSortedRelation of
ParsedTermsOSA(X) means :Def23:
for i being set st i in the carrier of S holds
it.i = {[x,y] where x,y is Element of TS(DTConOSA(X)):
[x,i] in (PTClasses X).y};
existence
proof
set PTA = ParsedTermsOSA(X),
SPTA = the Sorts of PTA,
D = DTConOSA(X),
F = PTClasses X;
deffunc F(set) = {[x,y] where x,y is Element of TS(D): [x,$1] in F.y};
consider R being ManySortedSet of the carrier of S such that
A1: for i being set st i in the carrier of S holds
R.i = F(i) from MSSLambda;
defpred IRREL[Element of TS D,Element of S] means
(ex s1 being Element of S, x be set st
s1 <= $2 & x in X.s1 & $1 = root-tree [x,s1]) or
ex o be OperSymbol of S st [o,the carrier of S] = $1.{}
& the_result_sort_of o <= $2;
for i be set st i in the carrier