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