let S be locally_directed OrderSortedSign; :: thesis:
let X be V5() ManySortedSet of ; :: thesis:
let R be ManySortedRelation of (ParsedTermsOSA X); :: thesis:
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 S₁[ ManySortedSet of ] means for s1, s2 being Element of S
for x being set st x in X . s1 holds
( ( s1 <= s2 implies [(root-tree [x,s1]),(root-tree [x,s1])] in $1 . s2 ) & ( for y being set 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 S₂[ ManySortedSet of ] 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) ) ) ) );
A1: for R1, R2 being ManySortedRelation of (ParsedTermsOSA X) st S₁[R1] & S₂[R1] & S₁[R2] & S₂[R2] holds
R1 = R2

proof

let R1, R2 be ManySortedRelation of (ParsedTermsOSA X); :: thesis:
assume that
A2: ( S₁[R1] & S₂[R1] ) and
A3: ( S₁[R2] & S₂[R2] ) ; :: thesis:
defpred S₃[ set ] means for x being set
for s being Element of S holds
( [$1,x] in R1 . s iff [$1,x] in R2 . s );
A4: for s being Symbol of (DTConOSA X) st s in Terminals (DTConOSA X) holds
S₃[ root-tree s]

proof

let sy be Symbol of (DTConOSA X); :: thesis:
assume A5: sy in Terminals (DTConOSA X) ; :: thesis:
consider s being Element of S, x being set such that
A6: ( x in X . s & sy = [x,s] ) by A5, Th4;
let y be set ; :: thesis:
let s1 be Element of S; :: thesis:

hereby :: thesis:

assume [(root-tree sy),y] in R1 . s1 ; :: thesis:
then ( s <= s1 & y = root-tree [x,s] ) by A2, A6;
hence [(root-tree sy),y] in R2 . s1 by A3, A6; :: thesis:

end;

assume [(root-tree sy),y] in R2 . s1 ; :: thesis:
then ( s <= s1 & y = root-tree [x,s] ) by A3, A6;
hence [(root-tree sy),y] in R1 . s1 by A2, A6; :: thesis:

end;

A7: for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts & ( for t being DecoratedTree of st t in rng ts holds
S₃[t] ) holds
S₃[nt -tree ts]

proof

let nt be Symbol of (DTConOSA X); :: thesis:
let ts be FinSequence of TS (DTConOSA X); :: thesis:
assume that
A8: nt ==> roots ts and
A9: for t being DecoratedTree of st t in rng ts holds
S₃[t] ; :: thesis:
nt in { s where s is Symbol of (DTConOSA X) : ex n being FinSequence st s ==> n } by A8;
then reconsider nt1 = nt as NonTerminal of (DTConOSA X) by LANG1:def 3;
reconsider tss = ts as SubtreeSeq of nt1 by A8, DTCONSTR:def 9;
let x be set ; :: thesis:
let s be Element of S; :: thesis:
A10: 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 set 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 ) ) } ;
A11: [nt,(roots ts)] in the Rules of (DTConOSA X) by A8, LANG1:def 1;
reconsider sy = nt as Element of [:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X)) ;
reconsider rt = roots ts as Element of ([:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X))) * by A11, ZFMISC_1:106;
[sy,rt] in OSREL X by A8, 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
A12: sy = [o,x2] by DOMAIN_1:9;
A13: x2 = the carrier of S by TARSKI:def 1;
then A14: (nt -tree tss) . {} = [o,the carrier of S] by A12, TREES_4:def 4;
A15: rng ts c= TS (DTConOSA X) by FINSEQ_1:def 4;

hereby :: thesis:

assume A16: [(nt -tree ts),x] in R1 . s ; :: thesis:
then ( nt -tree ts in the Sorts of (ParsedTermsOSA X) . s & x in the Sorts of (ParsedTermsOSA X) . s ) by ZFMISC_1:106;
then consider a1 being Element of TS (DTConOSA X) such that
A17: x = a1 and
A18: ( ex s1 being Element of S ex y being set 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 A10;
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 A19: ( s1 <= s & y in X . s1 & a1 = root-tree [y,s1] ) ; :: thesis:
nt -tree ts = root-tree [y,s1] by A2, A16, A17, A19;
then ( [y,s1] = nt & ts = {} ) by TREES_4:17;
then the carrier of S = s1 by A12, A13, ZFMISC_1:33;
then s1 in s1 ;
hence contradiction ; :: thesis:

end;

then consider o1 being OperSymbol of S such that
A20: ( [o1,the carrier of S] = a1 . {} & the_result_sort_of o1 <= s ) by A18;
consider ts1 being SubtreeSeq of OSSym o1,X such that
A21: ( a1 = (OSSym o1,X) -tree ts1 & OSSym o1,X ==> roots ts1 & ts1 in Args o1,(ParsedTermsOSA X) & a1 = (Den o1,(ParsedTermsOSA X)) . ts1 ) by A20, Th11;
consider ts2 being SubtreeSeq of OSSym o,X such that
A22: ( nt1 -tree tss = (OSSym o,X) -tree ts2 & OSSym o,X ==> roots ts2 & ts2 in Args o,(ParsedTermsOSA X) & nt1 -tree tss = (Den o,(ParsedTermsOSA X)) . ts2 ) by A14, Th11;
A23: ts2 = tss by A22, TREES_4:15;
reconsider tsa = ts1 as Element of Args o1,(ParsedTermsOSA X) by A21;
reconsider tsb = ts2 as Element of Args o,(ParsedTermsOSA X) by A22;
A24: ( o ~= o1 & len (the_arity_of o) = len (the_arity_of o1) & the_result_sort_of o <= s & the_result_sort_of o1 <= s & ex w3 being Element of the carrier of S * st
( dom w3 = dom tsb & ( for y being Nat st y in dom w3 holds
[(tsb . y),(tsa . y)] in R1 . (w3 /. y) ) ) ) by A2, A16, A17, A21, A22;
consider w3 being Element of the carrier of S * such that
A25: ( dom w3 = dom tsb & ( for y being Nat st y in dom w3 holds
[(tsb . y),(tsa . y)] in R1 . (w3 /. y) ) ) by A2, A16, A17, A21, A22;
for y being Nat st y in dom w3 holds
[(tsb . y),(tsa . y)] in R2 . (w3 /. y)

proof

let y be Nat; :: thesis:
assume A26: y in dom w3 ; :: thesis:
A27: tsb . y in rng ts by A23, A25, A26, FUNCT_1:12;
then reconsider t = tsb . y as Element of TS (DTConOSA X) by A15;
[t,(tsa . y)] in R1 . (w3 /. y) by A25, A26;
hence [(tsb . y),(tsa . y)] in R2 . (w3 /. y) by A9, A27; :: thesis:

end;

hence [(nt -tree ts),x] in R2 . s by A3, A17, A21, A22, A24, A25; :: thesis:

end;

assume A28: [(nt -tree ts),x] in R2 . s ; :: thesis:
then ( nt -tree ts in the Sorts of (ParsedTermsOSA X) . s & x in the Sorts of (ParsedTermsOSA X) . s ) by ZFMISC_1:106;
then consider a1 being Element of TS (DTConOSA X) such that
A29: x = a1 and
A30: ( ex s1 being Element of S ex y being set 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 A10;
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 A31: ( s1 <= s & y in X . s1 & a1 = root-tree [y,s1] ) ; :: thesis:
nt -tree ts = root-tree [y,s1] by A3, A28, A29, A31;
then ( [y,s1] = nt & ts = {} ) by TREES_4:17;
then the carrier of S = s1 by A12, A13, ZFMISC_1:33;
then s1 in s1 ;
hence contradiction ; :: thesis:

end;

then consider o1 being OperSymbol of S such that
A32: ( [o1,the carrier of S] = a1 . {} & the_result_sort_of o1 <= s ) by A30;
consider ts1 being SubtreeSeq of OSSym o1,X such that
A33: ( a1 = (OSSym o1,X) -tree ts1 & OSSym o1,X ==> roots ts1 & ts1 in Args o1,(ParsedTermsOSA X) & a1 = (Den o1,(ParsedTermsOSA X)) . ts1 ) by A32, Th11;
consider ts2 being SubtreeSeq of OSSym o,X such that
A34: ( nt1 -tree tss = (OSSym o,X) -tree ts2 & OSSym o,X ==> roots ts2 & ts2 in Args o,(ParsedTermsOSA X) & nt1 -tree tss = (Den o,(ParsedTermsOSA X)) . ts2 ) by A14, Th11;
A35: ts2 = tss by A34, TREES_4:15;
reconsider tsa = ts1 as Element of Args o1,(ParsedTermsOSA X) by A33;
reconsider tsb = ts2 as Element of Args o,(ParsedTermsOSA X) by A34;
A36: ( o ~= o1 & len (the_arity_of o) = len (the_arity_of o1) & the_result_sort_of o <= s & the_result_sort_of o1 <= s & ex w3 being Element of the carrier of S * st
( dom w3 = dom tsb & ( for y being Nat st y in dom w3 holds
[(tsb . y),(tsa . y)] in R2 . (w3 /. y) ) ) ) by A3, A28, A29, A33, A34;
consider w3 being Element of the carrier of S * such that
A37: ( dom w3 = dom tsb & ( for y being Nat st y in dom w3 holds
[(tsb . y),(tsa . y)] in R2 . (w3 /. y) ) ) by A3, A28, A29, A33, A34;
for y being Nat st y in dom w3 holds
[(tsb . y),(tsa . y)] in R1 . (w3 /. y)

proof

let y be Nat; :: thesis:
assume A38: y in dom w3 ; :: thesis:
A39: tsb . y in rng ts by A35, A37, A38, FUNCT_1:12;
then reconsider t = tsb . y as Element of TS (DTConOSA X) by A15;
[t,(tsa . y)] in R2 . (w3 /. y) by A37, A38;
hence [(tsb . y),(tsa . y)] in R1 . (w3 /. y) by A9, A39; :: thesis:

end;

hence [(nt -tree ts),x] in R1 . s by A2, A29, A33, A34, A36, A37; :: thesis:

end;

A40: for t being DecoratedTree of st t in TS (DTConOSA X) holds
S₃[t] from DTCONSTR:sch 7(A4, A7);
for i being set st i in the carrier of S holds
R1 . i = R2 . i

proof

let i be set ; :: thesis:
assume A41: i in the carrier of S ; :: thesis:
reconsider s = i as Element of S by A41;
for a, b being set holds
( [a,b] in R1 . s iff [a,b] in R2 . s )

proof

let a, b be set ; :: thesis:
A42: 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 set 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 :: thesis:

assume A43: [a,b] in R1 . s ; :: thesis:
then ( a in the Sorts of (ParsedTermsOSA X) . s & b in the Sorts of (ParsedTermsOSA X) . s ) by ZFMISC_1:106;
then consider a1 being Element of TS (DTConOSA X) such that
A44: a = a1 and
( ex s1 being Element of S ex x being set 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 A42;
thus [a,b] in R2 . s by A40, A43, A44; :: thesis:

end;

assume A45: [a,b] in R2 . s ; :: thesis:
then ( a in the Sorts of (ParsedTermsOSA X) . s & b in the Sorts of (ParsedTermsOSA X) . s ) by ZFMISC_1:106;
then consider a1 being Element of TS (DTConOSA X) such that
A46: a = a1 and
( ex s1 being Element of S ex x being set 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 A42;
thus [a,b] in R1 . s by A40, A45, A46; :: thesis:

end;

hence R1 . i = R2 . i by RELAT_1:def 2; :: thesis:

end;

hence R1 = R2 by PBOOLE:3; :: thesis:

end;

set P = PTCongruence X;
A47: S₁[ PTCongruence X]

proof

let s1, s2 be Element of S; :: thesis:
let x be set ; :: thesis:
assume A48: x in X . s1 ; :: thesis:
A49: (PTCongruence X) . s2 = { [x1,y] where x1, y is Element of TS (DTConOSA X) : [x1,s2] in (PTClasses X) . y } by Def23;
reconsider sy = [x,s1] as Terminal of (DTConOSA X) by A48, Th4;
A50: root-tree [x,s1] in the Sorts of (ParsedTermsOSA X) . s1 by A48, Th10;
A51: (PTClasses X) . (root-tree sy) = @ sy by Def22
.= { [(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 ) } ;

hereby :: thesis:

assume A52: s1 <= s2 ; :: thesis:
[(root-tree sy),s1] in (PTClasses X) . (root-tree sy) by A50, Th20;
then [(root-tree sy),s2] in (PTClasses X) . (root-tree sy) by A50, A52, Th22;
hence [(root-tree [x,s1]),(root-tree [x,s1])] in (PTCongruence X) . s2 by A49; :: thesis:

end;

field ((PTCongruence X) . s2) = the Sorts of (ParsedTermsOSA X) . s2 by ORDERS_1:97;
then A53: (PTCongruence X) . s2 is_symmetric_in the Sorts of (ParsedTermsOSA X) . s2 by RELAT_2:def 11;
let y be set ; :: thesis:
assume A54: ( [(root-tree [x,s1]),y] in (PTCongruence X) . s2 or [y,(root-tree [x,s1])] in (PTCongruence X) . s2 ) ; :: thesis:
then ( y in the Sorts of (ParsedTermsOSA X) . s2 & root-tree [x,s1] in the Sorts of (ParsedTermsOSA X) . s2 ) by ZFMISC_1:106;
then [y,(root-tree sy)] in (PTCongruence X) . s2 by A53, A54, RELAT_2:def 3;
then consider y1, r1 being Element of TS (DTConOSA X) such that
A55: [y,(root-tree sy)] = [y1,r1] and
A56: [y1,s2] in (PTClasses X) . r1 by A49;
A57: ( y = y1 & root-tree sy = r1 ) by A55, ZFMISC_1:33;
then consider s3 being Element of S such that
A58: [y1,s2] = [(root-tree sy),s3] and
A59: ex s4 being Element of S ex x being set st
( x in X . s4 & sy = [x,s4] & s4 <= s3 ) by A51, A56;
consider s4 being Element of S, x being set such that
A60: ( x in X . s4 & sy = [x,s4] & s4 <= s3 ) by A59;
( y = root-tree sy & s2 = s3 ) by A57, A58, ZFMISC_1:33;
hence ( s1 <= s2 & y = root-tree [x,s1] ) by A60, ZFMISC_1:33; :: thesis:

end;

S₂[ PTCongruence X]

proof

let o1, o2 be OperSymbol of S; :: thesis:
let x1 be Element of Args o1,(ParsedTermsOSA X); :: thesis:
let x2 be Element of Args o2,(ParsedTermsOSA X); :: thesis:
let s3 be Element of S; :: thesis:
A61: (PTCongruence X) . s3 = { [x3,y] where x3, y is Element of TS (DTConOSA X) : [x3,s3] in (PTClasses X) . y } by Def23;
A62: ( x1 is FinSequence of TS (DTConOSA X) & OSSym o1,X ==> roots x1 ) by Th13;
reconsider ts1 = x1 as FinSequence of TS (DTConOSA X) by Th13;
A63: (Den o1,(ParsedTermsOSA X)) . x1 = ((PTOper X) . o1) . x1 by MSUALG_1:def 11
.= (PTDenOp o1,X) . ts1 by Def10
.= (OSSym o1,X) -tree ts1 by A62, Def9 ;
A64: ( x2 is FinSequence of TS (DTConOSA X) & OSSym o2,X ==> roots x2 ) by Th13;
reconsider ts2 = x2 as FinSequence of TS (DTConOSA X) by Th13;
A65: (Den o2,(ParsedTermsOSA X)) . x2 = ((PTOper X) . o2) . x2 by MSUALG_1:def 11
.= (PTDenOp o2,X) . ts2 by Def10
.= (OSSym o2,X) -tree ts2 by A64, Def9 ;
reconsider x = (PTClasses X) * ts1, y = (PTClasses X) * ts2 as FinSequence of bool [:(TS (DTConOSA X)),the carrier of S:] ;
A66: ( rng ts1 c= TS (DTConOSA X) & rng ts2 c= TS (DTConOSA X) & dom (PTClasses X) = TS (DTConOSA X) ) by FINSEQ_1:def 4, FUNCT_2:def 1;
then A67: ( len x = len ts1 & len y = len ts2 ) by FINSEQ_2:33;
then A68: ( dom x = dom ts1 & dom y = dom ts2 ) by FINSEQ_3:31;
A69: (PTClasses X) . ((OSSym o1,X) -tree ts1) = @ (OSSym o1,X),x by A62, Def22
.= { [((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 ) ) ) } ;
A70: ( dom (the_arity_of o1) = dom x1 & dom (the_arity_of o2) = dom x2 ) by MSUALG_3:6;
reconsider tx = (OSSym o1,X) -tree ts1, ty = (OSSym o2,X) -tree ts2 as Element of TS (DTConOSA X) by A62, A64, Th12;

hereby :: thesis:

assume [((Den o1,(ParsedTermsOSA X)) . x1),((Den o2,(ParsedTermsOSA X)) . x2)] in (PTCongruence X) . s3 ; :: thesis:
then consider t1, t2 being Element of TS (DTConOSA X) such that
A71: [((Den o1,(ParsedTermsOSA X)) . x1),((Den o2,(ParsedTermsOSA X)) . x2)] = [t1,t2] and
A72: [t1,s3] in (PTClasses X) . t2 by A61;
A73: ( (Den o1,(ParsedTermsOSA X)) . x1 = t1 & (Den o2,(ParsedTermsOSA X)) . x2 = t2 ) by A71, ZFMISC_1:33;
[t2,s3] in (PTClasses X) . t1 by A72, Th20;
then consider o3 being OperSymbol of S, x3 being Element of Args o3,(ParsedTermsOSA X), s4 being Element of S such that
A74: [t2,s3] = [((Den o3,(ParsedTermsOSA X)) . x3),s4] and
A75: 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
A76: 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 A63, A69, A73;
consider o4 being OperSymbol of S such that
A77: ( 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 ) by A75;
A78: ( o1 = o4 & t2 = (Den o3,(ParsedTermsOSA X)) . x3 & s3 = s4 ) by A74, A77, ZFMISC_1:33;
A79: ( x3 is FinSequence of TS (DTConOSA X) & OSSym o3,X ==> roots x3 ) by Th13;
reconsider ts3 = x3 as FinSequence of TS (DTConOSA X) by Th13;
(Den o3,(ParsedTermsOSA X)) . x3 = ((PTOper X) . o3) . x3 by MSUALG_1:def 11
.= (PTDenOp o3,X) . ts3 by Def10
.= (OSSym o3,X) -tree ts3 by A79, Def9 ;
then A80: ( OSSym o3,X = OSSym o2,X & ts3 = ts2 ) by A65, A73, A78, TREES_4:15;
then A81: ( o3 = o2 & x3 = x2 ) by ZFMISC_1:33;
thus ( 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 A77, A78, A80, ZFMISC_1:33; :: thesis:
A82: dom (the_arity_of o1) = dom (the_arity_of o2) by A77, A78, A81, FINSEQ_3:31;
consider w3 being Element of the carrier of S * such that
A83: dom w3 = dom x and
A84: for y being Nat st y in dom x holds
[(x3 . y),(w3 /. y)] in x . y by A76;
take w3 = w3; :: thesis:
thus dom w3 = dom x1 by A67, A83, FINSEQ_3:31; :: thesis:
let y be Nat; :: thesis:
assume A85: y in dom w3 ; :: thesis:
A86: (PTCongruence X) . (w3 /. y) = { [x5,y5] where x5, y5 is Element of TS (DTConOSA X) : [x5,(w3 /. y)] in (PTClasses X) . y5 } by Def23;
( ts1 . y in rng ts1 & ts2 . y in rng ts2 ) by A68, A70, A82, A83, A85, FUNCT_1:12;
then reconsider t22 = ts2 . y, t11 = ts1 . y as Element of TS (DTConOSA X) by A66;
[(x3 . y),(w3 /. y)] in x . y by A83, A84, A85;
then [(ts2 . y),(w3 /. y)] in (PTClasses X) . (ts1 . y) by A80, A83, A85, FUNCT_1:22;
then [t11,(w3 /. y)] in (PTClasses X) . t22 by Th20;
hence [(x1 . y),(x2 . y)] in (PTCongruence X) . (w3 /. y) by A86; :: thesis:

end;

assume A87: ( 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) ) ) ) ; :: thesis:
then consider w3 being Element of the carrier of S * such that
A88: dom w3 = dom x1 and
A89: for y being Nat st y in dom w3 holds
[(x1 . y),(x2 . y)] in (PTCongruence X) . (w3 /. y) ;
for y being Nat st y in dom x holds
[(x2 . y),(w3 /. y)] in x . y

proof

let y be Nat; :: thesis:
assume A90: y in dom x ; :: thesis:
A91: (PTCongruence X) . (w3 /. y) = { [x5,y5] where x5, y5 is Element of TS (DTConOSA X) : [x5,(w3 /. y)] in (PTClasses X) . y5 } by Def23;
[(x1 . y),(x2 . y)] in (PTCongruence X) . (w3 /. y) by A68, A88, A89, A90;
then consider x5, y5 being Element of TS (DTConOSA X) such that
A92: [(x1 . y),(x2 . y)] = [x5,y5] and
A93: [x5,(w3 /. y)] in (PTClasses X) . y5 by A91;
A94: ( x1 . y = x5 & x2 . y = y5 ) by A92, ZFMISC_1:33;
[y5,(w3 /. y)] in (PTClasses X) . x5 by A93, Th20;
hence [(x2 . y),(w3 /. y)] in x . y by A90, A94, FUNCT_1:22; :: thesis:

end;

then [((Den o2,(ParsedTermsOSA X)) . x2),s3] in (PTClasses X) . ((OSSym o1,X) -tree ts1) by A68, A69, A87, A88;
then [tx,s3] in (PTClasses X) . ty by A65, Th20;
hence [((Den o1,(ParsedTermsOSA X)) . x1),((Den o2,(ParsedTermsOSA X)) . x2)] in (PTCongruence X) . s3 by A61, A63, A65; :: thesis:

end;

hence ( R = PTCongruence X iff ( ( for s1, s2 being Element of S
for x being set st x in X . s1 holds
( ( s1 <= s2 implies [(root-tree [x,s1]),(root-tree [x,s1])] in R . s2 ) & ( for y being set 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, A47; :: thesis: