let IIG be non empty non void Circuit-like monotonic ManySortedSign ; for SCS being non-empty Circuit of IIG
for v being Vertex of IIG
for iv being InputValues of SCS st v in InputVertices IIG holds
IGValue (v,iv) = iv . v
let SCS be non-empty Circuit of IIG; for v being Vertex of IIG
for iv being InputValues of SCS st v in InputVertices IIG holds
IGValue (v,iv) = iv . v
let v be Vertex of IIG; for iv being InputValues of SCS st v in InputVertices IIG holds
IGValue (v,iv) = iv . v
let iv be InputValues of SCS; ( v in InputVertices IIG implies IGValue (v,iv) = iv . v )
set X = the Sorts of SCS;
A1:
( (FreeSort the Sorts of SCS) . v = FreeSort ( the Sorts of SCS,v) & FreeSort ( the Sorts of SCS,v) = { a where a is Element of TS (DTConMSA the Sorts of SCS) : ( ex x being set st
( x in the Sorts of SCS . 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, MSAFREE:def 11;
assume A2:
v in InputVertices IIG
; IGValue (v,iv) = iv . v
then A3:
iv . v in the Sorts of SCS . v
by MSAFREE2:def 5;
then
root-tree [(iv . v),v] in FreeGen (v, the Sorts of SCS)
by MSAFREE:def 15;
then
root-tree [(iv . v),v] in (FreeSort the Sorts of SCS) . v
;
then A4:
root-tree [(iv . v),v] in FreeSort ( the Sorts of SCS,v)
by MSAFREE:def 11;
consider e being Element of the Sorts of (FreeEnv SCS) . v such that
card e = size (v,SCS)
and
A5:
IGTree (v,iv) = ((Fix_inp_ext iv) . v) . e
by Def3;
( e in the Sorts of (FreeMSA the Sorts of SCS) . v & FreeMSA the Sorts of SCS = MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #) )
by MSAFREE:def 14;
then
ex a being Element of TS (DTConMSA the Sorts of SCS) st
( a = e & ( ex x being set st
( x in the Sorts of SCS . 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 A1;
then A6:
e in FreeGen (v, the Sorts of SCS)
by A2, MSAFREE:def 15, MSAFREE2:2;
Fix_inp iv c= Fix_inp_ext iv
by Def2;
then A7:
(Fix_inp iv) . v c= (Fix_inp_ext iv) . v
;
A8:
(Fix_inp iv) . v = (FreeGen (v, the Sorts of SCS)) --> (root-tree [(iv . v),v])
by A2, Def1;
then
e in dom ((Fix_inp iv) . v)
by A6;
then
((Fix_inp iv) . v) . e = ((Fix_inp_ext iv) . v) . e
by A7, GRFUNC_1:2;
hence IGValue (v,iv) =
((Eval SCS) . v) . (root-tree [(iv . v),v])
by A5, A6, A8, FUNCOP_1:7
.=
iv . v
by A3, A4, MSAFREE2:def 9
;
verum