let S be locally_directed OrderSortedSign; for X being V2() ManySortedSet of S
for R being ManySortedRelation of (ParsedTermsOSA X) holds
( R = PTCongruence X iff ( ( for s1, s2 being Element of S
for 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 st ( [(root-tree [x,s1]),y] in R . s2 or [y,(root-tree [x,s1])] in R . s2 ) holds
( s1 <= s2 & y = root-tree [x,s1] ) ) ) ) & ( for o1, o2 being OperSymbol of S
for x1 being Element of Args (o1,(ParsedTermsOSA X))
for x2 being Element of Args (o2,(ParsedTermsOSA X))
for 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) ) ) ) ) ) ) )
let X be V2() ManySortedSet of S; for R being ManySortedRelation of (ParsedTermsOSA X) holds
( R = PTCongruence X iff ( ( for s1, s2 being Element of S
for 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 st ( [(root-tree [x,s1]),y] in R . s2 or [y,(root-tree [x,s1])] in R . s2 ) holds
( s1 <= s2 & y = root-tree [x,s1] ) ) ) ) & ( for o1, o2 being OperSymbol of S
for x1 being Element of Args (o1,(ParsedTermsOSA X))
for x2 being Element of Args (o2,(ParsedTermsOSA X))
for 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) ) ) ) ) ) ) )
let R be ManySortedRelation of (ParsedTermsOSA X); ( R = PTCongruence X iff ( ( for s1, s2 being Element of S
for 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 st ( [(root-tree [x,s1]),y] in R . s2 or [y,(root-tree [x,s1])] in R . s2 ) holds
( s1 <= s2 & y = root-tree [x,s1] ) ) ) ) & ( for o1, o2 being OperSymbol of S
for x1 being Element of Args (o1,(ParsedTermsOSA X))
for x2 being Element of Args (o2,(ParsedTermsOSA X))
for 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) ) ) ) ) ) ) )
set PTA = ParsedTermsOSA X;
set SPTA = the Sorts of (ParsedTermsOSA X);
set D = DTConOSA X;
set OU = [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));
set C = bool [:(TS (DTConOSA X)), the carrier of S:];
set F = PTClasses X;
defpred S1[ ManySortedSet of the carrier of S] means for s1, s2 being Element of S
for 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 st ( [(root-tree [x,s1]),y] in $1 . s2 or [y,(root-tree [x,s1])] in $1 . s2 ) holds
( s1 <= s2 & y = root-tree [x,s1] ) ) );
defpred S2[ ManySortedSet of the carrier of S] means for o1, o2 being OperSymbol of S
for x1 being Element of Args (o1,(ParsedTermsOSA X))
for x2 being Element of Args (o2,(ParsedTermsOSA X))
for 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 being ManySortedRelation of (ParsedTermsOSA X) st S1[R1] & S2[R1] & S1[R2] & S2[R2] holds
R1 = R2
proof
let R1,
R2 be
ManySortedRelation of
(ParsedTermsOSA X);
( S1[R1] & S2[R1] & S1[R2] & S2[R2] implies R1 = R2 )
assume that A2:
S1[
R1]
and A3:
S2[
R1]
and A4:
S1[
R2]
and A5:
S2[
R2]
;
R1 = R2
defpred S3[
set ]
means for
x being
object for
s being
Element of
S holds
(
[$1,x] in R1 . s iff
[$1,x] in R2 . s );
A6:
for
nt being
Symbol of
(DTConOSA X) for
ts being
FinSequence of
TS (DTConOSA X) st
nt ==> roots ts & ( for
t being
DecoratedTree of the
carrier of
(DTConOSA X) st
t in rng ts holds
S3[
t] ) holds
S3[
nt -tree ts]
proof
let nt be
Symbol of
(DTConOSA X);
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConOSA X) st t in rng ts holds
S3[t] ) holds
S3[nt -tree ts]let ts be
FinSequence of
TS (DTConOSA X);
( nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConOSA X) st t in rng ts holds
S3[t] ) implies S3[nt -tree ts] )
assume that A7:
nt ==> roots ts
and A8:
for
t being
DecoratedTree of the
carrier of
(DTConOSA X) st
t in rng ts holds
S3[
t]
;
S3[nt -tree ts]
nt in { s where s is Symbol of (DTConOSA X) : ex n being FinSequence st s ==> n }
by A7;
then reconsider nt1 =
nt as
NonTerminal of
(DTConOSA X) by LANG1:def 3;
reconsider tss =
ts as
SubtreeSeq of
nt1 by A7, DTCONSTR:def 6;
let x be
object ;
for s being Element of S holds
( [(nt -tree ts),x] in R1 . s iff [(nt -tree ts),x] in R2 . s )let s be
Element of
S;
( [(nt -tree ts),x] in R1 . s iff [(nt -tree ts),x] in R2 . s )
A9:
rng ts c= TS (DTConOSA X)
by FINSEQ_1:def 4;
[nt,(roots ts)] in the
Rules of
(DTConOSA X)
by A7, LANG1:def 1;
then reconsider rt =
roots ts as
Element of
([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by ZFMISC_1:87;
reconsider sy =
nt as
Element of
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) ;
[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,
(ParsedTermsOSA X))
and A15:
nt1 -tree tss = (Den (o,(ParsedTermsOSA X))) . ts2
by Th11;
A16: the
Sorts of
(ParsedTermsOSA X) . s =
ParsedTerms (
X,
s)
by Def8
.=
{ a1 where a1 is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being object st
( s1 <= s & x in X . s1 & a1 = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a1 . {} & the_result_sort_of o <= s ) ) }
;
hereby ( [(nt -tree ts),x] in R2 . s implies [(nt -tree ts),x] in R1 . s )
assume A17:
[(nt -tree ts),x] in R1 . s
;
[(nt -tree ts),x] in R2 . sthen
x in the
Sorts of
(ParsedTermsOSA X) . 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 ex
y being
object st
(
s1 <= s &
y in X . s1 &
a1 = root-tree [y,s1] ) or ex
o being
OperSymbol of
S st
(
[o, the carrier of S] = a1 . {} &
the_result_sort_of o <= s ) )
by A16;
for
s1 being
Element of
S for
y being
set holds
( not
s1 <= s or not
y in X . s1 or not
a1 = root-tree [y,s1] )
proof
given s1 being
Element of
S,
y being
set such that
s1 <= s
and A20:
y in X . s1
and A21:
a1 = root-tree [y,s1]
;
contradiction
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
;
verum
end; then consider o1 being
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,
(ParsedTermsOSA X))
and A24:
a1 = (Den (o1,(ParsedTermsOSA X))) . 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,
(ParsedTermsOSA X))
and A27:
nt1 -tree tss = (Den (o,(ParsedTermsOSA X))) . 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,
(ParsedTermsOSA X))
by A26;
reconsider tsa =
ts1 as
Element of
Args (
o1,
(ParsedTermsOSA X))
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)
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;
verum
end;
reconsider tsb =
ts2 as
Element of
Args (
o,
(ParsedTermsOSA X))
by A14;
assume A37:
[(nt -tree ts),x] in R2 . s
;
[(nt -tree ts),x] in R1 . s
then
x in the
Sorts of
(ParsedTermsOSA X) . 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 ex
y being
object st
(
s1 <= s &
y in X . s1 &
a1 = root-tree [y,s1] ) or ex
o being
OperSymbol of
S st
(
[o, the carrier of S] = a1 . {} &
the_result_sort_of o <= s ) )
by A16;
for
s1 being
Element of
S for
y being
set holds
( not
s1 <= s or not
y in X . s1 or not
a1 = root-tree [y,s1] )
proof
given s1 being
Element of
S,
y being
set such that
s1 <= s
and A40:
y in X . s1
and A41:
a1 = root-tree [y,s1]
;
contradiction
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
;
verum
end;
then consider o1 being
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,
(ParsedTermsOSA X))
and A44:
a1 = (Den (o1,(ParsedTermsOSA X))) . 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,
(ParsedTermsOSA X))
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)
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
[(nt -tree ts),x] in R1 . s
by A3, A38, A44, A15, A45, A53, A52, A46, A49;
verum
end;
A54:
for
s being
Symbol of
(DTConOSA X) st
s in Terminals (DTConOSA X) holds
S3[
root-tree s]
proof
let sy be
Symbol of
(DTConOSA X);
( sy in Terminals (DTConOSA X) implies S3[ root-tree sy] )
assume
sy in Terminals (DTConOSA X)
;
S3[ root-tree sy]
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 ;
for s being Element of S holds
( [(root-tree sy),y] in R1 . s iff [(root-tree sy),y] in R2 . s )let s1 be
Element of
S;
( [(root-tree sy),y] in R1 . s1 iff [(root-tree sy),y] in R2 . s1 )
hereby ( [(root-tree sy),y] in R2 . s1 implies [(root-tree sy),y] in R1 . s1 )
assume A57:
[(root-tree sy),y] in R1 . s1
;
[(root-tree sy),y] in R2 . s1then 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;
verum
end;
assume A59:
[(root-tree sy),y] in R2 . s1
;
[(root-tree sy),y] in R1 . s1
then A60:
y = root-tree [x,s]
by A4, A55, A56;
s <= s1
by A4, A55, A56, A59;
hence
[(root-tree sy),y] in R1 . s1
by A2, A55, A56, A60;
verum
end;
A61:
for
t being
DecoratedTree of the
carrier of
(DTConOSA X) st
t in TS (DTConOSA X) holds
S3[
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 ;
( i in the carrier of S implies R1 . i = R2 . i )
assume
i in the
carrier of
S
;
R1 . i = R2 . i
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 ;
( [a,b] in R1 . s iff [a,b] in R2 . s )
A62: the
Sorts of
(ParsedTermsOSA X) . s =
ParsedTerms (
X,
s)
by Def8
.=
{ a1 where a1 is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being object st
( s1 <= s & x in X . s1 & a1 = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a1 . {} & the_result_sort_of o <= s ) ) }
;
hereby ( [a,b] in R2 . s implies [a,b] in R1 . s )
end;
assume A64:
[a,b] in R2 . s
;
[a,b] in R1 . s
then
a in the
Sorts of
(ParsedTermsOSA X) . s
by ZFMISC_1:87;
then
ex
a1 being
Element of
TS (DTConOSA X) st
(
a = a1 & ( ex
s1 being
Element of
S ex
x being
object st
(
s1 <= s &
x in X . s1 &
a1 = root-tree [x,s1] ) or ex
o being
OperSymbol of
S st
(
[o, the carrier of S] = a1 . {} &
the_result_sort_of o <= s ) ) )
by A62;
hence
[a,b] in R1 . s
by A61, A64;
verum
end;
hence
R1 . i = R2 . i
by RELAT_1:def 2;
verum
end;
hence
R1 = R2
;
verum
end;
A65:
S2[ PTCongruence X]
proof
let o1,
o2 be
OperSymbol of
S;
for x1 being Element of Args (o1,(ParsedTermsOSA X))
for x2 being Element of Args (o2,(ParsedTermsOSA X))
for s3 being Element of S holds
( [((Den (o1,(ParsedTermsOSA X))) . x1),((Den (o2,(ParsedTermsOSA X))) . x2)] in (PTCongruence X) . 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 (PTCongruence X) . (w3 /. y) ) ) ) )let x1 be
Element of
Args (
o1,
(ParsedTermsOSA X));
for x2 being Element of Args (o2,(ParsedTermsOSA X))
for s3 being Element of S holds
( [((Den (o1,(ParsedTermsOSA X))) . x1),((Den (o2,(ParsedTermsOSA X))) . x2)] in (PTCongruence X) . 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 (PTCongruence X) . (w3 /. y) ) ) ) )let x2 be
Element of
Args (
o2,
(ParsedTermsOSA X));
for s3 being Element of S holds
( [((Den (o1,(ParsedTermsOSA X))) . x1),((Den (o2,(ParsedTermsOSA X))) . x2)] in (PTCongruence X) . 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 (PTCongruence X) . (w3 /. y) ) ) ) )let s3 be
Element of
S;
( [((Den (o1,(ParsedTermsOSA X))) . x1),((Den (o2,(ParsedTermsOSA X))) . x2)] in (PTCongruence X) . 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 (PTCongruence X) . (w3 /. y) ) ) ) )
A66:
dom (the_arity_of o2) = dom x2
by MSUALG_3:6;
A67:
(PTCongruence X) . s3 = { [x3,y] where x3, y is Element of TS (DTConOSA X) : [x3,s3] in (PTClasses X) . y }
by Def22;
reconsider ts2 =
x2 as
FinSequence of
TS (DTConOSA X) by Th13;
A68:
dom (the_arity_of o1) = dom x1
by MSUALG_3:6;
reconsider ts1 =
x1 as
FinSequence of
TS (DTConOSA X) by Th13;
A69:
rng ts1 c= TS (DTConOSA X)
by FINSEQ_1:def 4;
reconsider x =
(PTClasses X) * ts1 as
FinSequence of
bool [:(TS (DTConOSA X)), the carrier of S:] ;
dom (PTClasses X) = TS (DTConOSA X)
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:
(PTClasses X) . ((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 (DTConOSA X) by A72, Th12;
A75:
(Den (o2,(ParsedTermsOSA X))) . 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,(ParsedTermsOSA X))) . 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 (DTConOSA X)
by FINSEQ_1:def 4;
hereby ( 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 (PTCongruence X) . (w3 /. y) ) ) implies [((Den (o1,(ParsedTermsOSA X))) . x1),((Den (o2,(ParsedTermsOSA X))) . x2)] in (PTCongruence X) . s3 )
assume
[((Den (o1,(ParsedTermsOSA X))) . x1),((Den (o2,(ParsedTermsOSA X))) . x2)] in (PTCongruence X) . s3
;
( 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 (PTCongruence X) . (w3 /. y) ) ) )then consider t1,
t2 being
Element of
TS (DTConOSA X) such that A78:
[((Den (o1,(ParsedTermsOSA X))) . x1),((Den (o2,(ParsedTermsOSA X))) . x2)] = [t1,t2]
and A79:
[t1,s3] in (PTClasses X) . t2
by A67;
A80:
(Den (o1,(ParsedTermsOSA X))) . x1 = t1
by A78, XTUPLE_0:1;
A81:
(Den (o2,(ParsedTermsOSA X))) . x2 = t2
by A78, XTUPLE_0:1;
[t2,s3] in (PTClasses X) . 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,(ParsedTermsOSA X))) . 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 (DTConOSA X) by Th13;
A91:
OSSym (
o3,
X)
==> roots x3
by Th13;
A92:
t2 = (Den (o3,(ParsedTermsOSA X))) . x3
by A82, XTUPLE_0:1;
A93:
(Den (o3,(ParsedTermsOSA X))) . 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;
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 (PTCongruence X) . (w3 /. y) ) )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 =
w3;
( dom w3 = dom x1 & ( for y being Nat st y in dom w3 holds
[(x1 . y),(x2 . y)] in (PTCongruence X) . (w3 /. y) ) )thus
dom w3 = dom x1
by A70, A95, FINSEQ_3:29;
for y being Nat st y in dom w3 holds
[(x1 . y),(x2 . y)] in (PTCongruence X) . (w3 /. y)let y be
Nat;
( y in dom w3 implies [(x1 . y),(x2 . y)] in (PTCongruence X) . (w3 /. y) )assume A97:
y in dom w3
;
[(x1 . y),(x2 . y)] in (PTCongruence X) . (w3 /. y)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 (DTConOSA X) by A69, A77, A98;
[(x3 . y),(w3 /. y)] in x . y
by A95, A96, A97;
then
[(ts2 . y),(w3 /. y)] in (PTClasses X) . (ts1 . y)
by A99, A95, A97, FUNCT_1:12;
then A100:
[t11,(w3 /. y)] in (PTClasses X) . t22
by Th19;
(PTCongruence X) . (w3 /. y) = { [x5,y5] where x5, y5 is Element of TS (DTConOSA X) : [x5,(w3 /. y)] in (PTClasses X) . y5 }
by Def22;
hence
[(x1 . y),(x2 . y)] in (PTCongruence X) . (w3 /. y)
by A100;
verum
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 (PTCongruence X) . (w3 /. y) ) )
;
[((Den (o1,(ParsedTermsOSA X))) . x1),((Den (o2,(ParsedTermsOSA X))) . x2)] in (PTCongruence X) . s3
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 (PTCongruence X) . (w3 /. y)
by A105;
for
y being
Nat st
y in dom x holds
[(x2 . y),(w3 /. y)] in x . y
proof
let y be
Nat;
( y in dom x implies [(x2 . y),(w3 /. y)] in x . y )
assume A108:
y in dom x
;
[(x2 . y),(w3 /. y)] in x . y
A109:
(PTCongruence X) . (w3 /. y) = { [x5,y5] where x5, y5 is Element of TS (DTConOSA X) : [x5,(w3 /. y)] in (PTClasses X) . y5 }
by Def22;
[(x1 . y),(x2 . y)] in (PTCongruence X) . (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 (PTClasses X) . 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 (PTClasses X) . x5
by A111, Th19;
hence
[(x2 . y),(w3 /. y)] in x . y
by A108, A112, A113, FUNCT_1:12;
verum
end;
then
[((Den (o2,(ParsedTermsOSA X))) . x2),s3] in (PTClasses X) . ((OSSym (o1,X)) -tree ts1)
by A71, A73, A101, A102, A103, A104, A106;
then
[tx,s3] in (PTClasses X) . ty
by A75, Th19;
hence
[((Den (o1,(ParsedTermsOSA X))) . x1),((Den (o2,(ParsedTermsOSA X))) . x2)] in (PTCongruence X) . s3
by A67, A76, A75;
verum
end;
S1[ PTCongruence X]
proof
let s1,
s2 be
Element of
S;
for x being object st x in X . s1 holds
( ( s1 <= s2 implies [(root-tree [x,s1]),(root-tree [x,s1])] in (PTCongruence X) . s2 ) & ( for y being object st ( [(root-tree [x,s1]),y] in (PTCongruence X) . s2 or [y,(root-tree [x,s1])] in (PTCongruence X) . s2 ) holds
( s1 <= s2 & y = root-tree [x,s1] ) ) )let x be
object ;
( x in X . s1 implies ( ( s1 <= s2 implies [(root-tree [x,s1]),(root-tree [x,s1])] in (PTCongruence X) . s2 ) & ( for y being object st ( [(root-tree [x,s1]),y] in (PTCongruence X) . s2 or [y,(root-tree [x,s1])] in (PTCongruence X) . s2 ) holds
( s1 <= s2 & y = root-tree [x,s1] ) ) ) )
assume A114:
x in X . s1
;
( ( s1 <= s2 implies [(root-tree [x,s1]),(root-tree [x,s1])] in (PTCongruence X) . s2 ) & ( for y being object st ( [(root-tree [x,s1]),y] in (PTCongruence X) . s2 or [y,(root-tree [x,s1])] in (PTCongruence X) . s2 ) holds
( s1 <= s2 & y = root-tree [x,s1] ) ) )
reconsider sy =
[x,s1] as
Terminal of
(DTConOSA X) by A114, Th4;
A115:
(PTCongruence X) . s2 = { [x1,y] where x1, y is Element of TS (DTConOSA X) : [x1,s2] in (PTClasses X) . y }
by Def22;
A116:
root-tree [x,s1] in the
Sorts of
(ParsedTermsOSA X) . s1
by A114, Th10;
hereby for y being object st ( [(root-tree [x,s1]),y] in (PTCongruence X) . s2 or [y,(root-tree [x,s1])] in (PTCongruence X) . s2 ) holds
( s1 <= s2 & y = root-tree [x,s1] )
assume A117:
s1 <= s2
;
[(root-tree [x,s1]),(root-tree [x,s1])] in (PTCongruence X) . s2
[(root-tree sy),s1] in (PTClasses X) . (root-tree sy)
by A116, Th19;
then
[(root-tree sy),s2] in (PTClasses X) . (root-tree sy)
by A116, A117, Th21;
hence
[(root-tree [x,s1]),(root-tree [x,s1])] in (PTCongruence X) . s2
by A115;
verum
end;
let y be
object ;
( ( [(root-tree [x,s1]),y] in (PTCongruence X) . s2 or [y,(root-tree [x,s1])] in (PTCongruence X) . s2 ) implies ( s1 <= s2 & y = root-tree [x,s1] ) )
assume A118:
(
[(root-tree [x,s1]),y] in (PTCongruence X) . s2 or
[y,(root-tree [x,s1])] in (PTCongruence X) . s2 )
;
( s1 <= s2 & y = root-tree [x,s1] )
then A119:
root-tree [x,s1] in the
Sorts of
(ParsedTermsOSA X) . s2
by ZFMISC_1:87;
field ((PTCongruence X) . s2) = the
Sorts of
(ParsedTermsOSA X) . s2
by ORDERS_1:12;
then A120:
(PTCongruence X) . s2 is_symmetric_in the
Sorts of
(ParsedTermsOSA X) . s2
by RELAT_2:def 11;
A121:
(PTClasses X) . (root-tree sy) =
@ sy
by Def21
.=
{ [(root-tree sy),s3] where s3 is Element of S : ex s4 being Element of S ex x being set st
( x in X . s4 & sy = [x,s4] & s4 <= s3 ) }
;
y in the
Sorts of
(ParsedTermsOSA X) . s2
by A118, ZFMISC_1:87;
then
[y,(root-tree sy)] in (PTCongruence X) . s2
by A120, A118, A119, RELAT_2:def 3;
then consider y1,
r1 being
Element of
TS (DTConOSA X) such that A122:
[y,(root-tree sy)] = [y1,r1]
and A123:
[y1,s2] in (PTClasses X) . 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 being
Element of
S ex
x being
set st
(
x in X . s4 &
sy = [x,s4] &
s4 <= s3 )
by A121, A123;
s2 = s3
by A125, XTUPLE_0:1;
hence
(
s1 <= s2 &
y = root-tree [x,s1] )
by A124, A125, A126, XTUPLE_0:1;
verum
end;
hence
( R = PTCongruence X iff ( ( for s1, s2 being Element of S
for 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 st ( [(root-tree [x,s1]),y] in R . s2 or [y,(root-tree [x,s1])] in R . s2 ) holds
( s1 <= s2 & y = root-tree [x,s1] ) ) ) ) & ( for o1, o2 being OperSymbol of S
for x1 being Element of Args (o1,(ParsedTermsOSA X))
for x2 being Element of Args (o2,(ParsedTermsOSA X))
for 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) ) ) ) ) ) ) )
by A1, A65; verum