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
for x being set st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e = root-tree [x,v] holds
((Fix_inp_ext iv) . v) . e = e
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
for x being set st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e = root-tree [x,v] holds
((Fix_inp_ext iv) . v) . e = e
let iv be InputValues of A; for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v
for x being set st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e = root-tree [x,v] holds
((Fix_inp_ext iv) . v) . e = e
let v be Vertex of IIG; for e being Element of the Sorts of (FreeEnv A) . v
for x being set st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e = root-tree [x,v] holds
((Fix_inp_ext iv) . v) . e = e
let e be Element of the Sorts of (FreeEnv A) . v; for x being set st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e = root-tree [x,v] holds
((Fix_inp_ext iv) . v) . e = e
let x be set ; ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e = root-tree [x,v] implies ((Fix_inp_ext iv) . v) . e = e )
assume that
A1:
v in (InnerVertices IIG) \ (SortsWithConstants IIG)
and
A2:
e = root-tree [x,v]
; ((Fix_inp_ext iv) . v) . e = e
A3:
e . {} = [x,v]
by A2, TREES_4:3;
set X = the Sorts of A;
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 A6:
e in FreeSort ( the Sorts of A,v)
by MSAFREE:def 11;
Fix_inp iv c= Fix_inp_ext iv
by Def2;
then A7:
(Fix_inp iv) . v c= (Fix_inp_ext iv) . v
;
FreeSort ( the Sorts of A,v) = { 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
ex a being Element of TS (DTConMSA the Sorts of A) st
( a = e & ( 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;
then A8:
e in FreeGen (v, the Sorts of A)
by A4, MSAFREE:def 15;
then
e in (FreeGen the Sorts of A) . v
by MSAFREE:def 16;
then
e in dom ((Fix_inp iv) . v)
by FUNCT_2:def 1;
hence ((Fix_inp_ext iv) . v) . e =
((Fix_inp iv) . v) . e
by A7, GRFUNC_1:2
.=
(id (FreeGen (v, the Sorts of A))) . e
by A1, Def1
.=
e
by A8, FUNCT_1:17
;
verum