let S be monotone regular locally_directed OrderSortedSign; for X being V2() ManySortedSet of S
for R being MSEquivalence-like monotone OrderSortedRelation of ParsedTermsOSA X
for t being Element of TS (DTConOSA X) holds [t,((PTMin X) . t)] in R . (LeastSort t)
let X be V2() ManySortedSet of S; for R being MSEquivalence-like monotone OrderSortedRelation of ParsedTermsOSA X
for t being Element of TS (DTConOSA X) holds [t,((PTMin X) . t)] in R . (LeastSort t)
set PTA = ParsedTermsOSA X;
set SPTA = the Sorts of (ParsedTermsOSA X);
set D = DTConOSA X;
set M = PTMin X;
let R be MSEquivalence-like monotone OrderSortedRelation of ParsedTermsOSA X; for t being Element of TS (DTConOSA X) holds [t,((PTMin X) . t)] in R . (LeastSort t)
defpred S1[ set ] means ex t1 being Element of TS (DTConOSA X) st
( t1 = $1 & [t1,((PTMin X) . t1)] in R . (LeastSort t1) );
let t be Element of TS (DTConOSA X); [t,((PTMin X) . t)] in R . (LeastSort t)
A1:
R is os-compatible
by OSALG_4:def 2;
A2:
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
S1[dt1] ) holds
S1[nt -tree ts1]
proof
let nt be
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
S1[dt1] ) holds
S1[nt -tree ts1]let ts1 be
FinSequence of
TS (DTConOSA X);
( nt ==> roots ts1 & ( for dt1 being DecoratedTree of the carrier of (DTConOSA X) st dt1 in rng ts1 holds
S1[dt1] ) implies S1[nt -tree ts1] )
assume that A3:
nt ==> roots ts1
and A4:
for
dt1 being
DecoratedTree of the
carrier of
(DTConOSA X) st
dt1 in rng ts1 holds
S1[
dt1]
;
S1[nt -tree ts1]
consider o being
OperSymbol of
S such that A5:
nt = [o, the carrier of S]
and A6:
ts1 in Args (
o,
(ParsedTermsOSA X))
and A7:
nt -tree ts1 = (Den (o,(ParsedTermsOSA X))) . ts1
and
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 A3, Th12;
reconsider t1 =
nt -tree ts1 as
Element of
TS (DTConOSA X) by A3, Th12;
A8:
dom ((PTMin X) * ts1) = dom ts1
by FINSEQ_3:120;
reconsider tsa =
ts1 as
Element of
Args (
o,
(ParsedTermsOSA X))
by A6;
set w =
the_arity_of o;
A9:
rng ts1 c= TS (DTConOSA X)
by FINSEQ_1:def 4;
set lo =
LBound (
o,
(LeastSorts ((PTMin X) * ts1)));
set rs1 =
the_result_sort_of o;
A10:
t1 = (OSSym (o,X)) -tree ts1
by A5;
then A11:
OSSym (
(LBound (o,(LeastSorts ((PTMin X) * ts1)))),
X)
==> roots ((PTMin X) * ts1)
by A3, A5, Th40;
then reconsider tsm =
(PTMin X) * ts1 as
Element of
Args (
(LBound (o,(LeastSorts ((PTMin X) * ts1)))),
(ParsedTermsOSA X))
by Th13;
A12:
dom ts1 = dom (the_arity_of o)
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 be
Nat;
( y in dom tsm implies [(tsm . y),(tsa . y)] in R . ((the_arity_of o) /. y) )
assume A14:
y in dom tsm
;
[(tsm . y),(tsa . y)] in R . ((the_arity_of o) /. y)
ts1 . y in rng ts1
by A8, A14, FUNCT_1:3;
then reconsider td1 =
ts1 . y as
Element of
TS (DTConOSA X) by A9;
consider t2 being
Element of
TS (DTConOSA X) such that A15:
t2 = td1
and A16:
[t2,((PTMin X) . t2)] in R . (LeastSort t2)
by A4, A8, A14, FUNCT_1:3;
A17:
(PTMin X) . t2 = tsm . y
by A14, A15, FINSEQ_3:120;
A18:
(PTMin X) . t2 in the
Sorts of
(ParsedTermsOSA X) . (LeastSort t2)
by A16, ZFMISC_1:87;
tsa . y in the
Sorts of
(ParsedTermsOSA X) . ((the_arity_of o) /. y)
by A8, A12, A14, MSUALG_6:2;
then A19:
LeastSort t2 <= (the_arity_of o) /. y
by A15, Def12;
A20:
t2 in the
Sorts of
(ParsedTermsOSA X) . (LeastSort t2)
by A16, ZFMISC_1:87;
field (R . (LeastSort t2)) = the
Sorts of
(ParsedTermsOSA X) . (LeastSort t2)
by ORDERS_1:12;
then
R . (LeastSort t2) is_symmetric_in the
Sorts of
(ParsedTermsOSA X) . (LeastSort t2)
by RELAT_2:def 11;
then
[((PTMin X) . t2),t2] in R . (LeastSort t2)
by A16, A20, A18, RELAT_2:def 3;
hence
[(tsm . y),(tsa . y)] in R . ((the_arity_of o) /. y)
by A1, A15, A20, A18, A17, A19;
verum
end;
LeastSorts ((PTMin X) * ts1) <= the_arity_of o
by A3, A5, A10, Th40;
then
LBound (
o,
(LeastSorts ((PTMin X) * ts1)))
<= o
by OSALG_1:35;
then A21:
[((Den ((LBound (o,(LeastSorts ((PTMin X) * ts1)))),(ParsedTermsOSA X))) . tsm),((Den (o,(ParsedTermsOSA X))) . tsa)] in R . (the_result_sort_of o)
by A13, OSALG_4:def 26;
then A22:
(Den (o,(ParsedTermsOSA X))) . tsa in the
Sorts of
(ParsedTermsOSA X) . (the_result_sort_of o)
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
;
( t1 = nt -tree ts1 & [t1,((PTMin X) . t1)] in R . (LeastSort t1) )
thus
t1 = nt -tree ts1
;
[t1,((PTMin X) . t1)] in R . (LeastSort t1)
field (R . (the_result_sort_of o)) = the
Sorts of
(ParsedTermsOSA X) . (the_result_sort_of o)
by ORDERS_1:12;
then A25:
R . (the_result_sort_of o) is_symmetric_in the
Sorts of
(ParsedTermsOSA X) . (the_result_sort_of o)
by RELAT_2:def 11;
(Den ((LBound (o,(LeastSorts ((PTMin X) * ts1)))),(ParsedTermsOSA X))) . tsm in the
Sorts of
(ParsedTermsOSA X) . (the_result_sort_of o)
by A21, ZFMISC_1:87;
then A26:
[((Den (o,(ParsedTermsOSA X))) . tsa),((Den ((LBound (o,(LeastSorts ((PTMin X) * ts1)))),(ParsedTermsOSA X))) . tsm)] in R . (the_result_sort_of o)
by A21, A22, A25, RELAT_2:def 3;
consider o4 being
OperSymbol of
S such that A27:
OSSym (
(LBound (o,(LeastSorts ((PTMin X) * ts1)))),
X)
= [o4, the carrier of S]
and
(PTMin X) * ts1 in Args (
o4,
(ParsedTermsOSA X))
and A28:
(OSSym ((LBound (o,(LeastSorts ((PTMin X) * ts1)))),X)) -tree ((PTMin X) * ts1) = (Den (o4,(ParsedTermsOSA X))) . ((PTMin X) * ts1)
and
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 o4 <= s1 )
by A11, Th12;
LBound (
o,
(LeastSorts ((PTMin X) * ts1)))
= o4
by A27, XTUPLE_0:1;
hence
[t1,((PTMin X) . t1)] in R . (LeastSort t1)
by A5, A7, A24, A26, A23, A28, Th40;
verum
end;
A29:
for s being Symbol of (DTConOSA X) st s in Terminals (DTConOSA X) holds
S1[ root-tree s]
for dt being DecoratedTree of the carrier of (DTConOSA X) st dt in TS (DTConOSA X) holds
S1[dt]
from DTCONSTR:sch 7(A29, A2);
then
ex t1 being Element of TS (DTConOSA X) st
( t = t1 & [t1,((PTMin X) . t1)] in R . (LeastSort t1) )
;
hence
[t,((PTMin X) . t)] in R . (LeastSort t)
; verum