let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ((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 ) ) ) ;

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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ((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;

end;

( 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 A4:
ex x being set st

( x in the Sorts of A . v & e = root-tree [x,v] ) ; :: thesis: ((Fix_inp_ext iv) . v) . e = root-tree [(action_at v), the carrier of IIG]

( x in the Sorts of A . v & e = root-tree [x,v] ) ; :: thesis: ((Fix_inp_ext iv) . v) . e = root-tree [(action_at v), the carrier of IIG]

Fix_inp iv c= Fix_inp_ext iv
by Def2;

then A5: (Fix_inp iv) . v c= (Fix_inp_ext iv) . v ;

A6: 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 A5, GRFUNC_1:2

.= ((FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG])) . e by A1, Def1

.= root-tree [(action_at v), the carrier of IIG] by A6, FUNCOP_1:7 ;

:: thesis: verum

end;then A5: (Fix_inp iv) . v c= (Fix_inp_ext iv) . v ;

A6: 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 A5, GRFUNC_1:2

.= ((FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG])) . e by A1, Def1

.= root-tree [(action_at v), the carrier of IIG] by A6, FUNCOP_1:7 ;

:: thesis: verum

suppose
ex o being OperSymbol of IIG st

( [o, the carrier of IIG] = e . {} & the_result_sort_of o = v ) ; :: thesis: ((Fix_inp_ext iv) . v) . e = root-tree [(action_at v), the carrier of IIG]

( [o, the carrier of IIG] = e . {} & the_result_sort_of o = v ) ; :: thesis: ((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; :: thesis: verum

end;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; :: thesis: verum