:: Free Order Sorted Universal Algebra
:: by Josef Urban
::
:: Received September 19, 2002
:: Copyright (c) 2002-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies OSALG_1, MSUALG_2, OSALG_2, MSUALG_1, TARSKI, STRUCT_0, RELAT_1,
SEQM_3, PBOOLE, MSUALG_3, REALSET1, ZFMISC_1, XBOOLE_0, CARD_3, MSAFREE,
SUBSET_1, FINSEQ_1, MARGREL1, FUNCT_1, XXREAL_0, PARTFUN1, LANG1,
TDGROUP, DTCONSTR, TREES_3, TREES_4, NAT_1, TREES_2, OSALG_4, CARD_5,
NATTRA_1, CARD_LAR, QC_LANG1, EQREL_1, RELAT_2, MSUALG_4, COH_SP,
MCART_1, UNIALG_2, MEMBER_1, FUNCT_7, OSAFREE;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, RELAT_1,
RELSET_1, FUNCT_1, MCART_1, PARTFUN1, FUNCT_2, FINSEQ_1, FINSEQ_2,
PBOOLE, RELAT_2, TREES_2, CARD_3, EQREL_1, STRUCT_0, LANG1, TREES_3,
TREES_4, DTCONSTR, ORDERS_2, ORDERS_3, MSUALG_1, MSUALG_2, MSUALG_3,
MSUALG_4, OSALG_1, OSALG_2, OSALG_3, OSALG_4, MSAFREE, FUNCT_7;
constructors NAT_1, FINSEQOP, FUNCT_7, MSUALG_3, MSAFREE, ORDERS_3, OSALG_2,
OSALG_3, OSALG_4, RELSET_1, XTUPLE_0, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, PARTFUN1, FUNCOP_1,
FUNCT_1, PBOOLE, TREES_2, TREES_3, STRUCT_0, DTCONSTR, MSUALG_1,
MSUALG_3, MSAFREE, MSUALG_4, MSUALG_9, OSALG_1, OSALG_4, RELSET_1,
FINSEQ_1, XTUPLE_0;
requirements BOOLE, SUBSET;
definitions TARSKI, XBOOLE_0, PBOOLE, MSUALG_3, OSALG_1, OSALG_3, OSALG_4;
equalities TARSKI, OSALG_4;
expansions TARSKI, PBOOLE, MSUALG_3, OSALG_1, OSALG_3, OSALG_4;
theorems TARSKI, FUNCT_1, FUNCT_2, ZFMISC_1, PBOOLE, CARD_3, MSUALG_1,
MSUALG_2, MSUALG_3, RELAT_1, LANG1, DTCONSTR, FINSEQ_1, TREES_4, TREES_1,
DOMAIN_1, RELSET_1, XBOOLE_0, OSALG_1, OSALG_2, OSALG_4, MSAFREE,
MSUALG_6, MSAFREE2, CARD_5, FINSEQ_2, FINSEQ_3, MSUALG_9, MSUALG_4,
EQREL_1, ORDERS_2, RELAT_2, PARTFUN1, ORDERS_1, FUNCOP_1, TREES_3,
XTUPLE_0, SUBSET_1;
schemes CLASSES1, FUNCT_1, RELSET_1, DTCONSTR, XBOOLE_0, FUNCT_2, PBOOLE;
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 PBOOLE:def 18;
A1: A is OrderSortedSet of S by OSALG_1:17;
then reconsider A as OSSubset of U0 by OSALG_2:def 2;
take A;
set G = GenOSAlg(A);
A is OSSubset of G by OSALG_2:def 12;
then
A2: A c= the Sorts of G by PBOOLE:def 18;
the Sorts of G is MSSubset of U0 by MSUALG_2:def 9;
then
A3: the Sorts of G c= A by PBOOLE:def 18;
A = OSCl A by A1,OSALG_2:9;
hence thesis by A2,A3,PBOOLE:146;
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
reconsider U1 = U0 as MSSubAlgebra of U0 by MSUALG_2:5;
assume
A1: A is OSGeneratorSet of U0;
let O be OSSubset of U0;
assume O = OSCl A;
then the Sorts of GenOSAlg(O) = the Sorts of U1 by A1,Def1;
hence thesis by MSUALG_2:9;
end;
assume
A2: for O being OSSubset of U0 st O = OSCl A holds GenOSAlg(O) = U0;
let O be OSSubset of U0;
assume O = OSCl A;
hence thesis by A2;
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 carrier' of S,{the carrier of S}:] \/
Union (coprod X)), (([:the carrier' of S,{the carrier of S}:] \/ Union (coprod
X))*) means
:Def4:
for a be Element of [:the carrier' of S,{the carrier of S}:]
\/ Union (coprod X), b be Element of ([:the carrier' of S,{the carrier of S}:]
\/ Union (coprod X))* holds [a,b] in it iff a in [:the carrier' 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
carrier' of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the
carrier of S] = b.x holds (the_result_sort_of o1) <= (the_arity_of o)/.x) & (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 carrier' of S,{the carrier of S}:] \/ Union (coprod X);
defpred P[Element of O, Element of O*] means $1 in [:the carrier' 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 carrier' 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 RELSET_1:sch 2;
take R;
let a be Element of O, b be Element of O*;
thus [a,b] in R implies a in [:the carrier' 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 carrier' of S,
{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S]
= b.x holds the_result_sort_of o1 <= (the_arity_of o)/.x) & (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 that
A2: a in [:the carrier' of S,{the carrier of S}:] and
A3: 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 carrier'
of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier
of S] = b.x holds the_result_sort_of o1 <= (the_arity_of o)/.x) & (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));
thus thesis by A1,A2,A3;
end;
uniqueness
proof
set O = [:the carrier' of S,{the carrier of S}:] \/ Union (coprod X);
let R,P be Relation of O,O*;
assume that
A4: for a be Element of O, b be Element of O* holds [a,b] in R iff a
in [:the carrier' 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 carrier' of S,{the carrier of S}:] implies for o1 be
OperSymbol of S st [o1,the carrier of S] = b.x holds the_result_sort_of o1 <= (
the_arity_of o)/.x) & (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
A5: for a be Element of O, b be Element of O* holds [a,b] in P iff a
in [:the carrier' 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 carrier' of S,{the carrier of S}:] implies for o1 be
OperSymbol of S st [o1,the carrier of S] = b.x holds the_result_sort_of o1 <= (
the_arity_of o)/.x) & (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 object holds [x,y] in R iff [x,y] in P
proof
let x,y be object;
thus [x,y] in R implies [x,y] in P
proof
assume
A6: [x,y] in R;
then reconsider a = x as Element of O by ZFMISC_1:87;
reconsider b = y as Element of O* by A6,ZFMISC_1:87;
[a,b] in R by A6;
then
A7: a in [:the carrier' of S,{the carrier of S}:] by A4;
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
carrier' of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,
the carrier of S ] = b.x holds the_result_sort_of o1 <= (the_arity_of o)/.x) &
(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 A4,A6;
hence thesis by A5,A7;
end;
assume
A8: [x,y] in P;
then reconsider a = x as Element of O by ZFMISC_1:87;
reconsider b = y as Element of O* by A8,ZFMISC_1:87;
[a,b] in P by A8;
then
A9: a in [:the carrier' of S,{the carrier of S}:] by A5;
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 carrier'
of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier
of S ] = b.x holds the_result_sort_of o1 <= (the_arity_of o)/.x) & (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 A5,A8;
hence thesis by A4,A9;
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 carrier' 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 carrier' of S,
{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S]
= b.x holds (the_result_sort_of o1) <= (the_arity_of o)/.x) & (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 carrier' 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 carrier' 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 carrier' of S,{the carrier of S}:] by ZFMISC_1:87;
then reconsider
a as Element of [:the carrier' of S,{the carrier of S}:] \/ Union
(coprod X) by XBOOLE_0:def 3;
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 XTUPLE_0:1;
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
DTConstrStr (# [:the carrier' of S,{
the carrier of S}:] \/ Union (coprod X), OSREL(X) #);
correctness;
end;
registration
let S be OrderSortedSign, X be ManySortedSet of S;
cluster DTConOSA(X) -> strict non empty;
coherence;
end;
theorem Th3:
for S be OrderSortedSign, X be non-empty ManySortedSet of S holds
NonTerminals(DTConOSA(X)) = [:the carrier' of S,{the carrier of S}:] &
Terminals (DTConOSA(X)) = Union (coprod X)
proof
let S be OrderSortedSign, X be non-empty ManySortedSet of S;
set D = DTConOSA(X), A = [:the carrier' of S,{the carrier of S}:] \/ Union (
coprod (X qua ManySortedSet of S));
A1: the carrier of D = (Terminals D) \/ (NonTerminals D) by LANG1:1;
thus
A2: NonTerminals D c= [:the carrier' of S,{the carrier of S}:]
proof
let x be object;
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
A3: s = x and
A4: ex n being FinSequence st s ==> n;
consider n be FinSequence such that
A5: s ==> n by A4;
[s,n] in the Rules of D by A5,LANG1:def 1;
then reconsider n as Element of A* by ZFMISC_1:87;
reconsider s as Element of A;
[s,n] in OSREL X by A5,LANG1:def 1;
hence thesis by A3,Def4;
end;
A6: Union(coprod X) misses [:the carrier' of S,{the carrier of S}:] by
MSAFREE:4;
thus
A7: [:the carrier' of S,{the carrier of S}:] c= NonTerminals D
proof
let x be object;
assume
A8: x in [:the carrier' of S,{the carrier of S}:];
then consider
o being Element of the carrier' of S, x2 being Element of {the
carrier of S} such that
A9: x = [o,x2] by DOMAIN_1:1;
set O = the_arity_of o;
defpred P[object,object] means
ex i being Element of S st i <= O/.$1 & $2 in
coprod(i,X);
A10: for a be object st a in Seg len O ex b be object st P[a,b]
proof
let a be object;
assume a in Seg len O;
then
A11: a in dom O by FINSEQ_1:def 3;
then
A12: O.a in rng O by FUNCT_1:def 3;
A13: rng O c= the carrier of S by FINSEQ_1:def 4;
then consider x be object such that
A14: x in X.(O.a) by A12,XBOOLE_0:def 1;
take y = [x,O.a];
take O/.a;
y in coprod(O.a,X) by A12,A13,A14,MSAFREE:def 2;
hence thesis by A11,PARTFUN1:def 6;
end;
consider b be Function such that
A15: dom b = Seg len O & for a be object st a in Seg len O holds P[a,b.a]
from CLASSES1:sch 1(A10);
reconsider b as FinSequence by A15,FINSEQ_1:def 2;
rng b c= A
proof
let a be object;
assume a in rng b;
then consider c be object such that
A16: c in dom b and
A17: b.c = a by FUNCT_1:def 3;
consider i being Element of S such that
i <= O/.c and
A18: a in coprod(i,X) by A15,A16,A17;
dom coprod(X) = the carrier of S by PARTFUN1:def 2;
then (coprod(X)).(i) in rng coprod(X) by FUNCT_1:def 3;
then coprod(i,X) in rng coprod(X) by MSAFREE:def 3;
then a in union rng coprod(X) by A18,TARSKI:def 4;
then a in Union coprod(X) by CARD_3:def 4;
hence thesis by XBOOLE_0:def 3;
end;
then reconsider b as FinSequence of A by FINSEQ_1:def 4;
reconsider b as Element of A* by FINSEQ_1:def 11;
A19: now
let c be set;
assume c in dom b;
then consider i being Element of S such that
A20: i <= O/.c and
A21: b.c in coprod(i,X) by A15;
dom coprod(X) = the carrier of S by PARTFUN1:def 2;
then (coprod(X)).(i) in rng coprod(X) by FUNCT_1:def 3;
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 CARD_3:def 4;
hence b.c in [:the carrier' 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 A6,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 A20,A21
;
end;
A22: 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 A8,A9,
XBOOLE_0:def 3;
len b = len O by A15,FINSEQ_1:def 3;
then [xa,b] in OSREL(X) by A19,Th2;
then xa ==> b by LANG1:def 1;
then xa in { t where t is Symbol of D: ex n be FinSequence st t ==> n};
hence thesis by A9,A22,LANG1:def 3;
end;
A23: (Terminals D) misses (NonTerminals D) by DTCONSTR:8;
thus Terminals D c= Union (coprod X)
proof
let x be object;
assume
A24: x in Terminals D;
then
A25: x in A by A1,XBOOLE_0:def 3;
not x in [:the carrier' of S,{the carrier of S}:] by A23,A7,A24,XBOOLE_0:3;
hence thesis by A25,XBOOLE_0:def 3;
end;
let x be object;
assume
A26: x in Union (coprod X);
then x in A by XBOOLE_0:def 3;
then x in Terminals D or x in NonTerminals D by A1,XBOOLE_0:def 3;
hence thesis by A6,A2,A26,XBOOLE_0:3;
end;
reserve x for set;
registration
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 carrier' of S,{the carrier of S}:] \/ Union
(coprod (X qua ManySortedSet of S));
A1: Terminals D = Union (coprod X) by Th3;
A2: NonTerminals D = [:the carrier' of S,{the carrier of S}:] by Th3;
A3: Union (coprod X) misses [:the carrier' of S,{the carrier of S}:] by
MSAFREE:4;
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 carrier' of S, x2 being Element of {the
carrier of S} such that
A4: nt = [o,x2] by A2,DOMAIN_1:1;
set O = the_arity_of o;
A5: the carrier of S = x2 by TARSKI:def 1;
defpred P[object,object] means
ex i being Element of S st i <= O/.$1 & $2 in
coprod(i,X);
A6: for a be object st a in Seg len O ex b be object st P[a,b]
proof
let a be object;
assume a in Seg len O;
then
A7: a in dom O by FINSEQ_1:def 3;
then
A8: O.a in rng O by FUNCT_1:def 3;
A9: rng O c= the carrier of S by FINSEQ_1:def 4;
then consider x be object such that
A10: x in X.(O.a) by A8,XBOOLE_0:def 1;
take y = [x,O.a];
take O/.a;
y in coprod(O.a,X) by A8,A9,A10,MSAFREE:def 2;
hence thesis by A7,PARTFUN1:def 6;
end;
consider b be Function such that
A11: dom b = Seg len O & for a be object st a in Seg len O holds P[a,b.
a] from CLASSES1:sch 1(A6);
reconsider b as FinSequence by A11,FINSEQ_1:def 2;
A12: rng b c= A
proof
let a be object;
assume a in rng b;
then consider c be object such that
A13: c in dom b and
A14: b.c = a by FUNCT_1:def 3;
consider i being Element of S such that
i <= O/.c and
A15: a in coprod(i,X) by A11,A13,A14;
dom coprod(X) = the carrier of S by PARTFUN1:def 2;
then (coprod(X)).i in rng coprod(X) by FUNCT_1:def 3;
then coprod(i,X) in rng coprod(X) by MSAFREE:def 3;
then a in union rng coprod(X) by A15,TARSKI:def 4;
then a in Union coprod(X) by CARD_3:def 4;
hence thesis by XBOOLE_0:def 3;
end;
then reconsider b as FinSequence of A by FINSEQ_1:def 4;
reconsider b as Element of A* by FINSEQ_1:def 11;
deffunc F(object) = root-tree (b.$1);
consider f be Function such that
A16: dom f = dom b & for x being object st x in dom b holds f.x = F(x) from
FUNCT_1:sch 3;
reconsider f as FinSequence by A11,A16,FINSEQ_1:def 2;
rng f c= TS(D)
proof
let x be object;
assume x in rng f;
then consider y be object such that
A17: y in dom f and
A18: f.y = x by FUNCT_1:def 3;
b.y in rng b by A16,A17,FUNCT_1:def 3;
then reconsider a = b.y as Symbol of D by A12;
consider i being Element of S such that
i <= O/.y and
A19: b.y in coprod(i,X) by A11,A16,A17;
dom coprod(X) = the carrier of S by PARTFUN1:def 2;
then (coprod(X)).(i) in rng coprod(X) by FUNCT_1:def 3;
then coprod(i,X) in rng coprod(X) by MSAFREE:def 3;
then b.y in union rng coprod(X) by A19,TARSKI:def 4;
then
A20: a in Terminals D by A1,CARD_3:def 4;
x = root-tree(b.y) by A16,A17,A18;
hence thesis by A20,DTCONSTR:def 1;
end;
then reconsider f as FinSequence of TS(D) by FINSEQ_1:def 4;
A21: for x being object st x in dom b holds (roots f).x = b.x
proof
let x be object;
assume
A22: x in dom b;
then reconsider i = x as Nat;
A23: ex T be DecoratedTree st T = f.i & (roots f).i = T.{} by A16,A22,
TREES_3:def 18;
f.x = root-tree (b.x) by A16,A22;
hence thesis by A23,TREES_4:3;
end;
A24: now
let c be set;
assume c in dom b;
then consider i being Element of S such that
A25: i <= O/.c and
A26: b.c in coprod(i,X) by A11;
dom coprod(X) = the carrier of S by PARTFUN1:def 2;
then (coprod(X)).i in rng coprod(X) by FUNCT_1:def 3;
then coprod(i,X) in rng coprod(X) by MSAFREE:def 3;
then b.c in union rng coprod(X) by A26,TARSKI:def 4;
then b.c in Union coprod(X) by CARD_3:def 4;
hence
b.c in [:the carrier' 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 A3,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 A25
,A26;
end;
len b = len O by A11,FINSEQ_1:def 3;
then [nt,b] in OSREL(X) by A4,A5,A24,Th2;
then
A27: nt ==> b by LANG1:def 1;
take f;
dom (roots f) = dom f by TREES_3:def 18;
hence thesis by A27,A16,A21,FUNCT_1:2;
end;
hence thesis by A1,A2,DTCONSTR:def 3,def 4,def 5;
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 CARD_3:def 4;
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 and
A3: A in rng(coprod X) by A1,TARSKI:def 4;
consider s be object such that
A4: s in dom (coprod X) and
A5: (coprod X).s = A by A3,FUNCT_1:def 3;
reconsider s as Element of S by A4;
(coprod X).s = coprod(s,X) by MSAFREE:def 3;
then consider x be set such that
A6: x in X.s and
A7: t = [x,s] by A2,A5,MSAFREE:def 2;
take s;
take x;
thus thesis by A6,A7;
end;
given s be Element of S, x be set such that
A8: x in X.s and
A9: t = [x,s];
t in coprod(s,X) by A8,A9,MSAFREE:def 2;
then
A10: t in (coprod X).s by MSAFREE:def 3;
dom(coprod X) = the carrier of S by PARTFUN1:def 2;
then (coprod X).s in rng (coprod X) by FUNCT_1:def 3;
hence thesis by A1,A10,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
[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 carrier' of S,{the carrier of S}:] by
ZFMISC_1:87;
then [o,the carrier of S] in NonTerminals (DTConOSA X) by Th3;
hence thesis;
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
{a where a is
Element of TS(DTConOSA(X)):
(ex s1 being Element of S, x be object 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 object 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 object;
assume x in A;
then
ex a be Element of TS(DTConOSA(X)) st x = a &( (ex s1 being Element
of S, x be object 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);
hence thesis;
end;
hence thesis;
end;
end;
registration
let S be OrderSortedSign, X be non-empty ManySortedSet of S, s be Element of
S;
cluster ParsedTerms(X,s) -> non empty;
coherence
proof
dom coprod(X) = the carrier of S by PARTFUN1:def 2;
then (coprod(X)).s in rng coprod(X) by FUNCT_1:def 3;
then
A1: coprod(s,X) in rng coprod(X) by MSAFREE:def 3;
set A = {a where a is Element of TS(DTConOSA(X)): (ex s1 being Element of
S, x be object 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 object such that
A2: x in X.s by XBOOLE_0:def 1;
set a = [x,s];
A3: (Terminals (DTConOSA(X))) = Union (coprod X) by Th3;
a in coprod(s,X) by A2,MSAFREE:def 2;
then a in union rng coprod(X) by A1,TARSKI:def 4;
then
A4: a in Terminals (DTConOSA X) by A3,CARD_3:def 4;
then reconsider a as Symbol of DTConOSA(X);
reconsider b = root-tree a as Element of TS(DTConOSA X) by A4,
DTCONSTR:def 1;
b in A by A2;
hence thesis;
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 FUNCT_1:sch 4;
reconsider f as ManySortedSet of S by A1,PARTFUN1:def 2,RELAT_1:def 18;
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 object;
assume x1 in f.s1;
then x1 in ParsedTerms(X,s1) by A1;
then consider a being Element of TS(DTConOSA(X)) such that
A3: x1 = a and
A4: (ex s3 being Element of S, x be object 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 object 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 A4;
suppose
ex s3 being Element of S, x be object st s3 <= s1 & x in X.s3
& a = root-tree [x,s3];
then consider s3 being Element of S, x be set such that
A5: s3 <= s1 and
A6: x in X.s3 and
A7: a = root-tree [x,s3];
thus thesis by A2,A5,A6,A7,ORDERS_2:3;
end;
suppose
A8: ex o be OperSymbol of S st [o,the carrier of S] = a.{} &
the_result_sort_of o <= s1;
reconsider s21 = s2 as Element of S;
consider o be OperSymbol of S such that
A9: [o,the carrier of S] = a.{} and
A10: the_result_sort_of o <= s1 by A8;
the_result_sort_of o <= s21 by A2,A10,ORDERS_2:3;
hence thesis by A9;
end;
end;
then x1 in ParsedTerms(X,s2) by A3;
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
A11: for s be Element of S holds A.s = ParsedTerms(X,s) and
A12: for s be Element of S holds B.s = ParsedTerms(X,s);
for i be object st i in the carrier of S holds A.i = B.i
proof
let i be object;
assume i in the carrier of S;
then reconsider s = i as Element of S;
A.s = ParsedTerms(X,s) by A11;
hence thesis by A12;
end;
hence thesis;
end;
end;
registration
let S be OrderSortedSign, X be non-empty ManySortedSet of S;
cluster ParsedTerms(X) -> non-empty;
coherence
proof
let i be object;
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;
set D = DTConOSA(X), ar = the_arity_of o;
A1: (the Arity of S).o = ar by MSUALG_1:def 1;
assume x in ((ParsedTerms X)# * (the Arity of S)).o;
then x in product ((ParsedTerms X) * ar) by A1,MSAFREE:1;
then consider f be Function such that
A2: x = f and
A3: dom f = dom ((ParsedTerms X) * ar) and
A4: for y be object st y in dom ((ParsedTerms X)* ar) holds f.y in ((
ParsedTerms X) * ar).y by CARD_3:def 5;
A5: dom ((ParsedTerms X) * ar) = dom ar by PARTFUN1:def 2;
dom ar = Seg len ar by FINSEQ_1:def 3;
then reconsider f as FinSequence by A3,A5,FINSEQ_1:def 2;
rng f c= TS D
proof
let a be object;
assume a in rng f;
then consider b be object such that
A6: b in dom f and
A7: f.b = a by FUNCT_1:def 3;
A8: a in ((ParsedTerms X) * ar).b by A3,A4,A6,A7;
reconsider b as Nat by A6;
((ParsedTerms X) * ar).b = (ParsedTerms X).(ar.b) by A3,A6,FUNCT_1:12
.= (ParsedTerms X). (ar/.b) by A3,A5,A6,PARTFUN1:def 6
.= ParsedTerms(X,ar/.b) by Def8
.= { s where s is Element of TS D: (ex s1 being Element of S,
x be object
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};
then ex e be Element of TS D st a = e &( (ex s1 being Element of S,
x be object
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 A8;
hence thesis;
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
A1: AR.o = ar by MSUALG_1:def 1;
assume p in ((ParsedTerms X)# * (the Arity of S)).o;
then
A2: p in product ((ParsedTerms X) * ar) by A1,MSAFREE:1;
then
A3: dom p = dom ((ParsedTerms X) * ar) by CARD_3:9;
hence dom p = dom ar by PARTFUN1:def 2;
A4: dom ((ParsedTerms X) * ar) = dom ar by PARTFUN1:def 2;
let n be Nat;
assume
A5: n in dom p;
then ((ParsedTerms X) * ar).n = (ParsedTerms X).(ar.n) by A3,FUNCT_1:12
.= (ParsedTerms X). (ar/.n) by A3,A4,A5,PARTFUN1:def 6
.= ParsedTerms(X,ar/.n) by Def8;
hence thesis by A2,A3,A5,CARD_3:9;
end;
assume that
A6: dom p = dom (the_arity_of o) and
A7: for n be Nat st n in dom p holds p.n in ParsedTerms(X,(the_arity_of o)/.n);
A8: dom p = dom ((ParsedTerms X) * ar) by A6,PARTFUN1:def 2;
A9: for x be object st x in dom((ParsedTerms X) * ar) holds p.x in ((
ParsedTerms X) * ar).x
proof
let x be object;
assume
A10: 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 A6,A8,A10,PARTFUN1:def 6
.= ((ParsedTerms X) * ar).x by A10,FUNCT_1:12;
hence thesis by A7,A8,A10;
end;
AR.o = ar by MSUALG_1:def 1;
then ((ParsedTerms X)# * AR).o = product ((ParsedTerms X) * ar) by MSAFREE:1;
hence thesis by A8,A9,CARD_3:9;
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;
set r = roots p, OU = [:the carrier' of S,{the carrier of S}:] \/ Union (
coprod X);
A1: dom p = dom r by TREES_3:def 18;
thus OSSym(o,X) ==> roots p implies p in ((ParsedTerms X)# * (the Arity of S
)).o
proof
assume OSSym(o,X) ==> roots p;
then
A2: [[o,the carrier of S],roots p] in OSREL(X) by LANG1:def 1;
then reconsider
r = roots p as Element of ([:the carrier' of S,{the carrier of
S}:] \/ Union (coprod X))* by ZFMISC_1:87;
A3: dom p = dom r by TREES_3:def 18;
A4: 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;
A5: rng r c= [:the carrier' of S,{the carrier of S}:] \/ Union (coprod
X) by FINSEQ_1:def 4;
A6: rng p c= TS D by FINSEQ_1:def 4;
assume
A7: n in dom p;
then consider T be DecoratedTree such that
A8: T = p.n and
A9: r.n = T.{} by TREES_3:def 18;
p.n in rng p by A7,FUNCT_1:def 3;
then reconsider T as Element of TS(D) by A8,A6;
A10: r.n in rng r by A3,A7,FUNCT_1:def 3;
per cases by A5,A10,XBOOLE_0:def 3;
suppose
A11: r.n in [:the carrier' of S,{the carrier of S}:];
then consider
o1 being Element of the carrier' of S, x2 being Element of {
the carrier of S} such that
A12: r.n = [o1,x2] by DOMAIN_1:1;
A13: x2 = the carrier of S by TARSKI:def 1;
then the_result_sort_of o1 <= ar/.n by A2,A3,A7,A11,A12,Th2;
then ex o be OperSymbol of S st [o,the carrier of S] = T.{} &
the_result_sort_of o <= s by A9,A12,A13;
hence thesis by A8;
end;
suppose
A14: r.n in Union (coprod X);
then reconsider t = r.n as Terminal of D by Th3;
A15: T = root-tree t by A9,DTCONSTR:9;
consider i being Element of S such that
A16: i <= ar/.n and
A17: r.n in coprod(i,X) by A2,A3,A7,A14,Th2;
ex a be set st a in X.i & r.n = [a,i] by A17,MSAFREE:def 2;
hence thesis by A8,A16,A15;
end;
end;
A18: Seg len ar = dom ar by FINSEQ_1:def 3;
A19: dom r = Seg len r by FINSEQ_1:def 3;
len r = len ar by A2,Th2;
hence thesis by A3,A19,A18,A4,Th6;
end;
assume
A20: p in ((ParsedTerms X)# * (the Arity of S)).o;
A21: dom r = Seg len r by FINSEQ_1:def 3;
reconsider r as FinSequence of OU;
reconsider r as Element of OU* by FINSEQ_1:def 11;
A22: Union (coprod X) misses [:the carrier' of S,{the carrier of S}:] by
MSAFREE:4;
A23: for x be set st x in dom r holds (r.x in [:the carrier' 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
A24: x in dom r;
then reconsider n = x as Nat;
set s = ar/.n;
p.n in ParsedTerms(X,s) by A20,A1,A24,Th6;
then consider a be Element of TS D such that
A25: a = p.n and
A26: (ex s1 being Element of S, x be object 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;
A27: ex T be DecoratedTree st T = p.n & r.n = T.{} by A1,A24,TREES_3:def 18;
thus r.x in [:the carrier' 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
A28: r.x in [:the carrier' of S,{the carrier of S}:];
A29: now
given s1 being Element of S, y be set such that
s1 <= s and
A30: y in X.s1 and
A31: a = root-tree [y,s1];
A32: [y,s1] in coprod(s1,X) by A30,MSAFREE:def 2;
dom coprod(X) = the carrier of S by PARTFUN1:def 2;
then (coprod(X)).s1 in rng coprod(X) by FUNCT_1:def 3;
then
A33: coprod(s1,X) in rng coprod(X) by MSAFREE:def 3;
r.x = [y,s1] by A25,A27,A31,TREES_4:3;
then r.x in union rng coprod(X) by A32,A33,TARSKI:def 4;
then r.x in Union (coprod X) by CARD_3:def 4;
hence contradiction by A22,A28,XBOOLE_0:3;
end;
let o1 be OperSymbol of S;
assume [o1,the carrier of S] = r.x;
hence thesis by A25,A26,A27,A29,XTUPLE_0:1;
end;
assume
A34: r.x in Union (coprod X);
now
given o1 be OperSymbol of S such that
A35: [o1,the carrier of S] = a.{} and
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 carrier' of S,{the carrier of S}:]
by ZFMISC_1:87;
hence contradiction by A22,A25,A27,A34,A35,XBOOLE_0:3;
end;
then consider s1 being Element of S, y be set such that
A36: s1 <= s and
A37: y in X.s1 and
A38: a = root-tree [y,s1] by A26;
take s1;
r.x = [y,s1] by A25,A27,A38,TREES_4:3;
hence thesis by A36,A37,MSAFREE:def 2;
end;
dom p = dom ar by A20,Th6;
then len r = len ar by A1,A21,FINSEQ_1:def 3;
then [[o,the carrier of S],r] in OSREL X by A23,Th2;
hence thesis by 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 by PARTFUN1:def 2;
thus union rng (ParsedTerms X) c= TS D
proof
let x be object;
assume x in union rng (ParsedTerms X);
then consider A be set such that
A2: x in A and
A3: A in rng (ParsedTerms X) by TARSKI:def 4;
consider s be object such that
A4: s in dom (ParsedTerms X) and
A5: (ParsedTerms X).s = A by A3,FUNCT_1:def 3;
reconsider s as Element of S by A4;
A = ParsedTerms(X,s) by A5,Def8
.= {a where a is Element of TS(D):
(ex s1 being Element of S, x be object
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};
then
ex a be Element of TS(D) st a = x &(
(ex s1 being Element of S, x be object
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;
hence thesis;
end;
let x be object;
A6: the carrier of D = (Terminals D) \/ (NonTerminals D) by LANG1:1;
assume x in TS D;
then reconsider t = x as Element of TS(D);
A7: rng t c= the carrier of D by RELAT_1:def 19;
A8: NonTerminals D = [:the carrier' of S,{the carrier of S}:] by Th3;
A9: Terminals D = Union (coprod X) by Th3;
{} in dom t by TREES_1:22;
then
A10: t.{} in rng t by FUNCT_1:def 3;
per cases by A7,A10,A6,XBOOLE_0:def 3;
suppose
A11: t.{} in Terminals D;
then reconsider a = t.{} as Terminal of D;
a in union rng(coprod X) by A9,A11,CARD_3:def 4;
then consider A be set such that
A12: a in A and
A13: A in rng(coprod X) by TARSKI:def 4;
consider s be object such that
A14: s in dom coprod X and
A15: (coprod X).s = A by A13,FUNCT_1:def 3;
reconsider s as Element of S by A14;
A = coprod(s,X) by A15,MSAFREE:def 3;
then
A16: ex b be set st b in X.s & a = [b,s] by A12,MSAFREE:def 2;
t = root-tree a by DTCONSTR:9;
then t in ParsedTerms(X,s) by A16;
then
A17: t in (ParsedTerms X).s by Def8;
(ParsedTerms X).s in rng (ParsedTerms X) by A1,FUNCT_1:def 3;
hence thesis by A17,TARSKI:def 4;
end;
suppose
t.{} in NonTerminals D;
then reconsider a = t.{} as NonTerminal of D;
consider o being Element of the carrier' of S, x2 being Element of {the
carrier of S} such that
A18: a = [o,x2] by A8,DOMAIN_1:1;
set rs = the_result_sort_of o;
x2 = the carrier of S by TARSKI:def 1;
then t in ParsedTerms(X,rs) by A18;
then
A19: t in (ParsedTerms X).rs by Def8;
(ParsedTerms X).rs in rng (ParsedTerms X) by A1,FUNCT_1:def 3;
hence thesis by A19,TARSKI:def 4;
end;
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 carrier' of S, rs =
the_result_sort_of o, RS = the ResultSort of S;
defpred P[object,object] means
for p be FinSequence of TS D st p = $1 holds $2 =
(OSSym(o,X))-tree p;
A1: for x be object st x in AL ex y be object st y in AX & P[x,y]
proof
let x be object;
assume
A2: x in AL;
then reconsider p = x as FinSequence of TS(D) by Th5;
OSSym(o,X) ==> roots p by A2,Th7;
then reconsider a = (OSSym(o,X))-tree p as Element of TS D by
DTCONSTR:def 1;
take y = (OSSym(o,X))-tree p;
o in O;
then o in dom ((ParsedTerms X) * RS) by PARTFUN1:def 2;
then
A3: AX =(ParsedTerms X).(RS.o) by FUNCT_1:12
.= (ParsedTerms X).rs by MSUALG_1:def 2
.= ParsedTerms(X,rs) by Def8;
a.{} = OSSym(o,X) by TREES_4:def 4;
hence y in AX by A3;
thus thesis;
end;
consider f be Function such that
A4: dom f = AL & rng f c= AX & for x be object st x in AL holds P[x,f.x]
from FUNCT_1:sch 6(A1);
reconsider g = f as Function of AL,rng f by A4,FUNCT_2:1;
reconsider g as Function of AL,AX by A4,FUNCT_2:2;
take g;
let p be FinSequence of TS D;
assume OSSym(o,X) ==> roots p;
then p in AL by Th7;
hence thesis by A4;
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
A5: for p be FinSequence of TS D st OSSym(o,X) ==> roots p holds f.p
= (OSSym(o,X))-tree p and
A6: for p be FinSequence of TS D st OSSym(o,X) ==> roots p holds g.p
= (OSSym(o,X))-tree p;
A7: for x be object st x in AL holds f.x = g.x
proof
let x be object;
assume
A8: x in AL;
then reconsider p = x as FinSequence of TS(D) by Th5;
A9: OSSym(o,X) ==> roots p by A8,Th7;
then f.p = (OSSym(o,X))-tree p by A5;
hence thesis by A6,A9;
end;
A10: dom g = AL by FUNCT_2:def 1;
dom f = AL by FUNCT_2:def 1;
hence thesis by A10,A7,FUNCT_1:2;
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
defpred P[object,object] means
for o be OperSymbol of S st $1 = o holds $2 =
PTDenOp(o,X);
set Y = the carrier' of S;
A1: for x be object st x in Y ex y be object st P[x,y]
proof
let x be object;
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 object st x in Y holds P[x,f.x] from CLASSES1:
sch 1( A1);
reconsider f as ManySortedSet of Y by A2,PARTFUN1:def 2,RELAT_1:def 18;
for x be object st x in dom f holds f.x is Function
proof
let x be object;
assume x in dom f;
then reconsider o = x as OperSymbol of S;
f.o = PTDenOp(o,X) by A2;
hence thesis;
end;
then reconsider f as ManySortedFunction of Y by FUNCOP_1:def 6;
for x be object 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 object;
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 PBOOLE:def 15;
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 object st i in the carrier' of S holds A.i = B.i
proof
let i be object;
assume i in the carrier' of S;
then reconsider s = i as OperSymbol of S;
A.s = PTDenOp(s,X) by A3;
hence thesis by A4;
end;
hence thesis;
end;
end;
definition
let S be OrderSortedSign, X be non-empty ManySortedSet of S;
func ParsedTermsOSA(X) -> OSAlgebra of S equals
MSAlgebra (# ParsedTerms(X),
PTOper(X) #);
coherence by OSALG_1:17;
end;
registration
let S be OrderSortedSign, X be non-empty ManySortedSet of S;
cluster ParsedTermsOSA(X) -> strict non-empty;
coherence by MSUALG_1:def 3;
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; :: redefines OSSym (OSAFREE, definition)
coherence
proof
A1: the carrier of S in { the carrier of S } by TARSKI:def 1;
NonTerminals DTConOSA X = [:the carrier' of S,{the carrier of S}:] by Th3;
hence thesis by A1,ZFMISC_1:87;
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 object 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);
{a where a is Element of TS(DTConOSA(X)):
(ex s1 being Element of S, x be object
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
)
.= (the Sorts of PTA).s by 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 t = [x,s] as Terminal of D by A1,Th4;
reconsider s0 = s, s11 = s1 as Element of S;
reconsider SPTA = the Sorts of PTA as OrderSortedSet of S;
root-tree t is Element of TS D;
hence root-tree [x,s] is Element of TS D;
thus
A2: for z being set holds [z,the carrier of S] <> (root-tree [x,s]).{}
proof
let z be set;
assume
A3: [z,the carrier of S] = (root-tree [x,s]).{};
(root-tree [x,s]).{} = [x,s] by TREES_4:3;
then s = the carrier of S by A3,XTUPLE_0:1;
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 object
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
A4: a = root-tree [x,s] and
A5: (ex s2 being Element of S, x be object
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
A6: s2 <= s1 and
x1 in X.s2 and
A7: a = root-tree [x1,s2] by A2,A4,A5;
[x1,s2] = [x,s] by A4,A7,TREES_4:4;
hence s <= s1 by A6,XTUPLE_0:1;
end;
assume s <= s1;
then
A8: SPTA.s0 c= SPTA.s11 by OSALG_1:def 16;
root-tree t in {a where a is Element of TS(DTConOSA(X)): (ex s1 being
Element of S, x be object 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 root-tree [x,s] in SPTA.s0 by Th9;
hence thesis by A8;
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);
consider p being FinSequence of TS G such that
A2: t = OSSym(o,X)-tree p and
A3: OSSym(o,X) ==> roots p by A1,DTCONSTR:10;
reconsider p as SubtreeSeq of OSSym(o,X) by A3,DTCONSTR:def 6;
p in ((ParsedTerms X)# * (the Arity of S)).o by A3,Th7;
then
A4: p in Args(o,ParsedTermsOSA(X)) by MSUALG_1:def 4;
Den(o,PTA).p = ((the Charact of PTA).o).p by MSUALG_1:def 6
.= PTDenOp(o,X).p by Def10
.= t by A2,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 A2,A3,A4;
thus
A5: 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 XTUPLE_0:1;
then s2 in s2;
hence contradiction;
end;
set s = the_result_sort_of o;
let s1 be 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 object
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
A6: a = t and
A7: (ex s2 being Element of S, x be object
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;
thus s <= s1 by A1,A5,A6,A7,XTUPLE_0:1;
end;
reconsider s0 = s, s11 = s1 as Element of S;
reconsider SPTA = the Sorts of PTA as OrderSortedSet of S;
assume the_result_sort_of o <= s1;
then
A8: SPTA.s0 c= SPTA.s11 by OSALG_1:def 16;
t in {a where a is Element of TS(DTConOSA(X)): (ex s1 being Element of S
, x be object
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 t in SPTA.s by Th9;
hence thesis by A8;
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;
then reconsider nt1 = nt as NonTerminal of D by LANG1:def 3;
reconsider ts1 = ts as SubtreeSeq of nt1 by A1,DTCONSTR:def 6;
thus nt in NonTerminals D by A2,LANG1:def 3;
then nt in [:the carrier' of S,{the carrier of S}:] by Th3;
then consider o1,b1 being object such that
A3: o1 in the carrier' of S and
A4: b1 in {the carrier of S} and
A5: nt = [o1,b1] by ZFMISC_1:def 2;
nt1-tree ts1 in TS D;
hence nt-tree ts in TS DTConOSA(X);
reconsider o1 as OperSymbol of S by A3;
take o1;
thus nt = [o1,the carrier of S] by A4,A5,TARSKI:def 1;
b1 = the carrier of S by A4,TARSKI:def 1;
then
A6: (nt1-tree ts).{} = [o1,the carrier of S] by A5,TREES_4:def 4;
then ex p being SubtreeSeq of OSSym(o1,X) st (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;
hence thesis by 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);
hereby
assume
A1: x in Args(o,PTA);
then
A2: x in ((the Sorts of PTA)# * the Arity of S).o by MSUALG_1:def 4;
hence x is FinSequence of TS(DTConOSA(X)) by Th5;
x in ((ParsedTerms X)# * (the Arity of S)).o by A1,MSUALG_1:def 4;
then reconsider x1 = x as FinSequence of TS(DTConOSA(X)) by Th5;
OSSym(o,X) ==> roots x1 by A2,Th7;
hence OSSym(o,X) ==> roots x;
end;
assume that
A3: x is FinSequence of TS(DTConOSA(X)) and
A4: OSSym(o,X) ==> roots x;
reconsider x1 = x as FinSequence of TS(DTConOSA(X)) by A3;
x1 in ((ParsedTerms X)# * (the Arity of S)).o by A4,Th7;
hence thesis by MSUALG_1:def 4;
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
proof
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 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
A2: 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] and
ts in Args(o,ParsedTermsOSA(X)) and
nt-tree ts = Den(o,ParsedTermsOSA(X)).ts and
A3: 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 A2,Th12;
reconsider s = the_result_sort_of o as SortSymbol of S;
take s;
thus thesis by A3;
end;
A4: for s being Symbol of D st s in Terminals D holds P[root-tree s]
proof
let sy be Symbol of D;
assume sy in Terminals D;
then consider s being Element of S, x being set such that
A5: x in X.s and
A6: sy = [x,s] by Th4;
reconsider s as SortSymbol of S;
take s;
thus thesis by A5,A6,Th10;
end;
for t being DecoratedTree of the carrier of D st t in TS(D) holds P[t]
from DTCONSTR:sch 7(A4,A1);
hence thesis;
end;
uniqueness
proof
let s2,s3 be SortSymbol of S such that
A7: t in (the Sorts of ParsedTermsOSA(X)).s2 and
A8: for s1 being Element of S st t in (the Sorts of ParsedTermsOSA(X))
. s1 holds s2 <= s1 and
A9: t in (the Sorts of ParsedTermsOSA(X)).s3 and
A10: for s1 being Element of S st t in (the Sorts of ParsedTermsOSA(X))
. s1 holds s3 <= s1;
A11: s2 <= s3 by A8,A9;
s3 <= s2 by A7,A10;
hence thesis by A11,ORDERS_2:2;
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;
end;
theorem Th14:
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;
TS DTConOSA X = union rng (ParsedTerms X) by Th8
.= Union (the Sorts of ParsedTermsOSA(X)) by CARD_3:def 4;
hence thesis;
end;
theorem Th15:
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 PARTFUN1:def 2;
then SPTA.s in rng SPTA by FUNCT_1:def 3;
then x in union rng SPTA by A1,TARSKI:def 4;
then reconsider x1=x as Element of Union SPTA by CARD_3:def 4;
x1 is Element of PTA;
hence thesis by Th14;
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: for s1 being Element of S st t in (the Sorts of ParsedTermsOSA(X)).s1
holds s2 <= s1 by A1,A2,Th10;
t in (the Sorts of ParsedTermsOSA(X)).s2 by A1,A2,Th10;
hence thesis by A3,Def12;
end;
theorem Th17:
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));
reconsider x1 = x as FinSequence of TS(DTConOSA(X)) by Th13;
set PTA = ParsedTermsOSA(X);
let t being Element of TS DTConOSA(X) such that
A1: t = Den(o,ParsedTermsOSA(X)).x;
OSSym(o,X) ==> roots x by Th13;
then consider o1 being OperSymbol of S such that
A2: OSSym(o,X) = [o1,the carrier of S] and
x1 in Args(o1,ParsedTermsOSA(X)) and
A3: OSSym(o,X)-tree x1 = Den(o1,ParsedTermsOSA(X)).x1 and
A4: 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 Th12;
A5: o = o1 by A2,XTUPLE_0:1;
then t in (the Sorts of PTA).(the_result_sort_of o) by A1,A3,A4;
hence thesis by A1,A3,A4,A5,Def12;
end;
:: WHY is this necessary??? bug?
registration
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
:Def13:
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[object,object] means
ex t being Element of TS D st t = $1 & LeastSort
t = $2;
A1: rng x c= TS D by FINSEQ_1:def 4;
A2: for x being object st x in TS D
ex y being object st y in the carrier of S & P[x,y]
proof
let x being object;
assume x in TS D;
then reconsider t = x as Element of TS D;
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 object st x in TS D holds P[x,f.x] from FUNCT_2:sch 1(A2);
take f*x;
thus dom (f*x) = dom x by FINSEQ_3:120;
let y being Nat such that
A4: y in dom x;
x.y in rng x by A4,FUNCT_1:3;
then reconsider t1 = x.y as Element of TS D by A1;
take t1;
thus t1 = x.y;
A5: ex t2 being Element of TS D st t2 = t1 & LeastSort t2 = f.t1 by A3;
y in dom (f*x) by A4,FINSEQ_3:120;
hence thesis by A5,FINSEQ_3:120;
end;
uniqueness
proof
set D = DTConOSA(X);
let f1,f2 be Element of (the carrier of S)* such that
A6: dom f1 = dom x and
A7: 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
A8: dom f2 = dom x and
A9: 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;
A11: ex t2 being Element of TS D st t2 = x.k & f2.k = LeastSort t2 by A6,A9
,A10;
ex t1 being Element of TS D st t1 = x.k & f1.k = LeastSort t1 by A6,A7
,A10;
hence thesis by A11;
end;
hence thesis by A6,A8,FINSEQ_1:13;
end;
end;
:: all these should be generalized to any leastsorted osa
theorem Th18:
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;
reconsider SPTA = the Sorts of PTA as OrderSortedSet of S;
A1: dom LSx = dom x by Def13;
hereby
assume
A2: LeastSorts x <= w;
then
A3: len LSx = len w;
then
A4: dom LSx = dom w by FINSEQ_3:29;
A5: 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
A6: k in dom x;
consider t2 being Element of TS DTConOSA(X) such that
A7: t2 = x.k and
A8: LSx.k = LeastSort t2 by A6,Def13;
reconsider wk = (w/.k) as Element of S;
(w/.k) = w.k by A1,A4,A6,PARTFUN1:def 6;
then LeastSort t2 <= wk by A1,A2,A6,A8;
then
A9: SPTA.(LeastSort t2) c= SPTA.wk by OSALG_1:def 16;
t2 in (the Sorts of PTA).(LeastSort t2) by Def12;
hence thesis by A7,A9;
end;
len x = len w by A1,A3,FINSEQ_3:29;
hence x in Args(o,PTA) by A5,MSAFREE2:5;
end;
assume
A10: x in Args(o,PTA);
then
A11: dom x = dom w by MSUALG_6:2;
hence len LSx = len w by A1,FINSEQ_3:29;
let i be set such that
A12: i in dom LSx;
reconsider k = i as Nat by A12;
i in dom w by A11,A12,Def13;
then
A13: x.k in (the Sorts of PTA).(w/.k) by A10,MSUALG_6:2;
i in dom x by A12,Def13;
then
A14: ex t2 being Element of TS D st t2 = x.k & LSx.k = LeastSort t2 by Def13;
let s1,s2 be Element of S such that
A15: s1 = LSx.i and
A16: s2 = w.i;
w/.k = w.k by A1,A11,A12,PARTFUN1:def 6;
hence thesis by A15,A16,A14,A13,Def12;
end;
registration
cluster locally_directed regular for monotone OrderSortedSign;
existence
proof
set S1 = the 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
:Def14:
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
:Def15:
[it,the carrier of S] = t;
existence
proof
set D = DTConOSA(X), OU = [:the carrier' of S,{the carrier of S}:] \/
Union (coprod (X qua ManySortedSet of S));
reconsider a = t as Element of OU;
consider p be FinSequence such that
A2: t ==> p by A1;
[t,p] in the Rules of D by A2,LANG1:def 1;
then reconsider p as Element of OU* by ZFMISC_1:87;
[a,p] in OSREL(X) by A2,LANG1:def 1;
then a in [:the carrier' of S,{the carrier of S}:] by Def4;
then consider
o being Element of the carrier' of S, x2 being Element of {the
carrier of S} such that
A3: a = [o,x2] by DOMAIN_1:1;
take o;
thus thesis by A3,TARSKI:def 1;
end;
uniqueness by XTUPLE_0:1;
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
:Def16:
root-tree t;
correctness by A1,DTCONSTR:def 1;
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
:
Def17: for R be monotone OSCongruence of ParsedTermsOSA(X) holds it c= R;
existence
proof
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(object) =
{[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 object st i in the carrier of S holds f.i = F(i) from
PBOOLE:sch 4;
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 object;
assume z in f.i;
then
ex x,y being Element of TS D st z = [x,y] & x in SPTA.i & y in
SPTA.i & MC[x,y,i] by A4;
hence z in [:SPTA.i,SPTA.i:] by ZFMISC_1:87;
end;
then reconsider fi = f.i as Relation of SPTA.i by TARSKI:def 3;
now
let x,y,z be object such that
A5: x in SPTA.s and
A6: y in SPTA.s and
A7: z in SPTA.s and
A8: [x,y] in fi and
A9: [y,z] in fi;
thus [x,z] in fi
proof
reconsider t1=x,t2=y,t3=z as Element of TS D by A5,A6,A7,Th15;
A10: ex t6,t7 being Element of TS D st [t2,t3] = [t6,t7] & t6 in
SPTA.i & t7 in SPTA.i & MC[t6,t7,i] by A4,A9;
A11: ex t4,t5 being Element of TS D st [t1,t2] = [t4,t5] & t4 in
SPTA.i & t5 in SPTA.i & MC[t4,t5,i] by A4,A8;
now
let R be monotone OSCongruence of PTA;
A12: [t2,t3] in R.s by A10;
field(R.s) = SPTA.s by ORDERS_1:12;
then
A13: R.s is_transitive_in SPTA.s by RELAT_2:def 16;
[t1,t2] in R.s by A11;
hence [t1,t3] in R.s by A5,A6,A7,A12,A13,RELAT_2:def 8;
end;
hence thesis by A4,A5,A7;
end;
end;
then
A14: fi is_transitive_in SPTA.s by RELAT_2:def 8;
now
let x,y be object such that
A15: x in SPTA.s and
A16: y in SPTA.s and
A17: [x,y] in fi;
thus [y,x] in fi
proof
reconsider t1=x,t2=y as Element of TS D by A15,A16,Th15;
A18: ex t3,t4 being Element of TS D st [t1,t2] = [t3,t4] & t3 in
SPTA.i & t4 in SPTA.i & MC[t3,t4,i] by A4,A17;
now
let R be monotone OSCongruence of PTA;
field(R.s) = SPTA.s by ORDERS_1:12;
then
A19: R.s is_symmetric_in SPTA.s by RELAT_2:def 11;
[t1,t2] in R.s by A18;
hence [t2,t1] in R.s by A15,A16,A19,RELAT_2:def 3;
end;
hence thesis by A4,A15,A16;
end;
end;
then
A20: fi is_symmetric_in SPTA.s by RELAT_2:def 3;
now
let x be object such that
A21: x in SPTA.s;
thus [x,x] in fi
proof
reconsider t1 = x as Element of TS D by A21,Th15;
now
let R be monotone OSCongruence of PTA;
field(R.s) = SPTA.s by ORDERS_1:12;
then R.s is_reflexive_in SPTA.s by RELAT_2:def 9;
hence [t1,t1] in R.s by A21,RELAT_2:def 1;
end;
hence thesis by A4,A21;
end;
end;
then
A22: fi is_reflexive_in SPTA.s by RELAT_2:def 1;
then
A23: field fi = SPTA.s by ORDERS_1:13;
dom fi = SPTA.s by A22,ORDERS_1:13;
hence thesis by A23,A20,A14,PARTFUN1:def 2,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 1;
reconsider f as ManySortedRelation of PTA;
for i be object, 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 2;
then reconsider f as MSEquivalence-like ManySortedRelation of PTA by
MSUALG_4:def 3;
f is os-compatible
proof
let s1,s2 being Element of S such that
A24: s1 <= s2;
A25: 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;
A26: 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
A27: x in SPTA.s1 and
A28: y in SPTA.s1;
hereby
assume [x,y] in f.s1;
then consider t1,t2 being Element of TS D such that
A29: [x,y]=[t1,t2] and
A30: t1 in SPTA.s1 and
A31: t2 in SPTA.s1 and
A32: MC[t1,t2,s1] by A25;
now
let R be monotone OSCongruence of PTA;
A33: R is os-compatible by OSALG_4:def 2;
[t1,t2] in R.s1 by A32;
then [t1,t2] in R.s2 by A24,A30,A31,A33;
hence t1 in SPTA.s2 & t2 in SPTA.s2 & [t1,t2] in R.s2 by ZFMISC_1:87;
end;
hence [x,y] in f.s2 by A26,A29;
end;
assume [x,y] in f.s2;
then consider t1,t2 being Element of TS D such that
A34: [x,y]=[t1,t2] and
t1 in SPTA.s2 and
t2 in SPTA.s2 and
A35: MC[t1,t2,s2] by A26;
A36: y = t2 by A34,XTUPLE_0:1;
A37: now
let R be monotone OSCongruence of PTA;
A38: R is os-compatible by OSALG_4:def 2;
[t1,t2] in R.s2 by A35;
hence [t1,t2] in R.s1 by A24,A27,A28,A34,A38;
end;
x = t1 by A34,XTUPLE_0:1;
hence [x,y] in f.s1 by A25,A27,A28,A36,A37;
end;
then reconsider f as MSEquivalence-like OrderSortedRelation of PTA by
OSALG_4:def 2;
f is monotone
proof
let o1,o2 being OperSymbol of S such that
A39: 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
A40: for y being Nat st y in dom x1 holds [x1.y,x2.y] in f.(w2/.y);
set D1 = Den(o1,PTA).x1, D2 = Den(o2,PTA).x2;
A41: now
let R be monotone OSCongruence of PTA;
A42: now
let y being Nat;
assume y in dom x1;
then
A43: [x1.y,x2.y] in f.(w2/.y) by A40;
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;
then ex x,z being Element of TS D st [x1.y,x2.y] = [x,z] & x in
SPTA.(w2/.y) & z in SPTA.(w2/.y) & MC[x,z,w2/.y] by A43;
hence [x1.y,x2.y] in R.(w2/.y);
end;
then
A44: [D1,D2] in R.rs2 by A39,OSALG_4:def 26;
then
A45: D2 in SPTA.rs2 by ZFMISC_1:87;
D1 in SPTA.rs2 by A44,ZFMISC_1:87;
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 A39,A42,A45,Th15,OSALG_4:def 26;
end;
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;
hence thesis by A41;
end;
then reconsider
f as monotone MSEquivalence-like OrderSortedRelation of PTA;
take f;
let R be monotone OSCongruence of PTA;
let i be object;
assume i in the carrier of S;
then reconsider s = i as Element of S;
A46: 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 object;
assume z in f.i;
then ex x,y being Element of TS D st z = [x,y] & x in SPTA.s & y in
SPTA.s & MC[x,y,s] by A46;
hence thesis;
end;
uniqueness
proof
set PTA = ParsedTermsOSA(X);
let L1,L2 be monotone OSCongruence of PTA such that
A47: for R be monotone OSCongruence of ParsedTermsOSA(X) holds L1 c= R and
A48: for R be monotone OSCongruence of ParsedTermsOSA(X) holds L2 c= R;
A49: L2 c= L1 by A48;
L1 c= L2 by A47;
hence thesis by A49,PBOOLE:146;
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
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
{[
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 object;
assume y in RT;
then consider s1 being Element of S such that
A1: y = [root-tree t,s1] and
A2: ex s be Element of S, x be set st x in X.s & t = [x,s] & s <= s1;
consider s being Element of S, x be set such that
A3: x in X.s and
A4: t = [x,s] and
s <= s1 by A2;
root-tree [x,s] is Element of TS DTConOSA(X) by A3,Th10;
hence thesis by A1,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
{[
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 object;
assume y in NT;
then consider o2 being OperSymbol of S, x2 being Element of Args(o2,
ParsedTermsOSA(X)), s3 being Element of S such that
A1: 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 and
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;
A2: OSSym(o2,X) ==> roots x2 by Th13;
A3: x2 is FinSequence of TS(DTConOSA(X)) by Th13;
then
A4: OSSym(o2,X)-tree x2 in TS DTConOSA(X) by A2,Th12;
consider o being OperSymbol of S such that
A5: OSSym(o2,X) = [o,the carrier of S] and
x2 in Args(o,ParsedTermsOSA(X)) and
A6: OSSym(o2,X)-tree x2 = Den(o,ParsedTermsOSA(X)).x2 and
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,A2,Th12;
o2 = o by A5,XTUPLE_0:1;
hence thesis by A1,A4,A6,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
:Def21:
(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,set,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 DTCONSTR:sch 8;
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,set,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 DTCONSTR:sch 9(A1,A2);
end;
end;
theorem Th19:
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;
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;
defpred P[DecoratedTree of the carrier of D] means R1[$1] & R2[$1];
A1: 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
A2: nt ==> roots ts and
A3: 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
A4: nt = [o,the carrier of S] and
A5: ts in Args(o,PTA) and
A6: nt-tree ts = Den(o,PTA).ts and
A7: for s1 being Element of S holds nt-tree ts in (the Sorts of PTA).
s1 iff the_result_sort_of o <= s1 by A2,Th12;
reconsider x = F * ts as FinSequence of C;
A8: F.(nt-tree ts) = @(nt,x) by A2,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};
reconsider ts1 = ts as Element of Args(o,PTA) by A5;
set w = the_arity_of o;
A9: rng ts c= TS D by FINSEQ_1:def 4;
dom F = TS D by FUNCT_2:def 1;
then len x = len ts by A9,FINSEQ_2:29;
then
A10: dom x = dom ts by FINSEQ_3:29;
A11: dom w = dom ts by A5,MSUALG_3:6;
A12: for y being Nat st y in dom x holds [ts1.y,w/.y] in x.y
proof
let y being Nat such that
A13: y in dom x;
A14: ts1.y in rng ts1 by A10,A13,FUNCT_1:3;
then reconsider t1 = ts1.y as Element of TS D by A9;
ts1.y in SPTA.(w/.y) by A10,A11,A13,MSUALG_6:2;
then [t1,w/.y] in F.t1 by A3,A14;
hence thesis by A10,A13,FUNCT_1:13;
end;
thus R1[nt-tree ts]
proof
let s1 be Element of S;
hereby
assume nt-tree ts in SPTA.s1;
then
A15: the_result_sort_of o <= s1 by A7;
len the_arity_of o = len the_arity_of o;
hence [nt-tree ts,s1] in F.(nt-tree ts) by A4,A6,A10,A11,A12,A8,A15;
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
A16: [nt-tree ts,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 and
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 A8;
s1 = s3 by A16,XTUPLE_0:1;
then
A18: SPTA.(the_result_sort_of o2) c= SPTA.s1 by A17,OSALG_1:def 16;
A19: Den(o2,PTA).x2 in SPTA.(the_result_sort_of o2) by MSUALG_9:18;
nt-tree ts = Den(o2,PTA).x2 by A16,XTUPLE_0:1;
hence thesis by A19,A18;
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
A20: [y,s1] = [Den(o2,PTA).x2,s3] and
A21: 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 and
A22: 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 A8;
consider w3 being Element of (the carrier of S)* such that
A23: dom w3 = dom x and
A24: for y being Nat st y in dom x holds [x2.y,w3/.y] in x.y by A22;
consider o1 being OperSymbol of S such that
A25: nt = [o1,the carrier of S] and
A26: o1 ~= o2 and
A27: len the_arity_of o1 = len the_arity_of o2 and
A28: the_result_sort_of o1 <= s3 and
A29: the_result_sort_of o2 <= s3 by A21;
A30: y = Den(o2,PTA).x2 by A20,XTUPLE_0:1;
reconsider x3 = x2 as FinSequence of TS D by Th13;
reconsider xy = F * x3 as FinSequence of C;
A31: OSSym(o2,X) ==> roots x2 by Th13;
then consider o3 being OperSymbol of S such that
A32: OSSym(o2,X) = [o3,the carrier of S] and
x3 in Args(o3,PTA) and
A33: OSSym(o2,X)-tree x3 = Den(o3,PTA).x3 and
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 Th12;
o2 = o3 by A32,XTUPLE_0:1;
then
A34: F.y = @(OSSym(o2,X),xy) by A30,A31,A33,Def21
.= {[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};
A35: 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:29;
then
A36: dom x3 = dom xy by FINSEQ_3:29;
A37: o1 = o by A4,A25,XTUPLE_0:1;
then
A38: dom the_arity_of o2 = dom the_arity_of o by A27,FINSEQ_3:29;
then
A39: dom w3 = dom xy by A10,A11,A23,A36,MSUALG_3:6;
A40: dom x2 = dom x by A10,A11,A38,MSUALG_3:6;
A41: for y being Nat st y in dom xy holds [ts1.y,w3/.y] in xy.y
proof
let y be Nat such that
A42: y in dom xy;
A43: ts1.y in rng ts1 by A10,A23,A39,A42,FUNCT_1:3;
x2.y in rng x3 by A36,A42,FUNCT_1:3;
then reconsider t1 = ts1.y,t2 = x2.y as Element of TS D by A9,A35,A43;
[x2.y,w3/.y] in x.y by A24,A36,A40,A42;
then [x2.y,w3/.y] in F.(ts1.y) by A10,A23,A39,A42,FUNCT_1:13;
then [t1,w3/.y] in F.(t2) by A3,A43;
hence thesis by A42,FUNCT_1:12;
end;
A44: the_result_sort_of o2 <= s1 by A20,A29,XTUPLE_0:1;
the_result_sort_of o <= s1 by A20,A28,A37,XTUPLE_0:1;
hence thesis by A6,A26,A27,A37,A39,A41,A34,A44;
end;
end;
A45: 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
A46: sy in Terminals D;
reconsider sy1 = sy as Terminal of D by A46;
consider s being Element of S, x being set such that
A47: x in X.s and
A48: sy = [x,s] by A46,Th4;
A49: F.(root-tree sy) = @(sy) by A46,Def21
.= {[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};
root-tree sy1 in {a where a is Element of TS(DTConOSA(X)): (ex s1
being Element of S, x be object
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 A47,A48;
then
A50: root-tree sy1 in SPTA.s by Th9;
thus R1[root-tree sy]
proof
let s1 be Element of S;
hereby
assume root-tree sy in SPTA.s1;
then s <= s1 by A47,A48,Th10;
hence [root-tree sy,s1] in F.(root-tree sy) by A47,A48,A49;
end;
assume [root-tree sy,s1] in F.(root-tree sy);
then consider s3 being Element of S such that
A51: [root-tree sy,s1] = [root-tree sy,s3] and
A52: ex s2 be Element of S, x be set st x in X.s2 & sy = [x,s2] & s2
<= s3 by A49;
A53: s1 = s3 by A51,XTUPLE_0:1;
consider s2 be Element of S, x2 be set such that
x2 in X.s2 and
A54: sy = [x2,s2] and
A55: s2 <= s3 by A52;
s2 = s by A48,A54,XTUPLE_0:1;
then SPTA.s c= SPTA.s1 by A53,A55,OSALG_1:def 16;
hence thesis by A50;
end;
thus R2[root-tree sy]
proof
let s1 be Element of S, y be Element of TS(D);
assume
A56: [y,s1] in F.(root-tree sy);
then
ex s2 being Element of S st [y,s1] = [root-tree sy,s2] & ex s3 be
Element of S, x be set st x in X.s3 & sy = [x,s3] & s3 <= s2 by A49;
then y = root-tree sy by XTUPLE_0:1;
hence thesis by A56;
end;
end;
for t being DecoratedTree of the carrier of D st t in TS(D) holds P[t]
from DTCONSTR:sch 7(A45,A1);
hence thesis;
end;
:: switched to have easier prooving
theorem Th20:
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 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
A2: 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
A3: nt = [o,the carrier of S] and
A4: ts in Args(o,PTA) and
A5: nt-tree ts = Den(o,PTA).ts and
for s1 being Element of S holds nt-tree ts in (the Sorts of PTA).s1
iff the_result_sort_of o <= s1 by A2,Th12;
reconsider x = F * ts as FinSequence of C;
A6: F.(nt-tree ts) = @(nt,x) by A2,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};
reconsider ts1 = ts as Element of Args(o,PTA) by A4;
set w = the_arity_of o;
A7: len the_arity_of o = len the_arity_of o;
let s1 be Element of S;
A8: rng ts c= TS D by FINSEQ_1:def 4;
dom F = TS D by FUNCT_2:def 1;
then len x = len ts by A8,FINSEQ_2:29;
then
A9: dom x = dom ts by FINSEQ_3:29;
A10: dom w = dom ts by A4,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 A9,A12,FUNCT_1:3;
then reconsider t1 = ts1.y as Element of TS D by A8;
ts1.y in SPTA.(w/.y) by A9,A10,A12,MSUALG_6:2;
then [t1,w/.y] in F.t1 by Th19;
hence thesis by A9,A12,FUNCT_1:13;
end;
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
A13: [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
A14: [y,s1] = [Den(o2,PTA).x2,s3] and
A15: 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 and
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 A6,A13;
A16: s1 = s3 by A14,XTUPLE_0:1;
the_result_sort_of o <= s3 by A3,A15,XTUPLE_0:1;
hence thesis by A3,A5,A9,A10,A11,A6,A16,A7;
end;
A17: for s being Symbol of D st s in Terminals D holds R3[root-tree s]
proof
let sy be Symbol of D;
assume sy in Terminals D;
then
A18: F.(root-tree sy) = @(sy) by Def21
.= {[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};
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
A19: [y,s1] in F.(root-tree sy);
ex s3 being Element of S st [y,s1] = [root-tree sy,s3] & ex s2 be
Element of S, x be set st x in X.s2 & sy = [x,s2] & s2 <= s3 by A18,A19;
hence thesis by A19,XTUPLE_0:1;
end;
for t being DecoratedTree of the carrier of D st t in TS(D) holds R3[t]
from DTCONSTR:sch 7(A17,A1);
hence thesis;
end;
theorem Th21:
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);
A1: 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
A2: 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
A3: nt = [o,the carrier of S] and
ts in Args(o,PTA) and
nt-tree ts = Den(o,PTA).ts and
A4: for s1 being Element of S holds nt-tree ts in (the Sorts of PTA).
s1 iff the_result_sort_of o <= s1 by A2,Th12;
reconsider x = F * ts as FinSequence of C;
let s1,s2 be Element of S, y be Element of TS D such that
A5: s1 <= s2 and
A6: nt-tree ts in SPTA.s1 and
A7: y in SPTA.s1;
A8: F.(nt-tree ts) = @(nt,x) by A2,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};
hereby
reconsider s21 = s2 as Element of S;
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
A9: [y,s1] = [Den(o2,PTA).x2,s3] and
A10: 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 and
A11: 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 A8;
consider o1 being OperSymbol of S such that
A12: nt = [o1,the carrier of S] and
A13: o1 ~= o2 and
A14: len the_arity_of o1 = len the_arity_of o2 and
A15: the_result_sort_of o1 <= s3 and
A16: the_result_sort_of o2 <= s3 by A10;
A17: y = Den(o2,PTA).x2 by A9,XTUPLE_0:1;
A18: s1 = s3 by A9,XTUPLE_0:1;
then
A19: the_result_sort_of o2 <= s21 by A5,A16,ORDERS_2:3;
the_result_sort_of o1 <= s21 by A5,A18,A15,ORDERS_2:3;
hence [y,s2] in F.(nt-tree ts) by A8,A11,A17,A12,A13,A14,A19;
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
A20: [y,s2] = [Den(o2,PTA).x2,s3] and
A21: 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 and
A22: 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 A8;
reconsider x3 = x2 as FinSequence of TS D by Th13;
OSSym(o2,X) ==> roots x2 by Th13;
then consider o3 being OperSymbol of S such that
A23: OSSym(o2,X) = [o3,the carrier of S] and
x3 in Args(o3,PTA) and
A24: OSSym(o2,X)-tree x3 = Den(o3,PTA).x3 and
A25: 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 Th12;
A26: y = Den(o2,PTA).x2 by A20,XTUPLE_0:1;
o2 = o3 by A23,XTUPLE_0:1;
then
A27: the_result_sort_of o2 <= s1 by A7,A26,A24,A25;
consider o1 being OperSymbol of S such that
A28: nt = [o1,the carrier of S] and
A29: o1 ~= o2 and
A30: len the_arity_of o1 = len the_arity_of o2 and
the_result_sort_of o1 <= s3 and
the_result_sort_of o2 <= s3 by A21;
the_result_sort_of o <= s1 by A4,A6;
then the_result_sort_of o1 <= s1 by A3,A28,XTUPLE_0:1;
hence thesis by A8,A22,A26,A28,A29,A30,A27;
end;
A31: 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
A32: sy in Terminals D;
reconsider sy1 = sy as Terminal of D by A32;
A33: F.(root-tree sy) = @(sy) by A32,Def21
.= {[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};
let s1,s2 be Element of S, y be Element of TS D such that
A34: s1 <= s2 and
A35: root-tree sy in SPTA.s1 and
y in SPTA.s1;
SPTA.s1 c= SPTA.s2 by A34,OSALG_1:def 16;
then
A36: [root-tree sy1,s2] in F.(root-tree sy) by A35,Th19;
hereby
assume [y,s1] in F.(root-tree sy);
then
ex s3 being Element of S st [y,s1] = [root-tree sy,s3] & ex s2 be
Element of S, x be set st x in X.s2 & sy = [x,s2] & s2 <= s3 by A33;
hence [y,s2] in F.(root-tree sy) by A36,XTUPLE_0:1;
end;
assume [y,s2] in F.(root-tree sy);
then
A37: ex s3 being Element of S st [y,s2] = [root-tree sy,s3] & ex s4 be
Element of S, x be set st x in X.s4 & sy = [x,s4] & s4 <= s3 by A33;
[root-tree sy1,s1] in F.(root-tree sy) by A35,Th19;
hence thesis by A37,XTUPLE_0:1;
end;
for t being DecoratedTree of the carrier of D st t in TS(D) holds R3[t]
from DTCONSTR:sch 7(A31,A1);
hence thesis;
end;
theorem Th22:
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 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
A2: nt ==> roots ts and
A3: 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
A4: nt = [o,the carrier of S] and
A5: ts in Args(o,PTA) and
A6: nt-tree ts = Den(o,PTA).ts and
for s1 being Element of S holds nt-tree ts in (the Sorts of PTA).s1
iff the_result_sort_of o <= s1 by A2,Th12;
reconsider ts1 = ts as Element of Args(o,PTA) by A5;
set w = the_arity_of o;
A7: dom w = dom ts by A5,MSUALG_3:6;
reconsider x = F * ts as FinSequence of C;
A8: rng ts c= TS D by FINSEQ_1:def 4;
dom F = TS D by FUNCT_2:def 1;
then len x = len ts by A8,FINSEQ_2:29;
then
A9: dom x = dom ts by FINSEQ_3:29;
A10: F.(nt-tree ts) = @(nt,x) by A2,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};
thus R3[nt-tree ts]
proof
let s1 be Element of S, y,z be Element of TS(D);
assume that
A11: [y,s1] in F.(nt-tree ts) and
A12: [z,s1] in F.y;
consider o2 being OperSymbol of S, x2 being Element of Args(o2,PTA), s3
being Element of S such that
A13: [y,s1] = [Den(o2,PTA).x2,s3] and
A14: 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 and
A15: 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 A10,A11;
A16: y = Den(o2,PTA).x2 by A13,XTUPLE_0:1;
reconsider x3 = x2 as FinSequence of TS D by Th13;
reconsider xy = F * x3 as FinSequence of C;
A17: OSSym(o2,X) ==> roots x2 by Th13;
then consider o3 being OperSymbol of S such that
A18: OSSym(o2,X) = [o3,the carrier of S] and
x3 in Args(o3,PTA) and
A19: OSSym(o2,X)-tree x3 = Den(o3,PTA).x3 and
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 Th12;
o2 = o3 by A18,XTUPLE_0:1;
then F.y = @(OSSym(o2,X),xy) by A16,A17,A19,Def21
.= {[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};
then consider
o5 being OperSymbol of S, x5 being Element of Args(o5,PTA), s5
being Element of S such that
A20: [z,s1] = [Den(o5,PTA).x5,s5] and
A21: 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 and
A22: 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 A12;
consider o6 being OperSymbol of S such that
A23: OSSym(o2,X) = [o6,the carrier of S] and
A24: o6 ~= o5 and
A25: len the_arity_of o6 = len the_arity_of o5 and
the_result_sort_of o6 <= s5 and
A26: the_result_sort_of o5 <= s5 by A21;
A27: the_result_sort_of o5 <= s1 by A20,A26,XTUPLE_0:1;
reconsider x6 = x5 as FinSequence of TS D by Th13;
reconsider xz = F * x6 as FinSequence of C;
defpred P[object,object] means [ts1.$1,$2] in xz.$1;
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:29;
then
A28: dom x3 = dom xy by FINSEQ_3:29;
consider w5 being Element of (the carrier of S)* such that
dom w5 = dom xy and
A29: for y being Nat st y in dom xy holds [x5.y,w5/.y] in xy.y by A22;
consider w3 being Element of (the carrier of S)* such that
dom w3 = dom x and
A30: for y being Nat st y in dom x holds [x2.y,w3/.y] in x.y by A15;
A31: z = Den(o5,PTA).x5 by A20,XTUPLE_0:1;
A32: OSSym(o5,X) ==> roots x5 by Th13;
then consider o7 being OperSymbol of S such that
A33: OSSym(o5,X) = [o7,the carrier of S] and
x6 in Args(o7,PTA) and
A34: OSSym(o5,X)-tree x6 = Den(o7,PTA).x6 and
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 Th12;
o5 = o7 by A33,XTUPLE_0:1;
then
A35: F.z = @(OSSym(o5,X),xz) by A31,A32,A34,Def21
.= {[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};
consider o1 being OperSymbol of S such that
A36: nt = [o1,the carrier of S] and
A37: o1 ~= o2 and
A38: len the_arity_of o1 = len the_arity_of o2 and
A39: the_result_sort_of o1 <= s3 and
the_result_sort_of o2 <= s3 by A14;
A40: o1 = o by A4,A36,XTUPLE_0:1;
then
A41: the_result_sort_of o <= s1 by A13,A39,XTUPLE_0:1;
A42: dom the_arity_of o2 = dom the_arity_of o by A38,A40,FINSEQ_3:29;
then
A43: dom x2 = dom x by A9,A7,MSUALG_3:6;
A44: rng x6 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:29;
then
A45: dom x6 = dom xz by FINSEQ_3:29;
A46: o6 = o2 by A23,XTUPLE_0:1;
then dom the_arity_of o5 = dom the_arity_of o2 by A25,FINSEQ_3:29;
then
A47: dom x5 = dom (the_arity_of o2) by MSUALG_3:6
.= dom xy by A28,MSUALG_3:6;
A48: rng x3 c= TS D by FINSEQ_1:def 4;
A49: for y being object st y in dom xz
ex sy being object st sy in the carrier of S & P[y,sy]
proof
let y be object such that
A50: y in dom xz;
A51: x5.y in rng x6 by A45,A50,FUNCT_1:3;
A52: x2.y in rng x3 by A28,A45,A47,A50,FUNCT_1:3;
ts1.y in rng ts1 by A9,A28,A43,A45,A47,A50,FUNCT_1:3;
then reconsider
t1 = ts1.y,t2 = x3.y,t3 = x5.y as Element of TS D by A8,A44,A48,A51,A52
;
A53: [x2.y,w3/.y] in x.y by A30,A28,A43,A45,A47,A50;
y in dom ts1 by A7,A42,A28,A45,A47,A50,MSUALG_3:6;
then
A54: [t2,w3/.y] in F.(t1) by A53,FUNCT_1:13;
then [t1,w3/.y] in F.t1 by Th20;
then
A55: t1 in SPTA.(w3/.y) by Th19;
[t1,w3/.y] in F.t2 by A54,Th19;
then [t2,w3/.y] in F.t2 by Th20;
then
A56: t2 in SPTA.(w3/.y) by Th19;
then
A57: LeastSort t2 <= w3/.y by Def12;
[x5.y,w5/.y] in xy.y by A29,A45,A47,A50;
then
A58: [t3,w5/.y] in F.(t2) by A28,A45,A47,A50,FUNCT_1:13;
then [t2,w5/.y] in F.(t2) by Th20;
then
A59: t2 in SPTA.(w5/.y) by Th19;
then LeastSort t2 <= w5/.y by Def12;
then consider s7 being Element of S such that
A60: w5/.y <= s7 and
A61: w3/.y <= s7 by A57,OSALG_4:11;
[t2,w5/.y] in F.t3 by A58,Th19;
then [t3,w5/.y] in F.t3 by Th20;
then t3 in SPTA.(w5/.y) by Th19;
then
A62: [t3,s7] in F.t2 by A58,A59,A60,Th21;
take s7;
thus s7 in the carrier of S;
[x2.y,w3/.y] in F.(ts1.y) by A9,A28,A43,A45,A47,A50,A53,FUNCT_1:13;
then [t2,s7] in F.t1 by A56,A55,A61,Th21;
then [t1,s7] in F.t3 by A3,A9,A28,A43,A45,A47,A50,A62,FUNCT_1:3;
hence thesis by A50,FUNCT_1:12;
end;
consider f being Function of dom xz,(the carrier of S) such that
A63: for y being object st y in dom xz holds P[y,f.y] from FUNCT_2:sch
1(A49);
A64: 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 RELAT_1:def 19;
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;
A65: 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
A66: y in dom xz;
[ts1.y,f.y] in xz.y by A63,A66;
hence thesis by A64,A66,PARTFUN1:def 6;
end;
o5 ~= o by A37,A40,A24,A46,OSALG_1:2;
hence thesis by A6,A38,A40,A25,A46,A65,A35,A27,A41;
end;
end;
A67: for s being Symbol of D st s in Terminals D holds R3[root-tree s]
proof
let sy be Symbol of D;
assume sy in Terminals D;
then
A68: F.(root-tree sy) = @(sy) by Def21
.= {[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};
thus R3[root-tree sy]
proof
let s1 be Element of S, y,z be Element of TS(D);
assume that
A69: [y,s1] in F.(root-tree sy) and
A70: [z,s1] in F.y;
ex s2 being Element of S st [y,s1] = [root-tree sy,s2] & ex s0 be
Element of S, x be set st x in X.s0 & sy = [x,s0] & s0 <= s2 by A68,A69;
then
A71: y = root-tree sy by XTUPLE_0:1;
then
ex s3 being Element of S st [z,s1] = [root-tree sy,s3] & ex s0 be
Element of S, x be set st x in X.s0 & sy = [x,s0] & s0 <= s3 by A68,A70;
hence thesis by A69,A71,XTUPLE_0:1;
end;
end;
for t being DecoratedTree of the carrier of D st t in TS(D) holds R3[t
] from DTCONSTR:sch 7(A67,A1);
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
:Def22:
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(object) =
{[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 object st i in the carrier of S holds R.i = F(i) from
PBOOLE:sch 4;
for i be set st i in the carrier of S holds R.i is Relation of SPTA.i
proof
let i be set such that
A2: i in the carrier of S;
reconsider s = i as Element of S by A2;
A3: R.i = {[x,y] where x,y is Element of TS(D): [x,i] in F.y} by A1,A2;
R.s c= [:SPTA.s,SPTA.s:]
proof
let z be object;
assume z in R.s;
then consider x,y being Element of TS D such that
A4: z = [x,y] and
A5: [x,s] in F.y by A3;
[y,s] in F.x by A5,Th19;
then [x,s] in F.x by Th20;
then
A6: x in SPTA.s by Th19;
[y,s] in F.y by A5,Th20;
then y in SPTA.s by Th19;
hence thesis by A4,A6,ZFMISC_1:87;
end;
hence thesis;
end;
then reconsider R as ManySortedRelation of PTA by MSUALG_4:def 1;
for s1,s2 being Element of S st s1 <= s2 for x,y being set st x in
SPTA.s1 & y in SPTA.s1 holds [x,y] in R.s1 iff [x,y] in R.s2
proof
let s1,s2 be Element of S such that
A7: s1 <= s2;
A8: R.s1 = {[x,y] where x,y is Element of TS(D): [x,s1] in F.y} by A1;
A9: R.s2 = {[x,y] where x,y is Element of TS(D): [x,s2] in F.y} by A1;
let x,y be set such that
A10: x in SPTA.s1 and
A11: y in SPTA.s1;
hereby
assume [x,y] in R.s1;
then consider t1,t2 being Element of TS D such that
A12: [x,y] = [t1,t2] and
A13: [t1,s1] in F.t2 by A8;
A14: y = t2 by A12,XTUPLE_0:1;
x = t1 by A12,XTUPLE_0:1;
then [t1,s2] in F.t2 by A7,A10,A11,A13,A14,Th21;
hence [x,y] in R.s2 by A9,A12;
end;
assume [x,y] in R.s2;
then consider t1,t2 being Element of TS D such that
A15: [x,y] = [t1,t2] and
A16: [t1,s2] in F.t2 by A9;
A17: y = t2 by A15,XTUPLE_0:1;
x = t1 by A15,XTUPLE_0:1;
then [t1,s1] in F.t2 by A7,A10,A11,A16,A17,Th21;
hence thesis by A8,A15;
end;
then
A18: R is os-compatible;
defpred IRREL[Element of TS D,Element of S] means (ex s1 being Element of
S, x be object
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;
reconsider R as OrderSortedRelation of PTA by A18,OSALG_4:def 2;
for i be object, Ri be Relation of SPTA.i st i in the carrier of S & R.i
= Ri holds Ri is total symmetric transitive Relation of SPTA.i
proof
let i be object, Ri be Relation of SPTA.i such that
A19: i in the carrier of S and
A20: R.i = Ri;
reconsider s = i as Element of S by A19;
A21: Ri = {[x,y] where x,y is Element of TS(D): [x,i] in F.y} by A1,A19,A20;
for x,y being object holds x in SPTA.i & y in SPTA.i & [x,y] in Ri
implies [y,x] in Ri
proof
let x,y be object such that
x in SPTA.i and
y in SPTA.i and
A22: [x,y] in Ri;
consider t1,t2 being Element of TS D such that
A23: [x,y] = [t1,t2] and
A24: [t1,s] in F.t2 by A21,A22;
A25: x = t1 by A23,XTUPLE_0:1;
A26: y = t2 by A23,XTUPLE_0:1;
[t2,s] in F.t1 by A24,Th19;
hence thesis by A21,A25,A26;
end;
then
A27: Ri is_symmetric_in SPTA.i by RELAT_2:def 3;
now
let x,y,z be object such that
x in SPTA.i and
y in SPTA.i and
z in SPTA.i and
A28: [x,y] in Ri and
A29: [y,z] in Ri;
consider t1,t2 being Element of TS D such that
A30: [x,y] = [t1,t2] and
A31: [t1,s] in F.t2 by A21,A28;
A32: [t2,s] in F.t1 by A31,Th19;
consider t22,t3 being Element of TS D such that
A33: [y,z] = [t22,t3] and
A34: [t22,s] in F.t3 by A21,A29;
A35: y = t22 by A33,XTUPLE_0:1;
y = t2 by A30,XTUPLE_0:1;
then [t3,s] in F.t2 by A34,A35,Th19;
then
A36: [t1,s] in F.t3 by A32,Th22;
A37: z = t3 by A33,XTUPLE_0:1;
x = t1 by A30,XTUPLE_0:1;
hence [x,z] in Ri by A21,A37,A36;
end;
then
A38: Ri is_transitive_in SPTA.i by RELAT_2:def 8;
A39: SPTA.s = {a where a is Element of TS(DTConOSA(X)): IRREL[a,s]} by Th9;
now
let x be object such that
A40: x in SPTA.i;
consider t being Element of TS D such that
A41: x = t and
IRREL[t,s] by A39,A40;
[t,s] in F.t by A40,A41,Th19;
hence [x,x] in Ri by A21,A41;
end;
then
A42: Ri is_reflexive_in SPTA.i by RELAT_2:def 1;
then
A43: field Ri = SPTA.i by ORDERS_1:13;
dom Ri = SPTA.i by A42,ORDERS_1:13;
hence thesis by A43,A27,A38,PARTFUN1:def 2,RELAT_2:def 11,def 16;
end;
then R is MSEquivalence_Relation-like by MSUALG_4:def 2;
then reconsider R as MSEquivalence-like OrderSortedRelation of PTA by
MSUALG_4:def 3;
take R;
thus thesis by A1;
end;
uniqueness
proof
set D = DTConOSA(X), F = PTClasses X;
let R1,R2 be MSEquivalence-like OrderSortedRelation of ParsedTermsOSA(X)
such that
A44: for i being set st i in the carrier of S holds R1.i = {[x,y]
where x,y is Element of TS(D): [x,i] in F.y} and
A45: for i being set st i in the carrier of S holds R2.i = {[x,y]
where x,y is Element of TS(D): [x,i] in F.y};
now
let i be object such that
A46: i in the carrier of S;
R1.i = {[x,y] where x,y is Element of TS(D): [x,i] in F.y} by A44,A46;
hence R1.i = R2.i by A45,A46;
end;
hence R1 = R2;
end;
end;
theorem Th23:
for S be locally_directed OrderSortedSign, X be non-empty
ManySortedSet of S, x,y,s being object
st [x,s] in (PTClasses X).y holds x in TS
DTConOSA(X) & y in TS DTConOSA(X) & s in the carrier of S
proof
let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S;
set D = DTConOSA(X), F = PTClasses X;
A1: rng F c= bool [:TS(D), the carrier of S:] by RELAT_1:def 19;
let x,y,s being object such that
A2: [x,s] in (PTClasses X).y;
A3: y in TS D
proof
assume not y in TS D;
then not y in dom F;
hence contradiction by A2,FUNCT_1:def 2;
end;
dom F = TS(D) by FUNCT_2:def 1;
then F.y in rng F by A3,FUNCT_1:3;
hence thesis by A2,A1,A3,ZFMISC_1:87;
end;
theorem Th24:
for S be locally_directed OrderSortedSign, X be non-empty
ManySortedSet of S, C be Component of S, x,y being object
holds [x,y] in CompClass
(PTCongruence X,C) iff ex s1 being Element of S st s1 in C & [x,s1] in (
PTClasses X).y
proof
let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S
, C be Component of S, x,y being object;
hereby
assume [x,y] in CompClass(PTCongruence X,C);
then consider s1 being Element of S such that
A1: s1 in C and
A2: [x,y] in (PTCongruence X).s1 by OSALG_4:def 9;
A3: [x,y] in {[x1,y1] where x1,y1 is Element of TS(DTConOSA(X)): [x1,s1]
in (PTClasses X).y1} by A2,Def22;
take s1;
consider x1,y1 being Element of TS(DTConOSA(X)) such that
A4: [x,y] = [x1,y1] and
A5: [x1,s1] in (PTClasses X).y1 by A3;
x = x1 by A4,XTUPLE_0:1;
hence s1 in C & [x,s1] in (PTClasses X).y by A1,A4,A5,XTUPLE_0:1;
end;
given s1 being Element of S such that
A6: s1 in C and
A7: [x,s1] in (PTClasses X).y;
reconsider x2 = x, y2 = y as Element of TS(DTConOSA(X)) by A7,Th23;
[x2,y2] in {[x1,y1] where x1,y1 is Element of TS(DTConOSA(X)): [x1,s1]
in (PTClasses X).y1} by A7;
then [x2,y2] in (PTCongruence(X)).s1 by Def22;
hence thesis by A6,OSALG_4:def 9;
end;
theorem Th25:
for S be locally_directed OrderSortedSign, X be non-empty
ManySortedSet of S, s be Element of S, x be Element of (the Sorts of
ParsedTermsOSA(X)).s holds OSClass(PTCongruence X,x) = proj1((PTClasses X).x)
proof
let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S
, s be Element of S, x be Element of (the Sorts of ParsedTermsOSA(X)).s;
set R = PTCongruence X, PTA = ParsedTermsOSA(X), D = DTConOSA(X);
for z being object holds z in OSClass(R,x) iff z in proj1((PTClasses X).x)
proof
let z be object;
hereby
assume z in OSClass(R,x);
then [z,x] in CompClass(R, CComp(s)) by EQREL_1:19;
then
ex s1 being Element of S st s1 in CComp(s) & [z,s1] in ( PTClasses
X).x by Th24;
hence z in proj1((PTClasses X).x) by XTUPLE_0:def 12;
end;
assume z in proj1((PTClasses X).x);
then consider s1 being object such that
A1: [z,s1] in (PTClasses X).x by XTUPLE_0:def 12;
reconsider s2 = s1 as Element of S by A1,Th23;
reconsider x1=x,z1=z as Element of TS(D) by A1,Th23;
A2: LeastSort x1 <= s by Def12;
[z1,s2] in (PTClasses X).x1 by A1;
then [x1,s2] in (PTClasses X).x1 by Th20;
then x in (the Sorts of PTA).s1 by Th19;
then LeastSort x1 <= s2 by Def12;
then CComp(s2) = CComp(LeastSort x1) by OSALG_4:4
.= CComp(s) by A2,OSALG_4:4;
then s2 in CComp(s) by EQREL_1:20;
then [z,x] in CompClass(R,CComp(s)) by A1,Th24;
hence thesis by EQREL_1:19;
end;
hence thesis by TARSKI:2;
end;
:: more explicit description of PTCongruence
theorem Th26:
for S being locally_directed OrderSortedSign, X being non-empty
ManySortedSet of S, R being ManySortedRelation of ParsedTermsOSA(X) holds R =
PTCongruence(X) iff
( for s1,s2 being Element of S, x being object st x in X.s1
holds ( s1 <= s2 implies [root-tree [x,s1],root-tree[x,s1]] in R.s2 ) &
for y being object
holds ( [root-tree [x,s1],y] in R.s2 or [y,root-tree [x,s1]] in R.s2)
implies s1 <= s2 & y = root-tree [x,s1] ) & for o1,o2 being OperSymbol of S, x1
being Element of Args(o1,ParsedTermsOSA(X)), x2 being Element of Args(o2,
ParsedTermsOSA(X)), s3 being Element of S holds [Den(o1,ParsedTermsOSA(X)).x1,
Den(o2,ParsedTermsOSA(X)).x2] in R.s3 iff 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 x1 & for y being Nat
st y in dom w3 holds [x1.y,x2.y] in R.(w3/.y)
proof
let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S
, R be ManySortedRelation of ParsedTermsOSA(X);
set PTA = ParsedTermsOSA(X), SPTA = the Sorts of PTA, D = DTConOSA(X), OU =
[:the carrier' of S,{the carrier of S}:] \/ Union (coprod (X qua ManySortedSet
of S)), C = bool [:TS(D), the carrier of S:], F = PTClasses X;
defpred T[ ManySortedSet of the carrier of S] means
( for s1,s2 being Element of S, x being object st x in X.s1
holds ( s1 <= s2 implies [root-tree [x,s1],root-tree[x,s1]] in $1.s2 ) &
for y being object holds ( [root-tree [x,s1],y]
in $1.s2 or [y,root-tree [x,s1]] in $1.s2) implies s1 <= s2 & y = root-tree [x,
s1] );
defpred NT[ ManySortedSet of the carrier of S] means for o1,o2 being
OperSymbol of S, x1 being Element of Args(o1,ParsedTermsOSA(X)), x2 being
Element of Args(o2,ParsedTermsOSA(X)), s3 being Element of S holds [Den(o1,
ParsedTermsOSA(X)).x1,Den(o2,ParsedTermsOSA(X)).x2] in $1.s3 iff 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 x1 & ( for y being Nat st y in dom w3 holds [x1.y,x2.y] in $1.(w3/.y)
);
set P = PTCongruence X;
A1: for R1,R2 be ManySortedRelation of PTA st T[R1] & NT[R1] & T[R2] & NT[R2
] holds R1 = R2
proof
let R1,R2 be ManySortedRelation of PTA;
assume that
A2: T[R1] and
A3: NT[R1] and
A4: T[R2] and
A5: NT[R2];
defpred P[set] means
for x being object, s being Element of S holds [$1,x] in
R1.s iff [$1,x] in R2.s;
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 P
[t] holds P[nt-tree ts]
proof
let nt be Symbol of D, ts be FinSequence of TS(D) such that
A7: nt ==> roots ts and
A8: for t being DecoratedTree of the carrier of D st t in rng ts holds P[t];
nt in { s where s is Symbol of D: ex n being FinSequence st s ==> n
} by A7;
then reconsider nt1 = nt as NonTerminal of D by LANG1:def 3;
reconsider tss = ts as SubtreeSeq of nt1 by A7,DTCONSTR:def 6;
let x be object, s be Element of S;
A9: rng ts c= TS D by FINSEQ_1:def 4;
[nt,roots ts] in the Rules of D by A7,LANG1:def 1;
then reconsider rt = roots ts as Element of OU* by ZFMISC_1:87;
reconsider sy = nt as Element of OU;
[sy,rt] in OSREL(X) by A7,LANG1:def 1;
then sy in [:the carrier' of S,{the carrier of S}:] by Def4;
then consider
o being Element of the carrier' of S, x2 being Element of {the
carrier of S} such that
A10: sy = [o,x2] by DOMAIN_1:1;
A11: x2 = the carrier of S by TARSKI:def 1;
then
A12: (nt-tree tss).{} = [o,the carrier of S] by A10,TREES_4:def 4;
then consider ts2 being SubtreeSeq of OSSym(o,X) such that
A13: nt1-tree tss = OSSym(o,X)-tree ts2 and
OSSym(o,X) ==> roots ts2 and
A14: ts2 in Args(o,PTA) and
A15: nt1-tree tss = Den(o,PTA).ts2 by Th11;
A16: (the Sorts of PTA).s = ParsedTerms(X,s) by Def8
.= {a1 where a1 is Element of TS(DTConOSA(X)): (ex s1 being Element
of S, x be object st s1 <= s & x in X.s1 & a1 = root-tree [x,s1])
or ex o be
OperSymbol of S st [o,the carrier of S] = a1.{} & the_result_sort_of o <= s};
hereby
assume
A17: [nt-tree ts,x] in R1.s;
then x in (the Sorts of PTA).s by ZFMISC_1:87;
then consider a1 being Element of TS(DTConOSA(X)) such that
A18: x = a1 and
A19: (ex s1 being Element of S, y be object st s1 <= s & y in X.s1 &
a1 = root-tree [y,s1]) or ex o be OperSymbol of S st [o,the carrier of S] = a1.
{} & the_result_sort_of o <= s by A16;
not ex s1 being Element of S, y be set st s1 <= s & y in X.s1 &
a1 = root-tree [y,s1]
proof
given s1 being Element of S, y be set such that
s1 <= s and
A20: y in X.s1 and
A21: a1 = root-tree [y,s1];
nt-tree ts = root-tree [y,s1] by A2,A17,A18,A20,A21;
then [y,s1] = nt by TREES_4:17;
then the carrier of S = s1 by A10,A11,XTUPLE_0:1;
then s1 in s1;
hence contradiction;
end;
then consider o1 be OperSymbol of S such that
A22: [o1,the carrier of S] = a1.{} and
the_result_sort_of o1 <= s by A19;
consider ts1 being SubtreeSeq of OSSym(o1,X) such that
a1 = OSSym(o1,X)-tree ts1 and
OSSym(o1,X) ==> roots ts1 and
A23: ts1 in Args(o1,PTA) and
A24: a1 = Den(o1,PTA).ts1 by A22,Th11;
consider ts2 being SubtreeSeq of OSSym(o,X) such that
A25: nt1-tree tss = OSSym(o,X)-tree ts2 and
OSSym(o,X) ==> roots ts2 and
A26: ts2 in Args(o,PTA) and
A27: nt1-tree tss = Den(o,PTA).ts2 by A12,Th11;
A28: len the_arity_of o = len the_arity_of o1 by A3,A17,A18,A23,A24,A26,A27;
reconsider tsb = ts2 as Element of Args(o,PTA) by A26;
reconsider tsa = ts1 as Element of Args(o1,PTA) by A23;
consider w3 being Element of (the carrier of S)* such that
A29: dom w3 = dom tsb and
A30: for y being Nat st y in dom w3 holds [tsb.y,tsa.y] in R1.(w3
/.y) by A3,A17,A18,A24,A27;
A31: ts2 = tss by A25,TREES_4:15;
A32: for y being Nat st y in dom w3 holds [tsb.y,tsa.y] in R2.(w3/.y)
proof
let y be Nat such that
A33: y in dom w3;
A34: tsb.y in rng ts by A31,A29,A33,FUNCT_1:3;
then reconsider t = tsb.y as Element of TS(D) by A9;
[t,tsa.y] in R1.(w3/.y) by A30,A33;
hence thesis by A8,A34;
end;
A35: the_result_sort_of o1 <= s by A3,A17,A18,A23,A24,A26,A27;
A36: the_result_sort_of o <= s by A3,A17,A18,A23,A24,A26,A27;
o ~= o1 by A3,A17,A18,A23,A24,A26,A27;
hence [nt-tree ts,x] in R2.s by A5,A18,A24,A27,A28,A36,A35,A29,A32;
end;
reconsider tsb = ts2 as Element of Args(o,PTA) by A14;
assume
A37: [nt-tree ts,x] in R2.s;
then x in (the Sorts of PTA).s by ZFMISC_1:87;
then consider a1 being Element of TS(DTConOSA(X)) such that
A38: x = a1 and
A39: (ex s1 being Element of S, y be object st s1 <= s & y in X.s1 & a1
= root-tree [y,s1]) or ex o be OperSymbol of S st [o,the carrier of S] = a1.{}
& the_result_sort_of o <= s by A16;
not ex s1 being Element of S, y be set st s1 <= s & y in X.s1 & a1
= root-tree [y,s1]
proof
given s1 being Element of S, y be set such that
s1 <= s and
A40: y in X.s1 and
A41: a1 = root-tree [y,s1];
nt-tree ts = root-tree [y,s1] by A4,A37,A38,A40,A41;
then [y,s1] = nt by TREES_4:17;
then the carrier of S = s1 by A10,A11,XTUPLE_0:1;
then s1 in s1;
hence contradiction;
end;
then consider o1 be OperSymbol of S such that
A42: [o1,the carrier of S] = a1.{} and
the_result_sort_of o1 <= s by A39;
consider ts1 being SubtreeSeq of OSSym(o1,X) such that
a1 = OSSym(o1,X)-tree ts1 and
OSSym(o1,X) ==> roots ts1 and
A43: ts1 in Args(o1,PTA) and
A44: a1 = Den(o1,PTA).ts1 by A42,Th11;
A45: len the_arity_of o = len the_arity_of o1 by A5,A37,A38,A43,A44,A14,A15;
reconsider tsa = ts1 as Element of Args(o1,PTA) by A43;
consider w3 being Element of (the carrier of S)* such that
A46: dom w3 = dom tsb and
A47: for y being Nat st y in dom w3 holds [tsb.y,tsa.y] in R2.(w3/.y
) by A5,A37,A38,A44,A15;
A48: ts2 = tss by A13,TREES_4:15;
A49: for y being Nat st y in dom w3 holds [tsb.y,tsa.y] in R1.(w3/.y)
proof
let y be Nat such that
A50: y in dom w3;
A51: tsb.y in rng ts by A48,A46,A50,FUNCT_1:3;
then reconsider t = tsb.y as Element of TS(D) by A9;
[t,tsa.y] in R2.(w3/.y) by A47,A50;
hence thesis by A8,A51;
end;
A52: the_result_sort_of o1 <= s by A5,A37,A38,A43,A44,A14,A15;
A53: the_result_sort_of o <= s by A5,A37,A38,A43,A44,A14,A15;
o ~= o1 by A5,A37,A38,A43,A44,A14,A15;
hence thesis by A3,A38,A44,A15,A45,A53,A52,A46,A49;
end;
A54: for s being Symbol of D st s in Terminals D holds P[root-tree s]
proof
let sy be Symbol of D;
assume sy in Terminals D;
then consider s being Element of S, x being set such that
A55: x in X.s and
A56: sy = [x,s] by Th4;
let y be object, s1 be Element of S;
hereby
assume
A57: [root-tree sy,y] in R1.s1;
then
A58: y = root-tree [x,s] by A2,A55,A56;
s <= s1 by A2,A55,A56,A57;
hence [root-tree sy,y] in R2.s1 by A4,A55,A56,A58;
end;
assume
A59: [root-tree sy,y] in R2.s1;
then
A60: y = root-tree [x,s] by A4,A55,A56;
s <= s1 by A4,A55,A56,A59;
hence thesis by A2,A55,A56,A60;
end;
A61: for t being DecoratedTree of the carrier of D st t in TS(D) holds P[t
] from DTCONSTR:sch 7(A54,A6);
for i being object st i in the carrier of S holds R1.i = R2.i
proof
let i be object;
assume i in the carrier of S;
then reconsider s = i as Element of S;
for a,b being object holds [a,b] in R1.s iff [a,b] in R2.s
proof
let a,b be object;
A62: (the Sorts of PTA).s = ParsedTerms(X,s) by Def8
.= {a1 where a1 is Element of TS(DTConOSA(X)): (ex s1 being
Element of S, x be object
st s1 <= s & x in X.s1 & a1 = root-tree [x,s1]) or ex o
be OperSymbol of S st [o,the carrier of S] = a1.{} & the_result_sort_of o <= s}
;
hereby
assume
A63: [a,b] in R1.s;
then a in (the Sorts of PTA).s by ZFMISC_1:87;
then ex a1 being Element of TS(DTConOSA(X)) st a = a1 &( (ex s1
being Element of S, x be object
st s1 <= s & x in X.s1 & a1 = root-tree [x,s1]) or
ex o be OperSymbol of S st [o,the carrier of S] = a1.{} & the_result_sort_of o
<= s) by A62;
hence [a,b] in R2.s by A61,A63;
end;
assume
A64: [a,b] in R2.s;
then a in (the Sorts of PTA).s by ZFMISC_1:87;
then
ex a1 being Element of TS(DTConOSA(X)) st a = a1 &( (ex s1 being
Element of S, x be object
st s1 <= s & x in X.s1 & a1 = root-tree [x,s1]) or ex o
be OperSymbol of S st [o,the carrier of S] = a1.{} & the_result_sort_of o <= s)
by A62;
hence thesis by A61,A64;
end;
hence thesis by RELAT_1:def 2;
end;
hence thesis;
end;
A65: NT[PTCongruence X]
proof
let o1,o2 be OperSymbol of S, x1 be Element of Args(o1,ParsedTermsOSA(X)),
x2 be Element of Args(o2,ParsedTermsOSA(X)), s3 be Element of S;
A66: dom (the_arity_of o2) = dom x2 by MSUALG_3:6;
A67: P.s3 = {[x3,y] where x3,y is Element of TS(DTConOSA(X)): [x3,s3] in
F.y} by Def22;
reconsider ts2 = x2 as FinSequence of TS(D) by Th13;
A68: dom (the_arity_of o1) = dom x1 by MSUALG_3:6;
reconsider ts1 = x1 as FinSequence of TS(D) by Th13;
A69: rng ts1 c= TS D by FINSEQ_1:def 4;
reconsider x = F * ts1 as FinSequence of C;
dom F = TS D by FUNCT_2:def 1;
then
A70: len x = len ts1 by A69,FINSEQ_2:29;
then
A71: dom x = dom ts1 by FINSEQ_3:29;
A72: OSSym(o1,X) ==> roots x1 by Th13;
then
A73: F.(OSSym(o1,X)-tree ts1) = @(OSSym(o1,X),x) by Def21
.= {[Den(o3,ParsedTermsOSA(X)).x3,s4] where o3 is OperSymbol of S, x3
is Element of Args(o3,ParsedTermsOSA(X)), s4 is Element of S : ( ex o4 being
OperSymbol of S st OSSym(o1,X) = [o4,the carrier of S] & o4 ~= o3 & len
the_arity_of o4 = len the_arity_of o3 & the_result_sort_of o4 <= s4 &
the_result_sort_of o3 <= s4 ) & ex w3 being Element of (the carrier of S)* st
dom w3 = dom x & for y being Nat st y in dom x holds [x3.y,w3/.y] in x.y};
A74: OSSym(o2,X) ==> roots x2 by Th13;
then reconsider
tx = OSSym(o1,X)-tree ts1, ty = OSSym(o2,X)-tree ts2 as Element
of TS D by A72,Th12;
A75: Den(o2,PTA).x2 = ((PTOper(X)).o2).x2 by MSUALG_1:def 6
.= PTDenOp(o2,X).ts2 by Def10
.= OSSym(o2,X)-tree ts2 by A74,Def9;
A76: Den(o1,PTA).x1 = ((PTOper(X)).o1).x1 by MSUALG_1:def 6
.= PTDenOp(o1,X).ts1 by Def10
.= OSSym(o1,X)-tree ts1 by A72,Def9;
A77: rng ts2 c= TS D by FINSEQ_1:def 4;
hereby
assume [Den(o1,PTA).x1,Den(o2,PTA).x2] in P.s3;
then consider t1,t2 being Element of TS D such that
A78: [Den(o1,PTA).x1,Den(o2,PTA).x2] = [t1,t2] and
A79: [t1,s3] in F.t2 by A67;
A80: Den(o1,PTA).x1 = t1 by A78,XTUPLE_0:1;
A81: Den(o2,PTA).x2 = t2 by A78,XTUPLE_0:1;
[t2,s3] in F.t1 by A79,Th19;
then consider o3 being OperSymbol of S, x3 being Element of Args(o3,
ParsedTermsOSA(X)), s4 being Element of S such that
A82: [t2,s3] = [Den(o3,PTA).x3,s4] and
A83: ex o4 being OperSymbol of S st OSSym(o1,X) = [o4,the carrier
of S] & o4 ~= o3 & len the_arity_of o4 = len the_arity_of o3 &
the_result_sort_of o4 <= s4 & the_result_sort_of o3 <= s4 and
A84: ex w3 being Element of (the carrier of S)* st dom w3 = dom x &
for y being Nat st y in dom x holds [x3.y,w3/.y] in x.y by A76,A73,A80;
consider o4 being OperSymbol of S such that
A85: OSSym(o1,X) = [o4,the carrier of S] and
A86: o4 ~= o3 and
A87: len the_arity_of o4 = len the_arity_of o3 and
A88: the_result_sort_of o4 <= s4 and
A89: the_result_sort_of o3 <= s4 by A83;
A90: o1 = o4 by A85,XTUPLE_0:1;
reconsider ts3 = x3 as FinSequence of TS(D) by Th13;
A91: OSSym(o3,X) ==> roots x3 by Th13;
A92: t2 = Den(o3,PTA).x3 by A82,XTUPLE_0:1;
A93: Den(o3,PTA).x3 = ((PTOper(X)).o3).x3 by MSUALG_1:def 6
.= PTDenOp(o3,X).ts3 by Def10
.= OSSym(o3,X)-tree ts3 by A91,Def9;
then
A94: OSSym(o3,X) = OSSym(o2,X) by A75,A81,A92,TREES_4:15;
s3 = s4 by A82,XTUPLE_0:1;
hence 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 A86,A87,A88
,A89,A90,A94,XTUPLE_0:1;
consider w3 being Element of (the carrier of S)* such that
A95: dom w3 = dom x and
A96: for y being Nat st y in dom x holds [x3.y,w3/.y] in x.y by A84;
take w3;
thus dom w3 = dom x1 by A70,A95,FINSEQ_3:29;
let y be Nat such that
A97: y in dom w3;
A98: ts1.y in rng ts1 by A71,A95,A97,FUNCT_1:3;
A99: ts3 = ts2 by A75,A81,A92,A93,TREES_4:15;
o3 = o2 by A94,XTUPLE_0:1;
then dom the_arity_of o1 = dom the_arity_of o2 by A87,A90,FINSEQ_3:29;
then ts2.y in rng ts2 by A71,A68,A66,A95,A97,FUNCT_1:3;
then reconsider
t22 = ts2.y,t11=ts1.y as Element of TS D by A69,A77,A98;
[x3.y,w3/.y] in x.y by A95,A96,A97;
then [ts2.y,w3/.y] in F.(ts1.y) by A99,A95,A97,FUNCT_1:12;
then
A100: [t11,w3/.y] in F.(t22) by Th19;
P.(w3/.y) = {[x5,y5] where x5,y5 is Element of TS(DTConOSA(X)): [
x5,w3/.y] in F.y5} by Def22;
hence [x1.y,x2.y] in P.(w3/.y) by A100;
end;
assume that
A101: o1 ~= o2 and
A102: len the_arity_of o1 = len the_arity_of o2 and
A103: the_result_sort_of o1 <= s3 and
A104: the_result_sort_of o2 <= s3 and
A105: ex w3 being Element of (the carrier of S)* st dom w3 = dom x1 &
for y being Nat st y in dom w3 holds [x1.y,x2.y] in P.(w3/.y);
consider w3 being Element of (the carrier of S)* such that
A106: dom w3 = dom x1 and
A107: for y being Nat st y in dom w3 holds [x1.y,x2.y] in P.(w3/.y) by A105;
for y being Nat st y in dom x holds [x2.y,w3/.y] in x.y
proof
let y being Nat such that
A108: y in dom x;
A109: P.(w3/.y) = {[x5,y5] where x5,y5 is Element of TS(DTConOSA(X)): [
x5,w3/.y] in F.y5} by Def22;
[x1.y,x2.y] in P.(w3/.y) by A71,A106,A107,A108;
then consider x5,y5 being Element of TS(DTConOSA(X)) such that
A110: [x1.y,x2.y] = [x5,y5] and
A111: [x5,w3/.y] in F.y5 by A109;
A112: x1.y = x5 by A110,XTUPLE_0:1;
A113: x2.y = y5 by A110,XTUPLE_0:1;
[y5,w3/.y] in F.x5 by A111,Th19;
hence thesis by A108,A112,A113,FUNCT_1:12;
end;
then [Den(o2,PTA).x2,s3] in F.(OSSym(o1,X)-tree ts1) by A71,A73,A101,A102
,A103,A104,A106;
then [tx,s3] in F.(ty) by A75,Th19;
hence [Den(o1,PTA).x1,Den(o2,PTA).x2] in P.s3 by A67,A76,A75;
end;
T[P]
proof
let s1,s2 be Element of S, x be object such that
A114: x in X.s1;
reconsider sy = [x,s1] as Terminal of D by A114,Th4;
A115: P.s2 = {[x1,y] where x1,y is Element of TS(DTConOSA(X)): [x1,s2] in F
.y} by Def22;
A116: root-tree [x,s1] in SPTA.s1 by A114,Th10;
hereby
assume
A117: s1 <= s2;
[root-tree sy,s1] in F.(root-tree sy) by A116,Th19;
then [root-tree sy,s2] in F.(root-tree sy) by A116,A117,Th21;
hence [root-tree [x,s1],root-tree[x,s1]] in P.s2 by A115;
end;
let y be object;
assume
A118: [root-tree [x,s1],y] in P.s2 or [y,root-tree [x,s1]] in P.s2;
then
A119: root-tree [x,s1] in SPTA.s2 by ZFMISC_1:87;
field(P.s2) = SPTA.s2 by ORDERS_1:12;
then
A120: P.s2 is_symmetric_in SPTA.s2 by RELAT_2:def 11;
A121: F.(root-tree sy) = @(sy) by Def21
.= {[root-tree sy,s3] where s3 is Element of S: ex s4 be Element of S,
x be set st x in X.s4 & sy = [x,s4] & s4 <= s3};
y in SPTA.s2 by A118,ZFMISC_1:87;
then [y,root-tree sy] in P.s2 by A120,A118,A119,RELAT_2:def 3;
then consider y1,r1 being Element of TS D such that
A122: [y,root-tree sy] = [y1,r1] and
A123: [y1,s2] in F.(r1) by A115;
A124: y = y1 by A122,XTUPLE_0:1;
root-tree sy = r1 by A122,XTUPLE_0:1;
then consider s3 being Element of S such that
A125: [y1,s2] = [root-tree sy,s3] and
A126: ex s4 be Element of S, x be set st x in X.s4 & sy = [x,s4] & s4
<= s3 by A121,A123;
s2 = s3 by A125,XTUPLE_0:1;
hence thesis by A124,A125,A126,XTUPLE_0:1;
end;
hence thesis by A1,A65;
end;
:: the minimality for regular oss is done later
theorem Th27:
for S be locally_directed OrderSortedSign, X be non-empty
ManySortedSet of S holds PTCongruence(X) is monotone
proof
let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S;
set PTA = ParsedTermsOSA(X), P = PTCongruence X;
thus P is monotone
proof
let o1,o2 be OperSymbol of S such that
A1: o1 <= o2;
A2: o1 ~= o2 by A1;
A3: the_result_sort_of o1 <= the_result_sort_of o2 by A1;
let x1 be Element of Args(o1,PTA), x2 be Element of Args(o2,PTA) such that
A4: for y being Nat st y in dom x1 holds [x1.y,x2.y] in P.((
the_arity_of o2)/.y);
(the_arity_of o1) <= (the_arity_of o2) by A1;
then
A5: len (the_arity_of o1) = len (the_arity_of o2);
then dom (the_arity_of o2) = dom (the_arity_of o1) by FINSEQ_3:29;
then dom the_arity_of o2 = dom x1 by MSUALG_3:6;
hence thesis by A4,A2,A3,A5,Th26;
end;
end;
:: MSCongruence-like is ensured by the OSALG_4 cluster
registration
let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S;
cluster PTCongruence(X) -> monotone;
coherence by Th27;
end;
definition
let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S
, s be Element of S;
func PTVars(s,X) -> Subset of (the Sorts of ParsedTermsOSA(X)).s means
:Def23: for x be object
holds x in it iff ex a be object st a in X.s & x = root-tree [a,s];
existence
proof
defpred P[object] means
ex a be object st a in X.s & $1 = root-tree [a,s];
set D = DTConOSA(X), PTA = ParsedTermsOSA(X), SO = the Sorts of PTA;
consider A be set such that
A1: for x being object holds x in A iff x in SO.s & P[x] from XBOOLE_0:sch 1;
A c= SO.s
by A1;
then reconsider A as Subset of SO.s;
for x being object holds x in A iff P[x]
proof
dom coprod(X) = the carrier of S by PARTFUN1:def 2;
then (coprod(X)).s in rng coprod(X) by FUNCT_1:def 3;
then
A2: coprod(s,X) in rng coprod(X) by MSAFREE:def 3;
A3: Terminals D = Union (coprod X) by Th3;
set A1 = {aa where aa is Element of TS(D): (ex s1 being Element of S,x
be object
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};
let x be object;
thus x in A implies P[x] by A1;
assume
A4: P[x];
then consider a be set such that
A5: a in X.s and
A6: x = root-tree [a,s];
A7: (ParsedTerms X).s = ParsedTerms(X,s) by Def8;
set sa = [a,s];
sa in coprod(s,X) by A5,MSAFREE:def 2;
then sa in union rng coprod(X) by A2,TARSKI:def 4;
then
A8: sa in Terminals D by A3,CARD_3:def 4;
then reconsider sa as Symbol of D;
reconsider b = root-tree sa as Element of TS(D) by A8,DTCONSTR:def 1;
b in A1 by A5;
hence thesis by A1,A4,A6,A7;
end;
hence thesis;
end;
uniqueness
proof
set PTA = ParsedTermsOSA(X), SO = the Sorts of PTA;
let A,B be Subset of SO.s;
assume that
A9: for x be object holds x in A iff ex a be object st a in X.s & x =
root-tree [a,s] and
A10: for x be object holds x in B iff ex a be object st a in X.s & x =
root-tree [a,s];
thus A c= B
proof
let x be object;
assume x in A;
then ex a be object st a in X.s & x =root-tree [a,s] by A9;
hence thesis by A10;
end;
let x be object;
assume x in B;
then ex a be object st a in X.s & x = root-tree [a,s] by A10;
hence thesis by A9;
end;
end;
registration
let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S
, s be Element of S;
cluster PTVars(s,X) -> non empty;
coherence
proof
consider x being object such that
A1: x in X.s by XBOOLE_0:def 1;
ex a be set st a in X.s & root-tree [x,s] = root-tree [a,s] by A1;
hence thesis by Def23;
end;
end;
theorem Th28:
for S be locally_directed OrderSortedSign, X be non-empty
ManySortedSet of S, s be Element of S holds PTVars(s,X) = { root-tree t where t
is Symbol of DTConOSA(X): t in Terminals DTConOSA(X) & t`2 = s}
proof
let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S
, s be Element of S;
set D = DTConOSA(X), A = {root-tree t where t is Symbol of D : t in
Terminals D & t`2 = s};
thus PTVars(s,X) c= A
proof
let x be object;
assume x in PTVars(s,X);
then consider a be object such that
A1: a in X.s and
A2: x = root-tree [a,s] by Def23;
A3: [a,s] in Terminals D by A1,Th4;
then reconsider t = [a,s] as Symbol of D;
t`2 = s;
hence thesis by A2,A3;
end;
let x be object;
assume x in A;
then consider t be Symbol of D such that
A4: x = root-tree t and
A5: t in Terminals D and
A6: t`2 = s;
consider s1 be Element of S, a be set such that
A7: a in X.s1 and
A8: t = [a,s1] by A5,Th4;
s = s1 by A6,A8;
hence thesis by A4,A7,A8,Def23;
end;
definition
let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S;
func PTVars(X) -> MSSubset of ParsedTermsOSA(X) means
:Def24:
for s be Element of S holds it.s = PTVars(s,X);
existence
proof
deffunc F(Element of S) = PTVars($1,X);
set PTA = ParsedTermsOSA(X);
consider f be Function such that
A1: dom f = the carrier of S & for s be Element of S holds f.s = F(s)
from FUNCT_1:sch 4;
reconsider f as ManySortedSet of the carrier of S by A1,PARTFUN1:def 2
,RELAT_1:def 18;
f c= the Sorts of PTA
proof
let x be object;
assume x in the carrier of S;
then reconsider s = x as Element of S;
f.s = PTVars(s,X) by A1;
hence thesis;
end;
then reconsider f as MSSubset of PTA by PBOOLE:def 18;
take f;
thus thesis by A1;
end;
uniqueness
proof
let A,B be MSSubset of ParsedTermsOSA(X);
assume that
A2: for s be Element of S holds A.s = PTVars(s,X) and
A3: for s be Element of S holds B.s = PTVars(s,X);
for i be object st i in the carrier of S holds A.i = B.i
proof
let i be object;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
A.s = PTVars(s,X) by A2;
hence thesis by A3;
end;
hence thesis;
end;
end;
theorem
for S be locally_directed OrderSortedSign, X be non-empty
ManySortedSet of S holds PTVars(X) is non-empty
proof
let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S;
let x be object;
assume x in the carrier of S;
then reconsider s = x as Element of S;
(PTVars(X)).s = PTVars(s,X) by Def24;
hence thesis;
end;
definition
let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S
, s be Element of S;
func OSFreeGen(s,X) -> Subset of (the Sorts of FreeOSA(X)).s means
:Def25:
for x be object holds x in it
iff ex a be object st a in X.s & x = (OSNat_Hom(
ParsedTermsOSA(X),LCongruence(X)).s).(root-tree [a,s]);
existence
proof
set D = DTConOSA(X), PTA = ParsedTermsOSA(X), PTC = LCongruence(X), SO =
the Sorts of FreeOSA(X), NH = OSNat_Hom(ParsedTermsOSA(X),LCongruence(X));
defpred P[object] means
ex a be object st a in X.s & $1 = (NH.s).(root-tree [a,s]);
consider A be set such that
A1: for x being object holds x in A iff x in SO.s & P[x] from XBOOLE_0:sch 1;
A c= SO.s
by A1;
then reconsider A as Subset of SO.s;
for x being object holds x in A iff P[x]
proof
dom coprod(X) = the carrier of S by PARTFUN1:def 2;
then (coprod(X)).s in rng coprod(X) by FUNCT_1:def 3;
then
A2: coprod(s,X) in rng coprod(X) by MSAFREE:def 3;
A3: Terminals D = Union (coprod X) by Th3;
set A1 = {aa where aa is Element of TS(D): (ex s1 being Element of S,x
be object
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};
let x be object;
thus x in A implies P[x] by A1;
assume P[x];
then consider a be set such that
A4: a in X.s and
A5: x = (NH.s).(root-tree [a,s]);
A6: (ParsedTerms X).s = ParsedTerms(X,s) by Def8;
set sa = [a,s];
sa in coprod(s,X) by A4,MSAFREE:def 2;
then sa in union rng coprod(X) by A2,TARSKI:def 4;
then
A7: sa in Terminals D by A3,CARD_3:def 4;
then reconsider sa as Symbol of D;
reconsider b = root-tree sa as Element of TS(D) by A7,DTCONSTR:def 1;
b in A1 by A4;
then (NH.s).b in (the Sorts of QuotOSAlg(PTA,PTC)).s by A6,FUNCT_2:5;
hence thesis by A1,A4,A5;
end;
hence thesis;
end;
uniqueness
proof
set SO = the Sorts of FreeOSA(X), NH = OSNat_Hom(ParsedTermsOSA(X),
LCongruence(X));
let A,B be Subset of SO.s;
assume that
A8: for x be object holds x in A iff ex a be object st a in X.s & x = (NH.s
).root-tree [a,s] and
A9: for x be object holds x in B iff ex a be object st a in X.s & x = (NH.s
).root-tree [a,s];
thus A c= B
proof
let x be object;
assume x in A;
then ex a be object st a in X.s & x = (NH.s).root-tree [a,s] by A8;
hence thesis by A9;
end;
let x be object;
assume x in B;
then ex a be object st a in X.s & x = (NH.s).root-tree [a,s] by A9;
hence thesis by A8;
end;
end;
registration
let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S
, s be Element of S;
cluster OSFreeGen(s,X) -> non empty;
coherence
proof
set NH = OSNat_Hom(ParsedTermsOSA(X),LCongruence(X));
defpred P[set] means ex a be set st a in X.s & $1 = (NH.s).(root-tree [a,s
]);
consider x being object such that
A1: x in X.s by XBOOLE_0:def 1;
P[(NH.s).root-tree [x,s]] by A1;
hence thesis by Def25;
end;
end;
theorem Th30:
for S be locally_directed OrderSortedSign, X be non-empty
ManySortedSet of S, s be Element of S holds OSFreeGen(s,X) = { (OSNat_Hom(
ParsedTermsOSA(X),LCongruence(X)).s).root-tree t where t is Symbol of DTConOSA(
X): t in Terminals DTConOSA(X) & t`2 = s}
proof
let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S
, s be Element of S;
set D = DTConOSA(X), NH = OSNat_Hom(ParsedTermsOSA(X),LCongruence(X)), A = {
(NH.s).root-tree t where t is Symbol of D : t in Terminals D & t`2 = s};
thus OSFreeGen(s,X) c= A
proof
let x be object;
assume x in OSFreeGen(s,X);
then consider a be object such that
A1: a in X.s and
A2: x = (NH.s).root-tree [a,s] by Def25;
A3: [a,s] in Terminals D by A1,Th4;
then reconsider t = [a,s] as Symbol of D;
t`2 = s;
hence thesis by A2,A3;
end;
let x be object;
assume x in A;
then consider t be Symbol of D such that
A4: x = (NH.s).root-tree t and
A5: t in Terminals D and
A6: t`2 = s;
consider s1 be Element of S, a be set such that
A7: a in X.s1 and
A8: t = [a,s1] by A5,Th4;
s = s1 by A6,A8;
hence thesis by A4,A7,A8,Def25;
end;
definition
let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S;
func OSFreeGen(X) -> OSGeneratorSet of FreeOSA(X) means
:Def26:
for s be Element of S holds it.s = OSFreeGen(s,X);
existence
proof
deffunc F(Element of S) = OSFreeGen($1,X);
set FM = FreeOSA(X), D = DTConOSA(X), PTA = ParsedTermsOSA(X), SO = the
Sorts of FreeOSA(X), NH = OSNat_Hom(ParsedTermsOSA(X),LCongruence(X));
reconsider NH1 = NH as ManySortedFunction of PTA,FM;
A1: NH1 is order-sorted by OSALG_4:15;
reconsider SOS = SO as OrderSortedSet of S;
consider f be Function such that
A2: dom f = the carrier of S & for s be Element of S holds f.s = F(s)
from FUNCT_1:sch 4;
reconsider f as ManySortedSet of the carrier of S by A2,PARTFUN1:def 2
,RELAT_1:def 18;
A3: f c= the Sorts of FM
proof
let x be object;
assume x in the carrier of S;
then reconsider s = x as SortSymbol of S;
f.s = OSFreeGen(s,X) by A2;
hence thesis;
end;
then reconsider f as MSSubset of FM by PBOOLE:def 18;
OSCl f c= SOS by A3,OSALG_2:8;
then OSCl f is ManySortedSubset of the Sorts of FM by PBOOLE:def 18;
then reconsider O = OSCl f as OSSubset of FM by OSALG_2:def 2;
O is OSSubset of GenOSAlg(O) by OSALG_2:def 12;
then
A4: O c= the Sorts of GenOSAlg(O) by PBOOLE:def 18;
f c= O by OSALG_2:7;
then
A5: f c= the Sorts of GenOSAlg(O) by A4,PBOOLE:13;
A6: NH1 is_epimorphism PTA, FM by OSALG_4:15;
then
A7: NH1 is "onto";
A8: NH1 is_homomorphism PTA,FM by A6;
A9: the Sorts of GenOSAlg(O) = the Sorts of FM
proof
defpred P[set] means for s1 being Element of S st $1 in dom (NH1.s1)
holds (NH1.s1).$1 in (the Sorts of GenOSAlg(O)).s1;
reconsider O2 = (the Sorts of GenOSAlg(O)) as OrderSortedSet of S by
OSALG_1:17;
the Sorts of GenOSAlg(O) is MSSubset of FM by MSUALG_2:def 9;
then
A10: the Sorts of GenOSAlg(O) c= the Sorts of FM by PBOOLE:def 18;
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 P
[t] holds P[nt-tree ts]
proof
set G = GenOSAlg(O), OU = [:the carrier' of S,{the carrier of S}:] \/
Union (coprod (X qua ManySortedSet of S));
let nt be Symbol of D, ts be FinSequence of TS(D);
assume that
A12: nt ==> roots ts and
A13: for t being DecoratedTree of the carrier of D st t in rng ts
holds P[t];
[nt,roots ts] in the Rules of D by A12,LANG1:def 1;
then reconsider rt = roots ts as Element of OU* by ZFMISC_1:87;
reconsider sy = nt as Element of OU;
[sy,rt] in OSREL(X) by A12,LANG1:def 1;
then sy in [:the carrier' of S,{the carrier of S}:] by Def4;
then consider
o being Element of the carrier' of S, x2 being Element of {
the carrier of S} such that
A14: sy = [o,x2] by DOMAIN_1:1;
let s1 be Element of S;
assume (nt-tree ts) in dom (NH1.s1);
then (nt-tree ts) in (the Sorts of PTA).s1;
then (nt-tree ts) in ParsedTerms(X,s1) by Def8;
then consider a1 being Element of TS D such that
A15: (nt-tree ts) = a1 and
A16: (ex s2 being Element of S, x be object st s2 <= s1 & x in X.s2 &
a1 = root-tree [x,s2]) or ex o be OperSymbol of S st [o,the carrier of S] = a1.
{} & the_result_sort_of o <= s1;
A17: Seg len rt = dom rt by FINSEQ_1:def 3;
A18: x2 = the carrier of S by TARSKI:def 1;
not ex s2 being Element of S, x be set st s2 <= s1 & x in X.s2 &
a1 = root-tree [x,s2]
proof
given s2 being Element of S, x be set such that
s2 <= s1 and
x in X.s2 and
A19: a1 = root-tree [x,s2];
[x,s2] = (nt-tree ts).{} by A15,A19,TREES_4:3
.= [o,x2] by A14,TREES_4:def 4;
then s2 = the carrier of S by A18,XTUPLE_0:1;
then s2 in s2;
hence contradiction;
end;
then consider o1 being OperSymbol of S such that
A20: [o1,the carrier of S] = a1.{} and
A21: the_result_sort_of o1 <= s1 by A16;
set ar = the_arity_of o, rs = the_result_sort_of o;
A22: dom (roots ts) = dom ts by TREES_3:def 18;
[nt,roots ts] in OSREL(X) by A12,LANG1:def 1;
then
A23: len rt = len ar by A14,A18,Th2;
A24: Seg len ar = dom ar by FINSEQ_1:def 3;
reconsider B = the Sorts of G as MSSubset of FM by MSUALG_2:def 9;
A25: dom (B * ar) = dom ar by PARTFUN1:def 2;
set AR = the Arity of S, RS = the ResultSort of S, BH = B# * the Arity
of S;
AR.o = ar by MSUALG_1:def 1;
then
A26: BH.o = product (B * ar) by MSAFREE:1;
reconsider rs1 = rs,s11 = s1 as Element of S;
reconsider B1 = B as OrderSortedSet of S by OSALG_1:17;
A27: RS.o = rs by MSUALG_1:def 2;
B is opers_closed by MSUALG_2:def 9;
then B is_closed_on o by MSUALG_2:def 6;
then
A28: rng ((Den(o,FM))|(BH.o)) c= (B * RS).o by MSUALG_2:def 5;
A29: OSSym(o,X) = [o,the carrier of S];
A30: nt = [o,the carrier of S] by A14,TARSKI:def 1;
then
A31: ts in ((ParsedTerms X)# * (the Arity of S)).o by A12,A29,Th7;
then reconsider ts1 = ts as Element of Args(o,PTA) by MSUALG_1:def 4;
Den(o,PTA) = (PTOper X).o by MSUALG_1:def 6
.= PTDenOp(o,X) by Def10;
then
A32: (Den(o,PTA).ts) = nt-tree ts by A12,A29,A30,Def9;
A33: dom ((the Sorts of PTA) * ar) = dom ar by PARTFUN1:def 2;
A34: for x being object st x in dom (B * ar)
holds (NH1#ts1).x in (B * ar).x
proof
let x be object such that
A35: x in dom (B * ar);
reconsider x1 = x as Nat by A35;
A36: ts.x1 in rng ts by A25,A22,A23,A17,A24,A35,FUNCT_1:def 3;
rng ts c= TS D by FINSEQ_1:def 4;
then reconsider t = ts.x as Element of TS(D) by A36;
ts1.x in ((the Sorts of PTA) * ar).x by A25,A33,A35,MSUALG_3:6;
then ts1.x in (the Sorts of PTA).(ar.x) by A25,A33,A35,FUNCT_1:12;
then ts1.x in (the Sorts of PTA).(ar/.x) by A25,A35,PARTFUN1:def 6;
then ts1.x1 in dom (NH1.(ar/.x1)) by FUNCT_2:def 1;
then
(NH1.(ar/.x1)).t in (the Sorts of GenOSAlg(O)).(ar/.x1) by A13,A36;
then
A37: (NH1.(ar/.x1)).(ts1.x1) in B.(ar.x) by A25,A35,PARTFUN1:def 6;
(NH1#ts1).x1 = (NH1.(ar/.x1)).(ts1.x1) by A25,A22,A23,A17,A24,A35,
MSUALG_3:def 6;
hence thesis by A35,A37,FUNCT_1:12;
end;
NH1#ts1 in Args(o,FM);
then
A38: NH1#ts1 in dom Den(o,FM) by FUNCT_2:def 1;
[o1,the carrier of S] = [o,x2] by A14,A15,A20,TREES_4:def 4;
then
A39: o1 = o by XTUPLE_0:1;
then
A40: B1.rs1 c= B1.s11 by A21,OSALG_1:def 16;
dom (NH1#ts1) = dom ar by MSUALG_3:6;
then (NH1#ts1) in BH.o by A26,A25,A34,CARD_3:9;
then Den(o,FM).(NH1#ts1) in rng ((Den(o,FM))|(BH.o)) by A38,FUNCT_1:50;
then
A41: Den(o,FM).(NH1#ts1) in (B * RS).o by A28;
ts in Args(o,PTA) by A31,MSUALG_1:def 4;
then Den(o,PTA).ts in Result(o,PTA) by FUNCT_2:5;
then Den(o,PTA).ts in ((the Sorts of PTA) * RS).o by MSUALG_1:def 5;
then Den(o,PTA).ts in (the Sorts of PTA).rs by A27,FUNCT_2:15;
then (nt-tree ts) in dom (NH1.rs) by A32,FUNCT_2:def 1;
then
A42: (NH1.s11).(nt-tree ts) = (NH1.rs1).(nt-tree ts) by A1,A21,A39;
(NH1.rs).(Den(o,PTA).ts1) = Den(o,FM).(NH1#ts1) by A8;
then (NH1.rs).(nt-tree ts) in B.rs by A27,A32,A41,FUNCT_2:15;
hence thesis by A40,A42;
end;
let x be Element of S;
set s = x;
A43: for s be Symbol of D st s in Terminals D holds P[root-tree s]
proof
let t be Symbol of D;
assume
A44: t in Terminals D;
let s1 be Element of S;
assume (root-tree t) in dom (NH1.s1);
then root-tree t in (the Sorts of PTA).s1;
then (root-tree t) in ParsedTerms(X,s1) by Def8;
then consider a being Element of TS(D) such that
A45: root-tree t = a and
A46: (ex s2 being Element of S, x be object 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;
not ex o be OperSymbol of S st [o,the carrier of S] = a.{} &
the_result_sort_of o <= s1
proof
consider s3 being Element of S, x3 being set such that
x3 in X.s3 and
A47: t = [x3,s3] by A44,Th4;
given o be OperSymbol of S such that
A48: [o,the carrier of S] = a.{} and
the_result_sort_of o <= s1;
[o,the carrier of S] = t by A45,A48,TREES_4:3;
then the carrier of S = s3 by A47,XTUPLE_0:1;
then s3 in s3;
hence contradiction;
end;
then consider s2 being Element of S, x be set such that
A49: s2 <= s1 and
A50: x in X.s2 and
A51: a = root-tree [x,s2] by A46;
reconsider s11 = s1, s21 = s2 as Element of S;
a in ParsedTerms(X,s2) by A50,A51;
then a in (ParsedTerms(X)).s2 by Def8;
then (root-tree [x,s2]) in dom (NH1.s2) by A51,FUNCT_2:def 1;
then
A52: (NH1.s21).(root-tree [x,s2]) = (NH1.s11).(root-tree [x,s2] ) by A1,A49;
f.s2 c= (the Sorts of GenOSAlg(O)).s2 by A5;
then
A53: OSFreeGen(s2,X) c= (the Sorts of GenOSAlg(O)).s2 by A2;
O2.s21 c= O2.s11 by A49,OSALG_1:def 16;
then
A54: OSFreeGen(s2,X) c= (the Sorts of GenOSAlg(O)).s1 by A53;
(NH1.s2).(root-tree [x,s2]) in OSFreeGen(s2,X) by A50,Def25;
hence thesis by A45,A51,A52,A54;
end;
A55: for t being DecoratedTree of the carrier of D st t in TS D holds P
[t] from DTCONSTR:sch 7(A43,A11);
thus (the Sorts of GenOSAlg(O)).s c= (the Sorts of FM).s
by A10;
let x1 be object;
assume
A56: x1 in (the Sorts of FM).s;
A57: (the Sorts of PTA).s = ParsedTerms(X,s) by Def8
.= {a where a is Element of TS(D): (ex s2 being Element of S, x be
object
st s2 <= s & x in X.s2 & a = root-tree [x,s2]) or ex o1 be OperSymbol of S
st [o1,the carrier of S] = a.{} & the_result_sort_of o1 <= s};
rng(NH1.x) = (the Sorts of FM).x by A7;
then consider x2 being object such that
A58: x2 in dom (NH1.s) and
A59: x1 = (NH1.s).x2 by A56,FUNCT_1:def 3;
x2 in (the Sorts of PTA).s by A58;
then ex a be Element of TS(D) st a = x2 &( (ex s2 being Element of S
, x be object st s2 <= s & x in X.s2 & a = root-tree [x,s2])
or ex o1 be
OperSymbol of S st [o1,the carrier of S]=a.{} & the_result_sort_of o1 <= s) by
A57;
hence thesis by A55,A58,A59;
end;
f is OSGeneratorSet of FM
proof
let O1 be OSSubset of FM;
assume O1 = OSCl f;
hence thesis by A9;
end;
then reconsider f as OSGeneratorSet of FM;
take f;
thus thesis by A2;
end;
uniqueness
proof
let A,B be OSGeneratorSet of FreeOSA(X);
assume that
A60: for s be Element of S holds A.s = OSFreeGen(s,X) and
A61: for s be Element of S holds B.s = OSFreeGen(s,X);
for i be object st i in the carrier of S holds A.i = B.i
proof
let i be object;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
A.s = OSFreeGen(s,X) by A60;
hence thesis by A61;
end;
hence thesis;
end;
end;
theorem Th31:
for S be locally_directed OrderSortedSign, X be non-empty
ManySortedSet of S holds OSFreeGen(X) is non-empty
proof
let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S;
let x be object;
assume x in the carrier of S;
then reconsider s = x as Element of S;
(OSFreeGen(X)).s = OSFreeGen(s,X) by Def26;
hence thesis;
end;
registration
let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S;
cluster OSFreeGen(X) -> non-empty;
coherence by Th31;
end;
definition
let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S
, R be OSCongruence of ParsedTermsOSA(X), t be Element of TS DTConOSA(X);
func OSClass(R,t) -> Element of OSClass(R,LeastSort t) means
:Def27:
for s
being Element of S, x being Element of (the Sorts of ParsedTermsOSA(X)).s st t
= x holds it = OSClass(R,x);
existence
proof
set LS = LeastSort t, PTA = ParsedTermsOSA(X);
reconsider x1 = t as Element of (the Sorts of PTA).LS by Def12;
take OSClass(R,x1);
let s being Element of S, x being Element of (the Sorts of ParsedTermsOSA(
X)).s such that
A1: t = x;
LS <= s by A1,Def12;
hence thesis by A1,OSALG_4:13;
end;
uniqueness
proof
set LS = LeastSort t, PTA = ParsedTermsOSA(X);
reconsider x1 = t as Element of (the Sorts of PTA).LS by Def12;
let O1,O2 be Element of OSClass(R,LeastSort t) such that
A2: for s being Element of S, x being Element of (the Sorts of
ParsedTermsOSA(X)).s st t = x holds O1 = OSClass(R,x) and
A3: for s being Element of S, x being Element of (the Sorts of
ParsedTermsOSA(X)).s st t = x holds O2 = OSClass(R,x);
thus O1 = OSClass(R,x1) by A2
.= O2 by A3;
end;
end;
theorem Th32:
for S be locally_directed OrderSortedSign, X be non-empty
ManySortedSet of S, R be OSCongruence of ParsedTermsOSA(X), t be Element of TS
DTConOSA(X) holds t in OSClass(R,t)
proof
let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S
, R be OSCongruence of ParsedTermsOSA(X), t be Element of TS DTConOSA(X);
set PTA = ParsedTermsOSA(X);
reconsider x = t as Element of (the Sorts of PTA).(LeastSort t) by Def12;
OSClass(R,t) = OSClass(R,x) by Def27
.= Class( CompClass(R, CComp(LeastSort t)), x);
hence thesis by EQREL_1:20,OSALG_4:5;
end;
theorem Th33:
for S be locally_directed OrderSortedSign, X be non-empty
ManySortedSet of S, s be Element of S, t being Element of TS DTConOSA(X), x,x1
being set st x in X.s & t = root-tree [x,s] holds x1 in OSClass(PTCongruence(X)
,t) iff x1 = t
proof
let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S
, s be Element of S, t being Element of TS DTConOSA(X);
set PTA = ParsedTermsOSA(X), D = DTConOSA(X),R= PTCongruence(X);
reconsider y = t as Element of (the Sorts of PTA).(LeastSort t) by Def12;
let x,x1 being set such that
A1: x in X.s and
A2: t = root-tree [x,s];
A3: [x,s] in Terminals D by A1,Th4;
then reconsider sy = [x,s] as Symbol of D;
A4: OSClass(R,t) = OSClass(PTCongruence X,y) by Def27
.= proj1((PTClasses X).y) by Th25;
A5: (PTClasses X).(root-tree sy) = @(sy) by A3,Def21
.= {[root-tree sy,s1] where s1 is Element of S: ex s2 be Element of S,
x2 be set st x2 in X.s2 & sy = [x2,s2] & s2 <= s1};
hereby
assume x1 in OSClass(R,t);
then consider z being object such that
A6: [x1,z] in (PTClasses X).y by A4,XTUPLE_0:def 12;
ex s1 being Element of S st [x1,z] = [root-tree sy,s1] & ex s2 be
Element of S, x2 be set st x2 in X.s2 & sy = [x2,s2] & s2 <= s1 by A2,A5,A6;
hence x1 = t by A2,XTUPLE_0:1;
end;
assume x1 = t;
then [x1,s] in (PTClasses X).y by A1,A2,A5;
hence thesis by A4,XTUPLE_0:def 12;
end;
theorem Th34:
for S be locally_directed OrderSortedSign, X be non-empty
ManySortedSet of S, R be OSCongruence of ParsedTermsOSA(X), t1,t2 be Element of
TS DTConOSA(X) holds t2 in OSClass(R,t1) iff OSClass(R,t1) = OSClass(R,t2)
proof
let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S
, R be OSCongruence of ParsedTermsOSA(X), t1,t2 be Element of TS DTConOSA(X);
set PTA = ParsedTermsOSA(X), SPTA = (the Sorts of PTA);
reconsider x1=t1 as Element of SPTA.(LeastSort t1) by Def12;
set CC1 = CComp(LeastSort t1), CR1 = CompClass(R,CC1);
A1: OSClass(R,t1) = OSClass(R,x1) by Def27
.= Class( CompClass(R, CComp(LeastSort t1)), x1);
hereby
assume t2 in OSClass(R,t1);
then [t2,x1] in CR1 by A1,EQREL_1:19;
then consider s2 being Element of S such that
s2 in CC1 and
A2: [t2,x1] in R.s2 by OSALG_4:def 9;
reconsider x11=x1,x22=t2 as Element of SPTA.s2 by A2,ZFMISC_1:87;
thus OSClass(R,t1) = OSClass(R,x11) by Def27
.= OSClass(R,x22) by A2,OSALG_4:12
.= OSClass(R,t2) by Def27;
end;
assume OSClass(R,t1) = OSClass(R,t2);
hence thesis by Th32;
end;
theorem Th35:
for S be locally_directed OrderSortedSign, X be non-empty
ManySortedSet of S, R1,R2 be OSCongruence of ParsedTermsOSA(X), t be Element of
TS DTConOSA(X) holds R1 c= R2 implies OSClass(R1,t) c= OSClass(R2,t)
proof
let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S
, R1,R2 be OSCongruence of ParsedTermsOSA(X), t be Element of TS DTConOSA(X);
set s = LeastSort t, PTA = ParsedTermsOSA(X), SPTA = the Sorts of PTA, D =
DTConOSA(X);
set CC1 = CComp(s), CR1 = CompClass(R1,CC1);
reconsider xa=t as Element of SPTA.s by Def12;
assume
A1: R1 c= R2;
A2: OSClass(R1,t) = OSClass(R1,xa) by Def27
.= Class( CompClass(R1, CComp(s)), xa);
let x be object;
assume x in OSClass(R1,t);
then [x,xa] in CR1 by A2,EQREL_1:19;
then consider s1 being Element of S such that
s1 in CC1 and
A3: [x,xa] in R1.s1 by OSALG_4:def 9;
reconsider xa = t, xb = x as Element of SPTA.s1 by A3,ZFMISC_1:87;
A4: R1.s1 c= R2.s1 by A1;
x in SPTA.s1 by A3,ZFMISC_1:87;
then reconsider t1 = x as Element of TS D by Th15;
OSClass(R2,t1) = OSClass(R2,xb) by Def27
.= OSClass(R2,xa) by A3,A4,OSALG_4:12
.= OSClass(R2,t) by Def27;
hence thesis by Th34;
end;
theorem Th36:
for S be locally_directed OrderSortedSign, X be non-empty
ManySortedSet of S, s be Element of S, t being Element of TS DTConOSA(X), x,x1
being set st x in X.s & t = root-tree [x,s] holds x1 in OSClass(LCongruence(X),
t) iff x1 = t
proof
let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S
, s be Element of S, t being Element of TS DTConOSA(X);
set R = LCongruence(X),R1 = PTCongruence(X);
let x,x1 being set such that
A1: x in X.s and
A2: t = root-tree [x,s];
R c= R1 by Def17;
then OSClass(R,t) c= OSClass(R1,t) by Th35;
hence x1 in OSClass(R,t) implies x1 = t by A1,A2,Th33;
assume x1 = t;
hence thesis by Th32;
end;
definition
let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S
, A be non-empty ManySortedSet of the carrier of S, F be ManySortedFunction of
PTVars(X), A, t be Symbol of DTConOSA(X);
assume
A1: t in Terminals (DTConOSA(X));
func pi(F,A,t) -> Element of Union A means
:Def28:
for f be Function st f = F.(t`2) holds it = f.(root-tree t);
existence
proof
set FG = PTVars(X), D = DTConOSA(X);
consider s be Element of S, x be set such that
x in X.s and
A2: t = [x,s] by A1,Th4;
FG.s = PTVars(s,X) by Def24;
then
A3: dom (F.s) = PTVars(s,X) by FUNCT_2:def 1
.= {root-tree tt where tt is Symbol of D: tt in Terminals D & tt`2 = s
} by Th28;
t`2 = s by A2;
then root-tree t in dom (F.s) by A1,A3;
then
A4: (F.s).(root-tree t) in rng (F.s) by FUNCT_1:def 3;
dom A = the carrier of S by PARTFUN1:def 2;
then
A5: A.s in rng A by FUNCT_1:def 3;
rng (F.s) c= A.s by RELAT_1:def 19;
then (F.s).(root-tree t) in union rng A by A4,A5,TARSKI:def 4;
then reconsider eu = (F.s).(root-tree t) as Element of Union A by
CARD_3:def 4;
take eu;
let f be Function;
assume f = F.(t`2);
hence thesis by A2;
end;
uniqueness
proof
consider s be Element of S, x be set such that
x in X.s and
A6: t = [x,s] by A1,Th4;
reconsider f = F.s as Function;
let a,b be Element of Union A;
assume that
A7: for f be Function st f = F.(t`2) holds a = f.(root-tree t) and
A8: for f be Function st f = F.(t`2) holds b = f.(root-tree t);
A9: f = F.(t`2) by A6;
then a = f.(root-tree t) by A7;
hence thesis by A8,A9;
end;
end;
theorem Th37:
for S be locally_directed OrderSortedSign, X be non-empty
ManySortedSet of S, U1 be monotone non-empty OSAlgebra of S, f be
ManySortedFunction of PTVars(X),the Sorts of U1 ex h be ManySortedFunction of
ParsedTermsOSA(X),U1 st h is_homomorphism ParsedTermsOSA(X),U1 & h is
order-sorted & h || PTVars(X) = f
proof
let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S;
set D = DTConOSA(X), PTA = ParsedTermsOSA(X), PV = PTVars(X), SPTA = the
Sorts of PTA;
let U1 be non-empty monotone OSAlgebra of S, F be ManySortedFunction of PV,
the Sorts of U1;
set SA =the Sorts of PTA, AR = the Arity of S, S1 = the Sorts of U1, O = the
carrier' of S, RS = the ResultSort of S;
reconsider SAO=SA,S1O=S1 as OrderSortedSet of S by OSALG_1:17;
deffunc TermVal(Symbol of D) = pi(F,the Sorts of U1,$1);
deffunc NTermVal(Symbol of D,set,FinSequence) = pi(@(X,$1),U1, $3);
consider G being Function of TS(D), Union (the Sorts of U1) such that
A1: for t being Symbol of D st t in Terminals D holds G.(root-tree t) =
TermVal(t) and
A2: for nt be Symbol of D, ts be FinSequence of TS(D) st nt ==> roots ts
holds G.(nt-tree ts) = NTermVal(nt,roots ts,G * ts) from DTCONSTR:sch 8;
deffunc F(object) = G | ((the Sorts of PTA).$1);
consider h be Function such that
A3: dom h = the carrier of S & for s be object st s in the carrier of S
holds h.s = F(s) from FUNCT_1:sch 3;
reconsider h as ManySortedSet of the carrier of S by A3,PARTFUN1:def 2
,RELAT_1:def 18;
for s be object st s in dom h holds h.s is Function
proof
let s be object;
assume s in dom h;
then h.s = G | ((the Sorts of PTA).s) by A3;
hence thesis;
end;
then reconsider h as ManySortedFunction of the carrier of S by FUNCOP_1:def 6
;
defpred P[set] means for s be Element of S st $1 in (the Sorts of PTA).s
holds (h.s).$1 in (the Sorts of U1).s;
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);
assume that
A5: nt ==> roots ts and
A6: for t being DecoratedTree of the carrier of D st t in rng ts holds P[t];
set p = G * ts, o = @(X,nt), ar = the_arity_of o, rs = the_result_sort_of
o, OU = [:the carrier' of S,{the carrier of S}:] \/ Union (coprod (X qua
ManySortedSet of S)), rt = roots ts;
A7: [o,the carrier of S] = nt by A5,Def15;
then
A8: [[o,the carrier of S],rt] in the Rules of D by A5,LANG1:def 1;
let s be Element of S;
reconsider s2=s as Element of S;
assume
A9: nt-tree ts in SA.s;
consider op being OperSymbol of S such that
A10: nt = [op,the carrier of S] and
ts in Args(op,PTA) and
nt-tree ts = Den(op,PTA).ts and
A11: for s1 being Element of S holds nt-tree ts in SA.s1 iff
the_result_sort_of op <= s1 by A5,Th12;
op = o by A5,A10,Def15;
then rs <= s by A9,A11;
then
A12: S1O.rs c= S1O.s2 by OSALG_1:def 16;
A13: rng Den(o,U1) c= Result(o,U1) by RELAT_1:def 19;
A14: dom(S1* ar) = dom ar by PARTFUN1:def 2;
A15: [o,the carrier of S] = OSSym(o,X);
then
A16: (PTDenOp(o,X)).ts = nt-tree ts by A5,A7,Def9;
A17: dom(SA* ar) = dom ar by PARTFUN1:def 2;
dom (PTDenOp (o,X)) = ((ParsedTerms X)# * AR).o by FUNCT_2:def 1;
then ts in dom (PTDenOp(o,X)) by A5,A7,A15,Th7;
then
A18: nt-tree ts in rng (PTDenOp(o,X)) by A16,FUNCT_1:def 3;
A19: h.rs = (G | (SA.rs)) by A3;
A20: Seg len ar = dom ar by FINSEQ_1:def 3;
A21: rng ar c= the carrier of S by FINSEQ_1:def 4;
A22: ar = AR.o by MSUALG_1:def 1;
A23: dom rt = dom ts by TREES_3:def 18;
reconsider rt as Element of OU* by A8,ZFMISC_1:87;
A24: len rt = len ar by A8,Th2;
A25: dom rt = Seg len rt by FINSEQ_1:def 3;
A26: dom p = dom ts by FINSEQ_3:120;
then
A27: dom p = dom (S1 * ar) by A23,A14,A8,A25,A20,Th2;
A28: for x being object st x in dom (S1 * ar) holds p.x in (S1 * ar).x
proof
let x be object;
assume
A29: x in dom (S1 * ar);
then reconsider n = x as Nat;
A30: ts.n in rng ts by A23,A14,A24,A25,A20,A29,FUNCT_1:def 3;
rng ts c= TS D by FINSEQ_1:def 4;
then reconsider t = ts.n as Element of TS(D) by A30;
A31: p.n = G.(ts.n) by A27,A29,FINSEQ_3:120;
ar.x in rng ar by A14,A29,FUNCT_1:def 3;
then reconsider s = ar.x as Element of S by A21;
A32: h.s = G | (SA.s) by A3;
dom SA = the carrier of S by PARTFUN1:def 2;
then
A33: SA.s in rng SA by FUNCT_1:def 3;
dom G = TS D by FUNCT_2:def 1
.= union rng SA by Th8;
then
A34: dom (h.s) = SA.s by A32,A33,RELAT_1:62,ZFMISC_1:74;
ts in ((ParsedTerms X)# * AR).o by A5,A7,A15,Th7;
then ts in product ((ParsedTerms X) * ar) by A22,MSAFREE:1;
then ts.x in ((ParsedTerms X) * ar).x by A14,A17,A29,CARD_3:9;
then
A35: ts.x in (ParsedTerms X).(ar.x) by A14,A17,A29,FUNCT_1:12;
then (h.s).t in S1.s by A6,A30;
then G.t in S1.s by A35,A32,A34,FUNCT_1:47;
hence thesis by A29,A31,FUNCT_1:12;
end;
set ppi = pi(o,U1,p);
A36: dom Den(o,U1) = Args(o,U1) by FUNCT_2:def 1;
A37: dom RS = O by FUNCT_2:def 1;
Args(o,U1) = (S1# * AR).o by MSUALG_1:def 4
.= product (S1 * ar) by A22,MSAFREE:1;
then
A38: p in Args(o,U1) by A26,A23,A14,A24,A25,A20,A28,CARD_3:9;
then pi(o,U1,p) = Den(o,U1).p by MSAFREE:def 21;
then ppi in rng Den(o,U1) by A38,A36,FUNCT_1:def 3;
then
A39: ppi in Result(o,U1) by A13;
h.s = (G | (SA.s)) by A3;
then
A40: (h.s).(nt-tree ts) = G.(nt-tree ts) by A9,FUNCT_1:49;
A41: rng RS c= the carrier of S by RELAT_1:def 19;
dom SA = the carrier of S by PARTFUN1:def 2;
then
A42: dom (SA * RS) = dom RS by A41,RELAT_1:27;
dom S1 = the carrier of S by PARTFUN1:def 2;
then
A43: dom (S1 *RS) = dom RS by A41,RELAT_1:27;
rng (PTDenOp (o,X)) c= ((ParsedTerms X) * RS).o by RELAT_1:def 19;
then nt-tree ts in (SA * RS).o by A18;
then nt-tree ts in SA.(RS.o) by A37,A42,FUNCT_1:12;
then
A44: nt-tree ts in SA.rs by MSUALG_1:def 2;
G.(nt-tree ts) = ppi by A2,A5;
then
A45: ppi = (G | (SA.rs)).(nt-tree ts) by A44,FUNCT_1:49;
Result(o,U1) = (S1 *RS).o by MSUALG_1:def 5
.= S1.(RS.o) by A43,A37,FUNCT_1:12
.= S1.rs by MSUALG_1:def 2;
then (h.rs).(nt-tree ts) in S1.s by A39,A45,A19,A12;
hence thesis by A44,A19,A40,FUNCT_1:49;
end;
A46: for t being Symbol of D st t in Terminals D holds P[root-tree t]
proof
let t be Symbol of D;
assume
A47: t in Terminals D;
then consider s be Element of S, x be set such that
A48: x in X.s and
A49: t = [x,s] by Th4;
reconsider s as SortSymbol of S;
set E = {root-tree tt where tt is Symbol of D: tt in Terminals D & tt`2 =
s}, a = root-tree t;
A50: t`2 = s by A49;
then
A51: a in E by A47;
reconsider f = F.s as Function of PV.s,S1.s;
A52: dom f = PV.s by FUNCT_2:def 1;
A53: rng f c= S1.s by RELAT_1:def 19;
A54: E = PTVars(s,X) by Th28;
then PV.s = E by Def24;
then f.a in rng f by A51,A52,FUNCT_1:def 3;
then
A55: f.a in S1.s by A53;
let s1 be Element of S;
reconsider s0=s,s11=s1 as Element of S;
assume
A56: a in SA.s1;
then s <= s1 by A48,A49,Th10;
then
A57: S1O.s0 c= S1O.s11 by OSALG_1:def 16;
A58: h.s = G | (SA.s) by A3;
then
A59: (h.s).a = G.a by A51,A54,FUNCT_1:49
.= pi(F,S1,t) by A1,A47
.= f.a by A47,A50,Def28;
h.s1 = G | (SA.s1) by A3;
then (h.s1).a = G.a by A56,FUNCT_1:49
.= f.a by A51,A54,A58,A59,FUNCT_1:49;
hence thesis by A55,A57;
end;
A60: for t being DecoratedTree of the carrier of D st t in TS(D) holds P[t]
from DTCONSTR:sch 7(A46,A4);
for s be object st s in the carrier of S holds h.s is Function of (the
Sorts of PTA).s, (the Sorts of U1).s
proof
let x be object;
assume x in the carrier of S;
then reconsider s = x as Element of S;
A61: dom G = TS D by FUNCT_2:def 1
.= union rng SA by Th8;
dom SA = the carrier of S by PARTFUN1:def 2;
then
A62: SA.s in rng SA by FUNCT_1:def 3;
A63: h.s = G | (SA.s) by A3;
then
A64: dom (h.s) = SA.s by A61,A62,RELAT_1:62,ZFMISC_1:74;
A65: SA.s c= dom G by A61,A62,ZFMISC_1:74;
rng (h.s) c= S1.s
proof
let a be object;
assume a in rng (h.s);
then consider T be object such that
A66: T in dom (h.s) and
A67: (h.s).T = a by FUNCT_1:def 3;
reconsider T as Element of TS(D) by A65,A64,A66,FUNCT_2:def 1;
T in SA.s by A63,A61,A62,A66,RELAT_1:62,ZFMISC_1:74;
hence thesis by A60,A67;
end;
hence thesis by A64,FUNCT_2:def 1,RELSET_1:4;
end;
then reconsider h as ManySortedFunction of PTA,U1 by PBOOLE:def 15;
take h;
thus h is_homomorphism PTA,U1
proof
A68: dom SA = the carrier of S by PARTFUN1:def 2;
rng RS c= the carrier of S by RELAT_1:def 19;
then
A69: dom (SA * RS) = dom RS by A68,RELAT_1:27;
let op be Element of the carrier' of S such that
Args(op,PTA) <> {};
reconsider o=op as OperSymbol of S;
let x be Element of Args(op,PTA);
set rs = the_result_sort_of o, DA = Den(o,PTA), D1 = Den(o,U1), OU = [:the
carrier' of S,{the carrier of S}:] \/ Union (coprod (X qua ManySortedSet of S))
, ar = the_arity_of o;
A70: ar = AR.o by MSUALG_1:def 1;
A71: Args(o,PTA) = ((ParsedTerms X)# * AR).o by MSUALG_1:def 4;
then reconsider p = x as FinSequence of TS(D) by Th5;
A72: OSSym(o,X) ==> roots p by A71,Th7;
then
A73: @(X,OSSym(o,X)) = o by Def15;
A74: dom (G *p) = dom p by FINSEQ_3:120;
A75: x in ((ParsedTerms X)# * AR).o by A71;
A76: for a be object st a in dom p holds (G*p).a = (h#x).a
proof
set rt = roots p;
let a be object;
A77: dom(SA* ar) = dom ar by PARTFUN1:def 2;
A78: [[o,the carrier of S],rt] in the Rules of D by A72,LANG1:def 1;
assume
A79: a in dom p;
then reconsider n = a as Nat;
A80: (h#x).n = (h.(ar/.n)).(x.n) by A79,MSUALG_3:def 6;
A81: (G*p).n = G.(x.n) by A74,A79,FINSEQ_3:120;
A82: h.(ar/.n) = G | (SA.(ar/.n)) by A3;
A83: dom rt = dom p by TREES_3:def 18;
reconsider rt as Element of OU* by A78,ZFMISC_1:87;
A84: len rt = len ar by A78,Th2;
A85: Seg len rt = dom rt by FINSEQ_1:def 3;
A86: Seg len ar = dom ar by FINSEQ_1:def 3;
p in product((ParsedTerms X) * ar) by A75,A70,MSAFREE:1;
then
A87: p.n in ((ParsedTerms X) * ar).n by A79,A77,A83,A84,A85,A86,CARD_3:9;
((ParsedTerms X) * ar).n = SA.(ar.n) by A79,A77,A83,A84,A85,A86,
FUNCT_1:12
.= SA.(ar/.n) by A79,A83,A84,A85,A86,PARTFUN1:def 6;
hence thesis by A81,A80,A82,A87,FUNCT_1:49;
end;
dom (h#x) = dom ar by MSUALG_3:6;
then
A88: G*p = h#x by A74,A76,FUNCT_1:2,MSUALG_3:6;
A89: h.rs = G | (SA.rs) by A3;
A90: rng (PTDenOp (o,X)) c= ((ParsedTerms X) * RS).o by RELAT_1:def 19;
A91: dom (PTDenOp (o,X)) = ((ParsedTerms X)# * AR).o by FUNCT_2:def 1;
(PTDenOp(o,X)).p = (OSSym(o,X))-tree p by A72,Def9;
then (OSSym(o,X))-tree p in rng (PTDenOp(o,X)) by A71,A91,FUNCT_1:def 3;
then
A92: (OSSym(o,X))-tree p in (SA * RS).o by A90;
dom SA = the carrier of S by PARTFUN1:def 2;
then
A93: SA.rs in rng SA by FUNCT_1:def 3;
dom RS = O by FUNCT_2:def 1;
then (OSSym(o,X))-tree p in SA.(RS.o) by A69,A92,FUNCT_1:12;
then
A94: (OSSym(o,X))-tree p in SA.rs by MSUALG_1:def 2;
dom G = TS D by FUNCT_2:def 1
.= union rng SA by Th8;
then
A95: dom (h.rs) = SA.rs by A89,A93,RELAT_1:62,ZFMISC_1:74;
DA = (PTOper(X)).o by MSUALG_1:def 6
.= PTDenOp(o,X) by Def10;
then DA.x = (OSSym(o,X))-tree p by A72,Def9;
then (h.rs).(DA.x) = G.((OSSym(o,X))-tree p) by A94,A89,A95,FUNCT_1:47
.= pi(@(X,OSSym(o,X)),U1,G*p) by A2,A72
.= D1.(h#x) by A73,A88,MSAFREE:def 21;
hence thesis;
end;
thus h is order-sorted
proof
let s1,s2 being Element of S;
assume s1 <= s2;
then
A96: SAO.s1 c= SAO.s2 by OSALG_1:def 16;
let a1 being set such that
A97: a1 in dom (h.s1);
A98: a1 in SAO.s1 by A97;
then a1 in SA.s2 by A96;
hence a1 in dom (h.s2) by FUNCT_2:def 1;
A99: h.s2 = G | (SPTA.s2) by A3;
h.s1 = G | (SPTA.s1) by A3;
hence (h.s1).a1 = G.a1 by A97,FUNCT_1:49
.= (h.s2).a1 by A96,A98,A99,FUNCT_1:49;
end;
for x being object st x in the carrier of S holds (h || PV).x = F.x
proof
set hf = h || PV;
let x be object;
assume x in the carrier of S;
then reconsider s = x as Element of S;
A100: dom (h.s) = SA.s by FUNCT_2:def 1;
A101: dom (hf.s) = PV.s by FUNCT_2:def 1;
A102: PV.s = PTVars(s,X) by Def24;
A103: hf.s = (h.s) | (PV.s) by MSAFREE:def 1;
A104: for a be object st a in PV.s holds (hf.s).a = (F.s).a
proof
let a be object;
A105: h.s = G | (SA.s) by A3;
assume
A106: a in PV.s;
then a in {root-tree t where t is Symbol of D: t in Terminals D & t`2 =
s } by A102,Th28;
then consider t be Symbol of D such that
A107: a = root-tree t and
A108: t in Terminals D and
A109: t`2 = s;
thus (hf.s).a = (h.s).a by A103,A101,A106,FUNCT_1:47
.= G.a by A100,A102,A106,A105,FUNCT_1:47
.= pi(F,S1,t) by A1,A107,A108
.= (F.s).a by A107,A108,A109,Def28;
end;
dom (F.s) = PV.s by FUNCT_2:def 1;
hence thesis by A101,A104,FUNCT_1:2;
end;
hence thesis;
end;
:: NH stanbds for NatHom
definition
let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S
, s be Element of S;
func NHReverse(s,X) -> Function of OSFreeGen(s,X),PTVars(s,X) means
for t be
Symbol of DTConOSA(X) st (OSNat_Hom(ParsedTermsOSA(X),LCongruence(X)).s).(
root-tree t) in OSFreeGen(s,X) holds it.((OSNat_Hom(ParsedTermsOSA(X),
LCongruence(X)).s).(root-tree t)) = root-tree t;
existence
proof
set A = OSFreeGen(s,X), R = LCongruence(X), PTA = ParsedTermsOSA(X), SPTA
= the Sorts of PTA, NHs = OSNat_Hom(PTA,R,s), D = DTConOSA(X);
set NH = OSNat_Hom(ParsedTermsOSA(X),LCongruence(X));
defpred P[object,object] means
for t be Symbol of D st $1 = (NH.s).(root-tree t)
holds $2 = root-tree t;
A1: NH.s = OSNat_Hom(PTA,R,s) by OSALG_4:def 22;
A2: for x be object st x in A ex a be object st a in PTVars(s,X) & P[x,a]
proof
let x be object;
assume x in A;
then
x in {(NH.s).(root-tree t) where t is Symbol of D: t in Terminals D
& t`2 = s} by Th30;
then consider t be Symbol of D such that
A3: x = (NH.s).(root-tree t) and
A4: t in Terminals D and
A5: t`2 = s;
A6: x = NHs.(root-tree t) by A3,OSALG_4:def 22;
take root-tree t;
consider s1 be Element of S, a be set such that
A7: a in X.s1 and
A8: t = [a,s1] by A4,Th4;
A9: s = s1 by A5,A8;
hence root-tree t in PTVars(s,X) by A7,A8,Def23;
reconsider rt = root-tree t as Element of SPTA.s by A7,A8,A9,Th10;
A10: NHs.rt = OSClass(R,rt) by OSALG_4:def 21;
reconsider tt = root-tree t as Element of TS D by A7,A8,Th10;
let t1 be Symbol of D;
assume
A11: x = (NH.s).(root-tree t1);
A12: OSClass(R,tt) = OSClass(R,rt) by Def27;
OSClass(R,tt) <> {} by Th32;
then x <> {} by A12,A6,OSALG_4:def 21;
then root-tree t1 in dom NHs by A1,A11,FUNCT_1:def 2;
then reconsider rt1 = root-tree t1 as Element of SPTA.s;
reconsider tt2 = rt1 as Element of TS D by Th15;
A13: OSClass(R,tt2) = OSClass(R,rt1) by Def27;
x = NHs.(root-tree t1) by A11,OSALG_4:def 22;
then OSClass(R,rt1) = OSClass(R,rt) by A6,A10,OSALG_4:def 21;
then tt2 in OSClass(R,tt) by A12,A13,Th34;
hence thesis by A7,A8,Th36;
end;
consider f be Function such that
A14: dom f = A & rng f c= PTVars(s,X) & for x be object st x in A holds P
[x,f.x] from FUNCT_1:sch 6(A2);
reconsider f as Function of A,PTVars(s,X) by A14,FUNCT_2:2;
take f;
let t be Symbol of D;
assume (NH.s).(root-tree t) in A;
hence thesis by A14;
end;
uniqueness
proof
let A,B be Function of OSFreeGen(s,X),PTVars(s,X);
set NH = OSNat_Hom(ParsedTermsOSA(X),LCongruence(X));
assume that
A15: for t be Symbol of DTConOSA(X) st (NH.s).(root-tree t) in
OSFreeGen(s,X) holds A.((NH.s).(root-tree t)) = root-tree t and
A16: for t be Symbol of DTConOSA(X) st (NH.s).(root-tree t) in
OSFreeGen(s,X) holds B.((NH.s).(root-tree t)) = root-tree t;
set D = DTConOSA(X), C = {(NH.s).(root-tree t) where t is Symbol of D : t
in Terminals D & t`2 = s};
A17: OSFreeGen(s,X) = C by Th30;
then
A18: dom B = C by FUNCT_2:def 1;
A19: for i be object st i in C holds A.i = B.i
proof
let i be object;
assume
A20: i in C;
then consider t be Symbol of D such that
A21: i = (NH.s).(root-tree t) and
t in Terminals D and
t`2 = s;
A.((NH.s).(root-tree t)) = root-tree t by A15,A17,A20,A21;
hence thesis by A16,A17,A20,A21;
end;
dom A = C by A17,FUNCT_2:def 1;
hence thesis by A18,A19,FUNCT_1:2;
end;
end;
definition
let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S;
func NHReverse(X) -> ManySortedFunction of OSFreeGen(X),PTVars(X) means
for s be Element of S holds it.s = NHReverse(s,X);
existence
proof
defpred P[object,object] means
for s be Element of S st s = $1 holds $2 =
NHReverse(s,X);
set I = the carrier of S, FG = OSFreeGen(X);
A1: for i be object st i in I ex u be object st P[i,u]
proof
let i be object;
assume i in I;
then reconsider s = i as SortSymbol of S;
take NHReverse(s,X);
let s1 be Element of S;
assume s1 = i;
hence thesis;
end;
consider H be Function such that
A2: dom H = I & for i be object st i in I holds P[i,H.i] from CLASSES1:
sch 1 (A1);
reconsider H as ManySortedSet of I by A2,PARTFUN1:def 2,RELAT_1:def 18;
for x be object st x in dom H holds H.x is Function
proof
let i be object;
assume i in dom H;
then reconsider s = i as SortSymbol of S;
H.s = NHReverse(s,X) by A2;
hence thesis;
end;
then reconsider H as ManySortedFunction of I by FUNCOP_1:def 6;
for i be object st i in I holds H.i is Function of FG.i,(PTVars(X)).i
proof
let i be object;
assume i in I;
then reconsider s = i as SortSymbol of S;
A3: (PTVars X).s = PTVars(s,X) by Def24;
A4: H.i = NHReverse(s,X) by A2;
(OSFreeGen X).s = OSFreeGen(s,X) by Def26;
hence thesis by A3,A4;
end;
then reconsider H as ManySortedFunction of FG,PTVars(X) by PBOOLE:def 15;
take H;
let s be Element of S;
thus thesis by A2;
end;
uniqueness
proof
let A,B be ManySortedFunction of OSFreeGen(X),PTVars(X);
assume that
A5: for s be Element of S holds A.s = NHReverse(s,X) and
A6: for s be Element of S holds B.s =NHReverse(s,X);
for i be object st i in the carrier of S holds A.i = B.i
proof
let i be object;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
A.s = NHReverse(s,X) by A5;
hence thesis by A6;
end;
hence thesis;
end;
end;
theorem Th38:
for S be locally_directed OrderSortedSign, X be non-empty
ManySortedSet of S holds OSFreeGen(X) is osfree
proof
let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S;
set FA = FreeOSA(X), PTA = ParsedTermsOSA(X), SPTA = the Sorts of PTA, FG =
OSFreeGen(X);
let U1 be non-empty monotone OSAlgebra of S, F be ManySortedFunction of FG,
the Sorts of U1;
set SA =the Sorts of FA, S1 = the Sorts of U1, R = LCongruence(X), NH =
OSNat_Hom(PTA,R);
reconsider NH1= NH as ManySortedFunction of PTA, FA;
set NHP = (NH1 || PTVars(X));
A1: now
let s be Element of S;
A2: NHP.s = (NH1.s) | ((PTVars(X)).s) by MSAFREE:def 1;
hence NHP.s = (NH1.s) | (PTVars(s,X)) by Def24;
thus PTVars(s,X) c= SPTA.s;
thus dom (NH1.s) = SPTA.s & rng (NH1.s) c= SA.s by FUNCT_2:def 1
,RELAT_1:def 19;
A3: (PTVars(X)).s = PTVars(s,X) by Def24;
hence
A4: dom (NHP.s) = PTVars(s,X) by FUNCT_2:def 1;
for y being object holds
y in FG.s iff (ex x being object st x in dom (NHP.
s) & y = (NHP.s).x)
proof
let y be object;
thus y in FG.s implies
ex x being object st x in dom (NHP.s) & y = (NHP.s).
x
proof
assume y in FG.s;
then y in OSFreeGen(s,X) by Def26;
then consider a be object such that
A5: a in X.s and
A6: y = (NH.s).(root-tree [a,s]) by Def25;
take x = root-tree [a,s];
root-tree [a,s] in dom (NHP.s) by A4,A5,Def23;
hence thesis by A2,A6,FUNCT_1:47;
end;
given x being object such that
A7: x in dom (NHP.s) and
A8: y = (NHP.s).x;
consider a be object such that
A9: a in X.s and
A10: x = root-tree [a,s] by A3,A7,Def23;
y = (NH.s).(root-tree [a,s]) by A2,A7,A8,A10,FUNCT_1:47;
then y in OSFreeGen(s,X) by A9,Def25;
hence thesis by Def26;
end;
hence
A11: rng (NHP.s) = FG.s by FUNCT_1:def 3;
hence NHP.s is Function of PTVars(s,X),FG.s by A4,FUNCT_2:1;
thus NHP.s is Function of (PTVars(X)).s,FG.s by A3,A4,A11,FUNCT_2:1;
end;
then for i being object st i in the carrier of S
holds NHP.i is Function of (PTVars X).i, FG.i;
then reconsider
NHP = (NH1 || PTVars(X)) as ManySortedFunction of PTVars(X),FG by
PBOOLE:def 15;
consider h being ManySortedFunction of PTA,U1 such that
A12: h is_homomorphism PTA,U1 and
A13: h is order-sorted and
A14: h || PTVars(X) = F ** NHP by Th37;
reconsider hCng = OSCng(h) as monotone OSCongruence of PTA by A12,A13,
OSALG_4:24;
reconsider H = OSHomQuot(h,R) as ManySortedFunction of FA,U1;
take H;
A15: R c= hCng by Def17;
hence H is_homomorphism FA,U1 & H is order-sorted by A12,A13,OSALG_4:25;
for s be Element of S holds F.s = (H.s) | (FG.s)
proof
let s be Element of S;
A16: FG.s = OSFreeGen(s,X) by Def26;
then FG.s c= SA.s;
then FG.s c= dom OSHomQuot(h,R,s) by FUNCT_2:def 1;
then
A17: dom (OSHomQuot(h,R,s) | (FG.s)) = FG.s by RELAT_1:62;
rng (OSHomQuot(h,R,s) | (FG.s)) c= S1.s by RELAT_1:def 19;
then reconsider
OSF = OSHomQuot(h,R,s) | (FG.s) as Function of FG.s,S1.s by A17,FUNCT_2:2;
now
A18: dom (NHP.s) = PTVars(s,X) by A1;
A19: ((h.s) | ((PTVars(X)).s)) = (F ** NHP).s by A14,MSAFREE:def 1
.= (F.s )*(NHP.s) by MSUALG_3:2;
let x be object such that
A20: x in FG.s;
consider a being object such that
A21: a in X.s and
A22: x = (NH.s).(root-tree [a,s]) by A16,A20,Def25;
reconsider xa = root-tree [a,s] as Element of SPTA.s by A21,Th10;
A23: OSClass(R,xa) = (OSNat_Hom(PTA,R,s)).xa by OSALG_4:def 21
.= x by A22,OSALG_4:def 22;
A24: root-tree [a,s] in PTVars(s,X) by A21,Def23;
then xa in (PTVars(X)).s by Def24;
then
A25: (h.s).xa = (h.s | ((PTVars(X)).s)).xa by FUNCT_1:49;
A26: (OSHomQuot(h,R,s)).(OSClass(R,xa)) = (h.s).xa by A12,A13,A15,
OSALG_4:def 27;
(NHP.s).xa = ((NH.s) | (PTVars(s,X))).xa by A1
.= (NH.s).xa by A24,FUNCT_1:49;
then (h.s).xa = (F.s).x by A22,A24,A19,A25,A18,FUNCT_1:13;
hence (F.s).x = (OSHomQuot(h,R,s) | (FG.s)).x by A20,A23,A26,FUNCT_1:49;
end;
then F.s = OSF by FUNCT_2:12;
hence thesis by OSALG_4:def 28;
end;
then
for i be set st i in the carrier of S holds F.i = (H.i) | (FG.i);
hence thesis by MSAFREE:def 1;
end;
theorem Th39:
for S be locally_directed OrderSortedSign, X be non-empty
ManySortedSet of S holds FreeOSA(X) is osfree
proof
let S be locally_directed OrderSortedSign, X be non-empty ManySortedSet of S;
take OSFreeGen(X);
thus thesis by Th38;
end;
registration
let S be locally_directed OrderSortedSign;
cluster osfree strict for non-empty monotone OSAlgebra of S;
existence
proof
set U1 = the non-empty OSAlgebra of S;
reconsider X = the Sorts of U1 as non-empty ManySortedSet of S;
take FreeOSA(X);
thus thesis by Th39;
end;
end;
begin
:: PTMin ... minimality of PTCongruence on regular signatures
:: minimal terms
definition
let S be locally_directed regular monotone OrderSortedSign, X be non-empty
ManySortedSet of S;
func PTMin X -> Function of TS(DTConOSA(X)), TS(DTConOSA(X)) means
:Def31:
( for t being Symbol of DTConOSA(X) st t in Terminals DTConOSA(X) holds it.(
root-tree t) = pi t ) & for nt being Symbol of DTConOSA(X), ts being
FinSequence of TS(DTConOSA(X)) st nt ==> roots ts holds it.(nt-tree ts) = pi(@(
X,nt),it * ts);
existence
proof
set G = DTConOSA(X);
set D = TS G;
deffunc TermVal(Symbol of G) = pi $1;
deffunc NTermVal(Symbol of G,set,FinSequence of D) = In(pi(@(X,$1),$3),D);
consider f being Function of TS(G), D such that
A1: (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 qua FinSequence
of D) from DTCONSTR:sch 8;
take f;
thus for t being Symbol of G st t in Terminals G holds f.(root-tree t) =
TermVal(t) by A1;
let nt be Symbol of G, ts be FinSequence of TS(G);
reconsider fts = f * ts as FinSequence of D;
assume nt ==> roots ts;
then f.(nt-tree ts) = In(pi(@(X,nt),fts),D) by A1;
hence thesis;
end;
uniqueness
proof
set G = DTConOSA(X);
set D = TS G;
deffunc TermVal(Symbol of G) = pi $1;
deffunc NTermVal(Symbol of G,set,FinSequence of D) = pi(@(X,$1),$3 qua
FinSequence of D);
let M1,M2 be Function of TS(DTConOSA(X)), TS(DTConOSA(X)) such that
A2: (for t being Symbol of DTConOSA(X) st t in Terminals DTConOSA(X)
holds M1.(root-tree t) = TermVal(t) ) & for nt being Symbol of DTConOSA(X), ts
being FinSequence of TS(DTConOSA(X)) st nt ==> roots ts holds M1.(nt-tree ts) =
NTermVal(nt, roots ts, M1 * ts qua FinSequence of D) and
A3: (for t being Symbol of DTConOSA(X) st t in Terminals DTConOSA(X)
holds M2.(root-tree t) = TermVal(t) ) & for nt being Symbol of DTConOSA(X), ts
being FinSequence of TS(DTConOSA(X)) st nt ==> roots ts holds M2.(nt-tree ts) =
NTermVal(nt, roots ts, M2 * ts qua FinSequence of D);
thus M1 = M2 from DTCONSTR:sch 9(A2,A3);
end;
end;
theorem Th40:
for S be locally_directed regular monotone OrderSortedSign, X
be non-empty ManySortedSet of S, t being Element of TS DTConOSA(X) holds (PTMin
X).t in OSClass(PTCongruence(X),t) & LeastSort ((PTMin X).t) <= LeastSort t & (
for s being Element of S, x being set st x in X.s & t = root-tree [x,s] holds (
PTMin X).t = t ) & (for o being OperSymbol of S, ts being FinSequence of TS(
DTConOSA(X)) st OSSym(o,X) ==> roots ts & t = OSSym(o,X)-tree ts holds
LeastSorts ((PTMin X)*ts) <= the_arity_of o & OSSym(o,X) ==> roots ((PTMin X)*
ts) & OSSym(LBound(o,LeastSorts ((PTMin X)*ts)),X) ==> roots ((PTMin X)*ts) & (
PTMin X).t = OSSym(LBound(o,LeastSorts ((PTMin X)*ts)),X)-tree ((PTMin X)*ts))
proof
let S be locally_directed regular monotone OrderSortedSign, X be non-empty
ManySortedSet of S, t be Element of TS DTConOSA(X);
set PTA = ParsedTermsOSA(X), D = DTConOSA(X), R = PTCongruence(X), SPTA = (
the Sorts of PTA), M = PTMin(X), F = PTClasses(X);
defpred P1[Element of TS D] means (PTMin X).$1 in OSClass(R,$1);
defpred P2[Element of TS D] means LeastSort ((PTMin X).$1) <= LeastSort $1;
defpred P4[Element of TS D] means (for s being Element of S, x being set st
x in X.s & $1 = root-tree [x,s] holds (PTMin X).$1 = $1 );
defpred P5[Element of TS D] means for o being OperSymbol of S, ts being
FinSequence of TS(DTConOSA(X)) st OSSym(o,X) ==> roots ts & $1 = OSSym(o,X)
-tree ts holds LeastSorts ((PTMin X)*ts) <= the_arity_of o & OSSym(o,X) ==>
roots ((PTMin X)*ts) & OSSym(LBound(o,LeastSorts ((PTMin X)*ts)),X) ==> roots (
(PTMin X)*ts) & (PTMin X).$1 = OSSym(LBound(o,LeastSorts ((PTMin X)*ts)),X)
-tree ((PTMin X)*ts);
defpred P[DecoratedTree of the carrier of D] means ex t1 being Element of TS
D st t1 = $1 & P1[t1] & P2[t1] & P4[t1] & P5[t1];
A1: for nt being Symbol of D, ts1 being FinSequence of TS(D) st nt ==> roots
ts1 & (for dt1 being DecoratedTree of the carrier of D st dt1 in rng ts1 holds
P[dt1]) holds P[nt-tree ts1]
proof
let nt being Symbol of D, ts1 being FinSequence of TS(D) such that
A2: nt ==> roots ts1 and
A3: for dt1 being DecoratedTree of the carrier of D st dt1 in rng ts1
ex t2 being Element of TS D st t2 = dt1 & P1[t2] & P2[t2] & P4[t2] & P5[t2];
reconsider t1 = nt-tree ts1 as Element of TS D by A2,Th12;
A4: rng ts1 c= TS D by FINSEQ_1:def 4;
consider o being OperSymbol of S such that
A5: nt = [o,the carrier of S] and
A6: ts1 in Args(o,PTA) and
A7: nt-tree ts1 = Den(o,PTA).ts1 and
for s1 being Element of S holds nt-tree ts1 in SPTA.s1 iff
the_result_sort_of o <= s1 by A2,Th12;
set Ms = (PTMin X)*ts1, LSMs = LeastSorts Ms, w = the_arity_of o, so =
the_result_sort_of o, Lo = LBound(o,LSMs);
A8: dom ts1 = dom w by A6,MSUALG_3:6;
A9: dom ((PTMin X)*ts1) = dom ts1 by FINSEQ_3:120;
then
A10: dom LSMs = dom ts1 by Def13;
@(X,nt) = o by A2,A5,Def15;
then
A11: M.(nt-tree ts1) = pi(o,M*ts1) by A2,Def31;
A12: P5[t1]
proof
let o2 be OperSymbol of S, ts be FinSequence of TS(DTConOSA(X)) such
that
OSSym(o2,X) ==> roots ts and
A13: t1 = OSSym(o2,X)-tree ts;
set Ms1 = (PTMin X)*ts, LSMs1 = LeastSorts Ms1, Lo2 = LBound(o2,LSMs1);
A14: ts = ts1 by A13,TREES_4:15;
A15: OSSym(o2,X) = nt by A13,TREES_4:15;
then
A16: o2 = o by A5,XTUPLE_0:1;
A17: LeastSorts ((PTMin X)*ts1) <= the_arity_of o
proof
thus len LSMs = len w by A8,A10,FINSEQ_3:29;
let i be set such that
A18: i in dom LSMs;
reconsider k = i as Nat by A18;
ts1.k in rng ts1 by A10,A18,FUNCT_1:3;
then reconsider tr = ts1.k as Element of TS D by A4;
A19: ex tr1 being Element of TS D st tr1 = tr &( P1[tr1])&( P2 [tr1])
&( P4[tr1])& P5[tr1] by A3,A10,A18,FUNCT_1:3;
A20: w/.k = w.i by A8,A10,A18,PARTFUN1:def 6;
A21: Ms.k = (PTMin X).tr by A9,A10,A18,FINSEQ_3:120;
ts1.k in SPTA.(w/.k) by A6,A8,A10,A18,MSUALG_6:2;
then
A22: LeastSort (tr) <= (w/.k) by Def12;
let s1,s2 be Element of S such that
A23: s1 = LSMs.i and
A24: s2 = w.i;
ex t3 being Element of TS D st t3 = Ms.k & LSMs.k = LeastSort
t3 by A9,A10,A18,Def13;
hence thesis by A19,A23,A24,A21,A22,A20,ORDERS_2:3;
end;
hence LeastSorts ((PTMin X)*ts) <= the_arity_of o2 by A5,A15,A14,
XTUPLE_0:1;
LBound(o2,LSMs1) has_least_rank_for o2,LSMs1 by A14,A16,A17,OSALG_1:14;
then LBound(o2,LSMs1) has_least_args_for o2,LSMs1;
then LSMs1 <= the_arity_of Lo2;
then
A25: Ms1 in Args(Lo2,PTA) by Th18;
Ms1 in Args(o2,PTA) by A14,A16,A17,Th18;
hence OSSym(o2,X) ==> roots Ms1 & OSSym(Lo2,X) ==> roots Ms1 by A25,Th13;
hence thesis by A11,A14,A16,Def14;
end;
A26: for s being Element of S, x being set st x in X.s & t1 = root-tree [x
,s] holds M.t1 = t1
proof
let s being Element of S, x being set such that
A27: x in X.s and
A28: t1 = root-tree [x,s];
t1.{} = [o,the carrier of S] by A5,TREES_4:def 4;
hence thesis by A27,A28,Th10;
end;
A29: F.t1 = @(nt,F*ts1) by A2,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 (F*ts1) & for
y being Nat st y in dom (F*ts1) holds [x2.y,w3/.y] in (F*ts1).y};
take t1;
thus t1 = nt-tree ts1;
A30: ex l being Nat st dom ts1 = Seg l by FINSEQ_1:def 2;
reconsider ta1 = t1 as Element of SPTA.(LeastSort t1) by Def12;
A31: dom (F*ts1) = dom ts1 by FINSEQ_3:120;
A32: nt = OSSym(o,X) by A5;
then OSSym(LBound(o,LeastSorts ((PTMin X)*ts1)),X) ==> roots ((PTMin X)*
ts1) by A2,A12;
then consider o3 being OperSymbol of S such that
A33: OSSym(Lo,X) = [o3,the carrier of S] and
A34: Ms in Args(o3,ParsedTermsOSA(X)) and
A35: OSSym(Lo,X)-tree Ms = Den(o3,ParsedTermsOSA(X)).Ms and
for s1 being Element of S holds OSSym(Lo,X)-tree Ms in (the Sorts of
PTA).s1 iff the_result_sort_of o3 <= s1 by Th12;
reconsider Msr = Ms as Element of Args(Lo,PTA) by A33,A34,XTUPLE_0:1;
A36: Lo = o3 by A33,XTUPLE_0:1;
then
A37: M.t1 = Den(Lo,PTA).(Msr) by A2,A32,A12,A35;
A38: LeastSorts ((PTMin X)*ts1) <= the_arity_of o by A2,A32,A12;
then
A39: Lo has_least_rank_for o,LSMs by OSALG_1:14;
then
A40: Lo has_least_sort_for o,LSMs;
then
A41: o ~= Lo;
Lo has_least_args_for o,LSMs by A39;
then the_arity_of Lo <= w by A38;
then
A42: len the_arity_of Lo = len w;
A43: OSClass(R,t1) = OSClass(R,ta1) by Def27
.= proj1(F.t1) by Th25;
A44: the_result_sort_of Lo <= so by A38,A40;
A45: M.t1 in OSClass(R,t1)
proof
defpred P[object,object] means [Ms.$1,$2] in (F*ts1).$1;
A46: for i being object st i in dom (F*ts1)
ex s4 being object st s4 in the
carrier of S & P[i,s4]
proof
let i be object such that
A47: i in dom (F*ts1);
A48: (F*ts1).i = F.(ts1.i) by A47,FINSEQ_3:120;
ts1.i in rng ts1 by A31,A47,FUNCT_1:3;
then reconsider td1 = ts1.i as Element of TS D by A4;
A49: ex td2 being Element of TS D st td2 = td1 & M.td2 in OSClass(R,
td2) &( P2[td2])&( P4[td2])& P5[td2] by A3,A31,A47,FUNCT_1:3;
A50: Ms.i = M.(ts1.i) by A31,A47,FUNCT_1:13;
reconsider tda = td1 as Element of SPTA.(LeastSort td1) by Def12;
OSClass(R,td1) = OSClass(R,tda) by Def27
.= proj1((F*ts1).i) by A48,Th25;
then ex s4 being object st [Ms.i,s4] in (F*ts1).i by A50,A49,
XTUPLE_0:def 12;
hence thesis by A48,Th23;
end;
consider f being Function such that
A51: dom f = dom (F*ts1) & rng f c= the carrier of S & for z being
object st z in dom (F*ts1) holds P[z,f.z] from FUNCT_1:sch 6(A46);
reconsider wa = f as FinSequence by A31,A30,A51,FINSEQ_1:def 2;
reconsider wa as FinSequence of the carrier of S by A51,FINSEQ_1:def 4;
reconsider wa as Element of (the carrier of S)* by FINSEQ_1:def 11;
for y being Nat st y in dom (F*ts1) holds [Msr.y,wa/.y] in (F*ts1). y
proof
let y be Nat such that
A52: y in dom (F*ts1);
(wa/.y) = wa.y by A51,A52,PARTFUN1:def 6;
hence thesis by A51,A52;
end;
then [Den(Lo,PTA).Msr,so] in F.t1 by A5,A29,A41,A44,A42,A51;
hence thesis by A43,A37,XTUPLE_0:def 12;
end;
(PTMin X).t1 = OSSym(LBound(o,LeastSorts ((PTMin X)*ts1)),X)-tree ((
PTMin X)*ts1) by A2,A32,A12;
then
A53: LeastSort (M.t1) = the_result_sort_of Lo by A34,A35,A36,Th17;
LeastSort t1 = so by A6,A7,Th17;
hence thesis by A12,A38,A53,A40,A45,A26;
end;
A54: 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
A55: sy in Terminals D;
reconsider t1 = root-tree sy as Element of TS DTConOSA(X) by A55,
DTCONSTR:def 1;
take t1;
thus t1 = root-tree sy;
A56: M.(root-tree sy) = pi sy by A55,Def31
.= root-tree sy by A55,Def16;
hence M.t1 in OSClass(R,t1) by Th32;
thus LeastSort (M.t1) <= LeastSort t1 by A56;
thus for s1 being Element of S, x1 being set st x1 in X.s1 & t1 =
root-tree [x1,s1] holds M.t1 = t1 by A56;
A57: ex s be Element of S, x be set st x in X.s & sy = [x,s] by A55,Th4;
hereby
let o being OperSymbol of S, ts being FinSequence of TS(DTConOSA(X))
such that
OSSym(o,X) ==> roots ts and
A58: t1 = OSSym(o,X)-tree ts;
t1.{} = [o,the carrier of S] by A58,TREES_4:def 4;
hence LeastSorts ((PTMin X)*ts) <= the_arity_of o & OSSym(o,X) ==> roots
((PTMin X)*ts) & OSSym(LBound(o,LeastSorts ((PTMin X)*ts)),X) ==> roots ((PTMin
X)*ts) & (PTMin X).t1 = OSSym(LBound(o,LeastSorts ((PTMin X)*ts)),X)-tree ((
PTMin X)*ts) by A57,Th10;
end;
end;
for dt being DecoratedTree of the carrier of D st dt in TS(D) holds P[
dt] from DTCONSTR:sch 7(A54,A1);
then
ex t1 being Element of TS D st t1 = t &( P1[t1])&( P2[t1] )&( P4[t1])&
P5[t1];
hence thesis;
end;
theorem Th41:
for S be locally_directed regular monotone OrderSortedSign, X
be non-empty ManySortedSet of S, t,t1 being Element of TS DTConOSA(X) st t1 in
OSClass(PTCongruence(X),t) holds (PTMin X).t1 = (PTMin X).t
proof
let S be locally_directed regular monotone OrderSortedSign, X be non-empty
ManySortedSet of S, t be Element of TS DTConOSA(X);
set PTA = ParsedTermsOSA(X), D = DTConOSA(X), R = PTCongruence(X), SPTA = (
the Sorts of PTA), M = PTMin(X), F = PTClasses(X);
defpred P3[Element of TS D] means (for t1 being Element of TS DTConOSA(X) st
t1 in OSClass(R,$1) holds (PTMin X).t1 = (PTMin X).$1 );
defpred P[DecoratedTree of the carrier of D] means ex t1 being Element of TS
D st t1 = $1 & P3[t1];
A1: for nt being Symbol of D, ts1 being FinSequence of TS(D) st nt ==> roots
ts1 & (for dt1 being DecoratedTree of the carrier of D st dt1 in rng ts1 holds
P[dt1]) holds P[nt-tree ts1]
proof
let nt being Symbol of D, ts1 being FinSequence of TS(D) such that
A2: nt ==> roots ts1 and
A3: for dt1 being DecoratedTree of the carrier of D st dt1 in rng ts1
ex t2 being Element of TS D st t2 = dt1 & P3[t2];
reconsider t1 = nt-tree ts1 as Element of TS D by A2,Th12;
A4: F.t1 = @(nt,F*ts1) by A2,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 (F*ts1) & for
y being Nat st y in dom (F*ts1) holds [x2.y,w3/.y] in (F*ts1).y};
consider o being OperSymbol of S such that
A5: nt = [o,the carrier of S] and
A6: ts1 in Args(o,PTA) and
nt-tree ts1 = Den(o,PTA).ts1 and
for s1 being Element of S holds nt-tree ts1 in SPTA.s1 iff
the_result_sort_of o <= s1 by A2,Th12;
A7: t1 = OSSym(o,X)-tree ts1 by A5;
then
A8: LeastSorts (M*ts1) <= the_arity_of o by A2,A5,Th40;
set Ms = (PTMin X)*ts1, w = the_arity_of o;
A9: dom ts1 = dom w by A6,MSUALG_3:6;
reconsider ta1 = t1 as Element of SPTA.(LeastSort t1) by Def12;
take t1;
thus t1 = nt-tree ts1;
A10: dom (F*ts1) = dom ts1 by FINSEQ_3:120;
A11: OSClass(R,t1) = OSClass(R,ta1) by Def27
.= proj1(F.t1) by Th25;
A12: rng ts1 c= TS D by FINSEQ_1:def 4;
A13: dom ((PTMin X)*ts1) = dom ts1 by FINSEQ_3:120;
A14: M.t1 = OSSym(LBound(o,LeastSorts (M*ts1)),X)-tree (M*ts1) by A2,A5,A7,Th40
;
thus for t3 being Element of TS DTConOSA(X) st t3 in OSClass(R,t1) holds (
PTMin X).t3 = (PTMin X).t1
proof
let t3 be Element of TS D;
assume t3 in OSClass(R,t1);
then consider s4 being object such that
A15: [t3,s4] in F.t1 by A11,XTUPLE_0:def 12;
consider o2 being OperSymbol of S, x2 being Element of Args(o2,
ParsedTermsOSA(X)), s3 being Element of S such that
A16: [t3,s4] = [Den(o2,ParsedTermsOSA(X)).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 and
A18: ex w3 being Element of (the carrier of S)* st dom w3 = dom (F*
ts1) & for y being Nat st y in dom (F*ts1) holds [x2.y,w3/.y] in (F*ts1).y by
A4,A15;
consider o1 being OperSymbol of S such that
A19: nt = [o1,the carrier of S] and
A20: o1 ~= o2 and
A21: len the_arity_of o1 = len the_arity_of o2 and
the_result_sort_of o1 <= s3 and
the_result_sort_of o2 <= s3 by A17;
A22: o1 = o by A5,A19,XTUPLE_0:1;
then
A23: dom w = dom the_arity_of o2 by A21,FINSEQ_3:29;
reconsider ts3 = x2 as FinSequence of TS(D) by Th13;
A24: dom ts3 = dom the_arity_of o2 by MSUALG_3:6;
A25: dom (M*ts3) = dom ts3 by FINSEQ_3:120;
A26: rng ts3 c= TS D by FINSEQ_1:def 4;
for k being Nat st k in dom (M*ts3) holds (M*ts3).k = Ms.k
proof
consider w3 being Element of (the carrier of S)* such that
dom w3 = dom (F*ts1) and
A27: for y being Nat st y in dom (F*ts1) holds [x2.y,w3/.y] in (F*
ts1).y by A18;
let k being Nat such that
A28: k in dom (M*ts3);
A29: ts3.k in rng ts3 by A25,A28,FUNCT_1:3;
ts1.k in rng ts1 by A9,A23,A24,A25,A28,FUNCT_1:3;
then reconsider
tk1 = ts1.k, tk3 = ts3.k as Element of TS D by A12,A26,A29;
reconsider tak = tk1 as Element of SPTA.(LeastSort tk1) by Def12;
consider tk2 be Element of TS D such that
A30: tk2 = tk1 and
A31: for t4 being Element of TS D st t4 in OSClass(R,tk2) holds M
.t4 = M.tk2 by A3,A9,A23,A24,A25,A28,FUNCT_1:3;
[tk3,w3/.k] in (F*ts1).k by A10,A9,A23,A24,A25,A28,A27;
then
A32: [tk3,w3/.k] in F.tk1 by A10,A9,A23,A24,A25,A28,FINSEQ_3:120;
OSClass(R,tk1) = OSClass(R,tak) by Def27
.= proj1(F.tk1) by Th25;
then tk3 in OSClass(R,tk1) by A32,XTUPLE_0:def 12;
then M.tk3 = M.tk1 by A30,A31;
then M.tk3 = Ms.k by A13,A9,A23,A24,A25,A28,FINSEQ_3:120;
hence thesis by A28,FINSEQ_3:120;
end;
then
A33: M*ts3 = M*ts1 by A13,A9,A23,A25,FINSEQ_1:13,MSUALG_3:6;
A34: OSSym(o2,X) ==> roots x2 by Th13;
then ex o3 being OperSymbol of S st OSSym(o2,X) = [o3,the carrier of S]
& ts3 in Args(o3,PTA) & OSSym(o2,X)-tree ts3 = Den(o3,PTA).ts3 & for s1 being
Element of S holds OSSym(o2,X)-tree ts3 in SPTA.s1 iff the_result_sort_of o3 <=
s1 by Th12;
then consider o3 being OperSymbol of S such that
A35: OSSym(o2,X) = [o3,the carrier of S] and
ts3 in Args(o3,PTA) and
A36: OSSym(o2,X)-tree ts3 = Den(o3,PTA).ts3;
o2 = o3 by A35,XTUPLE_0:1;
then
A37: t3 = OSSym(o2,X)-tree ts3 by A16,A36,XTUPLE_0:1;
then
A38: LeastSorts (M*ts3) <= the_arity_of o2 by A34,Th40;
M.t3 = OSSym(LBound(o2,LeastSorts (M*ts3)),X)-tree (M*ts3) by A34,A37
,Th40;
hence thesis by A14,A8,A20,A22,A33,A38,OSALG_1:34;
end;
end;
A39: 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
A40: sy in Terminals D;
reconsider t1 = root-tree sy as Element of TS DTConOSA(X) by A40,
DTCONSTR:def 1;
take t1;
thus t1 = root-tree sy;
A41: ex s be Element of S, x be set st x in X.s & sy = [x,s] by A40,Th4;
let t2 be Element of TS DTConOSA(X);
assume t2 in OSClass(R,t1);
hence thesis by A41,Th33;
end;
for dt being DecoratedTree of the carrier of D st dt in TS(D) holds P[
dt] from DTCONSTR:sch 7(A39,A1);
then ex t1 being Element of TS D st t1 = t & P3[t1];
hence thesis;
end;
theorem Th42:
for S be locally_directed regular monotone OrderSortedSign, X
be non-empty ManySortedSet of S, t1,t2 be Element of TS DTConOSA(X) holds t2 in
OSClass(PTCongruence(X),t1) iff (PTMin X).t2 = (PTMin X).t1
proof
let S be locally_directed regular monotone OrderSortedSign, X be non-empty
ManySortedSet of S, t1,t2 be Element of TS DTConOSA(X);
set R = PTCongruence(X),M = PTMin(X);
thus t2 in OSClass(R,t1) implies M.t2 = M.t1 by Th41;
M.t2 in OSClass(R,t2) by Th40;
then
A1: OSClass(R,t2) = OSClass(R,M.t2) by Th34;
M.t1 in OSClass(R,t1) by Th40;
then
A2: OSClass(R,t1) = OSClass(R,M.t1) by Th34;
assume M.t2 = M.t1;
hence thesis by A2,A1,Th32;
end;
theorem Th43:
for S be locally_directed regular monotone OrderSortedSign, X
be non-empty ManySortedSet of S, t1 be Element of TS DTConOSA(X) holds (PTMin X
).((PTMin X).t1) = (PTMin X).t1
proof
let S be locally_directed regular monotone OrderSortedSign, X be non-empty
ManySortedSet of S, t1 be Element of TS DTConOSA(X);
(PTMin X).t1 in OSClass(PTCongruence(X),t1) by Th40;
hence thesis by Th42;
end;
theorem Th44:
for S be locally_directed regular monotone OrderSortedSign,
X be non-empty ManySortedSet of S,
R be monotone MSEquivalence-like (OrderSortedRelation of ParsedTermsOSA(X)),
t be Element of TS DTConOSA(X) holds
[t,(PTMin X).t] in R.(LeastSort t)
proof
let S be locally_directed regular monotone OrderSortedSign, X be non-empty
ManySortedSet of S;
set PTA = ParsedTermsOSA(X), SPTA = the Sorts of PTA, D = DTConOSA(X),
M = PTMin X;
let R be monotone MSEquivalence-like OrderSortedRelation of PTA;
defpred P3[set] means ex t1 being Element of TS D st t1 = $1 & [t1,M.t1] in
R.(LeastSort t1);
let t be Element of TS D;
A1: R is os-compatible by OSALG_4:def 2;
A2: for nt being Symbol of D, ts1 being FinSequence of TS(D) st nt ==> roots
ts1 & (for dt1 being DecoratedTree of the carrier of D st dt1 in rng ts1 holds
P3[dt1] ) holds P3[nt-tree ts1]
proof
let nt being Symbol of D, ts1 being FinSequence of TS(D) such that
A3: nt ==> roots ts1 and
A4: for dt1 being DecoratedTree of the carrier of D st dt1 in rng ts1
holds P3[dt1];
consider o being OperSymbol of S such that
A5: nt = [o,the carrier of S] and
A6: ts1 in Args(o,PTA) and
A7: nt-tree ts1 = Den(o,PTA).ts1 and
for s1 being Element of S holds nt-tree ts1 in SPTA.s1 iff
the_result_sort_of o <= s1 by A3,Th12;
reconsider t1 = nt-tree ts1 as Element of TS D by A3,Th12;
A8: dom ((PTMin X)*ts1) = dom ts1 by FINSEQ_3:120;
reconsider tsa =ts1 as Element of Args(o,PTA) by A6;
set w = the_arity_of o;
A9: rng ts1 c= TS D by FINSEQ_1:def 4;
set lo = LBound(o,LeastSorts (M*ts1)), rs1 = the_result_sort_of o;
A10: t1 = OSSym(o,X)-tree ts1 by A5;
then
A11: OSSym(LBound(o,LeastSorts (M*ts1)),X) ==> roots (M*ts1) by A3,A5,Th40;
then reconsider tsm =M*ts1 as Element of Args(lo,PTA) by Th13;
A12: dom ts1 = dom w by A6,MSUALG_3:6;
A13: for y being Nat st y in dom tsm holds [tsm.y,tsa.y] in R.((
the_arity_of o)/.y)
proof
let y being Nat such that
A14: y in dom tsm;
ts1.y in rng ts1 by A8,A14,FUNCT_1:3;
then reconsider td1=ts1.y as Element of TS D by A9;
consider t2 being Element of TS D such that
A15: t2 = td1 and
A16: [t2,M.t2] in R.(LeastSort t2) by A4,A8,A14,FUNCT_1:3;
A17: M.t2 = tsm.y by A14,A15,FINSEQ_3:120;
A18: M.t2 in SPTA.(LeastSort t2) by A16,ZFMISC_1:87;
tsa.y in SPTA.(w/.y) by A8,A12,A14,MSUALG_6:2;
then
A19: LeastSort t2 <= w/.y by A15,Def12;
A20: t2 in SPTA.(LeastSort t2) by A16,ZFMISC_1:87;
field(R.(LeastSort t2)) = SPTA.(LeastSort t2) by ORDERS_1:12;
then R.(LeastSort t2) is_symmetric_in SPTA.(LeastSort t2) by
RELAT_2:def 11;
then [M.t2,t2] in R.(LeastSort t2) by A16,A20,A18,RELAT_2:def 3;
hence thesis by A1,A15,A20,A18,A17,A19;
end;
LeastSorts (M*ts1) <= the_arity_of o by A3,A5,A10,Th40;
then lo <= o by OSALG_1:35;
then
A21: [Den(lo,PTA).tsm,Den(o,PTA).tsa] in R.(the_result_sort_of o) by A13,
OSALG_4:def 26;
then
A22: Den(o,PTA).tsa in SPTA.rs1 by ZFMISC_1:87;
A23: LeastSort t1 = the_result_sort_of o by A6,A7,Th17;
A24: OSSym(o,X) ==> roots ts1 by A3,A5;
take t1;
thus t1 = nt-tree ts1;
field(R.rs1) = SPTA.rs1 by ORDERS_1:12;
then
A25: R.rs1 is_symmetric_in SPTA.rs1 by RELAT_2:def 11;
Den(lo,PTA).tsm in SPTA.rs1 by A21,ZFMISC_1:87;
then
A26: [Den(o,PTA).tsa,Den(lo,PTA).tsm] in R.rs1 by A21,A22,A25,RELAT_2:def 3;
consider o4 being OperSymbol of S such that
A27: OSSym(lo,X) = [o4,the carrier of S] and
M*ts1 in Args(o4,PTA) and
A28: OSSym(lo,X)-tree (M*ts1) = Den(o4,PTA).(M*ts1) and
for s1 being Element of S holds OSSym(lo,X)-tree (M*ts1) in SPTA.s1
iff the_result_sort_of o4 <= s1 by A11,Th12;
lo = o4 by A27,XTUPLE_0:1;
hence thesis by A5,A7,A24,A26,A23,A28,Th40;
end;
A29: for s being Symbol of D st s in Terminals D holds P3[root-tree s]
proof
let sy being Symbol of D;
assume sy in Terminals D;
then
A30: ex s be Element of S, x be set st x in X.s & sy = [x,s] by Th4;
then reconsider t1 = root-tree sy as Element of TS D by Th10;
take t1;
A31: t1 in SPTA.(LeastSort t1) by Def12;
field(R.(LeastSort t1)) = SPTA.(LeastSort t1) by ORDERS_1:12;
then
A32: R.(LeastSort t1) is_reflexive_in SPTA.(LeastSort t1) by RELAT_2:def 9;
t1 = M.t1 by A30,Th40;
hence thesis by A31,A32,RELAT_2:def 1;
end;
for dt being DecoratedTree of the carrier of D st dt in TS(D) holds P3[
dt] from DTCONSTR:sch 7(A29,A2);
then
ex t1 being Element of TS D st t = t1 & [t1,M.t1] in R.( LeastSort t1 );
hence thesis;
end;
theorem Th45:
for S be locally_directed regular monotone OrderSortedSign, X
be non-empty ManySortedSet of S, R be monotone MSEquivalence-like
OrderSortedRelation of ParsedTermsOSA(X) holds PTCongruence(X) c= R
proof
let S be locally_directed regular monotone OrderSortedSign, X be non-empty
ManySortedSet of S;
set PTA = ParsedTermsOSA(X), SPTA = the Sorts of PTA, D = DTConOSA(X), M =
PTMin X, P = PTCongruence X;
reconsider O1 = SPTA as OrderSortedSet of S;
let R be monotone MSEquivalence-like OrderSortedRelation of PTA;
let i be object such that
A1: i in the carrier of S;
reconsider s = i as Element of S by A1;
A2: R is os-compatible by OSALG_4:def 2;
for a,b being object holds [a,b] in P.s implies [a,b] in R.s
proof
A3: field(R.s) = SPTA.s by ORDERS_1:12;
then
A4: R.s is_transitive_in SPTA.s by RELAT_2:def 16;
A5: R.s is_symmetric_in SPTA.s by A3,RELAT_2:def 11;
let a,b be object such that
A6: [a,b] in P.s;
reconsider ta=a,tb=b as Element of SPTA.s by A6,ZFMISC_1:87;
A7: a in SPTA.i by A6,ZFMISC_1:87;
A8: OSClass(P,ta) = OSClass(P,tb) by A6,OSALG_4:12;
A9: b in SPTA.i by A6,ZFMISC_1:87;
dom SPTA = the carrier of S by PARTFUN1:def 2;
then reconsider t1=a,t2=b as Element of PTA by A1,A7,A9,CARD_5:2;
reconsider t1,t2 as Element of TS D by Th14;
A10: t2 in SPTA.(LeastSort t2) by Def12;
A11: M.t2 in SPTA.(LeastSort M.t2) by Def12;
LeastSort (M.t2) <= LeastSort t2 by Th40;
then
A12: O1.(LeastSort (M.t2)) c= O1.(LeastSort t2) by OSALG_1:def 16;
A13: [t2,M.t2] in R.(LeastSort t2) by Th44;
LeastSort t2 <= s by A9,Def12;
then
A14: [t2,M.t2] in R.s by A2,A10,A11,A12,A13;
then M.t2 in SPTA.s by ZFMISC_1:87;
then
A15: [M.t2,t2] in R.s by A9,A14,A5,RELAT_2:def 3;
LeastSort (M.t1) <= LeastSort t1 by Th40;
then
A16: O1.(LeastSort (M.t1)) c= O1.(LeastSort t1) by OSALG_1:def 16;
A17: M.t1 in SPTA.(LeastSort M.t1) by Def12;
A18: [t1,M.t1] in R.(LeastSort t1) by Th44;
A19: OSClass(P,t2) = OSClass(P,tb) by Def27;
OSClass(P,t1) = OSClass(P,ta) by Def27;
then t1 in OSClass(P,t2) by A8,A19,Th34;
then
A20: M.t1 = M.t2 by Th42;
A21: t1 in SPTA.(LeastSort t1) by Def12;
LeastSort t1 <= s by A7,Def12;
then
A22: [t1,M.t1] in R.s by A2,A21,A17,A16,A18;
then M.t1 in SPTA.s by ZFMISC_1:87;
hence thesis by A7,A9,A20,A22,A4,A15,RELAT_2:def 8;
end;
hence thesis by RELAT_1:def 3;
end;
:: minimality of PTCongruence
theorem
for S be locally_directed regular monotone OrderSortedSign, X be
non-empty ManySortedSet of S holds LCongruence(X) = PTCongruence(X)
proof
let S be locally_directed regular monotone OrderSortedSign, X be non-empty
ManySortedSet of S;
A1: PTCongruence(X) c= LCongruence(X) by Th45;
LCongruence(X) c= PTCongruence(X) by Def17;
hence thesis by A1,PBOOLE:146;
end;
:: I would prefer attribute "minimal", but non-clusterable
definition
let S be locally_directed regular monotone OrderSortedSign, X be non-empty
ManySortedSet of S;
mode MinTerm of S,X -> Element of TS DTConOSA(X) means
:Def32:
(PTMin X).it = it;
existence
proof
set t = the Element of TS DTConOSA(X);
take (PTMin X).t;
thus thesis by Th43;
end;
end;
definition
let S be locally_directed regular monotone OrderSortedSign, X be non-empty
ManySortedSet of S;
func MinTerms X -> Subset of TS DTConOSA(X) equals
rng (PTMin X);
correctness by RELAT_1:def 19;
end;
theorem
for S be locally_directed regular monotone OrderSortedSign, X be
non-empty ManySortedSet of S, x being set holds x is MinTerm of S,X iff x in
MinTerms X
proof
let S be locally_directed regular monotone OrderSortedSign, X be non-empty
ManySortedSet of S, x be set;
hereby
assume x is MinTerm of S,X;
then reconsider t =x as MinTerm of S,X;
(PTMin X).t = t by Def32;
hence x in MinTerms X by FUNCT_2:4;
end;
assume x in MinTerms X;
then consider y being object such that
A1: y in dom (PTMin X) and
A2: x = (PTMin X).y by FUNCT_1:def 3;
reconsider t = y as Element of TS DTConOSA(X) by A1;
(PTMin X).t is Element of TS DTConOSA(X);
then reconsider tx = x as Element of TS DTConOSA(X) by A2;
(PTMin X).tx = tx by A1,A2,Th43;
hence thesis by Def32;
end;