let S be OrderSortedSign; for X being V2() ManySortedSet of S
for s, s1 being Element of S
for 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 implies s <= s1 ) & ( s <= s1 implies root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 ) )
let X be V2() ManySortedSet of S; for s, s1 being Element of S
for 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 implies s <= s1 ) & ( s <= s1 implies root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 ) )
let s, s1 be Element of S; for 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 implies s <= s1 ) & ( s <= s1 implies root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 ) )
let x be set ; ( x in X . s implies ( 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 implies s <= s1 ) & ( s <= s1 implies root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 ) ) )
assume A1:
x in X . s
; ( 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 implies s <= s1 ) & ( s <= s1 implies root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 ) )
set PTA = ParsedTermsOSA X;
set D = DTConOSA X;
reconsider t = [x,s] as Terminal of (DTConOSA X) by A1, Th4;
reconsider s0 = s, s11 = s1 as Element of S ;
reconsider SPTA = the Sorts of (ParsedTermsOSA X) as OrderSortedSet of S ;
root-tree t is Element of TS (DTConOSA X)
;
hence
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 implies s <= s1 ) & ( s <= s1 implies root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 ) )
thus A2:
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 implies s <= s1 ) & ( s <= s1 implies root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 ) )
hereby ( s <= s1 implies root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 )
assume
root-tree [x,s] in the
Sorts of
(ParsedTermsOSA X) . s1
;
s <= s1then
root-tree [x,s] in { a where a is Element of TS (DTConOSA X) : ( ex s2 being Element of S ex x being object st
( s2 <= s1 & x in X . s2 & a = root-tree [x,s2] ) or ex o being 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 A4:
a = root-tree [x,s]
and A5:
( ex
s2 being
Element of
S ex
x being
object st
(
s2 <= s1 &
x in X . s2 &
a = root-tree [x,s2] ) or ex
o being
OperSymbol of
S st
(
[o, the carrier of S] = a . {} &
the_result_sort_of o <= s1 ) )
;
consider s2 being
Element of
S,
x1 being
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;
verum
end;
assume
s <= s1
; root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . 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 ex x being object st
( s1 <= s & x in X . s1 & a = root-tree [x,s1] ) or ex o being 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
root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1
by A8; verum