:: CIRCUIT2 semantic presentation

begin

 Lm1:  for x being set holds not x in x
;

theorem Th1: :: CIRCUIT2:1
for IIG being non empty non void Circuit-like monotonic ManySortedSign
for X being V2() ManySortedSet of the carrier of IIG
for H being ManySortedFunction of (FreeMSA X),(FreeMSA X)
for HH being Function-yielding Function
for v being SortSymbol of IIG
for p being DTree-yielding FinSequence
for t being Element of the Sorts of (FreeMSA X) . v st v in InnerVertices IIG & t = [(action_at v), the carrier of IIG] -tree p & H is_homomorphism FreeMSA X, FreeMSA X & HH = H * (the_arity_of (action_at v)) holds
ex HHp being DTree-yielding FinSequence st
( HHp = HH .. p & (H . v) . t = [(action_at v), the carrier of IIG] -tree HHp )
proof
let IIG be non empty non void Circuit-like monotonic ManySortedSign ; ::_thesis: for X being V2() ManySortedSet of the carrier of IIG
for H being ManySortedFunction of (FreeMSA X),(FreeMSA X)
for HH being Function-yielding Function
for v being SortSymbol of IIG
for p being DTree-yielding FinSequence
for t being Element of the Sorts of (FreeMSA X) . v st v in InnerVertices IIG & t = [(action_at v), the carrier of IIG] -tree p & H is_homomorphism FreeMSA X, FreeMSA X & HH = H * (the_arity_of (action_at v)) holds
ex HHp being DTree-yielding FinSequence st
( HHp = HH .. p & (H . v) . t = [(action_at v), the carrier of IIG] -tree HHp )
let X be V2() ManySortedSet of the carrier of IIG; ::_thesis: for H being ManySortedFunction of (FreeMSA X),(FreeMSA X)
for HH being Function-yielding Function
for v being SortSymbol of IIG
for p being DTree-yielding FinSequence
for t being Element of the Sorts of (FreeMSA X) . v st v in InnerVertices IIG & t = [(action_at v), the carrier of IIG] -tree p & H is_homomorphism FreeMSA X, FreeMSA X & HH = H * (the_arity_of (action_at v)) holds
ex HHp being DTree-yielding FinSequence st
( HHp = HH .. p & (H . v) . t = [(action_at v), the carrier of IIG] -tree HHp )
let H be ManySortedFunction of (FreeMSA X),(FreeMSA X); ::_thesis: for HH being Function-yielding Function
for v being SortSymbol of IIG
for p being DTree-yielding FinSequence
for t being Element of the Sorts of (FreeMSA X) . v st v in InnerVertices IIG & t = [(action_at v), the carrier of IIG] -tree p & H is_homomorphism FreeMSA X, FreeMSA X & HH = H * (the_arity_of (action_at v)) holds
ex HHp being DTree-yielding FinSequence st
( HHp = HH .. p & (H . v) . t = [(action_at v), the carrier of IIG] -tree HHp )
let HH be Function-yielding Function; ::_thesis: for v being SortSymbol of IIG
for p being DTree-yielding FinSequence
for t being Element of the Sorts of (FreeMSA X) . v st v in InnerVertices IIG & t = [(action_at v), the carrier of IIG] -tree p & H is_homomorphism FreeMSA X, FreeMSA X & HH = H * (the_arity_of (action_at v)) holds
ex HHp being DTree-yielding FinSequence st
( HHp = HH .. p & (H . v) . t = [(action_at v), the carrier of IIG] -tree HHp )
let v be SortSymbol of IIG; ::_thesis: for p being DTree-yielding FinSequence
for t being Element of the Sorts of (FreeMSA X) . v st v in InnerVertices IIG & t = [(action_at v), the carrier of IIG] -tree p & H is_homomorphism FreeMSA X, FreeMSA X & HH = H * (the_arity_of (action_at v)) holds
ex HHp being DTree-yielding FinSequence st
( HHp = HH .. p & (H . v) . t = [(action_at v), the carrier of IIG] -tree HHp )
let p be DTree-yielding FinSequence; ::_thesis: for t being Element of the Sorts of (FreeMSA X) . v st v in InnerVertices IIG & t = [(action_at v), the carrier of IIG] -tree p & H is_homomorphism FreeMSA X, FreeMSA X & HH = H * (the_arity_of (action_at v)) holds
ex HHp being DTree-yielding FinSequence st
( HHp = HH .. p & (H . v) . t = [(action_at v), the carrier of IIG] -tree HHp )
let t be Element of the Sorts of (FreeMSA X) . v; ::_thesis: ( v in InnerVertices IIG & t = [(action_at v), the carrier of IIG] -tree p & H is_homomorphism FreeMSA X, FreeMSA X & HH = H * (the_arity_of (action_at v)) implies ex HHp being DTree-yielding FinSequence st
( HHp = HH .. p & (H . v) . t = [(action_at v), the carrier of IIG] -tree HHp ) )
assume that
A1: v in InnerVertices IIG and
A2: t = [(action_at v), the carrier of IIG] -tree p and
A3: H is_homomorphism FreeMSA X, FreeMSA X and
A4: HH = H * (the_arity_of (action_at v)) ; ::_thesis: ex HHp being DTree-yielding FinSequence st
( HHp = HH .. p & (H . v) . t = [(action_at v), the carrier of IIG] -tree HHp )
reconsider av = action_at v as OperSymbol of IIG ;
A5: the_result_sort_of av = v by A1, MSAFREE2:def_7;
then  len p = len (the_arity_of av) by A2, MSAFREE2:10;
then A6: dom p = dom (the_arity_of av) by FINSEQ_3:29;
A7: rng (the_arity_of av) c= the carrier of IIG by FINSEQ_1:def_4;
then A8: rng (the_arity_of av) c= dom H by PARTFUN1:def_2;
then A9: dom (the_arity_of av) = dom HH by A4, RELAT_1:27;
A10: FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def_14;
then  the Sorts of (FreeMSA X) . v = FreeSort (X,v) by MSAFREE:def_11;
then  [av, the carrier of IIG] -tree p in FreeSort (X,v) by A2;
then A11: [av, the carrier of IIG] -tree p in  {  a where a is Element of TS (DTConMSA X) : ( ex x being set st
( x in X . 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;
reconsider HHp = HH .. p as Function ;
A12: dom HHp = dom HH by PRALG_1:def_17;
 H * (the_arity_of av) is FinSequence by A8, FINSEQ_1:16;
then  ex n being Nat st dom HH = Seg n by A4, FINSEQ_1:def_2;
then reconsider HHp = HHp as FinSequence by A12, FINSEQ_1:def_2;
A13: now__::_thesis:_for_x9_being_set_st_x9_in_dom_HHp_holds_
HHp_._x9_is_DecoratedTree
reconsider HH9 = HH as FinSequence by A4, A8, FINSEQ_1:16;
let x9 be set ; ::_thesis: ( x9 in dom HHp implies HHp . x9 is DecoratedTree )
set x = HHp . x9;
reconsider g = HH . x9 as Function ;
assume A14: x9 in dom HHp ; ::_thesis: HHp . x9 is DecoratedTree
then reconsider k = x9 as Element of NAT ;
A15: HHp . x9 = g . (p . k) by A12, A14, PRALG_1:def_17;
 len HH9 = len (the_arity_of av) by A4, A8, FINSEQ_2:29;
then A16: dom HH9 = dom (the_arity_of av) by FINSEQ_3:29;
then reconsider s = (the_arity_of av) . k as SortSymbol of IIG by A12, A14, FINSEQ_2:11;
 g = H . s by A4, A12, A14, A16, FUNCT_1:13;
then  HHp . x9 in the Sorts of (FreeMSA X) . s by A2, A12, A5, A14, A16, A15, FUNCT_2:5, MSAFREE2:11;
hence  HHp . x9 is DecoratedTree ; ::_thesis: verum
end;
set f = the Sorts of (FreeMSA X) * (the_arity_of av);
 dom the Arity of IIG = the carrier' of IIG by FUNCT_2:def_1;
then A17: (( the Sorts of (FreeMSA X) #) * the Arity of IIG) . av = ( the Sorts of (FreeMSA X) #) . ( the Arity of IIG . av) by FUNCT_1:13
.= ( the Sorts of (FreeMSA X) #) . (the_arity_of av) by MSUALG_1:def_1
.= product ( the Sorts of (FreeMSA X) * (the_arity_of av)) by FINSEQ_2:def_5 ;
reconsider HHp = HHp as DTree-yielding FinSequence by A13, TREES_3:24;
consider a being Element of TS (DTConMSA X) such that
A18: a = [av, the carrier of IIG] -tree p and
A19: ( ex x being set st
( x in X . 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 A11;
consider x9 being set  such that
A20: ( ( x9 in X . v & a = root-tree [x9,v] ) or ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a . {} & the_result_sort_of o = v ) ) by A19;
 dom the Sorts of (FreeMSA X) = the carrier of IIG by PARTFUN1:def_2;
then A21: dom ( the Sorts of (FreeMSA X) * (the_arity_of av)) = dom (the_arity_of av) by A7, RELAT_1:27;
now__::_thesis:_for_x_being_set_st_x_in_dom_(_the_Sorts_of_(FreeMSA_X)_*_(the_arity_of_av))_holds_
p_._x_in_(_the_Sorts_of_(FreeMSA_X)_*_(the_arity_of_av))_._x
let x be set ; ::_thesis: ( x in dom ( the Sorts of (FreeMSA X) * (the_arity_of av)) implies p . x in ( the Sorts of (FreeMSA X) * (the_arity_of av)) . x )
assume A22: x in dom ( the Sorts of (FreeMSA X) * (the_arity_of av)) ; ::_thesis: p . x in ( the Sorts of (FreeMSA X) * (the_arity_of av)) . x
then reconsider n = x as Element of NAT by A21;
 (the_arity_of av) . x in rng (the_arity_of av) by A21, A22, FUNCT_1:def_3;
then reconsider s = (the_arity_of av) . x as SortSymbol of IIG by A7;
 ( n in dom (the_arity_of av) & ( the Sorts of (FreeMSA X) * (the_arity_of av)) . x = the Sorts of (FreeMSA X) . s ) by A21, A22, FUNCT_1:13;
hence  p . x in ( the Sorts of (FreeMSA X) * (the_arity_of av)) . x by A2, A5, MSAFREE2:11; ::_thesis: verum
end;
then  p in (( the Sorts of (FreeMSA X) #) * the Arity of IIG) . av by A17, A21, A6, CARD_3:def_5;
then reconsider x = p as Element of Args (av,(FreeMSA X)) by MSUALG_1:def_4;
A23: a . {} = [av, the carrier of IIG] by A18, TREES_4:def_4;
reconsider Hx = H # x as Function ;
A24: now__::_thesis:_for_x9_being_set_st_x9_in_dom_HH_holds_
Hx_._x9_=_(HH_._x9)_._(p_._x9)
let x9 be set ; ::_thesis: ( x9 in dom HH implies Hx . x9 = (HH . x9) . (p . x9) )
assume A25: x9 in dom HH ; ::_thesis: Hx . x9 = (HH . x9) . (p . x9)
then reconsider n = x9 as Element of NAT by A9;
 (the_arity_of av) . n in rng (the_arity_of av) by A9, A25, FUNCT_1:def_3;
then reconsider s = (the_arity_of av) . n as SortSymbol of IIG by A7;
Hx . n = (H . ((the_arity_of av) /. n)) . (p . n) by A9, A6, A25, MSUALG_3:def_6
.= (H . s) . (p . n) by A9, A25, PARTFUN1:def_6 ;
hence  Hx . x9 = (HH . x9) . (p . x9) by A4, A9, A25, FUNCT_1:13; ::_thesis: verum
end;
 dom Hx = dom HH by A9, MSUALG_3:6;
then A26: HHp = H # x by A24, PRALG_1:def_17;
now__::_thesis:_not_a_=_root-tree_[x9,v]
assume  a = root-tree [x9,v] ; ::_thesis: contradiction
then A27: a . {} = [x9,v] by TREES_4:3;
 a . {} = [av, the carrier of IIG] by A18, TREES_4:def_4;
then  the carrier of IIG = v by A27, XTUPLE_0:1;
hence  contradiction by Lm1; ::_thesis: verum
end;
then consider o being OperSymbol of IIG such that
A28: [o, the carrier of IIG] = a . {} and
 the_result_sort_of o = v by A20;
 the carrier of IIG in { the carrier of IIG} by TARSKI:def_1;
then  [o, the carrier of IIG] in [: the carrier' of IIG,{ the carrier of IIG}:] by ZFMISC_1:87;
then reconsider nt = [o, the carrier of IIG] as NonTerminal of (DTConMSA X) by MSAFREE:6;
consider ts being FinSequence of TS (DTConMSA X) such that
A29: a = nt -tree ts and
A30: nt ==> roots ts by A28, DTCONSTR:10;
take  HHp ; ::_thesis: ( HHp = HH .. p & (H . v) . t = [(action_at v), the carrier of IIG] -tree HHp )
thus  HHp = HH .. p ; ::_thesis: (H . v) . t = [(action_at v), the carrier of IIG] -tree HHp
A31: Sym (av,X) = [av, the carrier of IIG] by MSAFREE:def_9;
now__::_thesis:_for_x_being_set_st_x_in_dom_(_the_Sorts_of_(FreeMSA_X)_*_(the_arity_of_av))_holds_
HHp_._x_in_(_the_Sorts_of_(FreeMSA_X)_*_(the_arity_of_av))_._x
let x be set ; ::_thesis: ( x in dom ( the Sorts of (FreeMSA X) * (the_arity_of av)) implies HHp . x in ( the Sorts of (FreeMSA X) * (the_arity_of av)) . x )
reconsider g = HH . x as Function ;
assume A32: x in dom ( the Sorts of (FreeMSA X) * (the_arity_of av)) ; ::_thesis: HHp . x in ( the Sorts of (FreeMSA X) * (the_arity_of av)) . x
then A33: HHp . x = g . (p . x) by A21, A9, PRALG_1:def_17;
 (the_arity_of av) . x in rng (the_arity_of av) by A21, A32, FUNCT_1:def_3;
then reconsider s = (the_arity_of av) . x as SortSymbol of IIG by A7;
A34: the_result_sort_of av = v by A1, MSAFREE2:def_7;
 ( ( the Sorts of (FreeMSA X) * (the_arity_of av)) . x = the Sorts of (FreeMSA X) . s & g = H . s ) by A4, A21, A32, FUNCT_1:13;
hence  HHp . x in ( the Sorts of (FreeMSA X) * (the_arity_of av)) . x by A2, A21, A32, A34, A33, FUNCT_2:5, MSAFREE2:11; ::_thesis: verum
end;
then A35: HHp in (((FreeSort X) #) * the Arity of IIG) . av by A12, A17, A21, A9, A10, CARD_3:def_5;
then reconsider HHp9 = HHp as FinSequence of TS (DTConMSA X) by MSAFREE:8;
A36: Sym (av,X) ==> roots HHp9 by A35, MSAFREE:10;
reconsider p9 = p as FinSequence of TS (DTConMSA X) by A18, A29, TREES_4:15;
 ts = p by A18, A29, TREES_4:15;
then A37: (DenOp (av,X)) . p9 = t by A2, A28, A23, A30, A31, MSAFREE:def_12;
Den (av,(FreeMSA X)) = (FreeOper X) . av by A10, MSUALG_1:def_6
.= DenOp (av,X) by MSAFREE:def_13 ;
hence (H . v) . t = (DenOp (av,X)) . HHp by A3, A5, A37, A26, MSUALG_3:def_7
.= [(action_at v), the carrier of IIG] -tree HHp by A31, A36, MSAFREE:def_12 ;
::_thesis: verum
end;

definition
let IIG be non empty non void Circuit-like monotonic ManySortedSign ;
let SCS be non-empty Circuit of IIG;
let s be State of SCS;
let iv be InputValues of SCS;
:: original: +*
redefine funcs +* iv ->  State of SCS;
coherence
 s +* iv is State of SCS
proof
A1: dom iv = InputVertices IIG by PARTFUN1:def_2;
then  ( dom the Sorts of SCS = the carrier of IIG & ( for x being set st x in dom iv holds
iv . x in the Sorts of SCS . x ) ) by MSAFREE2:def_5, PARTFUN1:def_2;
hence  s +* iv is State of SCS by A1, PRE_CIRC:6; ::_thesis: verum
end;
end;

definition
let IIG be non empty non void Circuit-like monotonic ManySortedSign ;
let A be non-empty Circuit of IIG;
let iv be InputValues of A;
func Fix_inp iv ->  ManySortedFunction of FreeGen the Sorts of A, the Sorts of (FreeEnv A) means :Def1: :: CIRCUIT2:def 1
 for v being Vertex of IIG holds
( ( v in InputVertices IIG implies it . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies it . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies it . v = id (FreeGen (v, the Sorts of A)) ) );
existence
 ex b1 being ManySortedFunction of FreeGen the Sorts of A, the Sorts of (FreeEnv A) st
for v being Vertex of IIG holds
( ( v in InputVertices IIG implies b1 . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies b1 . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies b1 . v = id (FreeGen (v, the Sorts of A)) ) )
proof
defpred S1[ set , set ] means  ex v being Vertex of IIG st
( v = $1 & ( $1 in InputVertices IIG implies $2 = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( $1 in SortsWithConstants IIG implies $2 = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( $1 in (InnerVertices IIG) \ (SortsWithConstants IIG) implies $2 = id (FreeGen (v, the Sorts of A)) ) );
A1: now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_IIG_holds_
ex_j_being_set_st_S1[i,j]
let i be set ; ::_thesis: ( i in the carrier of IIG implies ex j being set st S1[i,j] )
assume A2: i in the carrier of IIG ; ::_thesis: ex j being set st S1[i,j]
then reconsider v = i as Vertex of IIG ;
 v in (InputVertices IIG) \/ (InnerVertices IIG) by A2, XBOOLE_1:45;
then A3: ( v in InputVertices IIG or v in InnerVertices IIG ) by XBOOLE_0:def_3;
A4: ((InnerVertices IIG) \ (SortsWithConstants IIG)) \/ (SortsWithConstants IIG) = InnerVertices IIG by MSAFREE2:3, XBOOLE_1:45;
thus  ex j being set st S1[i,j] ::_thesis: verum
proof
percases ( v in InputVertices IIG or v in SortsWithConstants IIG or v in (InnerVertices IIG) \ (SortsWithConstants IIG) ) by A4, A3, XBOOLE_0:def_3;
supposeA5: v in InputVertices IIG ; ::_thesis: ex j being set st S1[i,j]
reconsider j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) as set ;
take  j ; ::_thesis: S1[i,j]
take  v ; ::_thesis: ( v = i & ( i in InputVertices IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) ) )
thus  v = i ; ::_thesis: ( ( i in InputVertices IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) ) )
thus  ( i in InputVertices IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) ; ::_thesis: ( ( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) ) )
hereby  ::_thesis: ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) )
A6: InputVertices IIG misses SortsWithConstants IIG by MSAFREE2:4;
assume  i in SortsWithConstants IIG ; ::_thesis: j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG])
hence  j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) by A5, A6, XBOOLE_0:3; ::_thesis: verum
end;
A7: ( (InnerVertices IIG) \ (SortsWithConstants IIG) c= InnerVertices IIG & InputVertices IIG misses InnerVertices IIG ) by XBOOLE_1:36, XBOOLE_1:79;
assume  i in (InnerVertices IIG) \ (SortsWithConstants IIG) ; ::_thesis: j = id (FreeGen (v, the Sorts of A))
hence  j = id (FreeGen (v, the Sorts of A)) by A5, A7, XBOOLE_0:3; ::_thesis: verum
end;
supposeA8: v in SortsWithConstants IIG ; ::_thesis: ex j being set st S1[i,j]
reconsider j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) as set ;
take  j ; ::_thesis: S1[i,j]
take  v ; ::_thesis: ( v = i & ( i in InputVertices IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) ) )
thus  v = i ; ::_thesis: ( ( i in InputVertices IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) ) )
hereby  ::_thesis: ( ( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) ) )
A9: InputVertices IIG misses SortsWithConstants IIG by MSAFREE2:4;
assume  i in InputVertices IIG ; ::_thesis: j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v])
hence  j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) by A8, A9, XBOOLE_0:3; ::_thesis: verum
end;
thus  ( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) ; ::_thesis: ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) )
A10: (InnerVertices IIG) \ (SortsWithConstants IIG) misses SortsWithConstants IIG by XBOOLE_1:79;
assume  i in (InnerVertices IIG) \ (SortsWithConstants IIG) ; ::_thesis: j = id (FreeGen (v, the Sorts of A))
hence  j = id (FreeGen (v, the Sorts of A)) by A8, A10, XBOOLE_0:3; ::_thesis: verum
end;
supposeA11: v in (InnerVertices IIG) \ (SortsWithConstants IIG) ; ::_thesis: ex j being set st S1[i,j]
reconsider j = id (FreeGen (v, the Sorts of A)) as set ;
take  j ; ::_thesis: S1[i,j]
take  v ; ::_thesis: ( v = i & ( i in InputVertices IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) ) )
thus  v = i ; ::_thesis: ( ( i in InputVertices IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) ) )
hereby  ::_thesis: ( ( i in SortsWithConstants IIG implies j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) ) )
A12: ( (InnerVertices IIG) \ (SortsWithConstants IIG) c= InnerVertices IIG & InputVertices IIG misses InnerVertices IIG ) by XBOOLE_1:36, XBOOLE_1:79;
assume  i in InputVertices IIG ; ::_thesis: j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v])
hence  j = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) by A11, A12, XBOOLE_0:3; ::_thesis: verum
end;
hereby  ::_thesis: ( i in (InnerVertices IIG) \ (SortsWithConstants IIG) implies j = id (FreeGen (v, the Sorts of A)) )
A13: (InnerVertices IIG) \ (SortsWithConstants IIG) misses SortsWithConstants IIG by XBOOLE_1:79;
assume  i in SortsWithConstants IIG ; ::_thesis: j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG])
hence  j = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) by A11, A13, XBOOLE_0:3; ::_thesis: verum
end;
assume  i in (InnerVertices IIG) \ (SortsWithConstants IIG) ; ::_thesis: j = id (FreeGen (v, the Sorts of A))
thus  j = id (FreeGen (v, the Sorts of A)) ; ::_thesis: verum
end;
end;
end;
end;
consider M being ManySortedSet of the carrier of IIG such that
A14: for i being set st i in the carrier of IIG holds
S1[i,M . i] from PBOOLE:sch_3(A1);
A15: now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_IIG_holds_
M_._i_is_Function_of_((FreeGen_the_Sorts_of_A)_._i),(_the_Sorts_of_(FreeEnv_A)_._i)
let i be set ; ::_thesis: ( i in the carrier of IIG implies M . b1 is Function of ((FreeGen the Sorts of A) . b1),( the Sorts of (FreeEnv A) . b1) )
A16: ((InnerVertices IIG) \ (SortsWithConstants IIG)) \/ (SortsWithConstants IIG) = InnerVertices IIG by MSAFREE2:3, XBOOLE_1:45;
assume A17: i in the carrier of IIG ; ::_thesis: M . b1 is Function of ((FreeGen the Sorts of A) . b1),( the Sorts of (FreeEnv A) . b1)
then reconsider v = i as Vertex of IIG ;
 v in (InputVertices IIG) \/ (InnerVertices IIG) by A17, XBOOLE_1:45;
then A18: ( v in InputVertices IIG or v in InnerVertices IIG ) by XBOOLE_0:def_3;
A19: FreeGen (v, the Sorts of A) = (FreeGen the Sorts of A) . v by MSAFREE:def_16;
A20: FreeEnv A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #) by MSAFREE:def_14;
percases ( v in InputVertices IIG or v in SortsWithConstants IIG or v in (InnerVertices IIG) \ (SortsWithConstants IIG) ) by A16, A18, XBOOLE_0:def_3;
supposeA21: v in InputVertices IIG ; ::_thesis: M . b1 is Function of ((FreeGen the Sorts of A) . b1),( the Sorts of (FreeEnv A) . b1)
then  iv . v in the Sorts of A . v by MSAFREE2:def_5;
then A22: root-tree [(iv . v),v] in FreeGen (v, the Sorts of A) by MSAFREE:def_15;
 S1[v,M . v] by A14;
hence  M . i is Function of ((FreeGen the Sorts of A) . i),( the Sorts of (FreeEnv A) . i) by A19, A20, A21, A22, FUNCOP_1:45; ::_thesis: verum
end;
supposeA23: v in SortsWithConstants IIG ; ::_thesis: M . b1 is Function of ((FreeGen the Sorts of A) . b1),( the Sorts of (FreeEnv A) . b1)
reconsider sy = Sym ((action_at v), the Sorts of A) as NonTerminal of (DTConMSA the Sorts of A) ;
set p = <*> (TS (DTConMSA the Sorts of A));
set e = root-tree [(action_at v), the carrier of IIG];
A24: SortsWithConstants IIG c= InnerVertices IIG by MSAFREE2:3;
 v in  {  s where s is SortSymbol of IIG : s is with_const_op  }  by A23, 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
A25: the Arity of IIG . o = {} and
A26: the ResultSort of IIG . o = v by MSUALG_2:def_1;
A27: for n being Nat st n in dom (<*> (TS (DTConMSA the Sorts of A))) holds
(<*> (TS (DTConMSA the Sorts of A))) . n in FreeSort ( the Sorts of A,((the_arity_of o) /. n)) ;
 <*> (TS (DTConMSA the Sorts of A)) = the_arity_of o by A25, MSUALG_1:def_1;
then A28: <*> (TS (DTConMSA the Sorts of A)) in (((FreeSort the Sorts of A) #) * the Arity of IIG) . o by A27, MSAFREE:9;
 the_result_sort_of o = v by A26, MSUALG_1:def_2;
then  o = action_at v by A23, A24, MSAFREE2:def_7;
then  sy ==> roots (<*> (TS (DTConMSA the Sorts of A))) by A28, MSAFREE:10;
then  ( {} = <*> (IIG -Terms the Sorts of A) & <*> (TS (DTConMSA the Sorts of A)) is SubtreeSeq of Sym ((action_at v), the Sorts of A) ) by DTCONSTR:def_6;
then  ( root-tree [(action_at v), the carrier of IIG] = [(action_at v), the carrier of IIG] -tree {} & {} is ArgumentSeq of sy ) by MSATERM:def_2, TREES_4:20;
then  root-tree [(action_at v), the carrier of IIG] in IIG -Terms the Sorts of A by MSATERM:1;
then reconsider e = root-tree [(action_at v), the carrier of IIG] as Element of TS (DTConMSA the Sorts of A) by MSATERM:def_1;
 ( e . {} = [(action_at v), the carrier of IIG] & the_result_sort_of (action_at v) = v ) by A23, A24, MSAFREE2:def_7, TREES_4:3;
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 ) )  }  ;
then  e in FreeSort ( the Sorts of A,v) by MSAFREE:def_10;
then A29: e in the Sorts of (FreeEnv A) . v by A20, MSAFREE:def_11;
 S1[v,M . v] by A14;
hence  M . i is Function of ((FreeGen the Sorts of A) . i),( the Sorts of (FreeEnv A) . i) by A19, A23, A29, FUNCOP_1:45; ::_thesis: verum
end;
supposeA30: v in (InnerVertices IIG) \ (SortsWithConstants IIG) ; ::_thesis: M . b1 is Function of ((FreeGen the Sorts of A) . b1),( the Sorts of (FreeEnv A) . b1)
A31: ( dom (id (FreeGen (v, the Sorts of A))) = FreeGen (v, the Sorts of A) & rng (id (FreeGen (v, the Sorts of A))) = FreeGen (v, the Sorts of A) ) ;
 S1[v,M . v] by A14;
hence  M . i is Function of ((FreeGen the Sorts of A) . i),( the Sorts of (FreeEnv A) . i) by A19, A20, A30, A31, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;
end;
end;
now__::_thesis:_for_i_being_set_st_i_in_dom_M_holds_
M_._i_is_Function
let i be set ; ::_thesis: ( i in dom M implies M . i is Function )
assume  i in dom M ; ::_thesis: M . i is Function
then  i in the carrier of IIG by PARTFUN1:def_2;
hence  M . i is Function by A15; ::_thesis: verum
end;
then reconsider M = M as ManySortedFunction of the carrier of IIG by FUNCOP_1:def_6;
reconsider M = M as ManySortedFunction of FreeGen the Sorts of A, the Sorts of (FreeEnv A) by A15, PBOOLE:def_15;
take  M ; ::_thesis: for v being Vertex of IIG holds
( ( v in InputVertices IIG implies M . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies M . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies M . v = id (FreeGen (v, the Sorts of A)) ) )
let v be Vertex of IIG; ::_thesis: ( ( v in InputVertices IIG implies M . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies M . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies M . v = id (FreeGen (v, the Sorts of A)) ) )
hereby  ::_thesis: ( ( v in SortsWithConstants IIG implies M . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies M . v = id (FreeGen (v, the Sorts of A)) ) )
assume A32: v in InputVertices IIG ; ::_thesis: M . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v])
 S1[v,M . v] by A14;
hence  M . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) by A32; ::_thesis: verum
end;
hereby  ::_thesis: ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies M . v = id (FreeGen (v, the Sorts of A)) )
assume A33: v in SortsWithConstants IIG ; ::_thesis: M . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG])
 S1[v,M . v] by A14;
hence  M . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) by A33; ::_thesis: verum
end;
assume A34: v in (InnerVertices IIG) \ (SortsWithConstants IIG) ; ::_thesis: M . v = id (FreeGen (v, the Sorts of A))
 S1[v,M . v] by A14;
hence  M . v = id (FreeGen (v, the Sorts of A)) by A34; ::_thesis: verum
end;
uniqueness
 for b1, b2 being ManySortedFunction of FreeGen the Sorts of A, the Sorts of (FreeEnv A) st ( for v being Vertex of IIG holds
( ( v in InputVertices IIG implies b1 . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies b1 . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies b1 . v = id (FreeGen (v, the Sorts of A)) ) ) ) & ( for v being Vertex of IIG holds
( ( v in InputVertices IIG implies b2 . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies b2 . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies b2 . v = id (FreeGen (v, the Sorts of A)) ) ) ) holds
b1 = b2
proof
let M1, M2 be ManySortedFunction of FreeGen the Sorts of A, the Sorts of (FreeEnv A); ::_thesis: ( ( for v being Vertex of IIG holds
( ( v in InputVertices IIG implies M1 . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies M1 . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies M1 . v = id (FreeGen (v, the Sorts of A)) ) ) ) & ( for v being Vertex of IIG holds
( ( v in InputVertices IIG implies M2 . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies M2 . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies M2 . v = id (FreeGen (v, the Sorts of A)) ) ) ) implies M1 = M2 )
assume that
A35: for v being Vertex of IIG holds
( ( v in InputVertices IIG implies M1 . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies M1 . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies M1 . v = id (FreeGen (v, the Sorts of A)) ) ) and
A36: for v being Vertex of IIG holds
( ( v in InputVertices IIG implies M2 . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies M2 . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies M2 . v = id (FreeGen (v, the Sorts of A)) ) ) ; ::_thesis: M1 = M2
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_IIG_holds_
M1_._i_=_M2_._i
let i be set ; ::_thesis: ( i in the carrier of IIG implies M1 . b1 = M2 . b1 )
A37: ((InnerVertices IIG) \ (SortsWithConstants IIG)) \/ (SortsWithConstants IIG) = InnerVertices IIG by MSAFREE2:3, XBOOLE_1:45;
assume A38: i in the carrier of IIG ; ::_thesis: M1 . b1 = M2 . b1
then reconsider v = i as Vertex of IIG ;
 v in (InputVertices IIG) \/ (InnerVertices IIG) by A38, XBOOLE_1:45;
then A39: ( v in InputVertices IIG or v in InnerVertices IIG ) by XBOOLE_0:def_3;
percases ( v in InputVertices IIG or v in SortsWithConstants IIG or v in (InnerVertices IIG) \ (SortsWithConstants IIG) ) by A37, A39, XBOOLE_0:def_3;
supposeA40: v in InputVertices IIG ; ::_thesis: M1 . b1 = M2 . b1
then  M1 . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) by A35;
hence  M1 . i = M2 . i by A36, A40; ::_thesis: verum
end;
supposeA41: v in SortsWithConstants IIG ; ::_thesis: M1 . b1 = M2 . b1
then  M1 . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) by A35;
hence  M1 . i = M2 . i by A36, A41; ::_thesis: verum
end;
supposeA42: v in (InnerVertices IIG) \ (SortsWithConstants IIG) ; ::_thesis: M1 . b1 = M2 . b1
then  M1 . v = id (FreeGen (v, the Sorts of A)) by A35;
hence  M1 . i = M2 . i by A36, A42; ::_thesis: verum
end;
end;
end;
hence  M1 = M2 by PBOOLE:3; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines Fix_inp CIRCUIT2:def_1_:_
 for IIG being non empty non void Circuit-like monotonic ManySortedSign
for A being non-empty Circuit of IIG
for iv being InputValues of A
for b4 being ManySortedFunction of FreeGen the Sorts of A, the Sorts of (FreeEnv A) holds
( b4 = Fix_inp iv iff for v being Vertex of IIG holds
( ( v in InputVertices IIG implies b4 . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies b4 . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies b4 . v = id (FreeGen (v, the Sorts of A)) ) ) );

definition
let IIG be non empty non void Circuit-like monotonic ManySortedSign ;
let A be non-empty Circuit of IIG;
let iv be InputValues of A;
func Fix_inp_ext iv ->  ManySortedFunction of (FreeEnv A),(FreeEnv A) means :Def2: :: CIRCUIT2:def 2
( it is_homomorphism FreeEnv A, FreeEnv A & Fix_inp iv c= it );
existence
 ex b1 being ManySortedFunction of (FreeEnv A),(FreeEnv A) st
( b1 is_homomorphism FreeEnv A, FreeEnv A & Fix_inp iv c= b1 )
proof
reconsider G = FreeGen the Sorts of A as free GeneratorSet of FreeEnv A by MSAFREE:16;
consider h being ManySortedFunction of (FreeEnv A),(FreeEnv A) such that
A1: h is_homomorphism FreeEnv A, FreeEnv A and
A2: h || G = Fix_inp iv by MSAFREE:def_5;
take  h ; ::_thesis: ( h is_homomorphism FreeEnv A, FreeEnv A & Fix_inp iv c= h )
thus  h is_homomorphism FreeEnv A, FreeEnv A by A1; ::_thesis: Fix_inp iv c= h
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of IIG or (Fix_inp iv) . i c= h . i )
assume A3: i in the carrier of IIG ; ::_thesis: (Fix_inp iv) . i c= h . i
then reconsider hi = h . i as Function of ( the Sorts of (FreeEnv A) . i),( the Sorts of (FreeEnv A) . i) by PBOOLE:def_15;
 (Fix_inp iv) . i = hi | (G . i) by A2, A3, MSAFREE:def_1;
hence  (Fix_inp iv) . i c= h . i by RELAT_1:59; ::_thesis: verum
end;
uniqueness
 for b1, b2 being ManySortedFunction of (FreeEnv A),(FreeEnv A) st b1 is_homomorphism FreeEnv A, FreeEnv A & Fix_inp iv c= b1 & b2 is_homomorphism FreeEnv A, FreeEnv A & Fix_inp iv c= b2 holds
b1 = b2
proof
let h1, h2 be ManySortedFunction of (FreeEnv A),(FreeEnv A); ::_thesis: ( h1 is_homomorphism FreeEnv A, FreeEnv A & Fix_inp iv c= h1 & h2 is_homomorphism FreeEnv A, FreeEnv A & Fix_inp iv c= h2 implies h1 = h2 )
assume that
A4: h1 is_homomorphism FreeEnv A, FreeEnv A and
A5: Fix_inp iv c= h1 and
A6: h2 is_homomorphism FreeEnv A, FreeEnv A and
A7: Fix_inp iv c= h2 ; ::_thesis: h1 = h2
reconsider f1 = h1, f2 = h2 as ManySortedFunction of (FreeMSA the Sorts of A),(FreeMSA the Sorts of A) ;
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_IIG_holds_
for_f_being_Function_of_(_the_Sorts_of_(FreeMSA_the_Sorts_of_A)_._i),(_the_Sorts_of_(FreeMSA_the_Sorts_of_A)_._i)_st_f_=_f1_._i_holds_
(f2_||_(FreeGen_the_Sorts_of_A))_._i_=_f_|_((FreeGen_the_Sorts_of_A)_._i)
let i be set ; ::_thesis: ( i in the carrier of IIG implies for f being Function of ( the Sorts of (FreeMSA the Sorts of A) . i),( the Sorts of (FreeMSA the Sorts of A) . i) st f = f1 . i holds
(f2 || (FreeGen the Sorts of A)) . i = f | ((FreeGen the Sorts of A) . i) )
assume A8: i in the carrier of IIG ; ::_thesis: for f being Function of ( the Sorts of (FreeMSA the Sorts of A) . i),( the Sorts of (FreeMSA the Sorts of A) . i) st f = f1 . i holds
(f2 || (FreeGen the Sorts of A)) . i = f | ((FreeGen the Sorts of A) . i)
reconsider g = f2 . i as Function of ( the Sorts of (FreeMSA the Sorts of A) . i),( the Sorts of (FreeMSA the Sorts of A) . i) by A8, PBOOLE:def_15;
A9: (Fix_inp iv) . i c= g by A7, A8, PBOOLE:def_2;
reconsider Fi = (Fix_inp iv) . i as Function ;
 Fi is Function of ((FreeGen the Sorts of A) . i),( the Sorts of (FreeMSA the Sorts of A) . i) by A8, PBOOLE:def_15;
then A10: dom Fi = (FreeGen the Sorts of A) . i by A8, FUNCT_2:def_1;
let f be Function of ( the Sorts of (FreeMSA the Sorts of A) . i),( the Sorts of (FreeMSA the Sorts of A) . i); ::_thesis: ( f = f1 . i implies (f2 || (FreeGen the Sorts of A)) . i = f | ((FreeGen the Sorts of A) . i) )
assume  f = f1 . i ; ::_thesis: (f2 || (FreeGen the Sorts of A)) . i = f | ((FreeGen the Sorts of A) . i)
then A11: (Fix_inp iv) . i c= f by A5, A8, PBOOLE:def_2;
thus (f2 || (FreeGen the Sorts of A)) . i = g | ((FreeGen the Sorts of A) . i) by A8, MSAFREE:def_1
.= (Fix_inp iv) . i by A10, A9, GRFUNC_1:23
.= f | ((FreeGen the Sorts of A) . i) by A10, A11, GRFUNC_1:23 ; ::_thesis: verum
end;
then  f1 || (FreeGen the Sorts of A) = f2 || (FreeGen the Sorts of A) by MSAFREE:def_1;
hence  h1 = h2 by A4, A6, EXTENS_1:14; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines Fix_inp_ext CIRCUIT2:def_2_:_
 for IIG being non empty non void Circuit-like monotonic ManySortedSign
for A being non-empty Circuit of IIG
for iv being InputValues of A
for b4 being ManySortedFunction of (FreeEnv A),(FreeEnv A) holds
( b4 = Fix_inp_ext iv iff ( b4 is_homomorphism FreeEnv A, FreeEnv A & Fix_inp iv c= b4 ) );

theorem Th2: :: CIRCUIT2:2
for IIG being 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
proof
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
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; ::_thesis: 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; ::_thesis: 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; ::_thesis: 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; ::_thesis: 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 ; ::_thesis: ( 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] ; ::_thesis: ((Fix_inp_ext iv) . v) . e = e
A3: e . {} = [x,v] by A2, TREES_4:3;
A4: now__::_thesis:_for_o_being_OperSymbol_of_IIG_holds_
(_not_[o,_the_carrier_of_IIG]_=_e_._{}_or_not_the_result_sort_of_o_=_v_)
given o being OperSymbol of IIG such that A5: [o, the carrier of IIG] = e . {} and
 the_result_sort_of o = v ; ::_thesis: contradiction
 v = the carrier of IIG by A3, A5, XTUPLE_0:1;
hence  contradiction by Lm1; ::_thesis: verum
end;
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 by PBOOLE:def_2;
 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 ;
::_thesis: verum
end;

theorem Th3: :: CIRCUIT2:3
for IIG being 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 x being Element of the Sorts of A . v st v in InputVertices IIG holds
((Fix_inp_ext iv) . v) . (root-tree [x,v]) = root-tree [(iv . v),v]
proof
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 x being Element of the Sorts of A . v st v in InputVertices IIG holds
((Fix_inp_ext iv) . v) . (root-tree [x,v]) = root-tree [(iv . v),v]
let A be non-empty Circuit of IIG; ::_thesis: for iv being InputValues of A
for v being Vertex of IIG
for x being Element of the Sorts of A . v st v in InputVertices IIG holds
((Fix_inp_ext iv) . v) . (root-tree [x,v]) = root-tree [(iv . v),v]
let iv be InputValues of A; ::_thesis: for v being Vertex of IIG
for x being Element of the Sorts of A . v st v in InputVertices IIG holds
((Fix_inp_ext iv) . v) . (root-tree [x,v]) = root-tree [(iv . v),v]
let v be Vertex of IIG; ::_thesis: for x being Element of the Sorts of A . v st v in InputVertices IIG holds
((Fix_inp_ext iv) . v) . (root-tree [x,v]) = root-tree [(iv . v),v]
let x be Element of the Sorts of A . v; ::_thesis: ( v in InputVertices IIG implies ((Fix_inp_ext iv) . v) . (root-tree [x,v]) = root-tree [(iv . v),v] )
set e = root-tree [x,v];
assume A1: v in InputVertices IIG ; ::_thesis: ((Fix_inp_ext iv) . v) . (root-tree [x,v]) = root-tree [(iv . v),v]
A2: root-tree [x,v] in FreeGen (v, the Sorts of A) by MSAFREE:def_15;
 Fix_inp iv c= Fix_inp_ext iv by Def2;
then A3: (Fix_inp iv) . v c= (Fix_inp_ext iv) . v by PBOOLE:def_2;
 FreeEnv A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #) by MSAFREE:def_14;
then reconsider e = root-tree [x,v] as Element of the Sorts of (FreeEnv A) . v by A2;
 e in (FreeGen the Sorts of A) . v by A2, MSAFREE:def_16;
then  e in dom ((Fix_inp iv) . v) by FUNCT_2:def_1;
hence ((Fix_inp_ext iv) . v) . (root-tree [x,v]) = ((Fix_inp iv) . v) . e by A3, GRFUNC_1:2
.= ((FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v])) . e by A1, Def1
.= root-tree [(iv . v),v] by A2, FUNCOP_1:7 ;
::_thesis: verum
end;

theorem Th4: :: CIRCUIT2:4
for IIG being 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 p, q being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(action_at v), the carrier of IIG] -tree p & dom p = dom q & ( for k being Element of NAT st k in dom p holds
q . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) ) holds
((Fix_inp_ext iv) . v) . e = [(action_at v), the carrier of IIG] -tree q
proof
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
for p, q being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(action_at v), the carrier of IIG] -tree p & dom p = dom q & ( for k being Element of NAT st k in dom p holds
q . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) ) holds
((Fix_inp_ext iv) . v) . e = [(action_at v), the carrier of IIG] -tree q
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
for p, q being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(action_at v), the carrier of IIG] -tree p & dom p = dom q & ( for k being Element of NAT st k in dom p holds
q . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) ) holds
((Fix_inp_ext iv) . v) . e = [(action_at v), the carrier of IIG] -tree q
let iv be InputValues of A; ::_thesis: for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v
for p, q being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(action_at v), the carrier of IIG] -tree p & dom p = dom q & ( for k being Element of NAT st k in dom p holds
q . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) ) holds
((Fix_inp_ext iv) . v) . e = [(action_at v), the carrier of IIG] -tree q
let v be Vertex of IIG; ::_thesis: for e being Element of the Sorts of (FreeEnv A) . v
for p, q being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(action_at v), the carrier of IIG] -tree p & dom p = dom q & ( for k being Element of NAT st k in dom p holds
q . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) ) holds
((Fix_inp_ext iv) . v) . e = [(action_at v), the carrier of IIG] -tree q
let e be Element of the Sorts of (FreeEnv A) . v; ::_thesis: for p, q being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(action_at v), the carrier of IIG] -tree p & dom p = dom q & ( for k being Element of NAT st k in dom p holds
q . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) ) holds
((Fix_inp_ext iv) . v) . e = [(action_at v), the carrier of IIG] -tree q
let p, q be DTree-yielding FinSequence; ::_thesis: ( v in InnerVertices IIG & e = [(action_at v), the carrier of IIG] -tree p & dom p = dom q & ( for k being Element of NAT st k in dom p holds
q . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) ) implies ((Fix_inp_ext iv) . v) . e = [(action_at v), the carrier of IIG] -tree q )
assume that
A1: v in InnerVertices IIG and
A2: e = [(action_at v), the carrier of IIG] -tree p and
A3: dom p = dom q and
A4: for k being Element of NAT st k in dom p holds
q . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) ; ::_thesis: ((Fix_inp_ext iv) . v) . e = [(action_at v), the carrier of IIG] -tree q
set o = action_at v;
A5: the_result_sort_of (action_at v) = v by A1, MSAFREE2:def_7;
then A6: len p = len (the_arity_of (action_at v)) by A2, MSAFREE2:10;
A7: now__::_thesis:_for_k_being_Nat_st_k_in_dom_q_holds_
q_._k_in_the_Sorts_of_(FreeEnv_A)_._((the_arity_of_(action_at_v))_/._k)
let k be Nat; ::_thesis: ( k in dom q implies q . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k) )
assume A8: k in dom q ; ::_thesis: q . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k)
then A9: k in dom (the_arity_of (action_at v)) by A3, A6, FINSEQ_3:29;
then  p . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) . k) by A2, A5, MSAFREE2:11;
then A10: p . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k) by A9, PARTFUN1:def_6;
 q . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) by A3, A4, A8;
hence  q . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k) by A10, FUNCT_2:5; ::_thesis: verum
end;
A11: now__::_thesis:_for_k_being_Nat_st_k_in_dom_p_holds_
p_._k_in_the_Sorts_of_(FreeEnv_A)_._((the_arity_of_(action_at_v))_/._k)
let k be Nat; ::_thesis: ( k in dom p implies p . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k) )
assume  k in dom p ; ::_thesis: p . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k)
then A12: k in dom (the_arity_of (action_at v)) by A6, FINSEQ_3:29;
then  p . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) . k) by A2, A5, MSAFREE2:11;
hence  p . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k) by A12, PARTFUN1:def_6; ::_thesis: verum
end;
then reconsider x = p as Element of Args ((action_at v),(FreeEnv A)) by A6, MSAFREE2:5;
A13: FreeEnv A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #) by MSAFREE:def_14;
then A14: Args ((action_at v),(FreeEnv A)) = (((FreeSort the Sorts of A) #) * the Arity of IIG) . (action_at v) by MSUALG_1:def_4;
then reconsider pp = p as FinSequence of TS (DTConMSA the Sorts of A) by A6, A11, MSAFREE:8, MSAFREE2:5;
 p in Args ((action_at v),(FreeEnv A)) by A6, A11, MSAFREE2:5;
then A15: Sym ((action_at v), the Sorts of A) ==> roots pp by A14, MSAFREE:10;
A16: len q = len (the_arity_of (action_at v)) by A3, A6, FINSEQ_3:29;
then reconsider y = q as Element of Args ((action_at v),(FreeEnv A)) by A7, MSAFREE2:5;
A17: Fix_inp_ext iv is_homomorphism FreeEnv A, FreeEnv A by Def2;
reconsider qq = q as FinSequence of TS (DTConMSA the Sorts of A) by A14, A16, A7, MSAFREE:8, MSAFREE2:5;
 q in Args ((action_at v),(FreeEnv A)) by A16, A7, MSAFREE2:5;
then A18: Sym ((action_at v), the Sorts of A) ==> roots qq by A14, MSAFREE:10;
 for k being Nat st k in dom p holds
q . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) by A4;
then A19: y = (Fix_inp_ext iv) # x by MSUALG_3:def_6;
e = (Sym ((action_at v), the Sorts of A)) -tree pp by A2, MSAFREE:def_9
.= (DenOp ((action_at v), the Sorts of A)) . x by A15, MSAFREE:def_12
.= ( the Charact of (FreeEnv A) . (action_at v)) . x by A13, MSAFREE:def_13
.= (Den ((action_at v),(FreeEnv A))) . x by MSUALG_1:def_6 ;
hence ((Fix_inp_ext iv) . v) . e = (Den ((action_at v),(FreeEnv A))) . q by A5, A19, A17, MSUALG_3:def_7
.= ((FreeOper the Sorts of A) . (action_at v)) . q by A13, MSUALG_1:def_6
.= (DenOp ((action_at v), the Sorts of A)) . q by MSAFREE:def_13
.= (Sym ((action_at v), the Sorts of A)) -tree qq by A18, MSAFREE:def_12
.= [(action_at v), the carrier of IIG] -tree q by MSAFREE:def_9 ;
::_thesis: verum
end;

theorem Th5: :: CIRCUIT2:5
for IIG being 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]
proof
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 ) ) ) ;
percases ( 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;
supposeA4: 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]
 Fix_inp iv c= Fix_inp_ext iv by Def2;
then A5: (Fix_inp iv) . v c= (Fix_inp_ext iv) . v by PBOOLE:def_2;
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;
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]
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;
end;
end;

theorem Th6: :: CIRCUIT2:6
for IIG being 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, e1 being Element of the Sorts of (FreeEnv A) . v
for t, t1 being DecoratedTree st t = e & t1 = e1 & e1 = ((Fix_inp_ext iv) . v) . e holds
dom t = dom t1
proof
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, e1 being Element of the Sorts of (FreeEnv A) . v
for t, t1 being DecoratedTree st t = e & t1 = e1 & e1 = ((Fix_inp_ext iv) . v) . e holds
dom t = dom t1
let A be non-empty Circuit of IIG; ::_thesis: for iv being InputValues of A
for v being Vertex of IIG
for e, e1 being Element of the Sorts of (FreeEnv A) . v
for t, t1 being DecoratedTree st t = e & t1 = e1 & e1 = ((Fix_inp_ext iv) . v) . e holds
dom t = dom t1
let iv be InputValues of A; ::_thesis: for v being Vertex of IIG
for e, e1 being Element of the Sorts of (FreeEnv A) . v
for t, t1 being DecoratedTree st t = e & t1 = e1 & e1 = ((Fix_inp_ext iv) . v) . e holds
dom t = dom t1
let v be Vertex of IIG; ::_thesis: for e, e1 being Element of the Sorts of (FreeEnv A) . v
for t, t1 being DecoratedTree st t = e & t1 = e1 & e1 = ((Fix_inp_ext iv) . v) . e holds
dom t = dom t1
let e, e1 be Element of the Sorts of (FreeEnv A) . v; ::_thesis: for t, t1 being DecoratedTree st t = e & t1 = e1 & e1 = ((Fix_inp_ext iv) . v) . e holds
dom t = dom t1
let t, t1 be DecoratedTree; ::_thesis: ( t = e & t1 = e1 & e1 = ((Fix_inp_ext iv) . v) . e implies dom t = dom t1 )
set X = the Sorts of A;
set FX = the Sorts of (FreeEnv A);
defpred S1[ Element of NAT ] means  for v being Vertex of IIG
for e, e1 being Element of the Sorts of (FreeEnv A) . v
for t, t1 being DecoratedTree st t = e & t1 = e1 & depth (v,A) <= $1 & e1 = ((Fix_inp_ext iv) . v) . e holds
dom t = dom t1;
reconsider k = depth (v,A) as Element of NAT by ORDINAL1:def_12;
A1: depth (v,A) <= k ;
A2: FreeMSA the Sorts of A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #) by MSAFREE:def_14;
A3: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
A4: ((InnerVertices IIG) \ (SortsWithConstants IIG)) \/ (SortsWithConstants IIG) = InnerVertices IIG by MSAFREE2:3, XBOOLE_1:45;
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A5: S1[k] ; ::_thesis: S1[k + 1]
let v be Vertex of IIG; ::_thesis: for e, e1 being Element of the Sorts of (FreeEnv A) . v
for t, t1 being DecoratedTree st t = e & t1 = e1 & depth (v,A) <= k + 1 & e1 = ((Fix_inp_ext iv) . v) . e holds
dom t = dom t1
let e, e1 be Element of the Sorts of (FreeEnv A) . v; ::_thesis: for t, t1 being DecoratedTree st t = e & t1 = e1 & depth (v,A) <= k + 1 & e1 = ((Fix_inp_ext iv) . v) . e holds
dom t = dom t1
let t, t1 be DecoratedTree; ::_thesis: ( t = e & t1 = e1 & depth (v,A) <= k + 1 & e1 = ((Fix_inp_ext iv) . v) . e implies dom t = dom t1 )
assume that
A6: t = e and
A7: t1 = e1 and
A8: depth (v,A) <= k + 1 and
A9: e1 = ((Fix_inp_ext iv) . v) . e ; ::_thesis: dom t = dom t1
A10: 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;
 (InputVertices IIG) \/ (InnerVertices IIG) = the carrier of IIG by XBOOLE_1:45;
then A11: ( v in InputVertices IIG or v in InnerVertices IIG ) by XBOOLE_0:def_3;
 ( e in the Sorts of (FreeEnv A) . v & (FreeSort the Sorts of A) . v = FreeSort ( the Sorts of A,v) ) by MSAFREE:def_11;
then consider a being Element of TS (DTConMSA the Sorts of A) such that
A12: a = e and
A13: ( 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 A2, A10;
percases ( v in InputVertices IIG or ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) & ex x being set st
( x in the Sorts of A . v & a = root-tree [x,v] ) ) or ( v in SortsWithConstants IIG & ex x being set st
( x in the Sorts of A . v & a = root-tree [x,v] ) ) or ( v in InnerVertices IIG & ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a . {} & the_result_sort_of o = v ) ) ) by A13, A11, A4, XBOOLE_0:def_3;
supposeA14: v in InputVertices IIG ; ::_thesis: dom t = dom t1
then A15: ((Fix_inp_ext iv) . v) . a = root-tree [(iv . v),v] by A13, Th3, MSAFREE2:2;
thus  dom t = {{}} by A6, A12, A13, A14, MSAFREE2:2, TREES_1:29, TREES_4:3
.= dom t1 by A7, A9, A12, A15, TREES_1:29, TREES_4:3 ; ::_thesis: verum
end;
suppose ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) & ex x being set st
( x in the Sorts of A . v & a = root-tree [x,v] ) ) ; ::_thesis: dom t = dom t1
hence  dom t = dom t1 by A6, A7, A9, A12, Th2; ::_thesis: verum
end;
supposethat A16: v in SortsWithConstants IIG and
A17: ex x being set st
( x in the Sorts of A . v & a = root-tree [x,v] ) ; ::_thesis: dom t = dom t1
A18: ((Fix_inp_ext iv) . v) . a = root-tree [(action_at v), the carrier of IIG] by A12, A16, Th5;
thus  dom t = {{}} by A6, A12, A17, TREES_1:29, TREES_4:3
.= dom t1 by A7, A9, A12, A18, TREES_1:29, TREES_4:3 ; ::_thesis: verum
end;
supposethat A19: v in InnerVertices IIG and
A20: ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a . {} & the_result_sort_of o = v ) ; ::_thesis: dom t = dom t1
consider o being OperSymbol of IIG such that
A21: [o, the carrier of IIG] = a . {} and
A22: the_result_sort_of o = v by A20;
A23: o = action_at v by A19, A22, MSAFREE2:def_7;
then consider p being DTree-yielding FinSequence such that
A24: e = [(action_at v), the carrier of IIG] -tree p by A12, A21, CIRCUIT1:9;
deffunc H1( Nat) ->  set = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. $1)) . (p . $1);
consider q being FinSequence such that
A25: len q = len p and
A26: for k being Nat st k in dom q holds
q . k = H1(k) from FINSEQ_1:sch_2();
A27: dom p = dom q by A25, FINSEQ_3:29;
 len p = len (the_arity_of (action_at v)) by A22, A23, A24, MSAFREE2:10;
then A28: dom p = dom (the_arity_of (action_at v)) by FINSEQ_3:29;
A29: now__::_thesis:_for_x_being_set_st_x_in_dom_q_holds_
q_._x_is_DecoratedTree
let x be set ; ::_thesis: ( x in dom q implies q . x is DecoratedTree )
assume A30: x in dom q ; ::_thesis: q . x is DecoratedTree
then reconsider i = x as Element of NAT ;
set v1 = (the_arity_of (action_at v)) /. i;
 (the_arity_of (action_at v)) /. i = (the_arity_of o) . i by A23, A28, A27, A30, PARTFUN1:def_6;
then reconsider ee = p . i as Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. i) by A22, A23, A24, A28, A27, A30, MSAFREE2:11;
reconsider fv1 = (Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. i) as Function of ( the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. i)),( the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. i)) ;
 q . i = fv1 . ee by A26, A30;
hence  q . x is DecoratedTree ; ::_thesis: verum
end;
A31: for k being Element of NAT st k in dom q holds
q . k = H1(k) by A26;
reconsider q = q as DTree-yielding FinSequence by A29, TREES_3:24;
A32: ((Fix_inp_ext iv) . v) . e = [(action_at v), the carrier of IIG] -tree q by A19, A24, A31, A27, Th4;
A33: dom (doms p) = dom p by TREES_3:37;
A34: now__::_thesis:_for_i_being_Nat_st_i_in_dom_(doms_p)_holds_
(doms_p)_._i_=_(doms_q)_._i
let i be Nat; ::_thesis: ( i in dom (doms p) implies (doms p) . i = (doms q) . i )
set v1 = (the_arity_of (action_at v)) /. i;
reconsider fv1 = (Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. i) as Function of ( the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. i)),( the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. i)) ;
assume A35: i in dom (doms p) ; ::_thesis: (doms p) . i = (doms q) . i
then  (the_arity_of (action_at v)) /. i = (the_arity_of o) . i by A23, A28, A33, PARTFUN1:def_6;
then reconsider ee = p . i as Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. i) by A22, A23, A24, A28, A33, A35, MSAFREE2:11;
 q . i = fv1 . ee by A26, A33, A27, A35;
then reconsider ee1 = q . i as Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. i) ;
 (the_arity_of (action_at v)) /. i in rng (the_arity_of (action_at v)) by A28, A33, A35, PARTFUN2:2;
then  depth (((the_arity_of (action_at v)) /. i),A) < k + 1 by A8, A19, CIRCUIT1:19, XXREAL_0:2;
then A36: depth (((the_arity_of (action_at v)) /. i),A) <= k by NAT_1:13;
 q . i = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. i)) . (p . i) by A26, A33, A27, A35;
then  dom ee = dom ee1 by A5, A36;
hence (doms p) . i = dom ee1 by A33, A35, FUNCT_6:22
.= (doms q) . i by A33, A27, A35, FUNCT_6:22 ;
::_thesis: verum
end;
 dom q = dom (doms q) by TREES_3:37;
then  doms p = doms q by A27, A34, FINSEQ_1:13, TREES_3:37;
hence  dom t = tree (doms q) by A6, A24, TREES_4:10
.= dom t1 by A7, A9, A32, TREES_4:10 ;
::_thesis: verum
end;
end;
end;
A37: S1[ 0 ]
proof
let v be Vertex of IIG; ::_thesis: for e, e1 being Element of the Sorts of (FreeEnv A) . v
for t, t1 being DecoratedTree st t = e & t1 = e1 & depth (v,A) <= 0 & e1 = ((Fix_inp_ext iv) . v) . e holds
dom t = dom t1
let e, e1 be Element of the Sorts of (FreeEnv A) . v; ::_thesis: for t, t1 being DecoratedTree st t = e & t1 = e1 & depth (v,A) <= 0 & e1 = ((Fix_inp_ext iv) . v) . e holds
dom t = dom t1
let t, t1 be DecoratedTree; ::_thesis: ( t = e & t1 = e1 & depth (v,A) <= 0 & e1 = ((Fix_inp_ext iv) . v) . e implies dom t = dom t1 )
assume that
A38: t = e and
A39: t1 = e1 and
A40: depth (v,A) <= 0 and
A41: e1 = ((Fix_inp_ext iv) . v) . e ; ::_thesis: dom t = dom t1
A42: depth (v,A) = 0 by A40, NAT_1:3;
A43: 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;
 ( e in the Sorts of (FreeEnv A) . v & (FreeSort the Sorts of A) . v = FreeSort ( the Sorts of A,v) ) by MSAFREE:def_11;
then consider a being Element of TS (DTConMSA the Sorts of A) such that
A44: a = e and
A45: ( 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 A2, A43;
percases ( v in InputVertices IIG or ( v in SortsWithConstants IIG & ex x being set st
( x in the Sorts of A . v & a = root-tree [x,v] ) ) or ( v in SortsWithConstants IIG & ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a . {} & the_result_sort_of o = v ) ) ) by A42, A45, CIRCUIT1:18;
supposeA46: v in InputVertices IIG ; ::_thesis: dom t = dom t1
then A47: ((Fix_inp_ext iv) . v) . a = root-tree [(iv . v),v] by A45, Th3, MSAFREE2:2;
thus  dom t = {{}} by A38, A44, A45, A46, MSAFREE2:2, TREES_1:29, TREES_4:3
.= dom t1 by A39, A41, A44, A47, TREES_1:29, TREES_4:3 ; ::_thesis: verum
end;
supposethat A48: v in SortsWithConstants IIG and
A49: ex x being set st
( x in the Sorts of A . v & a = root-tree [x,v] ) ; ::_thesis: dom t = dom t1
A50: ((Fix_inp_ext iv) . v) . a = root-tree [(action_at v), the carrier of IIG] by A44, A48, Th5;
thus  dom t = {{}} by A38, A44, A49, TREES_1:29, TREES_4:3
.= dom t1 by A39, A41, A44, A50, TREES_1:29, TREES_4:3 ; ::_thesis: verum
end;
supposethat A51: v in SortsWithConstants IIG and
A52: ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a . {} & the_result_sort_of o = v ) ; ::_thesis: dom t = dom t1
A53: ((Fix_inp_ext iv) . v) . a = root-tree [(action_at v), the carrier of IIG] by A44, A51, Th5;
consider o being OperSymbol of IIG such that
A54: [o, the carrier of IIG] = a . {} and
A55: the_result_sort_of o = v by A52;
A56: SortsWithConstants IIG c= InnerVertices IIG by MSAFREE2:3;
then  o = action_at v by A51, A55, MSAFREE2:def_7;
then consider p being DTree-yielding FinSequence such that
A57: a = [(action_at v), the carrier of IIG] -tree p by A44, A54, CIRCUIT1:9;
 v in  {  s where s is SortSymbol of IIG : s is with_const_op  }  by A51, MSAFREE2:def_1;
then  ex s being SortSymbol of IIG st
( v = s & s is with_const_op ) ;
then consider o9 being OperSymbol of IIG such that
A58: the Arity of IIG . o9 = {} and
A59: the ResultSort of IIG . o9 = v by MSUALG_2:def_1;
A60: the_result_sort_of o9 = v by A59, MSUALG_1:def_2;
then A61: o9 = action_at v by A51, A56, MSAFREE2:def_7;
then  len p = len (the_arity_of o9) by A44, A60, A57, MSAFREE2:10
.= len {} by A58, MSUALG_1:def_1
.= 0 ;
then  p = {} ;
then  a = root-tree [o9, the carrier of IIG] by A61, A57, TREES_4:20;
hence  dom t = {{}} by A38, A44, TREES_1:29, TREES_4:3
.= dom t1 by A39, A41, A44, A53, TREES_1:29, TREES_4:3 ;
::_thesis: verum
end;
end;
end;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A37, A3);
hence  ( t = e & t1 = e1 & e1 = ((Fix_inp_ext iv) . v) . e implies dom t = dom t1 ) by A1; ::_thesis: verum
end;

theorem Th7: :: CIRCUIT2:7
for IIG being 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, e1 being Element of the Sorts of (FreeEnv A) . v st e1 = ((Fix_inp_ext iv) . v) . e holds
card e = card e1
proof
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, e1 being Element of the Sorts of (FreeEnv A) . v st e1 = ((Fix_inp_ext iv) . v) . e holds
card e = card e1
let A be non-empty Circuit of IIG; ::_thesis: for iv being InputValues of A
for v being Vertex of IIG
for e, e1 being Element of the Sorts of (FreeEnv A) . v st e1 = ((Fix_inp_ext iv) . v) . e holds
card e = card e1
let iv be InputValues of A; ::_thesis: for v being Vertex of IIG
for e, e1 being Element of the Sorts of (FreeEnv A) . v st e1 = ((Fix_inp_ext iv) . v) . e holds
card e = card e1
let v be Vertex of IIG; ::_thesis: for e, e1 being Element of the Sorts of (FreeEnv A) . v st e1 = ((Fix_inp_ext iv) . v) . e holds
card e = card e1
let e, e1 be Element of the Sorts of (FreeEnv A) . v; ::_thesis: ( e1 = ((Fix_inp_ext iv) . v) . e implies card e = card e1 )
assume  e1 = ((Fix_inp_ext iv) . v) . e ; ::_thesis: card e = card e1
then  dom e = dom e1 by Th6;
hence  card e = card (dom e1) by CARD_1:62
.= card e1 by CARD_1:62 ;
::_thesis: verum
end;

definition
let IIG be non empty non void Circuit-like monotonic ManySortedSign ;
let SCS be non-empty Circuit of IIG;
let v be Vertex of IIG;
let iv be InputValues of SCS;
func IGTree (v,iv) ->  Element of the Sorts of (FreeEnv SCS) . v means :Def3: :: CIRCUIT2:def 3
 ex e being Element of the Sorts of (FreeEnv SCS) . v st
( card e = size (v,SCS) & it = ((Fix_inp_ext iv) . v) . e );
existence
 ex b1, e being Element of the Sorts of (FreeEnv SCS) . v st
( card e = size (v,SCS) & b1 = ((Fix_inp_ext iv) . v) . e )
proof
reconsider SFv = the Sorts of (FreeEnv SCS) . v as non empty set ;
consider s being non empty finite Subset of NAT such that
A1: s =  {  (card t) where t is Element of the Sorts of (FreeEnv SCS) . v : verum  }  and
A2: size (v,SCS) = max s by CIRCUIT1:def_4;
 size (v,SCS) in s by A2, XXREAL_2:def_8;
then consider e being Element of the Sorts of (FreeEnv SCS) . v such that
A3: size (v,SCS) = card e by A1;
reconsider Fiev = (Fix_inp_ext iv) . v as Function of SFv,SFv ;
reconsider e9 = e as Element of SFv ;
reconsider IT = Fiev . e9 as Element of SFv ;
reconsider IT = IT as Element of the Sorts of (FreeEnv SCS) . v ;
take  IT ; ::_thesis: ex e being Element of the Sorts of (FreeEnv SCS) . v st
( card e = size (v,SCS) & IT = ((Fix_inp_ext iv) . v) . e )
take  e ; ::_thesis: ( card e = size (v,SCS) & IT = ((Fix_inp_ext iv) . v) . e )
thus  card e = size (v,SCS) by A3; ::_thesis: IT = ((Fix_inp_ext iv) . v) . e
thus  IT = ((Fix_inp_ext iv) . v) . e ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of the Sorts of (FreeEnv SCS) . v st ex e being Element of the Sorts of (FreeEnv SCS) . v st
( card e = size (v,SCS) & b1 = ((Fix_inp_ext iv) . v) . e ) & ex e being Element of the Sorts of (FreeEnv SCS) . v st
( card e = size (v,SCS) & b2 = ((Fix_inp_ext iv) . v) . e ) holds
b1 = b2
proof
defpred S1[ Nat] means  ex v being Vertex of IIG ex it1, it2 being Element of the Sorts of (FreeEnv SCS) . v st
( size (v,SCS) = $1 & ex e1 being Element of the Sorts of (FreeEnv SCS) . v st
( card e1 = size (v,SCS) & it1 = ((Fix_inp_ext iv) . v) . e1 ) & ex e2 being Element of the Sorts of (FreeEnv SCS) . v st
( card e2 = size (v,SCS) & it2 = ((Fix_inp_ext iv) . v) . e2 ) & it1 <> it2 );
let it1, it2 be Element of the Sorts of (FreeEnv SCS) . v; ::_thesis: ( ex e being Element of the Sorts of (FreeEnv SCS) . v st
( card e = size (v,SCS) & it1 = ((Fix_inp_ext iv) . v) . e ) & ex e being Element of the Sorts of (FreeEnv SCS) . v st
( card e = size (v,SCS) & it2 = ((Fix_inp_ext iv) . v) . e ) implies it1 = it2 )
now__::_thesis:_for_n_being_Nat_holds_not_S1[n]
assume A4: ex n being Nat st S1[n] ; ::_thesis: contradiction
consider n being Nat such that
A5: S1[n] and
A6: for k being Nat st S1[k] holds
n <= k from NAT_1:sch_5(A4);
consider v being Vertex of IIG, it1, it2 being Element of the Sorts of (FreeEnv SCS) . v such that
A7: size (v,SCS) = n and
A8: ex e1 being Element of the Sorts of (FreeEnv SCS) . v st
( card e1 = size (v,SCS) & it1 = ((Fix_inp_ext iv) . v) . e1 ) and
A9: ex e2 being Element of the Sorts of (FreeEnv SCS) . v st
( card e2 = size (v,SCS) & it2 = ((Fix_inp_ext iv) . v) . e2 ) and
A10: it1 <> it2 by A5;
consider e2 being Element of the Sorts of (FreeEnv SCS) . v such that
A11: card e2 = size (v,SCS) and
A12: it2 = ((Fix_inp_ext iv) . v) . e2 by A9;
consider e1 being Element of the Sorts of (FreeEnv SCS) . v such that
A13: card e1 = size (v,SCS) and
A14: it1 = ((Fix_inp_ext iv) . v) . e1 by A8;
percases ( v in InputVertices IIG or v in SortsWithConstants IIG or ( not v in InputVertices IIG & not v in SortsWithConstants IIG ) ) ;
supposeA15: v in InputVertices IIG ; ::_thesis: contradiction
then A16: ex x2 being Element of the Sorts of SCS . v st e2 = root-tree [x2,v] by MSAFREE2:9;
 ex x1 being Element of the Sorts of SCS . v st e1 = root-tree [x1,v] by A15, MSAFREE2:9;
then it1 = root-tree [(iv . v),v] by A14, A15, Th3
.= it2 by A12, A15, A16, Th3 ;
hence  contradiction by A10; ::_thesis: verum
end;
supposeA17: v in SortsWithConstants IIG ; ::_thesis: contradiction
then it1 = root-tree [(action_at v), the carrier of IIG] by A14, Th5
.= it2 by A12, A17, Th5 ;
hence  contradiction by A10; ::_thesis: verum
end;
supposethat A18: not v in InputVertices IIG and
A19: not v in SortsWithConstants IIG ; ::_thesis: contradiction
set Ht = (Fix_inp_ext iv) * (the_arity_of (action_at v));
 (InputVertices IIG) \/ (InnerVertices IIG) = the carrier of IIG by XBOOLE_1:45;
then A20: v in InnerVertices IIG by A18, XBOOLE_0:def_3;
then A21: v in (InnerVertices IIG) \ (SortsWithConstants IIG) by A19, XBOOLE_0:def_5;
then consider q1 being DTree-yielding FinSequence such that
A22: e1 = [(action_at v), the carrier of IIG] -tree q1 by A13, CIRCUIT1:12;
consider q2 being DTree-yielding FinSequence such that
A23: e2 = [(action_at v), the carrier of IIG] -tree q2 by A11, A21, CIRCUIT1:12;
 [(action_at v), the carrier of IIG] -tree q2 in the Sorts of (FreeEnv SCS) . v by A23;
then A24: [(action_at v), the carrier of IIG] -tree q2 in the Sorts of (FreeEnv SCS) . (the_result_sort_of (action_at v)) by A20, MSAFREE2:def_7;
A25: Fix_inp_ext iv is_homomorphism FreeEnv SCS, FreeEnv SCS by Def2;
then consider p1 being DTree-yielding FinSequence such that
A26: p1 = ((Fix_inp_ext iv) * (the_arity_of (action_at v))) .. q1 and
A27: it1 = [(action_at v), the carrier of IIG] -tree p1 by A14, A20, A22, Th1;
consider p2 being DTree-yielding FinSequence such that
A28: p2 = ((Fix_inp_ext iv) * (the_arity_of (action_at v))) .. q2 and
A29: it2 = [(action_at v), the carrier of IIG] -tree p2 by A12, A20, A23, A25, Th1;
A30: dom p1 = dom ((Fix_inp_ext iv) * (the_arity_of (action_at v))) by A26, PRALG_1:def_17;
 dom p2 = dom ((Fix_inp_ext iv) * (the_arity_of (action_at v))) by A28, PRALG_1:def_17;
then  len p1 = len p2 by A30, FINSEQ_3:29;
then consider i being Nat such that
A31: i in dom p1 and
A32: p1 . i <> p2 . i by A10, A27, A29, FINSEQ_2:9;
 rng (the_arity_of (action_at v)) c= the carrier of IIG by FINSEQ_1:def_4;
then  rng (the_arity_of (action_at v)) c= dom (Fix_inp_ext iv) by PARTFUN1:def_2;
then A33: dom (the_arity_of (action_at v)) = dom ((Fix_inp_ext iv) * (the_arity_of (action_at v))) by RELAT_1:27;
then reconsider w = (the_arity_of (action_at v)) . i as Vertex of IIG by A30, A31, FINSEQ_2:11;
 [(action_at v), the carrier of IIG] -tree q1 in the Sorts of (FreeEnv SCS) . v by A22;
then A34: [(action_at v), the carrier of IIG] -tree q1 in the Sorts of (FreeEnv SCS) . (the_result_sort_of (action_at v)) by A20, MSAFREE2:def_7;
then reconsider E1 = q1 . i, E2 = q2 . i as Element of the Sorts of (FreeEnv SCS) . w by A30, A33, A31, A24, MSAFREE2:11;
 [(action_at v), the carrier of IIG] -tree p2 in the Sorts of (FreeEnv SCS) . v by A29;
then A35: [(action_at v), the carrier of IIG] -tree p2 in the Sorts of (FreeEnv SCS) . (the_result_sort_of (action_at v)) by A20, MSAFREE2:def_7;
 [(action_at v), the carrier of IIG] -tree p1 in the Sorts of (FreeEnv SCS) . v by A27;
then  [(action_at v), the carrier of IIG] -tree p1 in the Sorts of (FreeEnv SCS) . (the_result_sort_of (action_at v)) by A20, MSAFREE2:def_7;
then reconsider It1 = p1 . i, It2 = p2 . i as Element of the Sorts of (FreeEnv SCS) . w by A30, A33, A31, A35, MSAFREE2:11;
reconsider Hti = ((Fix_inp_ext iv) * (the_arity_of (action_at v))) . i as Function ;
A36: Hti = (Fix_inp_ext iv) . ((the_arity_of (action_at v)) . i) by A30, A31, FUNCT_1:12;
then A37: It2 = ((Fix_inp_ext iv) . w) . E2 by A28, A30, A31, PRALG_1:def_17;
 len q2 = len (the_arity_of (action_at v)) by A24, MSAFREE2:10;
then  i in dom q2 by A30, A33, A31, FINSEQ_3:29;
then  E2 in rng q2 by FUNCT_1:def_3;
then A38: card E2 = size (w,SCS) by A11, A21, A23, CIRCUIT1:11;
 len q1 = len (the_arity_of (action_at v)) by A34, MSAFREE2:10;
then  i in dom q1 by A30, A33, A31, FINSEQ_3:29;
then  E1 in rng q1 by FUNCT_1:def_3;
then A39: card E1 = size (w,SCS) by A13, A21, A22, CIRCUIT1:11;
A40: w in rng (the_arity_of (action_at v)) by A30, A33, A31, FUNCT_1:def_3;
 It1 = ((Fix_inp_ext iv) . w) . E1 by A26, A30, A31, A36, PRALG_1:def_17;
hence  contradiction by A6, A7, A20, A32, A39, A38, A37, A40, CIRCUIT1:14; ::_thesis: verum
end;
end;
end;
hence  ( ex e being Element of the Sorts of (FreeEnv SCS) . v st
( card e = size (v,SCS) & it1 = ((Fix_inp_ext iv) . v) . e ) & ex e being Element of the Sorts of (FreeEnv SCS) . v st
( card e = size (v,SCS) & it2 = ((Fix_inp_ext iv) . v) . e ) implies it1 = it2 ) ; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines IGTree CIRCUIT2:def_3_:_
 for IIG being 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
for b5 being Element of the Sorts of (FreeEnv SCS) . v holds
( b5 = IGTree (v,iv) iff ex e being Element of the Sorts of (FreeEnv SCS) . v st
( card e = size (v,SCS) & b5 = ((Fix_inp_ext iv) . v) . e ) );

theorem Th8: :: CIRCUIT2:8
for IIG being 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 holds IGTree (v,iv) = ((Fix_inp_ext iv) . v) . (IGTree (v,iv))
proof
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 holds IGTree (v,iv) = ((Fix_inp_ext iv) . v) . (IGTree (v,iv))
let SCS be non-empty Circuit of IIG; ::_thesis: for v being Vertex of IIG
for iv being InputValues of SCS holds IGTree (v,iv) = ((Fix_inp_ext iv) . v) . (IGTree (v,iv))
let v be Vertex of IIG; ::_thesis: for iv being InputValues of SCS holds IGTree (v,iv) = ((Fix_inp_ext iv) . v) . (IGTree (v,iv))
let iv be InputValues of SCS; ::_thesis: IGTree (v,iv) = ((Fix_inp_ext iv) . v) . (IGTree (v,iv))
reconsider igt = IGTree (v,iv) as Element of the Sorts of (FreeEnv SCS) . v ;
 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;
then  card igt = size (v,SCS) by Th7;
hence  IGTree (v,iv) = ((Fix_inp_ext iv) . v) . (IGTree (v,iv)) by Def3; ::_thesis: verum
end;

theorem Th9: :: CIRCUIT2:9
for IIG being 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
for p being DTree-yielding FinSequence st v in InnerVertices IIG & dom p = dom (the_arity_of (action_at v)) & ( for k being Element of NAT st k in dom p holds
p . k = IGTree (((the_arity_of (action_at v)) /. k),iv) ) holds
IGTree (v,iv) = [(action_at v), the carrier of IIG] -tree p
proof
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
for p being DTree-yielding FinSequence st v in InnerVertices IIG & dom p = dom (the_arity_of (action_at v)) & ( for k being Element of NAT st k in dom p holds
p . k = IGTree (((the_arity_of (action_at v)) /. k),iv) ) holds
IGTree (v,iv) = [(action_at v), the carrier of IIG] -tree p
let SCS be non-empty Circuit of IIG; ::_thesis: for v being Vertex of IIG
for iv being InputValues of SCS
for p being DTree-yielding FinSequence st v in InnerVertices IIG & dom p = dom (the_arity_of (action_at v)) & ( for k being Element of NAT st k in dom p holds
p . k = IGTree (((the_arity_of (action_at v)) /. k),iv) ) holds
IGTree (v,iv) = [(action_at v), the carrier of IIG] -tree p
let v be Vertex of IIG; ::_thesis: for iv being InputValues of SCS
for p being DTree-yielding FinSequence st v in InnerVertices IIG & dom p = dom (the_arity_of (action_at v)) & ( for k being Element of NAT st k in dom p holds
p . k = IGTree (((the_arity_of (action_at v)) /. k),iv) ) holds
IGTree (v,iv) = [(action_at v), the carrier of IIG] -tree p
let iv be InputValues of SCS; ::_thesis: for p being DTree-yielding FinSequence st v in InnerVertices IIG & dom p = dom (the_arity_of (action_at v)) & ( for k being Element of NAT st k in dom p holds
p . k = IGTree (((the_arity_of (action_at v)) /. k),iv) ) holds
IGTree (v,iv) = [(action_at v), the carrier of IIG] -tree p
let p be DTree-yielding FinSequence; ::_thesis: ( v in InnerVertices IIG & dom p = dom (the_arity_of (action_at v)) & ( for k being Element of NAT st k in dom p holds
p . k = IGTree (((the_arity_of (action_at v)) /. k),iv) ) implies IGTree (v,iv) = [(action_at v), the carrier of IIG] -tree p )
assume that
A1: v in InnerVertices IIG and
A2: dom p = dom (the_arity_of (action_at v)) and
A3: for k being Element of NAT st k in dom p holds
p . k = IGTree (((the_arity_of (action_at v)) /. k),iv) ; ::_thesis: IGTree (v,iv) = [(action_at v), the carrier of IIG] -tree p
set U1 = FreeEnv SCS;
set o = action_at v;
A4: now__::_thesis:_for_k_being_Nat_st_k_in_dom_p_holds_
p_._k_in_the_Sorts_of_(FreeEnv_SCS)_._((the_arity_of_(action_at_v))_/._k)
let k be Nat; ::_thesis: ( k in dom p implies p . k in the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at v)) /. k) )
assume  k in dom p ; ::_thesis: p . k in the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at v)) /. k)
then  p . k = IGTree (((the_arity_of (action_at v)) /. k),iv) by A3;
hence  p . k in the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at v)) /. k) ; ::_thesis: verum
end;
 len p = len (the_arity_of (action_at v)) by A2, FINSEQ_3:29;
then reconsider p99 = p as Element of Args ((action_at v),(FreeEnv SCS)) by A4, MSAFREE2:5;
set X = the Sorts of SCS;
A5: dom the ResultSort of IIG = the carrier' of IIG by FUNCT_2:def_1;
A6: Result ((action_at v),(FreeEnv SCS)) = ( the Sorts of (FreeEnv SCS) * the ResultSort of IIG) . (action_at v) by MSUALG_1:def_5
.= the Sorts of (FreeEnv SCS) . ( the ResultSort of IIG . (action_at v)) by A5, FUNCT_1:13 ;
A7: ( FreeEnv SCS = MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #) & Args ((action_at v),(FreeEnv SCS)) = (( the Sorts of (FreeEnv SCS) #) * the Arity of IIG) . (action_at v) ) by MSAFREE:def_14, MSUALG_1:def_4;
then reconsider p9 = p99 as FinSequence of TS (DTConMSA the Sorts of SCS) by MSAFREE:8;
 FreeEnv SCS = MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #) by MSAFREE:def_14;
then A8: 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 ;
 Sym ((action_at v), the Sorts of SCS) ==> roots p9 by A7, MSAFREE:10;
then A9: (Den ((action_at v),(FreeEnv SCS))) . p = (Sym ((action_at v), the Sorts of SCS)) -tree p9 by A8, MSAFREE:def_12
.= [(action_at v), the carrier of IIG] -tree p9 by MSAFREE:def_9 ;
the ResultSort of IIG . (action_at v) = the_result_sort_of (action_at v) by MSUALG_1:def_2
.= v by A1, MSAFREE2:def_7 ;
then reconsider t = [(action_at v), the carrier of IIG] -tree p as Element of the Sorts of (FreeMSA the Sorts of SCS) . v by A9, A6, FUNCT_2:5;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_p_holds_
ex_ek_being_Element_of_the_Sorts_of_(FreeEnv_SCS)_._((the_arity_of_(action_at_v))_/._k)_st_
(_ek_=_p_._k_&_card_ek_=_size_(((the_arity_of_(action_at_v))_/._k),SCS)_)
let k be Element of NAT ; ::_thesis: ( k in dom p implies ex ek being Element of the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at v)) /. k) st
( ek = p . k & card ek = size (((the_arity_of (action_at v)) /. k),SCS) ) )
set v1 = (the_arity_of (action_at v)) /. k;
assume  k in dom p ; ::_thesis: ex ek being Element of the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at v)) /. k) st
( ek = p . k & card ek = size (((the_arity_of (action_at v)) /. k),SCS) )
then A10: p . k = IGTree (((the_arity_of (action_at v)) /. k),iv) by A3;
then reconsider ek = p . k as Element of the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at v)) /. k) ;
take ek = ek; ::_thesis: ( ek = p . k & card ek = size (((the_arity_of (action_at v)) /. k),SCS) )
thus  ek = p . k ; ::_thesis: card ek = size (((the_arity_of (action_at v)) /. k),SCS)
 ex e1 being Element of the Sorts of (FreeMSA the Sorts of SCS) . ((the_arity_of (action_at v)) /. k) st
( card e1 = size (((the_arity_of (action_at v)) /. k),SCS) & ek = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . e1 ) by A10, Def3;
hence  card ek = size (((the_arity_of (action_at v)) /. k),SCS) by Th7; ::_thesis: verum
end;
then A11: card t = size (v,SCS) by A1, CIRCUIT1:16;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_p_holds_
p_._k_=_((Fix_inp_ext_iv)_._((the_arity_of_(action_at_v))_/._k))_._(p_._k)
let k be Element of NAT ; ::_thesis: ( k in dom p implies p . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) )
assume  k in dom p ; ::_thesis: p . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k)
then  p . k = IGTree (((the_arity_of (action_at v)) /. k),iv) by A3;
hence  p . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) by Th8; ::_thesis: verum
end;
then  [(action_at v), the carrier of IIG] -tree p = ((Fix_inp_ext iv) . v) . t by A1, Th4;
hence  IGTree (v,iv) = [(action_at v), the carrier of IIG] -tree p by A11, Def3; ::_thesis: verum
end;

definition
let IIG be non empty non void Circuit-like monotonic ManySortedSign ;
let SCS be non-empty Circuit of IIG;
let v be Vertex of IIG;
let iv be InputValues of SCS;
func IGValue (v,iv) ->  Element of the Sorts of SCS . v equals :: CIRCUIT2:def 4
((Eval SCS) . v) . (IGTree (v,iv));
coherence
 ((Eval SCS) . v) . (IGTree (v,iv)) is Element of the Sorts of SCS . v ;
end;

:: deftheorem  defines IGValue CIRCUIT2:def_4_:_
 for IIG being 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 holds IGValue (v,iv) = ((Eval SCS) . v) . (IGTree (v,iv));

theorem Th10: :: CIRCUIT2:10
for IIG being 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
proof
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 InputVertices IIG holds
IGValue (v,iv) = iv . v
let SCS be non-empty Circuit of IIG; ::_thesis: 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; ::_thesis: for iv being InputValues of SCS st v in InputVertices IIG holds
IGValue (v,iv) = iv . v
let iv be InputValues of SCS; ::_thesis: ( 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 ; ::_thesis: 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 by PBOOLE:def_2;
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, FUNCOP_1:13;
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 ;
::_thesis: verum
end;

theorem Th11: :: CIRCUIT2:11
for IIG being 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 SortsWithConstants IIG holds
IGValue (v,iv) = (Set-Constants SCS) . v
proof
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
end;

begin

definition
let IIG be non empty non void Circuit-like ManySortedSign ;
let SCS be non-empty Circuit of IIG;
let s be State of SCS;
func Following s ->  State of SCS means :Def5: :: CIRCUIT2:def 5
 for v being Vertex of IIG holds
( ( v in InputVertices IIG implies it . v = s . v ) & ( v in InnerVertices IIG implies it . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) ) );
existence
 ex b1 being State of SCS st
for v being Vertex of IIG holds
( ( v in InputVertices IIG implies b1 . v = s . v ) & ( v in InnerVertices IIG implies b1 . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) ) )
proof
deffunc H1( Vertex of IIG) ->  Element of Result ((action_at $1),SCS) = (Den ((action_at $1),SCS)) . ((action_at $1) depends_on_in s);
deffunc H2( set ) ->  set = s . $1;
defpred S1[ set ] means $1 in InputVertices IIG;
consider f being ManySortedSet of the carrier of IIG such that
A1: for v being Vertex of IIG st v in the carrier of IIG holds
( ( S1[v] implies f . v = H2(v) ) & ( not S1[v] implies f . v = H1(v) ) ) from PRE_CIRC:sch_2();
A2: now__::_thesis:_for_x_being_set_st_x_in_dom_the_Sorts_of_SCS_holds_
f_._x_in_the_Sorts_of_SCS_._x
let x be set ; ::_thesis: ( x in dom the Sorts of SCS implies f . b1 in the Sorts of SCS . b1 )
assume  x in dom the Sorts of SCS ; ::_thesis: f . b1 in the Sorts of SCS . b1
then reconsider v = x as Vertex of IIG by PARTFUN1:def_2;
percases ( v in InputVertices IIG or not v in InputVertices IIG ) ;
suppose v in InputVertices IIG ; ::_thesis: f . b1 in the Sorts of SCS . b1
then  f . v = s . v by A1;
hence  f . x in the Sorts of SCS . x by CIRCUIT1:4; ::_thesis: verum
end;
supposeA3: not v in InputVertices IIG ; ::_thesis: f . b1 in the Sorts of SCS . b1
 v in the carrier of IIG ;
then  v in (InputVertices IIG) \/ (InnerVertices IIG) by XBOOLE_1:45;
then  v in InnerVertices IIG by A3, XBOOLE_0:def_3;
then A4: the_result_sort_of (action_at v) = v by MSAFREE2:def_7;
 f . x = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) by A1, A3;
hence  f . x in the Sorts of SCS . x by A4, CIRCUIT1:8; ::_thesis: verum
end;
end;
end;
 ( dom f = the carrier of IIG & dom the Sorts of SCS = the carrier of IIG ) by PARTFUN1:def_2;
then reconsider f = f as State of SCS by A2, CARD_3:def_5;
take  f ; ::_thesis: for v being Vertex of IIG holds
( ( v in InputVertices IIG implies f . v = s . v ) & ( v in InnerVertices IIG implies f . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) ) )
let v be Vertex of IIG; ::_thesis: ( ( v in InputVertices IIG implies f . v = s . v ) & ( v in InnerVertices IIG implies f . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) ) )
thus  ( v in InputVertices IIG implies f . v = s . v ) by A1; ::_thesis: ( v in InnerVertices IIG implies f . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) )
A5: InputVertices IIG misses InnerVertices IIG by XBOOLE_1:79;
assume  v in InnerVertices IIG ; ::_thesis: f . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s)
then  not v in InputVertices IIG by A5, XBOOLE_0:3;
hence  f . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being State of SCS st ( for v being Vertex of IIG holds
( ( v in InputVertices IIG implies b1 . v = s . v ) & ( v in InnerVertices IIG implies b1 . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) ) ) ) & ( for v being Vertex of IIG holds
( ( v in InputVertices IIG implies b2 . v = s . v ) & ( v in InnerVertices IIG implies b2 . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) ) ) ) holds
b1 = b2
proof
let it1, it2 be State of SCS; ::_thesis: ( ( for v being Vertex of IIG holds
( ( v in InputVertices IIG implies it1 . v = s . v ) & ( v in InnerVertices IIG implies it1 . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) ) ) ) & ( for v being Vertex of IIG holds
( ( v in InputVertices IIG implies it2 . v = s . v ) & ( v in InnerVertices IIG implies it2 . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) ) ) ) implies it1 = it2 )
assume that
A6: for v being Vertex of IIG holds
( ( v in InputVertices IIG implies it1 . v = s . v ) & ( v in InnerVertices IIG implies it1 . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) ) ) and
A7: for v being Vertex of IIG holds
( ( v in InputVertices IIG implies it2 . v = s . v ) & ( v in InnerVertices IIG implies it2 . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) ) ) ; ::_thesis: it1 = it2
assume A8: it1 <> it2 ; ::_thesis: contradiction
 dom it2 = the carrier of IIG by CIRCUIT1:3;
then consider x being set  such that
A9: x in dom it1 and
A10: it1 . x <> it2 . x by A8, CIRCUIT1:3, FUNCT_1:2;
reconsider v = x as Vertex of IIG by A9, CIRCUIT1:3;
A11: ( v in InnerVertices IIG implies it1 . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) ) by A6;
 dom it1 = the carrier of IIG by CIRCUIT1:3;
then  v in (InputVertices IIG) \/ (InnerVertices IIG) by A9, XBOOLE_1:45;
then A12: ( v in InputVertices IIG or v in InnerVertices IIG ) by XBOOLE_0:def_3;
 ( v in InputVertices IIG implies it1 . v = s . v ) by A6;
hence  contradiction by A7, A10, A12, A11; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines Following CIRCUIT2:def_5_:_
 for IIG being non empty non void Circuit-like ManySortedSign
for SCS being non-empty Circuit of IIG
for s, b4 being State of SCS holds
( b4 = Following s iff for v being Vertex of IIG holds
( ( v in InputVertices IIG implies b4 . v = s . v ) & ( v in InnerVertices IIG implies b4 . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) ) ) );

theorem Th12: :: CIRCUIT2:12
for IIG being non empty non void Circuit-like monotonic ManySortedSign
for SCS being non-empty Circuit of IIG
for s being State of SCS
for iv being InputValues of SCS st iv c= s holds
iv c= Following s
proof
let IIG be non empty non void Circuit-like monotonic ManySortedSign ; ::_thesis: for SCS being non-empty Circuit of IIG
for s being State of SCS
for iv being InputValues of SCS st iv c= s holds
iv c= Following s
let SCS be non-empty Circuit of IIG; ::_thesis: for s being State of SCS
for iv being InputValues of SCS st iv c= s holds
iv c= Following s
let s be State of SCS; ::_thesis: for iv being InputValues of SCS st iv c= s holds
iv c= Following s
let iv be InputValues of SCS; ::_thesis: ( iv c= s implies iv c= Following s )
assume A1: iv c= s ; ::_thesis: iv c= Following s
now__::_thesis:_(_dom_iv_c=_dom_(Following_s)_&_(_for_x_being_set_st_x_in_dom_iv_holds_
iv_._x_=_(Following_s)_._x_)_)
dom s = the carrier of IIG by CIRCUIT1:3
.= dom (Following s) by CIRCUIT1:3 ;
hence  dom iv c= dom (Following s) by A1, RELAT_1:11; ::_thesis: for x being set st x in dom iv holds
iv . x = (Following s) . x
let x be set ; ::_thesis: ( x in dom iv implies iv . x = (Following s) . x )
assume A2: x in dom iv ; ::_thesis: iv . x = (Following s) . x
A3: dom iv = InputVertices IIG by PARTFUN1:def_2;
then reconsider v = x as Vertex of IIG by A2;
 iv . v = s . v by A1, A2, GRFUNC_1:2;
hence  iv . x = (Following s) . x by A2, A3, Def5; ::_thesis: verum
end;
hence  iv c= Following s by GRFUNC_1:2; ::_thesis: verum
end;

definition
let IIG be non empty non void Circuit-like ManySortedSign ;
let SCS be non-empty Circuit of IIG;
let IT be State of SCS;
attrIT is stable  means :Def6: :: CIRCUIT2:def 6
IT = Following IT;
end;

:: deftheorem Def6 defines stable CIRCUIT2:def_6_:_
 for IIG being non empty non void Circuit-like ManySortedSign
for SCS being non-empty Circuit of IIG
for IT being State of SCS holds
( IT is stable iff IT = Following IT );

definition
let IIG be non empty non void Circuit-like monotonic ManySortedSign ;
let SCS be non-empty Circuit of IIG;
let s be State of SCS;
let iv be InputValues of SCS;
func Following (s,iv) ->  State of SCS equals :: CIRCUIT2:def 7
 Following (s +* iv);
coherence
 Following (s +* iv) is State of SCS ;
end;

:: deftheorem  defines Following CIRCUIT2:def_7_:_
 for IIG being non empty non void Circuit-like monotonic ManySortedSign
for SCS being non-empty Circuit of IIG
for s being State of SCS
for iv being InputValues of SCS holds Following (s,iv) = Following (s +* iv);

definition
let IIG be non empty non void Circuit-like monotonic ManySortedSign ;
let SCS be non-empty Circuit of IIG;
let InpFs be InputFuncs of SCS;
let s be State of SCS;
func InitialComp (s,InpFs) ->  State of SCS equals :: CIRCUIT2:def 8
(s +* (0 -th_InputValues InpFs)) +* (Set-Constants SCS);
coherence
 (s +* (0 -th_InputValues InpFs)) +* (Set-Constants SCS) is State of SCS
proof
set sc = Set-Constants SCS;
A1: dom (Set-Constants SCS) = SortsWithConstants IIG by PARTFUN1:def_2;
A2: now__::_thesis:_for_x_being_set_st_x_in_dom_(Set-Constants_SCS)_holds_
(Set-Constants_SCS)_._x_in_the_Sorts_of_SCS_._x
let x be set ; ::_thesis: ( x in dom (Set-Constants SCS) implies (Set-Constants SCS) . x in the Sorts of SCS . x )
assume A3: x in dom (Set-Constants SCS) ; ::_thesis: (Set-Constants SCS) . x in the Sorts of SCS . x
then reconsider v = x as Vertex of IIG by A1;
 (Set-Constants SCS) . x in Constants (SCS,v) by A3, CIRCUIT1:def_1;
hence  (Set-Constants SCS) . x in the Sorts of SCS . x ; ::_thesis: verum
end;
 dom the Sorts of SCS = the carrier of IIG by PARTFUN1:def_2;
hence  (s +* (0 -th_InputValues InpFs)) +* (Set-Constants SCS) is State of SCS by A1, A2, PRE_CIRC:6; ::_thesis: verum
end;
end;

:: deftheorem  defines InitialComp CIRCUIT2:def_8_:_
 for IIG being non empty non void Circuit-like monotonic ManySortedSign
for SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS
for s being State of SCS holds InitialComp (s,InpFs) = (s +* (0 -th_InputValues InpFs)) +* (Set-Constants SCS);

definition
let IIG be non empty non void Circuit-like monotonic ManySortedSign ;
let SCS be non-empty Circuit of IIG;
let InpFs be InputFuncs of SCS;
let s be State of SCS;
func Computation (s,InpFs) ->  Function of NAT,(product the Sorts of SCS) means :Def9: :: CIRCUIT2:def 9
( it . 0 = InitialComp (s,InpFs) & ( for i being Nat holds it . (i + 1) = Following ((it . i),((i + 1) -th_InputValues InpFs)) ) );
correctness
existence
ex b1 being Function of NAT,(product the Sorts of SCS) st
( b1 . 0 = InitialComp (s,InpFs) & ( for i being Nat holds b1 . (i + 1) = Following ((b1 . i),((i + 1) -th_InputValues InpFs)) ) );
uniqueness
for b1, b2 being Function of NAT,(product the Sorts of SCS) st b1 . 0 = InitialComp (s,InpFs) & ( for i being Nat holds b1 . (i + 1) = Following ((b1 . i),((i + 1) -th_InputValues InpFs)) ) & b2 . 0 = InitialComp (s,InpFs) & ( for i being Nat holds b2 . (i + 1) = Following ((b2 . i),((i + 1) -th_InputValues InpFs)) ) holds
b1 = b2;
proof
deffunc H1( Nat, State of SCS) ->  State of SCS = Following ($2,(($1 + 1) -th_InputValues InpFs));
thus  ( ex IT being Function of NAT,(product the Sorts of SCS) st
( IT . 0 = InitialComp (s,InpFs) & ( for i being Nat holds IT . (i + 1) = H1(i,IT . i) ) ) & ( for IT1, IT2 being Function of NAT,(product the Sorts of SCS) st IT1 . 0 = InitialComp (s,InpFs) & ( for i being Nat holds IT1 . (i + 1) = H1(i,IT1 . i) ) & IT2 . 0 = InitialComp (s,InpFs) & ( for i being Nat holds IT2 . (i + 1) = H1(i,IT2 . i) ) holds
IT1 = IT2 ) ) from PRE_CIRC:sch_3(); ::_thesis: verum
end;
end;

:: deftheorem Def9 defines Computation CIRCUIT2:def_9_:_
 for IIG being non empty non void Circuit-like monotonic ManySortedSign
for SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS
for s being State of SCS
for b5 being Function of NAT,(product the Sorts of SCS) holds
( b5 = Computation (s,InpFs) iff ( b5 . 0 = InitialComp (s,InpFs) & ( for i being Nat holds b5 . (i + 1) = Following ((b5 . i),((i + 1) -th_InputValues InpFs)) ) ) );


theorem Th13: :: CIRCUIT2:13
for IIG being non empty non void Circuit-like monotonic ManySortedSign
for SCS being non-empty Circuit of IIG
for s being State of SCS
for iv being InputValues of SCS
for k being Element of NAT st ( for v being Vertex of IIG st depth (v,SCS) <= k holds
s . v = IGValue (v,iv) ) holds
for v1 being Vertex of IIG st depth (v1,SCS) <= k + 1 holds
(Following s) . v1 = IGValue (v1,iv)
proof
let IIG be non empty non void Circuit-like monotonic ManySortedSign ; ::_thesis: for SCS being non-empty Circuit of IIG
for s being State of SCS
for iv being InputValues of SCS
for k being Element of NAT st ( for v being Vertex of IIG st depth (v,SCS) <= k holds
s . v = IGValue (v,iv) ) holds
for v1 being Vertex of IIG st depth (v1,SCS) <= k + 1 holds
(Following s) . v1 = IGValue (v1,iv)
let SCS be non-empty Circuit of IIG; ::_thesis: for s being State of SCS
for iv being InputValues of SCS
for k being Element of NAT st ( for v being Vertex of IIG st depth (v,SCS) <= k holds
s . v = IGValue (v,iv) ) holds
for v1 being Vertex of IIG st depth (v1,SCS) <= k + 1 holds
(Following s) . v1 = IGValue (v1,iv)
let s be State of SCS; ::_thesis: for iv being InputValues of SCS
for k being Element of NAT st ( for v being Vertex of IIG st depth (v,SCS) <= k holds
s . v = IGValue (v,iv) ) holds
for v1 being Vertex of IIG st depth (v1,SCS) <= k + 1 holds
(Following s) . v1 = IGValue (v1,iv)
let iv be InputValues of SCS; ::_thesis: for k being Element of NAT st ( for v being Vertex of IIG st depth (v,SCS) <= k holds
s . v = IGValue (v,iv) ) holds
for v1 being Vertex of IIG st depth (v1,SCS) <= k + 1 holds
(Following s) . v1 = IGValue (v1,iv)
let k be Element of NAT ; ::_thesis: ( ( for v being Vertex of IIG st depth (v,SCS) <= k holds
s . v = IGValue (v,iv) ) implies for v1 being Vertex of IIG st depth (v1,SCS) <= k + 1 holds
(Following s) . v1 = IGValue (v1,iv) )
assume A1: for v being Vertex of IIG st depth (v,SCS) <= k holds
s . v = IGValue (v,iv) ; ::_thesis: for v1 being Vertex of IIG st depth (v1,SCS) <= k + 1 holds
(Following s) . v1 = IGValue (v1,iv)
let v be Vertex of IIG; ::_thesis: ( depth (v,SCS) <= k + 1 implies (Following s) . v = IGValue (v,iv) )
assume A2: depth (v,SCS) <= k + 1 ; ::_thesis: (Following s) . v = IGValue (v,iv)
 v in the carrier of IIG ;
then A3: v in (InputVertices IIG) \/ (InnerVertices IIG) by XBOOLE_1:45;
percases ( v in InputVertices IIG or v in InnerVertices IIG ) by A3, XBOOLE_0:def_3;
supposeA4: v in InputVertices IIG ; ::_thesis: (Following s) . v = IGValue (v,iv)
then A5: depth (v,SCS) = 0 by CIRCUIT1:18;
thus (Following s) . v = s . v by A4, Def5
.= IGValue (v,iv) by A1, A5, NAT_1:2 ; ::_thesis: verum
end;
supposeA6: v in InnerVertices IIG ; ::_thesis: (Following s) . v = IGValue (v,iv)
set F = Eval SCS;
set X = the Sorts of SCS;
set U1 = FreeEnv SCS;
set o = action_at v;
set taofo = the_arity_of (action_at v);
deffunc H1( Nat) ->  Element of the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at v)) /. $1) = IGTree (((the_arity_of (action_at v)) /. $1),iv);
consider p being FinSequence such that
A7: len p = len (the_arity_of (action_at v)) and
A8: for k being Nat st k in dom p holds
p . k = H1(k) from FINSEQ_1:sch_2();
A9: for k being Element of NAT st k in dom p holds
p . k = H1(k) by A8;
A10: now__::_thesis:_for_k_being_Nat_st_k_in_dom_p_holds_
p_._k_in_the_Sorts_of_(FreeEnv_SCS)_._((the_arity_of_(action_at_v))_/._k)
let k be Nat; ::_thesis: ( k in dom p implies p . k in the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at v)) /. k) )
assume  k in dom p ; ::_thesis: p . k in the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at v)) /. k)
then  p . k = IGTree (((the_arity_of (action_at v)) /. k),iv) by A8;
hence  p . k in the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at v)) /. k) ; ::_thesis: verum
end;
 FreeEnv SCS = MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #) by MSAFREE:def_14;
then A11: 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 ;
reconsider ods = (action_at v) depends_on_in s as Function ;
A12: Eval SCS is_homomorphism FreeEnv SCS,SCS by MSAFREE2:def_9;
 dom the Arity of IIG = the carrier' of IIG by FUNCT_2:def_1;
then A13: (( the Sorts of SCS #) * the Arity of IIG) . (action_at v) = ( the Sorts of SCS #) . ( the Arity of IIG . (action_at v)) by FUNCT_1:13
.= ( the Sorts of SCS #) . (the_arity_of (action_at v)) by MSUALG_1:def_1
.= product ( the Sorts of SCS * (the_arity_of (action_at v))) by FINSEQ_2:def_5 ;
A14: dom p = dom (the_arity_of (action_at v)) by A7, FINSEQ_3:29;
reconsider p = p as Element of Args ((action_at v),(FreeEnv SCS)) by A7, A10, MSAFREE2:5;
A15: ( FreeEnv SCS = MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #) & Args ((action_at v),(FreeEnv SCS)) = (( the Sorts of (FreeEnv SCS) #) * the Arity of IIG) . (action_at v) ) by MSAFREE:def_14, MSUALG_1:def_4;
then reconsider p9 = p as FinSequence of TS (DTConMSA the Sorts of SCS) by MSAFREE:8;
 Sym ((action_at v), the Sorts of SCS) ==> roots p9 by A15, MSAFREE:10;
then A16: (Den ((action_at v),(FreeEnv SCS))) . p = (Sym ((action_at v), the Sorts of SCS)) -tree p9 by A11, MSAFREE:def_12
.= [(action_at v), the carrier of IIG] -tree p9 by MSAFREE:def_9
.= IGTree (v,iv) by A6, A9, A14, Th9 ;
reconsider Fp = (Eval SCS) # p as Function ;
A17: Args ((action_at v),SCS) = (( the Sorts of SCS #) * the Arity of IIG) . (action_at v) by MSUALG_1:def_4;
now__::_thesis:_(_dom_(the_arity_of_(action_at_v))_=_dom_Fp_&_dom_(the_arity_of_(action_at_v))_=_dom_ods_&_(_for_x_being_set_st_x_in_dom_(the_arity_of_(action_at_v))_holds_
Fp_._x_=_ods_._x_)_)
 ( dom the Sorts of SCS = the carrier of IIG & rng (the_arity_of (action_at v)) c= the carrier of IIG ) by FINSEQ_1:def_4, PARTFUN1:def_2;
hence  dom (the_arity_of (action_at v)) = dom ( the Sorts of SCS * (the_arity_of (action_at v))) by RELAT_1:27
.= dom Fp by A13, A17, CARD_3:9 ;
::_thesis: ( dom (the_arity_of (action_at v)) = dom ods & ( for x being set st x in dom (the_arity_of (action_at v)) holds
Fp . x = ods . x ) )
 ( dom s = the carrier of IIG & rng (the_arity_of (action_at v)) c= the carrier of IIG ) by CIRCUIT1:3, FINSEQ_1:def_4;
hence  dom (the_arity_of (action_at v)) = dom (s * (the_arity_of (action_at v))) by RELAT_1:27
.= dom ods by CIRCUIT1:def_3 ;
::_thesis: for x being set st x in dom (the_arity_of (action_at v)) holds
Fp . x = ods . x
let x be set ; ::_thesis: ( x in dom (the_arity_of (action_at v)) implies Fp . x = ods . x )
reconsider v1 = (the_arity_of (action_at v)) /. x as Element of IIG ;
assume A18: x in dom (the_arity_of (action_at v)) ; ::_thesis: Fp . x = ods . x
then reconsider x9 = x as Element of NAT ;
A19: v1 = (the_arity_of (action_at v)) . x9 by A18, PARTFUN1:def_6;
then  v1 in rng (the_arity_of (action_at v)) by A18, FUNCT_1:def_3;
then  depth (v1,SCS) < k + 1 by A2, A6, CIRCUIT1:19, XXREAL_0:2;
then A20: depth (v1,SCS) <= k by NAT_1:13;
thus Fp . x = ((Eval SCS) . v1) . (p9 . x9) by A14, A18, MSUALG_3:def_6
.= IGValue (v1,iv) by A8, A14, A18
.= s . v1 by A1, A20
.= (s * (the_arity_of (action_at v))) . x by A18, A19, FUNCT_1:13
.= ods . x by CIRCUIT1:def_3 ; ::_thesis: verum
end;
then  (Eval SCS) # p = (action_at v) depends_on_in s by FUNCT_1:2;
hence (Following s) . v = (Den ((action_at v),SCS)) . ((Eval SCS) # p) by A6, Def5
.= ((Eval SCS) . (the_result_sort_of (action_at v))) . ((Den ((action_at v),(FreeEnv SCS))) . p) by A12, MSUALG_3:def_7
.= IGValue (v,iv) by A6, A16, MSAFREE2:def_7 ;
::_thesis: verum
end;
end;
end;


theorem Th14: :: CIRCUIT2:14
for IIG being non empty finite non void Circuit-like monotonic ManySortedSign
for SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS st commute InpFs is constant & not InputVertices IIG is empty holds
for s being State of SCS
for iv being InputValues of SCS st iv = (commute InpFs) . 0 holds
for k being Element of NAT holds iv c= (Computation (s,InpFs)) . k
proof
let IIG be non empty finite non void Circuit-like monotonic ManySortedSign ; ::_thesis: for SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS st commute InpFs is constant & not InputVertices IIG is empty holds
for s being State of SCS
for iv being InputValues of SCS st iv = (commute InpFs) . 0 holds
for k being Element of NAT holds iv c= (Computation (s,InpFs)) . k
let SCS be non-empty Circuit of IIG; ::_thesis: for InpFs being InputFuncs of SCS st commute InpFs is constant & not InputVertices IIG is empty holds
for s being State of SCS
for iv being InputValues of SCS st iv = (commute InpFs) . 0 holds
for k being Element of NAT holds iv c= (Computation (s,InpFs)) . k
let InpFs be InputFuncs of SCS; ::_thesis: ( commute InpFs is constant & not InputVertices IIG is empty implies for s being State of SCS
for iv being InputValues of SCS st iv = (commute InpFs) . 0 holds
for k being Element of NAT holds iv c= (Computation (s,InpFs)) . k )
assume that
A1: commute InpFs is constant and
A2: not InputVertices IIG is empty ; ::_thesis: for s being State of SCS
for iv being InputValues of SCS st iv = (commute InpFs) . 0 holds
for k being Element of NAT holds iv c= (Computation (s,InpFs)) . k
A3: dom (commute InpFs) = NAT by A2, PRE_CIRC:5;
let s be State of SCS; ::_thesis: for iv being InputValues of SCS st iv = (commute InpFs) . 0 holds
for k being Element of NAT holds iv c= (Computation (s,InpFs)) . k
let iv be InputValues of SCS; ::_thesis: ( iv = (commute InpFs) . 0 implies for k being Element of NAT holds iv c= (Computation (s,InpFs)) . k )
assume A4: iv = (commute InpFs) . 0 ; ::_thesis: for k being Element of NAT holds iv c= (Computation (s,InpFs)) . k
let k be Element of NAT ; ::_thesis: iv c= (Computation (s,InpFs)) . k
 IIG is with_input_V by A2, MSAFREE2:def_4;
then A5: k -th_InputValues InpFs = (commute InpFs) . k by CIRCUIT1:def_2
.= iv by A1, A4, A3, FUNCT_1:def_10 ;
set Ck = (Computation (s,InpFs)) . k;
 ( dom iv = InputVertices IIG & dom (Set-Constants SCS) = SortsWithConstants IIG ) by PARTFUN1:def_2;
then A6: dom iv misses dom (Set-Constants SCS) by MSAFREE2:4;
percases ( k = 0 or ex n being Nat st k = n + 1 ) by NAT_1:6;
supposeA7: k = 0 ; ::_thesis: iv c= (Computation (s,InpFs)) . k
then (Computation (s,InpFs)) . k = InitialComp (s,InpFs) by Def9
.= (s +* (0 -th_InputValues InpFs)) +* (Set-Constants SCS) ;
hence  iv c= (Computation (s,InpFs)) . k by A5, A6, A7, FUNCT_4:25, FUNCT_4:124; ::_thesis: verum
end;
suppose ex n being Nat st k = n + 1 ; ::_thesis: iv c= (Computation (s,InpFs)) . k
then consider n being Nat such that
A8: k = n + 1 ;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
reconsider Cn = (Computation (s,InpFs)) . n as State of SCS ;
(Computation (s,InpFs)) . k = Following (Cn,(k -th_InputValues InpFs)) by A8, Def9
.= Following (Cn +* iv) by A5 ;
hence  iv c= (Computation (s,InpFs)) . k by Th12, FUNCT_4:25; ::_thesis: verum
end;
end;
end;

theorem :: CIRCUIT2:15
for IIG being non empty finite non void Circuit-like monotonic ManySortedSign
for SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS
for s being State of SCS
for n being Element of NAT st commute InpFs is constant & not InputVertices IIG is empty & (Computation (s,InpFs)) . n is stable holds
for m being Element of NAT st n <= m holds
(Computation (s,InpFs)) . n = (Computation (s,InpFs)) . m
proof
let IIG be non empty finite non void Circuit-like monotonic ManySortedSign ; ::_thesis: for SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS
for s being State of SCS
for n being Element of NAT st commute InpFs is constant & not InputVertices IIG is empty & (Computation (s,InpFs)) . n is stable holds
for m being Element of NAT st n <= m holds
(Computation (s,InpFs)) . n = (Computation (s,InpFs)) . m
let SCS be non-empty Circuit of IIG; ::_thesis: for InpFs being InputFuncs of SCS
for s being State of SCS
for n being Element of NAT st commute InpFs is constant & not InputVertices IIG is empty & (Computation (s,InpFs)) . n is stable holds
for m being Element of NAT st n <= m holds
(Computation (s,InpFs)) . n = (Computation (s,InpFs)) . m
let InpFs be InputFuncs of SCS; ::_thesis: for s being State of SCS
for n being Element of NAT st commute InpFs is constant & not InputVertices IIG is empty & (Computation (s,InpFs)) . n is stable holds
for m being Element of NAT st n <= m holds
(Computation (s,InpFs)) . n = (Computation (s,InpFs)) . m
let s be State of SCS; ::_thesis: for n being Element of NAT st commute InpFs is constant & not InputVertices IIG is empty & (Computation (s,InpFs)) . n is stable holds
for m being Element of NAT st n <= m holds
(Computation (s,InpFs)) . n = (Computation (s,InpFs)) . m
let n be Element of NAT ; ::_thesis: ( commute InpFs is constant & not InputVertices IIG is empty & (Computation (s,InpFs)) . n is stable implies for m being Element of NAT st n <= m holds
(Computation (s,InpFs)) . n = (Computation (s,InpFs)) . m )
assume that
A1: commute InpFs is constant and
A2: not InputVertices IIG is empty and
A3: (Computation (s,InpFs)) . n is stable ; ::_thesis: for m being Element of NAT st n <= m holds
(Computation (s,InpFs)) . n = (Computation (s,InpFs)) . m
defpred S1[ Element of NAT ] means ( n <= $1 implies (Computation (s,InpFs)) . n = (Computation (s,InpFs)) . $1 );
A4: now__::_thesis:_for_m_being_Element_of_NAT_st_S1[m]_holds_
S1[m_+_1]
let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A5: S1[m] ; ::_thesis: S1[m + 1]
thus  S1[m + 1] ::_thesis: verum
proof
A6: IIG is with_input_V by A2, MSAFREE2:def_4;
then reconsider iv = (commute InpFs) . 0 as InputValues of SCS by CIRCUIT1:2;
reconsider Ckm = (Computation (s,InpFs)) . m as State of SCS ;
A7: dom (commute InpFs) = NAT by A2, PRE_CIRC:5;
(m + 1) -th_InputValues InpFs = (commute InpFs) . (m + 1) by A6, CIRCUIT1:def_2
.= iv by A1, A7, FUNCT_1:def_10 ;
then A8: (m + 1) -th_InputValues InpFs c= (Computation (s,InpFs)) . m by A1, A2, Th14;
assume A9: n <= m + 1 ; ::_thesis: (Computation (s,InpFs)) . n = (Computation (s,InpFs)) . (m + 1)
percases ( n <= m or n = m + 1 ) by A9, NAT_1:8;
suppose n <= m ; ::_thesis: (Computation (s,InpFs)) . n = (Computation (s,InpFs)) . (m + 1)
hence (Computation (s,InpFs)) . n = Following Ckm by A3, A5, Def6
.= Following (((Computation (s,InpFs)) . m),((m + 1) -th_InputValues InpFs)) by A8, FUNCT_4:98
.= (Computation (s,InpFs)) . (m + 1) by Def9 ;
::_thesis: verum
end;
suppose n = m + 1 ; ::_thesis: (Computation (s,InpFs)) . n = (Computation (s,InpFs)) . (m + 1)
hence  (Computation (s,InpFs)) . n = (Computation (s,InpFs)) . (m + 1) ; ::_thesis: verum
end;
end;
end;
end;
A10: S1[ 0 ] by NAT_1:3;
thus  for m being Element of NAT holds S1[m] from NAT_1:sch_1(A10, A4); ::_thesis: verum
end;

theorem Th16: :: CIRCUIT2:16
for IIG being non empty finite non void Circuit-like monotonic ManySortedSign
for SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS st commute InpFs is constant & not InputVertices IIG is empty holds
for s being State of SCS
for iv being InputValues of SCS st iv = (commute InpFs) . 0 holds
for k being Element of NAT
for v being Vertex of IIG st depth (v,SCS) <= k holds
((Computation (s,InpFs)) . k) . v = IGValue (v,iv)
proof
let IIG be non empty finite non void Circuit-like monotonic ManySortedSign ; ::_thesis: for SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS st commute InpFs is constant & not InputVertices IIG is empty holds
for s being State of SCS
for iv being InputValues of SCS st iv = (commute InpFs) . 0 holds
for k being Element of NAT
for v being Vertex of IIG st depth (v,SCS) <= k holds
((Computation (s,InpFs)) . k) . v = IGValue (v,iv)
let SCS be non-empty Circuit of IIG; ::_thesis: for InpFs being InputFuncs of SCS st commute InpFs is constant & not InputVertices IIG is empty holds
for s being State of SCS
for iv being InputValues of SCS st iv = (commute InpFs) . 0 holds
for k being Element of NAT
for v being Vertex of IIG st depth (v,SCS) <= k holds
((Computation (s,InpFs)) . k) . v = IGValue (v,iv)
let InpFs be InputFuncs of SCS; ::_thesis: ( commute InpFs is constant & not InputVertices IIG is empty implies for s being State of SCS
for iv being InputValues of SCS st iv = (commute InpFs) . 0 holds
for k being Element of NAT
for v being Vertex of IIG st depth (v,SCS) <= k holds
((Computation (s,InpFs)) . k) . v = IGValue (v,iv) )
assume that
A1: commute InpFs is constant and
A2: not InputVertices IIG is empty ; ::_thesis: for s being State of SCS
for iv being InputValues of SCS st iv = (commute InpFs) . 0 holds
for k being Element of NAT
for v being Vertex of IIG st depth (v,SCS) <= k holds
((Computation (s,InpFs)) . k) . v = IGValue (v,iv)
let s be State of SCS; ::_thesis: for iv being InputValues of SCS st iv = (commute InpFs) . 0 holds
for k being Element of NAT
for v being Vertex of IIG st depth (v,SCS) <= k holds
((Computation (s,InpFs)) . k) . v = IGValue (v,iv)
let iv be InputValues of SCS; ::_thesis: ( iv = (commute InpFs) . 0 implies for k being Element of NAT
for v being Vertex of IIG st depth (v,SCS) <= k holds
((Computation (s,InpFs)) . k) . v = IGValue (v,iv) )
assume A3: iv = (commute InpFs) . 0 ; ::_thesis: for k being Element of NAT
for v being Vertex of IIG st depth (v,SCS) <= k holds
((Computation (s,InpFs)) . k) . v = IGValue (v,iv)
defpred S1[ Element of NAT ] means  for v being Vertex of IIG st depth (v,SCS) <= $1 holds
((Computation (s,InpFs)) . $1) . v = IGValue (v,iv);
A4: IIG is with_input_V by A2, MSAFREE2:def_4;
A5: S1[ 0 ]
proof
let v be Vertex of IIG; ::_thesis: ( depth (v,SCS) <= 0 implies ((Computation (s,InpFs)) . 0) . v = IGValue (v,iv) )
assume  depth (v,SCS) <= 0 ; ::_thesis: ((Computation (s,InpFs)) . 0) . v = IGValue (v,iv)
then A6: depth (v,SCS) = 0 by NAT_1:3;
A7: (Computation (s,InpFs)) . 0 = InitialComp (s,InpFs) by Def9
.= (s +* (0 -th_InputValues InpFs)) +* (Set-Constants SCS) ;
percases ( v in InputVertices IIG or v in SortsWithConstants IIG ) by A6, CIRCUIT1:18;
supposeA8: v in InputVertices IIG ; ::_thesis: ((Computation (s,InpFs)) . 0) . v = IGValue (v,iv)
A9: dom (0 -th_InputValues InpFs) = InputVertices IIG by PARTFUN1:def_2;
 InputVertices IIG misses SortsWithConstants IIG by MSAFREE2:4;
then  not v in SortsWithConstants IIG by A8, XBOOLE_0:3;
then  not v in dom (Set-Constants SCS) by PARTFUN1:def_2;
hence ((Computation (s,InpFs)) . 0) . v = (s +* (0 -th_InputValues InpFs)) . v by A7, FUNCT_4:11
.= (0 -th_InputValues InpFs) . v by A8, A9, FUNCT_4:13
.= iv . v by A4, A3, CIRCUIT1:def_2
.= IGValue (v,iv) by A8, Th10 ;
::_thesis: verum
end;
supposeA10: v in SortsWithConstants IIG ; ::_thesis: ((Computation (s,InpFs)) . 0) . v = IGValue (v,iv)
then  v in dom (Set-Constants SCS) by PARTFUN1:def_2;
hence ((Computation (s,InpFs)) . 0) . v = (Set-Constants SCS) . v by A7, FUNCT_4:13
.= IGValue (v,iv) by A10, Th11 ;
::_thesis: verum
end;
end;
end;
A11: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
reconsider Ck = (Computation (s,InpFs)) . k as State of SCS ;
assume A12: S1[k] ; ::_thesis: S1[k + 1]
let v be Vertex of IIG; ::_thesis: ( depth (v,SCS) <= k + 1 implies ((Computation (s,InpFs)) . (k + 1)) . v = IGValue (v,iv) )
assume A13: depth (v,SCS) <= k + 1 ; ::_thesis: ((Computation (s,InpFs)) . (k + 1)) . v = IGValue (v,iv)
A14: dom (commute InpFs) = NAT by A2, PRE_CIRC:5;
A15: (k + 1) -th_InputValues InpFs = (commute InpFs) . (k + 1) by A4, CIRCUIT1:def_2
.= (commute InpFs) . 0 by A1, A14, FUNCT_1:def_10 ;
A16: iv c= Ck by A1, A2, A3, Th14;
thus ((Computation (s,InpFs)) . (k + 1)) . v = (Following (Ck,((k + 1) -th_InputValues InpFs))) . v by Def9
.= (Following Ck) . v by A3, A15, A16, FUNCT_4:98
.= IGValue (v,iv) by A12, A13, Th13 ; ::_thesis: verum
end;
thus  for k being Element of NAT holds S1[k] from NAT_1:sch_1(A5, A11); ::_thesis: verum
end;

theorem Th17: :: CIRCUIT2:17
for IIG being non empty finite non void Circuit-like monotonic ManySortedSign
for SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS
for iv being InputValues of SCS st commute InpFs is constant & not InputVertices IIG is empty & iv = (commute InpFs) . 0 holds
for s being State of SCS
for v being Vertex of IIG
for n being Element of NAT st n = depth SCS holds
((Computation (s,InpFs)) . n) . v = IGValue (v,iv)
proof
let IIG be non empty finite non void Circuit-like monotonic ManySortedSign ; ::_thesis: for SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS
for iv being InputValues of SCS st commute InpFs is constant & not InputVertices IIG is empty & iv = (commute InpFs) . 0 holds
for s being State of SCS
for v being Vertex of IIG
for n being Element of NAT st n = depth SCS holds
((Computation (s,InpFs)) . n) . v = IGValue (v,iv)
let SCS be non-empty Circuit of IIG; ::_thesis: for InpFs being InputFuncs of SCS
for iv being InputValues of SCS st commute InpFs is constant & not InputVertices IIG is empty & iv = (commute InpFs) . 0 holds
for s being State of SCS
for v being Vertex of IIG
for n being Element of NAT st n = depth SCS holds
((Computation (s,InpFs)) . n) . v = IGValue (v,iv)
let InpFs be InputFuncs of SCS; ::_thesis: for iv being InputValues of SCS st commute InpFs is constant & not InputVertices IIG is empty & iv = (commute InpFs) . 0 holds
for s being State of SCS
for v being Vertex of IIG
for n being Element of NAT st n = depth SCS holds
((Computation (s,InpFs)) . n) . v = IGValue (v,iv)
let iv be InputValues of SCS; ::_thesis: ( commute InpFs is constant & not InputVertices IIG is empty & iv = (commute InpFs) . 0 implies for s being State of SCS
for v being Vertex of IIG
for n being Element of NAT st n = depth SCS holds
((Computation (s,InpFs)) . n) . v = IGValue (v,iv) )
assume A1: ( commute InpFs is constant & not InputVertices IIG is empty & iv = (commute InpFs) . 0 ) ; ::_thesis: for s being State of SCS
for v being Vertex of IIG
for n being Element of NAT st n = depth SCS holds
((Computation (s,InpFs)) . n) . v = IGValue (v,iv)
let s be State of SCS; ::_thesis: for v being Vertex of IIG
for n being Element of NAT st n = depth SCS holds
((Computation (s,InpFs)) . n) . v = IGValue (v,iv)
let v be Vertex of IIG; ::_thesis: for n being Element of NAT st n = depth SCS holds
((Computation (s,InpFs)) . n) . v = IGValue (v,iv)
A2: depth (v,SCS) <= depth SCS by CIRCUIT1:17;
let n be Element of NAT ; ::_thesis: ( n = depth SCS implies ((Computation (s,InpFs)) . n) . v = IGValue (v,iv) )
assume  n = depth SCS ; ::_thesis: ((Computation (s,InpFs)) . n) . v = IGValue (v,iv)
hence  ((Computation (s,InpFs)) . n) . v = IGValue (v,iv) by A1, A2, Th16; ::_thesis: verum
end;

theorem :: CIRCUIT2:18
for IIG being non empty finite non void Circuit-like monotonic ManySortedSign
for SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS st commute InpFs is constant & not InputVertices IIG is empty holds
for s being State of SCS
for n being Element of NAT st n = depth SCS holds
(Computation (s,InpFs)) . n is stable
proof
let IIG be non empty finite non void Circuit-like monotonic ManySortedSign ; ::_thesis: for SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS st commute InpFs is constant & not InputVertices IIG is empty holds
for s being State of SCS
for n being Element of NAT st n = depth SCS holds
(Computation (s,InpFs)) . n is stable
let SCS be non-empty Circuit of IIG; ::_thesis: for InpFs being InputFuncs of SCS st commute InpFs is constant & not InputVertices IIG is empty holds
for s being State of SCS
for n being Element of NAT st n = depth SCS holds
(Computation (s,InpFs)) . n is stable
let InpFs be InputFuncs of SCS; ::_thesis: ( commute InpFs is constant & not InputVertices IIG is empty implies for s being State of SCS
for n being Element of NAT st n = depth SCS holds
(Computation (s,InpFs)) . n is stable )
assume that
A1: commute InpFs is constant and
A2: not InputVertices IIG is empty ; ::_thesis: for s being State of SCS
for n being Element of NAT st n = depth SCS holds
(Computation (s,InpFs)) . n is stable
A3: dom (commute InpFs) = NAT by A2, PRE_CIRC:5;
A4: IIG is with_input_V by A2, MSAFREE2:def_4;
then reconsider iv = (commute InpFs) . 0 as InputValues of SCS by CIRCUIT1:2;
let s be State of SCS; ::_thesis: for n being Element of NAT st n = depth SCS holds
(Computation (s,InpFs)) . n is stable
let n be Element of NAT ; ::_thesis: ( n = depth SCS implies (Computation (s,InpFs)) . n is stable )
assume A5: n = depth SCS ; ::_thesis: (Computation (s,InpFs)) . n is stable
reconsider Cn = (Computation (s,InpFs)) . n as State of SCS ;
A6: iv c= Cn by A1, A2, Th14;
A7: (n + 1) -th_InputValues InpFs = (commute InpFs) . (n + 1) by A4, CIRCUIT1:def_2
.= (commute InpFs) . 0 by A1, A3, FUNCT_1:def_10 ;
reconsider Cn1 = (Computation (s,InpFs)) . (n + 1) as State of SCS ;
now__::_thesis:_(_the_carrier_of_IIG_=_dom_Cn_&_the_carrier_of_IIG_=_dom_Cn1_&_(_for_x_being_set_st_x_in_the_carrier_of_IIG_holds_
Cn_._x_=_Cn1_._x_)_)
thus  the carrier of IIG = dom Cn by CIRCUIT1:3; ::_thesis: ( the carrier of IIG = dom Cn1 & ( for x being set st x in the carrier of IIG holds
Cn . x = Cn1 . x ) )
thus  the carrier of IIG = dom Cn1 by CIRCUIT1:3; ::_thesis: for x being set st x in the carrier of IIG holds
Cn . x = Cn1 . x
let x be set ; ::_thesis: ( x in the carrier of IIG implies Cn . x = Cn1 . x )
assume  x in the carrier of IIG ; ::_thesis: Cn . x = Cn1 . x
then reconsider x9 = x as Vertex of IIG ;
A8: depth (x9,SCS) <= n by A5, CIRCUIT1:17;
then  Cn . x9 = IGValue (x9,iv) by A1, A2, Th16;
hence  Cn . x = Cn1 . x by A1, A2, A8, Th16, NAT_1:12; ::_thesis: verum
end;
hence (Computation (s,InpFs)) . n = (Computation (s,InpFs)) . (n + 1) by FUNCT_1:2
.= Following (Cn,((n + 1) -th_InputValues InpFs)) by Def9
.= Following ((Computation (s,InpFs)) . n) by A7, A6, FUNCT_4:98 ;
:: according to CIRCUIT2:def_6 ::_thesis: verum
end;

theorem :: CIRCUIT2:19
for IIG being non empty finite non void Circuit-like monotonic ManySortedSign
for SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS st commute InpFs is constant & not InputVertices IIG is empty holds
for s1, s2 being State of SCS holds (Computation (s1,InpFs)) . (depth SCS) = (Computation (s2,InpFs)) . (depth SCS)
proof
let IIG be non empty finite non void Circuit-like monotonic ManySortedSign ; ::_thesis: for SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS st commute InpFs is constant & not InputVertices IIG is empty holds
for s1, s2 being State of SCS holds (Computation (s1,InpFs)) . (depth SCS) = (Computation (s2,InpFs)) . (depth SCS)
let SCS be non-empty Circuit of IIG; ::_thesis: for InpFs being InputFuncs of SCS st commute InpFs is constant & not InputVertices IIG is empty holds
for s1, s2 being State of SCS holds (Computation (s1,InpFs)) . (depth SCS) = (Computation (s2,InpFs)) . (depth SCS)
let InpFs be InputFuncs of SCS; ::_thesis: ( commute InpFs is constant & not InputVertices IIG is empty implies for s1, s2 being State of SCS holds (Computation (s1,InpFs)) . (depth SCS) = (Computation (s2,InpFs)) . (depth SCS) )
assume that
A1: commute InpFs is constant and
A2: not InputVertices IIG is empty ; ::_thesis: for s1, s2 being State of SCS holds (Computation (s1,InpFs)) . (depth SCS) = (Computation (s2,InpFs)) . (depth SCS)
 IIG is with_input_V by A2, MSAFREE2:def_4;
then reconsider iv = (commute InpFs) . 0 as InputValues of SCS by CIRCUIT1:2;
reconsider dSCS = depth SCS as Element of NAT by ORDINAL1:def_12;
let s1, s2 be State of SCS; ::_thesis: (Computation (s1,InpFs)) . (depth SCS) = (Computation (s2,InpFs)) . (depth SCS)
reconsider Cs1 = (Computation (s1,InpFs)) . dSCS as State of SCS ;
reconsider Cs2 = (Computation (s2,InpFs)) . dSCS as State of SCS ;
now__::_thesis:_(_the_carrier_of_IIG_=_dom_Cs1_&_the_carrier_of_IIG_=_dom_Cs2_&_(_for_x_being_set_st_x_in_the_carrier_of_IIG_holds_
Cs1_._x_=_Cs2_._x_)_)
thus  the carrier of IIG = dom Cs1 by CIRCUIT1:3; ::_thesis: ( the carrier of IIG = dom Cs2 & ( for x being set st x in the carrier of IIG holds
Cs1 . x = Cs2 . x ) )
thus  the carrier of IIG = dom Cs2 by CIRCUIT1:3; ::_thesis: for x being set st x in the carrier of IIG holds
Cs1 . x = Cs2 . x
let x be set ; ::_thesis: ( x in the carrier of IIG implies Cs1 . x = Cs2 . x )
assume  x in the carrier of IIG ; ::_thesis: Cs1 . x = Cs2 . x
then reconsider x9 = x as Vertex of IIG ;
 Cs1 . x9 = IGValue (x9,iv) by A1, A2, Th17;
hence  Cs1 . x = Cs2 . x by A1, A2, Th17; ::_thesis: verum
end;
hence  (Computation (s1,InpFs)) . (depth SCS) = (Computation (s2,InpFs)) . (depth SCS) by FUNCT_1:2; ::_thesis: verum
end;