let IIG be non empty non void Circuit-like monotonic ManySortedSign ; for A being non-empty finite-yielding MSAlgebra over IIG
for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e = size (v,A) holds
ex q being DTree-yielding FinSequence st e = [(action_at v), the carrier of IIG] -tree q
let A be non-empty finite-yielding MSAlgebra over IIG; for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e = size (v,A) holds
ex q being DTree-yielding FinSequence st e = [(action_at v), the carrier of IIG] -tree q
let v be Vertex of IIG; for e being Element of the Sorts of (FreeEnv A) . v st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e = size (v,A) holds
ex q being DTree-yielding FinSequence st e = [(action_at v), the carrier of IIG] -tree q
let e be Element of the Sorts of (FreeEnv A) . v; ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e = size (v,A) implies ex q being DTree-yielding FinSequence st e = [(action_at v), the carrier of IIG] -tree q )
assume that
A1:
v in (InnerVertices IIG) \ (SortsWithConstants IIG)
and
A2:
card e = size (v,A)
; ex q being DTree-yielding FinSequence st e = [(action_at v), the carrier of IIG] -tree q
A3:
not v in SortsWithConstants IIG
by A1, XBOOLE_0:def 5;
InputVertices IIG misses InnerVertices IIG
by XBOOLE_1:79;
then A4:
(InputVertices IIG) /\ (InnerVertices IIG) = {}
by XBOOLE_0:def 7;
v in InnerVertices IIG
by A1, XBOOLE_0:def 5;
then
not v in InputVertices IIG
by A4, XBOOLE_0:def 4;
then
not v in (InputVertices IIG) \/ (SortsWithConstants IIG)
by A3, XBOOLE_0:def 3;
then A5:
card e <> 1
by A2, Th10;
reconsider e9 = e as non empty finite set ;
FreeEnv A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #)
by MSAFREE:def 14;
then
the Sorts of (FreeEnv A) . v = FreeSort ( the Sorts of A,v)
by MSAFREE:def 11;
then
e in FreeSort ( the Sorts of A,v)
;
then A6:
e in { a where a is Element of TS (DTConMSA the Sorts of A) : ( ex x being set st
( x in the Sorts of A . v & a = root-tree [x,v] ) or ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a . {} & the_result_sort_of o = v ) ) }
by MSAFREE:def 10;
1 <= card e9
by NAT_1:14;
then
1 < card e9
by A5, XXREAL_0:1;
then consider o being OperSymbol of IIG such that
A7:
e . {} = [o, the carrier of IIG]
by Th7;
( NonTerminals (DTConMSA the Sorts of A) = [: the carrier' of IIG,{ the carrier of IIG}:] & the carrier of IIG in { the carrier of IIG} )
by MSAFREE:6, TARSKI:def 1;
then reconsider nt = [o, the carrier of IIG] as NonTerminal of (DTConMSA the Sorts of A) by ZFMISC_1:87;
consider a being Element of TS (DTConMSA the Sorts of A) such that
A8:
a = e
and
A9:
( ex x being set st
( x in the Sorts of A . v & a = root-tree [x,v] ) or ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a . {} & the_result_sort_of o = v ) )
by A6;
consider x being set such that
A10:
( ( x in the Sorts of A . v & a = root-tree [x,v] ) or ex o9 being OperSymbol of IIG st
( [o9, the carrier of IIG] = a . {} & the_result_sort_of o9 = v ) )
by A9;
consider ts being FinSequence of TS (DTConMSA the Sorts of A) such that
A11:
a = nt -tree ts
and
nt ==> roots ts
by A8, A7, DTCONSTR:10;
reconsider q = ts as DTree-yielding FinSequence ;
take
q
; e = [(action_at v), the carrier of IIG] -tree q
A12:
v in InnerVertices IIG
by A1, XBOOLE_0:def 5;
then consider o9 being OperSymbol of IIG such that
A14:
[o9, the carrier of IIG] = a . {}
and
A15:
the_result_sort_of o9 = v
by A10;
o =
o9
by A8, A7, A14, XTUPLE_0:1
.=
action_at v
by A15, A12, MSAFREE2:def 7
;
hence
e = [(action_at v), the carrier of IIG] -tree q
by A8, A11; verum