let S be OrderSortedSign; for X being V2() ManySortedSet of S
for o being OperSymbol of S
for p being FinSequence of TS (DTConOSA X) holds
( OSSym (o,X) ==> roots p iff p in (((ParsedTerms X) #) * the Arity of S) . o )
let X be V2() ManySortedSet of S; for o being OperSymbol of S
for p being FinSequence of TS (DTConOSA X) holds
( OSSym (o,X) ==> roots p iff p in (((ParsedTerms X) #) * the Arity of S) . o )
let o be OperSymbol of S; for p being FinSequence of TS (DTConOSA X) holds
( OSSym (o,X) ==> roots p iff p in (((ParsedTerms X) #) * the Arity of S) . o )
let p be FinSequence of TS (DTConOSA X); ( OSSym (o,X) ==> roots p iff p in (((ParsedTerms X) #) * the Arity of S) . o )
set D = DTConOSA X;
set ar = the_arity_of o;
set r = roots p;
set OU = [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));
A1:
dom p = dom (roots p)
by TREES_3:def 18;
thus
( OSSym (o,X) ==> roots p implies p in (((ParsedTerms X) #) * the Arity of S) . o )
( p in (((ParsedTerms X) #) * the Arity of S) . o implies OSSym (o,X) ==> roots p )proof
assume
OSSym (
o,
X)
==> roots p
;
p in (((ParsedTerms X) #) * the Arity of S) . o
then A2:
[[o, the carrier of S],(roots p)] in OSREL X
by LANG1:def 1;
then reconsider r =
roots p as
Element of
([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by ZFMISC_1:87;
A3:
dom p = dom r
by TREES_3:def 18;
A4:
for
n being
Nat st
n in dom p holds
p . n in ParsedTerms (
X,
((the_arity_of o) /. n))
proof
let n be
Nat;
( n in dom p implies p . n in ParsedTerms (X,((the_arity_of o) /. n)) )
set s =
(the_arity_of o) /. n;
A5:
rng r c= [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
by FINSEQ_1:def 4;
A6:
rng p c= TS (DTConOSA X)
by FINSEQ_1:def 4;
assume A7:
n in dom p
;
p . n in ParsedTerms (X,((the_arity_of o) /. n))
then consider T being
DecoratedTree such that A8:
T = p . n
and A9:
r . n = T . {}
by TREES_3:def 18;
p . n in rng p
by A7, FUNCT_1:def 3;
then reconsider T =
T as
Element of
TS (DTConOSA X) by A8, A6;
A10:
r . n in rng r
by A3, A7, FUNCT_1:def 3;
per cases
( r . n in [: the carrier' of S,{ the carrier of S}:] or r . n in Union (coprod X) )
by A5, A10, XBOOLE_0:def 3;
suppose A11:
r . n in [: the carrier' of S,{ the carrier of S}:]
;
p . n in ParsedTerms (X,((the_arity_of o) /. n))then consider o1 being
Element of the
carrier' of
S,
x2 being
Element of
{ the carrier of S} such that A12:
r . n = [o1,x2]
by DOMAIN_1:1;
A13:
x2 = the
carrier of
S
by TARSKI:def 1;
then
the_result_sort_of o1 <= (the_arity_of o) /. n
by A2, A3, A7, A11, A12, Th2;
then
ex
o being
OperSymbol of
S st
(
[o, the carrier of S] = T . {} &
the_result_sort_of o <= (the_arity_of o) /. n )
by A9, A12, A13;
hence
p . n in ParsedTerms (
X,
((the_arity_of o) /. n))
by A8;
verum end; suppose A14:
r . n in Union (coprod X)
;
p . n in ParsedTerms (X,((the_arity_of o) /. n))then reconsider t =
r . n as
Terminal of
(DTConOSA X) by Th3;
A15:
T = root-tree t
by A9, DTCONSTR:9;
consider i being
Element of
S such that A16:
i <= (the_arity_of o) /. n
and A17:
r . n in coprod (
i,
X)
by A2, A3, A7, A14, Th2;
ex
a being
set st
(
a in X . i &
r . n = [a,i] )
by A17, MSAFREE:def 2;
hence
p . n in ParsedTerms (
X,
((the_arity_of o) /. n))
by A8, A16, A15;
verum end;
end;
A18:
Seg (len (the_arity_of o)) = dom (the_arity_of o)
by FINSEQ_1:def 3;
A19:
dom r = Seg (len r)
by FINSEQ_1:def 3;
len r = len (the_arity_of o)
by A2, Th2;
hence
p in (((ParsedTerms X) #) * the Arity of S) . o
by A3, A19, A18, A4, Th6;
verum
end;
assume A20:
p in (((ParsedTerms X) #) * the Arity of S) . o
; OSSym (o,X) ==> roots p
A21:
dom (roots p) = Seg (len (roots p))
by FINSEQ_1:def 3;
reconsider r = roots p as FinSequence of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) ;
reconsider r = r as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by FINSEQ_1:def 11;
A22:
Union (coprod X) misses [: the carrier' of S,{ the carrier of S}:]
by MSAFREE:4;
A23:
for x being set st x in dom r holds
( ( r . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = r . x holds
the_result_sort_of o1 <= (the_arity_of o) /. x ) & ( r . x in Union (coprod X) implies ex i being Element of S st
( i <= (the_arity_of o) /. x & r . x in coprod (i,X) ) ) )
proof
let x be
set ;
( x in dom r implies ( ( r . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = r . x holds
the_result_sort_of o1 <= (the_arity_of o) /. x ) & ( r . x in Union (coprod X) implies ex i being Element of S st
( i <= (the_arity_of o) /. x & r . x in coprod (i,X) ) ) ) )
assume A24:
x in dom r
;
( ( r . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = r . x holds
the_result_sort_of o1 <= (the_arity_of o) /. x ) & ( r . x in Union (coprod X) implies ex i being Element of S st
( i <= (the_arity_of o) /. x & r . x in coprod (i,X) ) ) )
then reconsider n =
x as
Nat ;
set s =
(the_arity_of o) /. n;
p . n in ParsedTerms (
X,
((the_arity_of o) /. n))
by A20, A1, A24, Th6;
then consider a being
Element of
TS (DTConOSA X) such that A25:
a = p . n
and A26:
( ex
s1 being
Element of
S ex
x being
object st
(
s1 <= (the_arity_of o) /. n &
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 <= (the_arity_of o) /. n ) )
;
A27:
ex
T being
DecoratedTree st
(
T = p . n &
r . n = T . {} )
by A1, A24, TREES_3:def 18;
thus
(
r . x in [: the carrier' of S,{ the carrier of S}:] implies for
o1 being
OperSymbol of
S st
[o1, the carrier of S] = r . x holds
the_result_sort_of o1 <= (the_arity_of o) /. x )
( r . x in Union (coprod X) implies ex i being Element of S st
( i <= (the_arity_of o) /. x & r . x in coprod (i,X) ) )proof
assume A28:
r . x in [: the carrier' of S,{ the carrier of S}:]
;
for o1 being OperSymbol of S st [o1, the carrier of S] = r . x holds
the_result_sort_of o1 <= (the_arity_of o) /. x
A29:
now for s1 being Element of S
for y being set holds
( not s1 <= (the_arity_of o) /. n or not y in X . s1 or not a = root-tree [y,s1] )given s1 being
Element of
S,
y being
set such that
s1 <= (the_arity_of o) /. n
and A30:
y in X . s1
and A31:
a = root-tree [y,s1]
;
contradictionA32:
[y,s1] in coprod (
s1,
X)
by A30, MSAFREE:def 2;
dom (coprod X) = the
carrier of
S
by PARTFUN1:def 2;
then
(coprod X) . s1 in rng (coprod X)
by FUNCT_1:def 3;
then A33:
coprod (
s1,
X)
in rng (coprod X)
by MSAFREE:def 3;
r . x = [y,s1]
by A25, A27, A31, TREES_4:3;
then
r . x in union (rng (coprod X))
by A32, A33, TARSKI:def 4;
then
r . x in Union (coprod X)
by CARD_3:def 4;
hence
contradiction
by A22, A28, XBOOLE_0:3;
verum end;
let o1 be
OperSymbol of
S;
( [o1, the carrier of S] = r . x implies the_result_sort_of o1 <= (the_arity_of o) /. x )
assume
[o1, the carrier of S] = r . x
;
the_result_sort_of o1 <= (the_arity_of o) /. x
hence
the_result_sort_of o1 <= (the_arity_of o) /. x
by A25, A26, A27, A29, XTUPLE_0:1;
verum
end;
assume A34:
r . x in Union (coprod X)
;
ex i being Element of S st
( i <= (the_arity_of o) /. x & r . x in coprod (i,X) )
then consider s1 being
Element of
S,
y being
set such that A36:
s1 <= (the_arity_of o) /. n
and A37:
y in X . s1
and A38:
a = root-tree [y,s1]
by A26;
take
s1
;
( s1 <= (the_arity_of o) /. x & r . x in coprod (s1,X) )
r . x = [y,s1]
by A25, A27, A38, TREES_4:3;
hence
(
s1 <= (the_arity_of o) /. x &
r . x in coprod (
s1,
X) )
by A36, A37, MSAFREE:def 2;
verum
end;
dom p = dom (the_arity_of o)
by A20, Th6;
then
len r = len (the_arity_of o)
by A1, A21, FINSEQ_1:def 3;
then
[[o, the carrier of S],r] in OSREL X
by A23, Th2;
hence
OSSym (o,X) ==> roots p
by LANG1:def 1; verum