let IIG be non empty non void Circuit-like monotonic ManySortedSign ; for A being non-empty Circuit of IIG
for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v st e . {} = [(action_at v), the carrier of IIG] holds
ex p being DTree-yielding FinSequence st e = [(action_at v), the carrier of IIG] -tree p
let A be non-empty Circuit of IIG; for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v st e . {} = [(action_at v), the carrier of IIG] holds
ex p being DTree-yielding FinSequence st e = [(action_at v), the carrier of IIG] -tree p
let v be Vertex of IIG; for e being Element of the Sorts of (FreeEnv A) . v st e . {} = [(action_at v), the carrier of IIG] holds
ex p being DTree-yielding FinSequence st e = [(action_at v), the carrier of IIG] -tree p
let e be Element of the Sorts of (FreeEnv A) . v; ( e . {} = [(action_at v), the carrier of IIG] implies ex p being DTree-yielding FinSequence st e = [(action_at v), the carrier of IIG] -tree p )
assume A1:
e . {} = [(action_at v), the carrier of IIG]
; ex p being DTree-yielding FinSequence st e = [(action_at v), the carrier of IIG] -tree p
set X = the Sorts of A;
( 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 = [(action_at v), the carrier of IIG] as NonTerminal of (DTConMSA the Sorts of A) by ZFMISC_1:87;
( FreeMSA the Sorts of A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #) & e in the Sorts of (FreeEnv A) . v )
by MSAFREE:def 14;
then
e in FreeSort ( the Sorts of A,v)
by MSAFREE:def 11;
then reconsider tsg = e as Element of TS (DTConMSA the Sorts of A) ;
consider ts being FinSequence of TS (DTConMSA the Sorts of A) such that
A2:
tsg = nt -tree ts
and
nt ==> roots ts
by A1, DTCONSTR:10;
take
ts
; e = [(action_at v), the carrier of IIG] -tree ts
thus
e = [(action_at v), the carrier of IIG] -tree ts
by A2; verum