let S be monotone regular locally_directed OrderSortedSign; :: thesis: for X being V5 ManySortedSet of S
for 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
for x being set st x in X . s & t = root-tree [x,s] holds
(PTMin X) . t = t ) & ( for o being OperSymbol of S
for 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) ) ) )
let X be V5 ManySortedSet of S; :: thesis: for 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
for x being set st x in X . s & t = root-tree [x,s] holds
(PTMin X) . t = t ) & ( for o being OperSymbol of S
for 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) ) ) )
let t be Element of TS (DTConOSA X); :: thesis: ( (PTMin X) . t in OSClass (PTCongruence X),t & LeastSort ((PTMin X) . t) <= LeastSort t & ( for s being Element of S
for x being set st x in X . s & t = root-tree [x,s] holds
(PTMin X) . t = t ) & ( for o being OperSymbol of S
for 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) ) ) )
set PTA = ParsedTermsOSA X;
set D = DTConOSA X;
set R = PTCongruence X;
set SPTA = the Sorts of (ParsedTermsOSA X);
set M = PTMin X;
set F = PTClasses X;
defpred S1[ Element of TS (DTConOSA X)] means (PTMin X) . $1 in OSClass (PTCongruence X),$1;
defpred S2[ Element of TS (DTConOSA X)] means LeastSort ((PTMin X) . $1) <= LeastSort $1;
defpred S3[ Element of TS (DTConOSA X)] means for s being Element of S
for x being set st x in X . s & $1 = root-tree [x,s] holds
(PTMin X) . $1 = $1;
defpred S4[ Element of TS (DTConOSA X)] means for o being OperSymbol of S
for 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 S5[ DecoratedTree of the carrier of (DTConOSA X)] means ex t1 being Element of TS (DTConOSA X) st
( t1 = $1 & S1[t1] & S2[t1] & S3[t1] & S4[t1] );
A1:
for s being Symbol of (DTConOSA X) st s in Terminals (DTConOSA X) holds
S5[ root-tree s]
proof
let sy be
Symbol of
(DTConOSA X);
:: thesis: ( sy in Terminals (DTConOSA X) implies S5[ root-tree sy] )
assume A2:
sy in Terminals (DTConOSA X)
;
:: thesis: S5[ root-tree sy]
reconsider t1 =
root-tree sy as
Element of
TS (DTConOSA X) by A2, DTCONSTR:def 4;
take
t1
;
:: thesis: ( t1 = root-tree sy & S1[t1] & S2[t1] & S3[t1] & S4[t1] )
thus
t1 = root-tree sy
;
:: thesis: ( S1[t1] & S2[t1] & S3[t1] & S4[t1] )
consider s being
Element of
S,
x being
set such that A3:
(
x in X . s &
sy = [x,s] )
by A2, Th4;
A4:
(PTMin X) . (root-tree sy) =
pi sy
by A2, Def32
.=
root-tree sy
by A2, Def17
;
hence
(PTMin X) . t1 in OSClass (PTCongruence X),
t1
by Th33;
:: thesis: ( S2[t1] & S3[t1] & S4[t1] )
thus
LeastSort ((PTMin X) . t1) <= LeastSort t1
by A4;
:: thesis: ( S3[t1] & S4[t1] )
thus
for
s1 being
Element of
S for
x1 being
set st
x1 in X . s1 &
t1 = root-tree [x1,s1] holds
(PTMin X) . t1 = t1
by A4;
:: thesis: S4[t1]
hereby :: thesis: verum
let o be
OperSymbol of
S;
:: thesis: for ts being FinSequence of TS (DTConOSA X) st OSSym o,X ==> roots ts & t1 = (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) . t1 = (OSSym (LBound o,(LeastSorts ((PTMin X) * ts))),X) -tree ((PTMin X) * ts) )let ts be
FinSequence of
TS (DTConOSA X);
:: thesis: ( OSSym o,X ==> roots ts & t1 = (OSSym o,X) -tree ts implies ( 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) ) )assume A5:
(
OSSym o,
X ==> roots ts &
t1 = (OSSym o,X) -tree ts )
;
:: thesis: ( 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) )
t1 . {} = [o,the carrier of S]
by A5, 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 A3, Th10;
:: thesis: verum
end;
end;
A6:
for nt being Symbol of (DTConOSA X)
for ts1 being FinSequence of TS (DTConOSA X) st nt ==> roots ts1 & ( for dt1 being DecoratedTree of the carrier of (DTConOSA X) st dt1 in rng ts1 holds
S5[dt1] ) holds
S5[nt -tree ts1]
proof
let nt be
Symbol of
(DTConOSA X);
:: thesis: for ts1 being FinSequence of TS (DTConOSA X) st nt ==> roots ts1 & ( for dt1 being DecoratedTree of the carrier of (DTConOSA X) st dt1 in rng ts1 holds
S5[dt1] ) holds
S5[nt -tree ts1]let ts1 be
FinSequence of
TS (DTConOSA X);
:: thesis: ( nt ==> roots ts1 & ( for dt1 being DecoratedTree of the carrier of (DTConOSA X) st dt1 in rng ts1 holds
S5[dt1] ) implies S5[nt -tree ts1] )
assume that A7:
nt ==> roots ts1
and A8:
for
dt1 being
DecoratedTree of the
carrier of
(DTConOSA X) st
dt1 in rng ts1 holds
ex
t2 being
Element of
TS (DTConOSA X) st
(
t2 = dt1 &
S1[
t2] &
S2[
t2] &
S3[
t2] &
S4[
t2] )
;
:: thesis: S5[nt -tree ts1]
reconsider t1 =
nt -tree ts1 as
Element of
TS (DTConOSA X) by A7, Th12;
take
t1
;
:: thesis: ( t1 = nt -tree ts1 & S1[t1] & S2[t1] & S3[t1] & S4[t1] )
thus
t1 = nt -tree ts1
;
:: thesis: ( S1[t1] & S2[t1] & S3[t1] & S4[t1] )
reconsider ta1 =
t1 as
Element of the
Sorts of
(ParsedTermsOSA X) . (LeastSort t1) by Def12;
consider o being
OperSymbol of
S such that A9:
(
nt = [o,the carrier of S] &
ts1 in Args o,
(ParsedTermsOSA X) &
nt -tree ts1 = (Den o,(ParsedTermsOSA X)) . ts1 & ( for
s1 being
Element of
S holds
(
nt -tree ts1 in the
Sorts of
(ParsedTermsOSA X) . s1 iff
the_result_sort_of o <= s1 ) ) )
by A7, Th12;
A10:
OSClass (PTCongruence X),
t1 =
OSClass (PTCongruence X),
ta1
by Def28
.=
proj1 ((PTClasses X) . t1)
by Th26
;
set Ms =
(PTMin X) * ts1;
set LSMs =
LeastSorts ((PTMin X) * ts1);
set w =
the_arity_of o;
set so =
the_result_sort_of o;
set Lo =
LBound o,
(LeastSorts ((PTMin X) * ts1));
A11:
(
dom ((PTClasses X) * ts1) = dom ts1 &
dom ((PTMin X) * ts1) = dom ts1 &
dom (LeastSorts ts1) = dom ts1 &
dom ts1 = dom (the_arity_of o) )
by A9, Def14, ALG_1:1, MSUALG_3:6;
then A12:
dom (LeastSorts ((PTMin X) * ts1)) = dom ts1
by Def14;
A13:
rng ts1 c= TS (DTConOSA X)
by FINSEQ_1:def 4;
@ X,
nt = o
by A7, A9, Def16;
then A14:
(PTMin X) . (nt -tree ts1) = pi o,
((PTMin X) * ts1)
by A7, Def32;
A15:
nt = OSSym o,
X
by A9;
A16:
LeastSort t1 = the_result_sort_of o
by A9, Th18;
consider l being
Nat such that A17:
dom ts1 = Seg l
by FINSEQ_1:def 2;
A18:
(PTClasses X) . t1 =
@ nt,
((PTClasses X) * ts1)
by A7, Def22
.=
{ [((Den o2,(ParsedTermsOSA X)) . x2),s3] where o2 is OperSymbol of S, x2 is Element of Args o2,(ParsedTermsOSA X), s3 is Element of S : ( ex o1 being OperSymbol of S st
( nt = [o1,the carrier of S] & o1 ~= o2 & len (the_arity_of o1) = len (the_arity_of o2) & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of the carrier of S * st
( dom w3 = dom ((PTClasses X) * ts1) & ( for y being Nat st y in dom ((PTClasses X) * ts1) holds
[(x2 . y),(w3 /. y)] in ((PTClasses X) * ts1) . y ) ) ) }
;
A19:
S4[
t1]
proof
let o2 be
OperSymbol of
S;
:: thesis: for ts being FinSequence of TS (DTConOSA X) st OSSym o2,X ==> roots ts & t1 = (OSSym o2,X) -tree ts holds
( LeastSorts ((PTMin X) * ts) <= the_arity_of o2 & OSSym o2,X ==> roots ((PTMin X) * ts) & OSSym (LBound o2,(LeastSorts ((PTMin X) * ts))),X ==> roots ((PTMin X) * ts) & (PTMin X) . t1 = (OSSym (LBound o2,(LeastSorts ((PTMin X) * ts))),X) -tree ((PTMin X) * ts) )let ts be
FinSequence of
TS (DTConOSA X);
:: thesis: ( OSSym o2,X ==> roots ts & t1 = (OSSym o2,X) -tree ts implies ( LeastSorts ((PTMin X) * ts) <= the_arity_of o2 & OSSym o2,X ==> roots ((PTMin X) * ts) & OSSym (LBound o2,(LeastSorts ((PTMin X) * ts))),X ==> roots ((PTMin X) * ts) & (PTMin X) . t1 = (OSSym (LBound o2,(LeastSorts ((PTMin X) * ts))),X) -tree ((PTMin X) * ts) ) )
assume A20:
(
OSSym o2,
X ==> roots ts &
t1 = (OSSym o2,X) -tree ts )
;
:: thesis: ( LeastSorts ((PTMin X) * ts) <= the_arity_of o2 & OSSym o2,X ==> roots ((PTMin X) * ts) & OSSym (LBound o2,(LeastSorts ((PTMin X) * ts))),X ==> roots ((PTMin X) * ts) & (PTMin X) . t1 = (OSSym (LBound o2,(LeastSorts ((PTMin X) * ts))),X) -tree ((PTMin X) * ts) )
A21:
(
OSSym o2,
X = nt &
ts = ts1 )
by A20, TREES_4:15;
then A22:
o2 = o
by A9, ZFMISC_1:33;
set Ms1 =
(PTMin X) * ts;
set LSMs1 =
LeastSorts ((PTMin X) * ts);
set Lo2 =
LBound o2,
(LeastSorts ((PTMin X) * ts));
A23:
LeastSorts ((PTMin X) * ts1) <= the_arity_of o
proof
thus
len (LeastSorts ((PTMin X) * ts1)) = len (the_arity_of o)
by A11, A12, FINSEQ_3:31;
:: according to OSALG_1:def 7 :: thesis: for b1 being set holds
( not b1 in dom (LeastSorts ((PTMin X) * ts1)) or for b2, b3 being Element of the carrier of S holds
( not b2 = (LeastSorts ((PTMin X) * ts1)) . b1 or not b3 = (the_arity_of o) . b1 or b2 <= b3 ) )
let i be
set ;
:: thesis: ( not i in dom (LeastSorts ((PTMin X) * ts1)) or for b1, b2 being Element of the carrier of S holds
( not b1 = (LeastSorts ((PTMin X) * ts1)) . i or not b2 = (the_arity_of o) . i or b1 <= b2 ) )
assume A24:
i in dom (LeastSorts ((PTMin X) * ts1))
;
:: thesis: for b1, b2 being Element of the carrier of S holds
( not b1 = (LeastSorts ((PTMin X) * ts1)) . i or not b2 = (the_arity_of o) . i or b1 <= b2 )
reconsider k =
i as
Nat by A24;
A25:
ts1 . k in rng ts1
by A12, A24, FUNCT_1:12;
then reconsider tr =
ts1 . k as
Element of
TS (DTConOSA X) by A13;
consider tr1 being
Element of
TS (DTConOSA X) such that A26:
(
tr1 = tr &
S1[
tr1] &
S2[
tr1] &
S3[
tr1] &
S4[
tr1] )
by A8, A25;
let s1,
s2 be
Element of
S;
:: thesis: ( not s1 = (LeastSorts ((PTMin X) * ts1)) . i or not s2 = (the_arity_of o) . i or s1 <= s2 )
assume A27:
(
s1 = (LeastSorts ((PTMin X) * ts1)) . i &
s2 = (the_arity_of o) . i )
;
:: thesis: s1 <= s2
consider t3 being
Element of
TS (DTConOSA X) such that A28:
(
t3 = ((PTMin X) * ts1) . k &
(LeastSorts ((PTMin X) * ts1)) . k = LeastSort t3 )
by A11, A12, A24, Def14;
A29:
((PTMin X) * ts1) . k = (PTMin X) . tr
by A11, A12, A24, ALG_1:1;
ts1 . k in the
Sorts of
(ParsedTermsOSA X) . ((the_arity_of o) /. k)
by A9, A11, A12, A24, MSUALG_6:2;
then A30:
LeastSort tr <= (the_arity_of o) /. k
by Def12;
(the_arity_of o) /. k = (the_arity_of o) . i
by A11, A12, A24, PARTFUN1:def 8;
hence
s1 <= s2
by A26, A27, A28, A29, A30, ORDERS_2:26;
:: thesis: verum
end;
hence
LeastSorts ((PTMin X) * ts) <= the_arity_of o2
by A9, A21, ZFMISC_1:33;
:: thesis: ( OSSym o2,X ==> roots ((PTMin X) * ts) & OSSym (LBound o2,(LeastSorts ((PTMin X) * ts))),X ==> roots ((PTMin X) * ts) & (PTMin X) . t1 = (OSSym (LBound o2,(LeastSorts ((PTMin X) * ts))),X) -tree ((PTMin X) * ts) )
LBound o2,
(LeastSorts ((PTMin X) * ts)) has_least_rank_for o2,
LeastSorts ((PTMin X) * ts)
by A21, A22, A23, OSALG_1:14;
then
(
LBound o2,
(LeastSorts ((PTMin X) * ts)) has_least_args_for o2,
LeastSorts ((PTMin X) * ts) &
LBound o2,
(LeastSorts ((PTMin X) * ts)) has_least_sort_for o2,
LeastSorts ((PTMin X) * ts) )
by OSALG_1:def 12;
then
(
o2 ~= LBound o2,
(LeastSorts ((PTMin X) * ts)) &
LeastSorts ((PTMin X) * ts) <= the_arity_of (LBound o2,(LeastSorts ((PTMin X) * ts))) & ( for
o3 being
OperSymbol of
S st
o2 ~= o3 &
LeastSorts ((PTMin X) * ts) <= the_arity_of o3 holds
the_arity_of (LBound o2,(LeastSorts ((PTMin X) * ts))) <= the_arity_of o3 ) )
by OSALG_1:def 10;
then
(
(PTMin X) * ts in Args (LBound o2,(LeastSorts ((PTMin X) * ts))),
(ParsedTermsOSA X) &
(PTMin X) * ts in Args o2,
(ParsedTermsOSA X) )
by A21, A22, A23, Th19;
hence
(
OSSym o2,
X ==> roots ((PTMin X) * ts) &
OSSym (LBound o2,(LeastSorts ((PTMin X) * ts))),
X ==> roots ((PTMin X) * ts) )
by Th13;
:: thesis: (PTMin X) . t1 = (OSSym (LBound o2,(LeastSorts ((PTMin X) * ts))),X) -tree ((PTMin X) * ts)
hence
(PTMin X) . t1 = (OSSym (LBound o2,(LeastSorts ((PTMin X) * ts))),X) -tree ((PTMin X) * ts)
by A14, A21, A22, Def15;
:: thesis: verum
end;
then A31:
(
LeastSorts ((PTMin X) * ts1) <= the_arity_of o &
OSSym o,
X ==> roots ((PTMin X) * ts1) &
OSSym (LBound o,(LeastSorts ((PTMin X) * ts1))),
X ==> roots ((PTMin X) * ts1) &
(PTMin X) . t1 = (OSSym (LBound o,(LeastSorts ((PTMin X) * ts1))),X) -tree ((PTMin X) * ts1) )
by A7, A15;
then consider o3 being
OperSymbol of
S such that A32:
(
OSSym (LBound o,(LeastSorts ((PTMin X) * ts1))),
X = [o3,the carrier of S] &
(PTMin X) * ts1 in Args o3,
(ParsedTermsOSA X) &
(OSSym (LBound o,(LeastSorts ((PTMin X) * ts1))),X) -tree ((PTMin X) * ts1) = (Den o3,(ParsedTermsOSA X)) . ((PTMin X) * ts1) & ( for
s1 being
Element of
S holds
(
(OSSym (LBound o,(LeastSorts ((PTMin X) * ts1))),X) -tree ((PTMin X) * ts1) in the
Sorts of
(ParsedTermsOSA X) . s1 iff
the_result_sort_of o3 <= s1 ) ) )
by Th12;
A33:
LBound o,
(LeastSorts ((PTMin X) * ts1)) = o3
by A32, ZFMISC_1:33;
reconsider Msr =
(PTMin X) * ts1 as
Element of
Args (LBound o,(LeastSorts ((PTMin X) * ts1))),
(ParsedTermsOSA X) by A32, ZFMISC_1:33;
A34:
(PTMin X) . t1 = (Den (LBound o,(LeastSorts ((PTMin X) * ts1))),(ParsedTermsOSA X)) . Msr
by A7, A15, A19, A32, A33;
A35:
LeastSort ((PTMin X) . t1) = the_result_sort_of (LBound o,(LeastSorts ((PTMin X) * ts1)))
by A31, A32, A33, Th18;
LBound o,
(LeastSorts ((PTMin X) * ts1)) has_least_rank_for o,
LeastSorts ((PTMin X) * ts1)
by A31, OSALG_1:14;
then A36:
(
LBound o,
(LeastSorts ((PTMin X) * ts1)) has_least_args_for o,
LeastSorts ((PTMin X) * ts1) &
LBound o,
(LeastSorts ((PTMin X) * ts1)) has_least_sort_for o,
LeastSorts ((PTMin X) * ts1) )
by OSALG_1:def 12;
then A37:
(
o ~= LBound o,
(LeastSorts ((PTMin X) * ts1)) &
LeastSorts ((PTMin X) * ts1) <= the_arity_of (LBound o,(LeastSorts ((PTMin X) * ts1))) & ( for
o3 being
OperSymbol of
S st
o ~= o3 &
LeastSorts ((PTMin X) * ts1) <= the_arity_of o3 holds
the_result_sort_of (LBound o,(LeastSorts ((PTMin X) * ts1))) <= the_result_sort_of o3 ) )
by OSALG_1:def 11;
A38:
(
the_result_sort_of (LBound o,(LeastSorts ((PTMin X) * ts1))) <= the_result_sort_of o &
the_arity_of (LBound o,(LeastSorts ((PTMin X) * ts1))) <= the_arity_of o )
by A31, A36, OSALG_1:def 10, OSALG_1:def 11;
then A39:
len (the_arity_of (LBound o,(LeastSorts ((PTMin X) * ts1)))) = len (the_arity_of o)
by OSALG_1:def 7;
A40:
(PTMin X) . t1 in OSClass (PTCongruence X),
t1
proof
defpred S6[
set ,
set ]
means [(((PTMin X) * ts1) . $1),$2] in ((PTClasses X) * ts1) . $1;
A41:
for
i being
set st
i in dom ((PTClasses X) * ts1) holds
ex
s4 being
set st
(
s4 in the
carrier of
S &
S6[
i,
s4] )
proof
let i be
set ;
:: thesis: ( i in dom ((PTClasses X) * ts1) implies ex s4 being set st
( s4 in the carrier of S & S6[i,s4] ) )
assume A42:
i in dom ((PTClasses X) * ts1)
;
:: thesis: ex s4 being set st
( s4 in the carrier of S & S6[i,s4] )
A43:
(
((PTMin X) * ts1) . i = (PTMin X) . (ts1 . i) &
((PTClasses X) * ts1) . i = (PTClasses X) . (ts1 . i) &
ts1 . i in rng ts1 )
by A11, A42, FUNCT_1:12, FUNCT_1:23;
then reconsider td1 =
ts1 . i as
Element of
TS (DTConOSA X) by A13;
reconsider tda =
td1 as
Element of the
Sorts of
(ParsedTermsOSA X) . (LeastSort td1) by Def12;
consider td2 being
Element of
TS (DTConOSA X) such that A44:
(
td2 = td1 &
(PTMin X) . td2 in OSClass (PTCongruence X),
td2 &
S2[
td2] &
S3[
td2] &
S4[
td2] )
by A8, A43;
OSClass (PTCongruence X),
td1 =
OSClass (PTCongruence X),
tda
by Def28
.=
proj1 (((PTClasses X) * ts1) . i)
by A43, Th26
;
then consider s4 being
set such that A45:
[(((PTMin X) * ts1) . i),s4] in ((PTClasses X) * ts1) . i
by A43, A44, RELAT_1:def 4;
s4 in the
carrier of
S
by A43, A45, Th24;
hence
ex
s4 being
set st
(
s4 in the
carrier of
S &
S6[
i,
s4] )
by A45;
:: thesis: verum
end;
consider f being
Function such that A46:
(
dom f = dom ((PTClasses X) * ts1) &
rng f c= the
carrier of
S & ( for
z being
set st
z in dom ((PTClasses X) * ts1) holds
S6[
z,
f . z] ) )
from WELLORD2:sch 1(A41);
reconsider wa =
f as
FinSequence by A11, A17, A46, FINSEQ_1:def 2;
reconsider wa =
wa as
FinSequence of the
carrier of
S by A46, FINSEQ_1:def 4;
reconsider wa =
wa as
Element of the
carrier of
S * by FINSEQ_1:def 11;
for
y being
Nat st
y in dom ((PTClasses X) * ts1) holds
[(Msr . y),(wa /. y)] in ((PTClasses X) * ts1) . y
then
[((Den (LBound o,(LeastSorts ((PTMin X) * ts1))),(ParsedTermsOSA X)) . Msr),(the_result_sort_of o)] in (PTClasses X) . t1
by A9, A18, A37, A38, A39, A46;
hence
(PTMin X) . t1 in OSClass (PTCongruence X),
t1
by A10, A34, FUNCT_5:4;
:: thesis: verum
end;
for
s being
Element of
S for
x being
set st
x in X . s &
t1 = root-tree [x,s] holds
(PTMin X) . t1 = t1
hence
(
S1[
t1] &
S2[
t1] &
S3[
t1] &
S4[
t1] )
by A16, A19, A31, A35, A36, A40, OSALG_1:def 11;
:: thesis: verum
end;
for dt being DecoratedTree of the carrier of (DTConOSA X) st dt in TS (DTConOSA X) holds
S5[dt]
from DTCONSTR:sch 7(A1, A6);
then consider t1 being Element of TS (DTConOSA X) such that
A49:
( t1 = t & S1[t1] & S2[t1] & S3[t1] & S4[t1] )
;
thus
( S1[t] & S2[t] & S3[t] & S4[t] )
by A49; :: thesis: verum