let IIG be non empty non void Circuit-like monotonic ManySortedSign ; for A being non-empty Circuit of IIG
for iv being InputValues of A
for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v st v in SortsWithConstants IIG holds
((Fix_inp_ext iv) . v) . e = root-tree [(action_at v), the carrier of IIG]
let A be non-empty Circuit of IIG; for iv being InputValues of A
for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v st v in SortsWithConstants IIG holds
((Fix_inp_ext iv) . v) . e = root-tree [(action_at v), the carrier of IIG]
let iv be InputValues of A; for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v st v in SortsWithConstants IIG holds
((Fix_inp_ext iv) . v) . e = root-tree [(action_at v), the carrier of IIG]
let v be Vertex of IIG; for e being Element of the Sorts of (FreeEnv A) . v st v in SortsWithConstants IIG holds
((Fix_inp_ext iv) . v) . e = root-tree [(action_at v), the carrier of IIG]
let e be Element of the Sorts of (FreeEnv A) . v; ( v in SortsWithConstants IIG implies ((Fix_inp_ext iv) . v) . e = root-tree [(action_at v), the carrier of IIG] )
set X = the Sorts of A;
assume A1:
v in SortsWithConstants IIG
; ((Fix_inp_ext iv) . v) . e = root-tree [(action_at v), the carrier of IIG]
A2:
FreeEnv A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #)
by MSAFREE:def 14;
then
e in (FreeSort the Sorts of A) . v
;
then
e in FreeSort ( the Sorts of A,v)
by MSAFREE:def 11;
then
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;
then A3:
ex a being Element of TS (DTConMSA the Sorts of A) st
( e = 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 ) ) )
;
per cases
( ex x being set st
( x in the Sorts of A . v & e = root-tree [x,v] ) or ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = e . {} & the_result_sort_of o = v ) )
by A3;
suppose
ex
o being
OperSymbol of
IIG st
(
[o, the carrier of IIG] = e . {} &
the_result_sort_of o = v )
;
((Fix_inp_ext iv) . v) . e = root-tree [(action_at v), the carrier of IIG]then consider o9 being
OperSymbol of
IIG such that A7:
[o9, the carrier of IIG] = e . {}
and A8:
the_result_sort_of o9 = v
;
A9:
SortsWithConstants IIG c= InnerVertices IIG
by MSAFREE2:3;
then
o9 = action_at v
by A1, A8, MSAFREE2:def 7;
then consider q being
DTree-yielding FinSequence such that A10:
e = [(action_at v), the carrier of IIG] -tree q
by A7, CIRCUIT1:9;
v in { s where s is SortSymbol of IIG : s is with_const_op }
by A1, MSAFREE2:def 1;
then
ex
s being
SortSymbol of
IIG st
(
v = s &
s is
with_const_op )
;
then consider o being
OperSymbol of
IIG such that A11:
the
Arity of
IIG . o = {}
and A12:
the
ResultSort of
IIG . o = v
by MSUALG_2:def 1;
A13:
Fix_inp_ext iv is_homomorphism FreeEnv A,
FreeEnv A
by Def2;
the_result_sort_of o = v
by A12, MSUALG_1:def 2;
then A14:
o = action_at v
by A1, A9, MSAFREE2:def 7;
action_at v in the
carrier' of
IIG
;
then A15:
action_at v in dom the
Arity of
IIG
by FUNCT_2:def 1;
A16:
Args (
(action_at v),
(FreeEnv A)) =
(( the Sorts of (FreeEnv A) #) * the Arity of IIG) . (action_at v)
by MSUALG_1:def 4
.=
( the Sorts of (FreeEnv A) #) . (<*> the carrier of IIG)
by A11, A14, A15, FUNCT_1:13
.=
{{}}
by PRE_CIRC:2
;
then reconsider x =
{} as
Element of
Args (
(action_at v),
(FreeEnv A))
by TARSKI:def 1;
A17:
x = (Fix_inp_ext iv) # x
by A16, TARSKI:def 1;
A18:
Args (
(action_at v),
(FreeEnv A))
= (((FreeSort the Sorts of A) #) * the Arity of IIG) . o
by A2, A14, MSUALG_1:def 4;
then reconsider p =
x as
FinSequence of
TS (DTConMSA the Sorts of A) by MSAFREE:8;
A19:
Sym (
(action_at v), the
Sorts of
A)
==> roots p
by A14, A18, MSAFREE:10;
A20:
the_result_sort_of (action_at v) = v
by A1, A9, MSAFREE2:def 7;
then len q =
len (the_arity_of (action_at v))
by A10, MSAFREE2:10
.=
len {}
by A11, A14, MSUALG_1:def 1
.=
0
;
then
q = {}
;
then A21:
e = root-tree [(action_at v), the carrier of IIG]
by A10, TREES_4:20;
(Den ((action_at v),(FreeEnv A))) . x =
((FreeOper the Sorts of A) . (action_at v)) . x
by A2, MSUALG_1:def 6
.=
(DenOp ((action_at v), the Sorts of A)) . x
by MSAFREE:def 13
.=
(Sym ((action_at v), the Sorts of A)) -tree p
by A19, MSAFREE:def 12
.=
[(action_at v), the carrier of IIG] -tree p
by MSAFREE:def 9
.=
root-tree [(action_at v), the carrier of IIG]
by TREES_4:20
;
hence
((Fix_inp_ext iv) . v) . e = root-tree [(action_at v), the carrier of IIG]
by A20, A17, A13, A21, MSUALG_3:def 7;
verum end;