let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis: for SCS being non-empty Circuit of IIG

for v being Vertex of IIG

for iv being InputValues of SCS st v in SortsWithConstants IIG holds

IGValue (v,iv) = (Set-Constants SCS) . v

reconsider p = {} as DTree-yielding FinSequence ;

let SCS be non-empty Circuit of IIG; :: thesis: for v being Vertex of IIG

for iv being InputValues of SCS st v in SortsWithConstants IIG holds

IGValue (v,iv) = (Set-Constants SCS) . v

let v be Vertex of IIG; :: thesis: for iv being InputValues of SCS st v in SortsWithConstants IIG holds

IGValue (v,iv) = (Set-Constants SCS) . v

let iv be InputValues of SCS; :: thesis: ( v in SortsWithConstants IIG implies IGValue (v,iv) = (Set-Constants SCS) . v )

assume A1: v in SortsWithConstants IIG ; :: thesis: IGValue (v,iv) = (Set-Constants SCS) . v

set e = ((Eval SCS) . v) . (root-tree [(action_at v), the carrier of IIG]);

A2: {} = <*> the carrier of IIG ;

set X = the Sorts of SCS;

set F = Eval SCS;

A3: dom the Arity of IIG = the carrier' of IIG by FUNCT_2:def 1;

A4: dom the ResultSort of IIG = the carrier' of IIG by FUNCT_2:def 1;

set o = action_at v;

A5: SortsWithConstants IIG c= InnerVertices IIG by MSAFREE2:3;

then A6: v = the_result_sort_of (action_at v) by A1, MSAFREE2:def 7;

SortsWithConstants IIG = { v1 where v1 is SortSymbol of IIG : v1 is with_const_op } by MSAFREE2:def 1;

then consider x9 being SortSymbol of IIG such that

A7: x9 = v and

A8: x9 is with_const_op by A1;

consider o1 being OperSymbol of IIG such that

A9: the Arity of IIG . o1 = {} and

A10: the ResultSort of IIG . o1 = x9 by A8, MSUALG_2:def 1;

the ResultSort of IIG . o1 = the_result_sort_of o1 by MSUALG_1:def 2;

then A11: action_at v = o1 by A1, A5, A7, A10, MSAFREE2:def 7;

A12: Args ((action_at v),(FreeEnv SCS)) = (( the Sorts of (FreeEnv SCS) #) * the Arity of IIG) . (action_at v) by MSUALG_1:def 4

.= ( the Sorts of (FreeEnv SCS) #) . ( the Arity of IIG . (action_at v)) by A3, FUNCT_1:13

.= {{}} by A9, A11, A2, PRE_CIRC:2 ;

then reconsider x = {} as Element of Args ((action_at v),(FreeEnv SCS)) by TARSKI:def 1;

reconsider Fx = (Eval SCS) # x as Element of Args ((action_at v),SCS) ;

Eval SCS is_homomorphism FreeEnv SCS,SCS by MSAFREE2:def 9;

then A13: ((Eval SCS) . (the_result_sort_of (action_at v))) . ((Den ((action_at v),(FreeEnv SCS))) . x) = (Den ((action_at v),SCS)) . Fx by MSUALG_3:def 7;

A14: FreeMSA the Sorts of SCS = MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #) by MSAFREE:def 14;

then A15: Den ((action_at v),(FreeEnv SCS)) = (FreeOper the Sorts of SCS) . (action_at v) by MSUALG_1:def 6

.= DenOp ((action_at v), the Sorts of SCS) by MSAFREE:def 13 ;

{} in Args ((action_at v),(FreeEnv SCS)) by A12, TARSKI:def 1;

then A16: p in (((FreeSort the Sorts of SCS) #) * the Arity of IIG) . (action_at v) by A14, MSUALG_1:def 4;

then reconsider p9 = {} as FinSequence of TS (DTConMSA the Sorts of SCS) by MSAFREE:8;

Sym ((action_at v), the Sorts of SCS) ==> roots p9 by A16, MSAFREE:10;

then A17: (Den ((action_at v),(FreeEnv SCS))) . {} = (Sym ((action_at v), the Sorts of SCS)) -tree p by A15, MSAFREE:def 12

.= [(action_at v), the carrier of IIG] -tree {} by MSAFREE:def 9

.= root-tree [(action_at v), the carrier of IIG] by TREES_4:20 ;

dom (Den ((action_at v),SCS)) = Args ((action_at v),SCS) by FUNCT_2:def 1;

then A18: ((Eval SCS) . v) . (root-tree [(action_at v), the carrier of IIG]) in rng (Den ((action_at v),SCS)) by A6, A17, A13, FUNCT_1:def 3;

Result ((action_at v),SCS) = ( the Sorts of SCS * the ResultSort of IIG) . (action_at v) by MSUALG_1:def 5

.= the Sorts of SCS . ( the ResultSort of IIG . (action_at v)) by A4, FUNCT_1:13 ;

then reconsider e = ((Eval SCS) . v) . (root-tree [(action_at v), the carrier of IIG]) as Element of the Sorts of SCS . v by A6, A17, A13, MSUALG_1:def 2;

ex A being non empty set st

( A = the Sorts of SCS . v & Constants (SCS,v) = { a where a is Element of A : ex o being OperSymbol of IIG st

( the Arity of IIG . o = {} & the ResultSort of IIG . o = v & a in rng (Den (o,SCS)) ) } ) by MSUALG_2:def 3;

then A19: e in Constants (SCS,v) by A7, A9, A10, A11, A18;

ex e being Element of the Sorts of (FreeEnv SCS) . v st

( card e = size (v,SCS) & IGTree (v,iv) = ((Fix_inp_ext iv) . v) . e ) by Def3;

hence IGValue (v,iv) = e by A1, Th5

.= (Set-Constants SCS) . v by A1, A19, CIRCUIT1:1 ;

:: thesis: verum

for v being Vertex of IIG

for iv being InputValues of SCS st v in SortsWithConstants IIG holds

IGValue (v,iv) = (Set-Constants SCS) . v

reconsider p = {} as DTree-yielding FinSequence ;

let SCS be non-empty Circuit of IIG; :: thesis: for v being Vertex of IIG

for iv being InputValues of SCS st v in SortsWithConstants IIG holds

IGValue (v,iv) = (Set-Constants SCS) . v

let v be Vertex of IIG; :: thesis: for iv being InputValues of SCS st v in SortsWithConstants IIG holds

IGValue (v,iv) = (Set-Constants SCS) . v

let iv be InputValues of SCS; :: thesis: ( v in SortsWithConstants IIG implies IGValue (v,iv) = (Set-Constants SCS) . v )

assume A1: v in SortsWithConstants IIG ; :: thesis: IGValue (v,iv) = (Set-Constants SCS) . v

set e = ((Eval SCS) . v) . (root-tree [(action_at v), the carrier of IIG]);

A2: {} = <*> the carrier of IIG ;

set X = the Sorts of SCS;

set F = Eval SCS;

A3: dom the Arity of IIG = the carrier' of IIG by FUNCT_2:def 1;

A4: dom the ResultSort of IIG = the carrier' of IIG by FUNCT_2:def 1;

set o = action_at v;

A5: SortsWithConstants IIG c= InnerVertices IIG by MSAFREE2:3;

then A6: v = the_result_sort_of (action_at v) by A1, MSAFREE2:def 7;

SortsWithConstants IIG = { v1 where v1 is SortSymbol of IIG : v1 is with_const_op } by MSAFREE2:def 1;

then consider x9 being SortSymbol of IIG such that

A7: x9 = v and

A8: x9 is with_const_op by A1;

consider o1 being OperSymbol of IIG such that

A9: the Arity of IIG . o1 = {} and

A10: the ResultSort of IIG . o1 = x9 by A8, MSUALG_2:def 1;

the ResultSort of IIG . o1 = the_result_sort_of o1 by MSUALG_1:def 2;

then A11: action_at v = o1 by A1, A5, A7, A10, MSAFREE2:def 7;

A12: Args ((action_at v),(FreeEnv SCS)) = (( the Sorts of (FreeEnv SCS) #) * the Arity of IIG) . (action_at v) by MSUALG_1:def 4

.= ( the Sorts of (FreeEnv SCS) #) . ( the Arity of IIG . (action_at v)) by A3, FUNCT_1:13

.= {{}} by A9, A11, A2, PRE_CIRC:2 ;

then reconsider x = {} as Element of Args ((action_at v),(FreeEnv SCS)) by TARSKI:def 1;

reconsider Fx = (Eval SCS) # x as Element of Args ((action_at v),SCS) ;

Eval SCS is_homomorphism FreeEnv SCS,SCS by MSAFREE2:def 9;

then A13: ((Eval SCS) . (the_result_sort_of (action_at v))) . ((Den ((action_at v),(FreeEnv SCS))) . x) = (Den ((action_at v),SCS)) . Fx by MSUALG_3:def 7;

A14: FreeMSA the Sorts of SCS = MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #) by MSAFREE:def 14;

then A15: Den ((action_at v),(FreeEnv SCS)) = (FreeOper the Sorts of SCS) . (action_at v) by MSUALG_1:def 6

.= DenOp ((action_at v), the Sorts of SCS) by MSAFREE:def 13 ;

{} in Args ((action_at v),(FreeEnv SCS)) by A12, TARSKI:def 1;

then A16: p in (((FreeSort the Sorts of SCS) #) * the Arity of IIG) . (action_at v) by A14, MSUALG_1:def 4;

then reconsider p9 = {} as FinSequence of TS (DTConMSA the Sorts of SCS) by MSAFREE:8;

Sym ((action_at v), the Sorts of SCS) ==> roots p9 by A16, MSAFREE:10;

then A17: (Den ((action_at v),(FreeEnv SCS))) . {} = (Sym ((action_at v), the Sorts of SCS)) -tree p by A15, MSAFREE:def 12

.= [(action_at v), the carrier of IIG] -tree {} by MSAFREE:def 9

.= root-tree [(action_at v), the carrier of IIG] by TREES_4:20 ;

dom (Den ((action_at v),SCS)) = Args ((action_at v),SCS) by FUNCT_2:def 1;

then A18: ((Eval SCS) . v) . (root-tree [(action_at v), the carrier of IIG]) in rng (Den ((action_at v),SCS)) by A6, A17, A13, FUNCT_1:def 3;

Result ((action_at v),SCS) = ( the Sorts of SCS * the ResultSort of IIG) . (action_at v) by MSUALG_1:def 5

.= the Sorts of SCS . ( the ResultSort of IIG . (action_at v)) by A4, FUNCT_1:13 ;

then reconsider e = ((Eval SCS) . v) . (root-tree [(action_at v), the carrier of IIG]) as Element of the Sorts of SCS . v by A6, A17, A13, MSUALG_1:def 2;

ex A being non empty set st

( A = the Sorts of SCS . v & Constants (SCS,v) = { a where a is Element of A : ex o being OperSymbol of IIG st

( the Arity of IIG . o = {} & the ResultSort of IIG . o = v & a in rng (Den (o,SCS)) ) } ) by MSUALG_2:def 3;

then A19: e in Constants (SCS,v) by A7, A9, A10, A11, A18;

ex e being Element of the Sorts of (FreeEnv SCS) . v st

( card e = size (v,SCS) & IGTree (v,iv) = ((Fix_inp_ext iv) . v) . e ) by Def3;

hence IGValue (v,iv) = e by A1, Th5

.= (Set-Constants SCS) . v by A1, A19, CIRCUIT1:1 ;

:: thesis: verum