:: CIRCUIT1 semantic presentation

begin

definition
let S be non empty non void Circuit-like ManySortedSign ;
mode Circuit of S is finite-yielding MSAlgebra over S;
end;

definition
let IIG be non empty non void Circuit-like ManySortedSign ;
let SCS be non-empty Circuit of IIG;
func Set-Constants SCS ->  ManySortedSet of SortsWithConstants IIG means :Def1: :: CIRCUIT1:def 1
 for x being Vertex of IIG st x in dom it holds
it . x in Constants (SCS,x);
existence
 ex b1 being ManySortedSet of SortsWithConstants IIG st
for x being Vertex of IIG st x in dom b1 holds
b1 . x in Constants (SCS,x)
proof
defpred S1[ set , set ] means  ex v being Vertex of IIG st
( v = $1 & $2 in Constants (SCS,v) );
set SW = SortsWithConstants IIG;
A1: now__::_thesis:_for_i_being_set_st_i_in_SortsWithConstants_IIG_holds_
ex_y_being_set_st_S1[i,y]
let i be set ; ::_thesis: ( i in SortsWithConstants IIG implies ex y being set st S1[i,y] )
A2: SortsWithConstants IIG =  {  v where v is SortSymbol of IIG : v is with_const_op  }  by MSAFREE2:def_1;
assume A3: i in SortsWithConstants IIG ; ::_thesis: ex y being set st S1[i,y]
then reconsider x = i as Vertex of IIG ;
consider v being Vertex of IIG such that
A4: v = x and
A5: v is with_const_op by A3, A2;
consider o being OperSymbol of IIG such that
A6: the Arity of IIG . o = {} and
A7: the ResultSort of IIG . o = v by A5, MSUALG_2:def_1;
A8: dom the ResultSort of IIG = the carrier' of IIG by FUNCT_2:def_1;
set y = the Element of rng (Den (o,SCS));
Result (o,SCS) = ( the Sorts of SCS * the ResultSort of IIG) . o by MSUALG_1:def_5
.= the Sorts of SCS . ( the ResultSort of IIG . o) by A8, FUNCT_1:13 ;
then reconsider y9 = the Element of rng (Den (o,SCS)) as Element of the Sorts of SCS . v by A7;
reconsider y = the Element of rng (Den (o,SCS)) as set ;
take y = y; ::_thesis: S1[i,y]
 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  y9 in Constants (SCS,x) by A4, A6, A7;
hence  S1[i,y] ; ::_thesis: verum
end;
consider f being ManySortedSet of SortsWithConstants IIG such that
A9: for i being set st i in SortsWithConstants IIG holds
S1[i,f . i] from PBOOLE:sch_3(A1);
take  f ; ::_thesis: for x being Vertex of IIG st x in dom f holds
f . x in Constants (SCS,x)
let x be Vertex of IIG; ::_thesis: ( x in dom f implies f . x in Constants (SCS,x) )
assume  x in dom f ; ::_thesis: f . x in Constants (SCS,x)
then  x in SortsWithConstants IIG ;
then  S1[x,f . x] by A9;
hence  f . x in Constants (SCS,x) ; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being ManySortedSet of SortsWithConstants IIG st ( for x being Vertex of IIG st x in dom b1 holds
b1 . x in Constants (SCS,x) ) & ( for x being Vertex of IIG st x in dom b2 holds
b2 . x in Constants (SCS,x) ) holds
b1 = b2;
proof
let it1, it2 be ManySortedSet of SortsWithConstants IIG; ::_thesis: ( ( for x being Vertex of IIG st x in dom it1 holds
it1 . x in Constants (SCS,x) ) & ( for x being Vertex of IIG st x in dom it2 holds
it2 . x in Constants (SCS,x) ) implies it1 = it2 )
assume A10: for x being Vertex of IIG st x in dom it1 holds
it1 . x in Constants (SCS,x) ; ::_thesis: ( ex x being Vertex of IIG st
( x in dom it2 & not it2 . x in Constants (SCS,x) ) or it1 = it2 )
assume A11: for x being Vertex of IIG st x in dom it2 holds
it2 . x in Constants (SCS,x) ; ::_thesis: it1 = it2
now__::_thesis:_for_i_being_set_st_i_in_SortsWithConstants_IIG_holds_
it1_._i_=_it2_._i
let i be set ; ::_thesis: ( i in SortsWithConstants IIG implies it1 . i = it2 . i )
A12: dom the Arity of IIG = the carrier' of IIG by FUNCT_2:def_1;
assume A13: i in SortsWithConstants IIG ; ::_thesis: it1 . i = it2 . i
then reconsider v = i as Vertex of IIG ;
A14: 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;
 dom it2 = SortsWithConstants IIG by PARTFUN1:def_2;
then  it2 . v in Constants (SCS,v) by A11, A13;
then consider a2 being Element of the Sorts of SCS . v such that
A15: it2 . v = a2 and
A16: ex o being OperSymbol of IIG st
( the Arity of IIG . o = {} & the ResultSort of IIG . o = v & a2 in rng (Den (o,SCS)) ) by A14;
consider o2 being OperSymbol of IIG such that
 the Arity of IIG . o2 = {} and
A17: the ResultSort of IIG . o2 = v and
A18: a2 in rng (Den (o2,SCS)) by A16;
A19: the_result_sort_of o2 = v by A17, MSUALG_1:def_2;
 dom it1 = SortsWithConstants IIG by PARTFUN1:def_2;
then  it1 . v in Constants (SCS,v) by A10, A13;
then consider a1 being Element of the Sorts of SCS . v such that
A20: it1 . v = a1 and
A21: ex o being OperSymbol of IIG st
( the Arity of IIG . o = {} & the ResultSort of IIG . o = v & a1 in rng (Den (o,SCS)) ) by A14;
consider o1 being OperSymbol of IIG such that
A22: the Arity of IIG . o1 = {} and
A23: the ResultSort of IIG . o1 = v and
A24: a1 in rng (Den (o1,SCS)) by A21;
A25: {} = <*> the carrier of IIG ;
A26: ex x2 being set st
( x2 in dom (Den (o2,SCS)) & a2 = (Den (o2,SCS)) . x2 ) by A18, FUNCT_1:def_3;
 the_result_sort_of o1 = v by A23, MSUALG_1:def_2;
then A27: o1 = o2 by A19, MSAFREE2:def_6;
consider x1 being set  such that
A28: x1 in dom (Den (o1,SCS)) and
A29: a1 = (Den (o1,SCS)) . x1 by A24, FUNCT_1:def_3;
A30: dom (Den (o1,SCS)) = Args (o1,SCS) by FUNCT_2:def_1
.= (( the Sorts of SCS #) * the Arity of IIG) . o1 by MSUALG_1:def_4
.= ( the Sorts of SCS #) . ( the Arity of IIG . o1) by A12, FUNCT_1:13
.= {{}} by A22, A25, PRE_CIRC:2 ;
then  x1 = {} by A28, TARSKI:def_1;
hence  it1 . i = it2 . i by A20, A15, A27, A30, A29, A26, TARSKI:def_1; ::_thesis: verum
end;
hence  it1 = it2 by PBOOLE:3; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines Set-Constants CIRCUIT1:def_1_:_
 for IIG being non empty non void Circuit-like ManySortedSign
for SCS being non-empty Circuit of IIG
for b3 being ManySortedSet of SortsWithConstants IIG holds
( b3 = Set-Constants SCS iff for x being Vertex of IIG st x in dom b3 holds
b3 . x in Constants (SCS,x) );

theorem :: CIRCUIT1:1
for IIG being non empty non void Circuit-like ManySortedSign
for SCS being non-empty Circuit of IIG
for v being Vertex of IIG
for e being Element of the Sorts of SCS . v st v in SortsWithConstants IIG & e in Constants (SCS,v) holds
(Set-Constants SCS) . v = e
proof
let IIG be non empty non void Circuit-like ManySortedSign ; ::_thesis: for SCS being non-empty Circuit of IIG
for v being Vertex of IIG
for e being Element of the Sorts of SCS . v st v in SortsWithConstants IIG & e in Constants (SCS,v) holds
(Set-Constants SCS) . v = e
let SCS be non-empty Circuit of IIG; ::_thesis: for v being Vertex of IIG
for e being Element of the Sorts of SCS . v st v in SortsWithConstants IIG & e in Constants (SCS,v) holds
(Set-Constants SCS) . v = e
let v be Vertex of IIG; ::_thesis: for e being Element of the Sorts of SCS . v st v in SortsWithConstants IIG & e in Constants (SCS,v) holds
(Set-Constants SCS) . v = e
let e be Element of the Sorts of SCS . v; ::_thesis: ( v in SortsWithConstants IIG & e in Constants (SCS,v) implies (Set-Constants SCS) . v = e )
assume that
A1: v in SortsWithConstants IIG and
A2: e in Constants (SCS,v) ; ::_thesis: (Set-Constants SCS) . v = e
A3: 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  ex a being Element of the Sorts of SCS . v st
( a = e & 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 A2;
then consider o being OperSymbol of IIG such that
A4: the Arity of IIG . o = {} and
A5: the ResultSort of IIG . o = v and
A6: e in rng (Den (o,SCS)) ;
A7: {} = <*> the carrier of IIG ;
 v in dom (Set-Constants SCS) by A1, PARTFUN1:def_2;
then  (Set-Constants SCS) . v in Constants (SCS,v) by Def1;
then  ex a being Element of the Sorts of SCS . v st
( a = (Set-Constants SCS) . v & 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 A3;
then consider o1 being OperSymbol of IIG such that
 the Arity of IIG . o1 = {} and
A8: the ResultSort of IIG . o1 = v and
A9: (Set-Constants SCS) . v in rng (Den (o1,SCS)) ;
A10: ex d1 being set st
( d1 in dom (Den (o1,SCS)) & (Set-Constants SCS) . v = (Den (o1,SCS)) . d1 ) by A9, FUNCT_1:def_3;
 ( the_result_sort_of o = the ResultSort of IIG . o & the_result_sort_of o1 = the ResultSort of IIG . o1 ) by MSUALG_1:def_2;
then A11: o = o1 by A5, A8, MSAFREE2:def_6;
consider d being set  such that
A12: d in dom (Den (o,SCS)) and
A13: e = (Den (o,SCS)) . d by A6, FUNCT_1:def_3;
A14: dom the Arity of IIG = the carrier' of IIG by FUNCT_2:def_1;
A15: dom (Den (o,SCS)) = Args (o,SCS) by FUNCT_2:def_1
.= (( the Sorts of SCS #) * the Arity of IIG) . o by MSUALG_1:def_4
.= ( the Sorts of SCS #) . ( the Arity of IIG . o) by A14, FUNCT_1:13
.= {{}} by A4, A7, PRE_CIRC:2 ;
then  d = {} by A12, TARSKI:def_1;
hence  (Set-Constants SCS) . v = e by A11, A15, A13, A10, TARSKI:def_1; ::_thesis: verum
end;

definition
let IIG be non empty non void Circuit-like ManySortedSign ;
let CS be Circuit of IIG;
mode InputFuncs of CS is ManySortedFunction of (InputVertices IIG) --> NAT, the Sorts of CS | (InputVertices IIG);
end;

theorem Th2: :: CIRCUIT1:2
for IIG being non empty non void Circuit-like ManySortedSign
for SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS
for n being Element of NAT st IIG is with_input_V holds
(commute InpFs) . n is InputValues of SCS
proof
let IIG be non empty non void Circuit-like ManySortedSign ; ::_thesis: for SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS
for n being Element of NAT st IIG is with_input_V holds
(commute InpFs) . n is InputValues of SCS
let SCS be non-empty Circuit of IIG; ::_thesis: for InpFs being InputFuncs of SCS
for n being Element of NAT st IIG is with_input_V holds
(commute InpFs) . n is InputValues of SCS
let InpFs be InputFuncs of SCS; ::_thesis: for n being Element of NAT st IIG is with_input_V holds
(commute InpFs) . n is InputValues of SCS
let n be Element of NAT ; ::_thesis: ( IIG is with_input_V implies (commute InpFs) . n is InputValues of SCS )
reconsider A = InputVertices IIG as Subset of IIG ;
reconsider SS = the Sorts of SCS as V2() ManySortedSet of the carrier of IIG ;
assume  IIG is with_input_V ; ::_thesis: (commute InpFs) . n is InputValues of SCS
then reconsider A = A as non empty Subset of IIG ;
reconsider SI = SS | A as ManySortedSet of A ;
reconsider SI = SI as V2() ManySortedSet of A ;
consider ivm being ManySortedSet of A such that
A1: ivm = (commute InpFs) . n and
A2: ivm in SI by PRE_CIRC:7;
now__::_thesis:_for_v_being_Vertex_of_IIG_st_v_in_InputVertices_IIG_holds_
ivm_._v_in_the_Sorts_of_SCS_._v
let v be Vertex of IIG; ::_thesis: ( v in InputVertices IIG implies ivm . v in the Sorts of SCS . v )
assume A3: v in InputVertices IIG ; ::_thesis: ivm . v in the Sorts of SCS . v
then  SI . v = the Sorts of SCS . v by FUNCT_1:49;
hence  ivm . v in the Sorts of SCS . v by A2, A3, PBOOLE:def_1; ::_thesis: verum
end;
hence  (commute InpFs) . n is InputValues of SCS by A1, MSAFREE2:def_5; ::_thesis: verum
end;

definition
let IIG be non empty non void Circuit-like ManySortedSign ;
assume A1: IIG is with_input_V ;
let SCS be non-empty Circuit of IIG;
let InpFs be InputFuncs of SCS;
let n be Element of NAT ;
funcn -th_InputValues InpFs ->  InputValues of SCS equals :: CIRCUIT1:def 2
(commute InpFs) . n;
coherence
 (commute InpFs) . n is InputValues of SCS by A1, Th2;
correctness
;
end;

:: deftheorem  defines -th_InputValues CIRCUIT1:def_2_:_
 for IIG being non empty non void Circuit-like ManySortedSign st IIG is with_input_V holds
for SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS
for n being Element of NAT holds n -th_InputValues InpFs = (commute InpFs) . n;

definition
let IIG be non empty non void Circuit-like ManySortedSign ;
let SCS be Circuit of IIG;
mode State of SCS is Element of product the Sorts of SCS;
end;

theorem :: CIRCUIT1:3
for IIG being non empty non void Circuit-like ManySortedSign
for SCS being non-empty Circuit of IIG
for s being State of SCS holds dom s = the carrier of IIG by PARTFUN1:def_2;

theorem :: CIRCUIT1:4
for IIG being non empty non void Circuit-like ManySortedSign
for SCS being non-empty Circuit of IIG
for s being State of SCS
for v being Vertex of IIG holds s . v in the Sorts of SCS . v
proof
let IIG be non empty non void Circuit-like ManySortedSign ; ::_thesis: for SCS being non-empty Circuit of IIG
for s being State of SCS
for v being Vertex of IIG holds s . v in the Sorts of SCS . v
let SCS be non-empty Circuit of IIG; ::_thesis: for s being State of SCS
for v being Vertex of IIG holds s . v in the Sorts of SCS . v
let s be State of SCS; ::_thesis: for v being Vertex of IIG holds s . v in the Sorts of SCS . v
let v be Vertex of IIG; ::_thesis: s . v in the Sorts of SCS . v
 ( dom the Sorts of SCS = the carrier of IIG & ex g being Function st
( s = g & dom g = dom the Sorts of SCS & ( for x being set st x in dom the Sorts of SCS holds
g . x in the Sorts of SCS . x ) ) ) by CARD_3:def_5, PARTFUN1:def_2;
hence  s . v in the Sorts of SCS . v ; ::_thesis: verum
end;

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;
let o be OperSymbol of IIG;
funco depends_on_in s ->  Element of Args (o,SCS) equals :: CIRCUIT1:def 3
s * (the_arity_of o);
coherence
 s * (the_arity_of o) is Element of Args (o,SCS)
proof
 Args (o,SCS) = product ( the Sorts of SCS * (the_arity_of o)) by PRALG_2:3;
hence  s * (the_arity_of o) is Element of Args (o,SCS) by CARD_3:83; ::_thesis: verum
end;
correctness
;
end;

:: deftheorem  defines depends_on_in CIRCUIT1:def_3_:_
 for IIG being non empty non void Circuit-like ManySortedSign
for SCS being non-empty Circuit of IIG
for s being State of SCS
for o being OperSymbol of IIG holds o depends_on_in s = s * (the_arity_of o);

theorem Th5: :: CIRCUIT1:5
for IIG being non empty non void Circuit-like monotonic ManySortedSign
for SCS being non-empty finite-yielding MSAlgebra over IIG
for v, w being Vertex of IIG
for e1 being Element of the Sorts of (FreeEnv SCS) . v
for q1 being DTree-yielding FinSequence st v in InnerVertices IIG & e1 = [(action_at v), the carrier of IIG] -tree q1 holds
for k being Element of NAT st k in dom q1 & q1 . k in the Sorts of (FreeEnv SCS) . w holds
w = (the_arity_of (action_at v)) /. k
proof
let IIG be non empty non void Circuit-like monotonic ManySortedSign ; ::_thesis: for SCS being non-empty finite-yielding MSAlgebra over IIG
for v, w being Vertex of IIG
for e1 being Element of the Sorts of (FreeEnv SCS) . v
for q1 being DTree-yielding FinSequence st v in InnerVertices IIG & e1 = [(action_at v), the carrier of IIG] -tree q1 holds
for k being Element of NAT st k in dom q1 & q1 . k in the Sorts of (FreeEnv SCS) . w holds
w = (the_arity_of (action_at v)) /. k
let SCS be non-empty finite-yielding MSAlgebra over IIG; ::_thesis: for v, w being Vertex of IIG
for e1 being Element of the Sorts of (FreeEnv SCS) . v
for q1 being DTree-yielding FinSequence st v in InnerVertices IIG & e1 = [(action_at v), the carrier of IIG] -tree q1 holds
for k being Element of NAT st k in dom q1 & q1 . k in the Sorts of (FreeEnv SCS) . w holds
w = (the_arity_of (action_at v)) /. k
let v, w be Vertex of IIG; ::_thesis: for e1 being Element of the Sorts of (FreeEnv SCS) . v
for q1 being DTree-yielding FinSequence st v in InnerVertices IIG & e1 = [(action_at v), the carrier of IIG] -tree q1 holds
for k being Element of NAT st k in dom q1 & q1 . k in the Sorts of (FreeEnv SCS) . w holds
w = (the_arity_of (action_at v)) /. k
let e1 be Element of the Sorts of (FreeEnv SCS) . v; ::_thesis: for q1 being DTree-yielding FinSequence st v in InnerVertices IIG & e1 = [(action_at v), the carrier of IIG] -tree q1 holds
for k being Element of NAT st k in dom q1 & q1 . k in the Sorts of (FreeEnv SCS) . w holds
w = (the_arity_of (action_at v)) /. k
let q1 be DTree-yielding FinSequence; ::_thesis: ( v in InnerVertices IIG & e1 = [(action_at v), the carrier of IIG] -tree q1 implies for k being Element of NAT st k in dom q1 & q1 . k in the Sorts of (FreeEnv SCS) . w holds
w = (the_arity_of (action_at v)) /. k )
assume that
A1: v in InnerVertices IIG and
A2: e1 = [(action_at v), the carrier of IIG] -tree q1 ; ::_thesis: for k being Element of NAT st k in dom q1 & q1 . k in the Sorts of (FreeEnv SCS) . w holds
w = (the_arity_of (action_at v)) /. k
thus  for k being Element of NAT st k in dom q1 & q1 . k in the Sorts of (FreeEnv SCS) . w holds
w = (the_arity_of (action_at v)) /. k ::_thesis: verum
proof
reconsider av = action_at v as OperSymbol of IIG ;
let k be Element of NAT ; ::_thesis: ( k in dom q1 & q1 . k in the Sorts of (FreeEnv SCS) . w implies w = (the_arity_of (action_at v)) /. k )
assume that
A3: k in dom q1 and
A4: q1 . k in the Sorts of (FreeEnv SCS) . w ; ::_thesis: w = (the_arity_of (action_at v)) /. k
A5: FreeEnv SCS = MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #) by MSAFREE:def_14;
 e1 in the Sorts of (FreeEnv SCS) . v ;
then A6: e1 in the Sorts of (FreeEnv SCS) . (the_result_sort_of av) by A1, MSAFREE2:def_7;
then  len q1 = len (the_arity_of av) by A2, MSAFREE2:10;
then A7: k in dom (the_arity_of av) by A3, FINSEQ_3:29;
then  q1 . k in the Sorts of (FreeEnv SCS) . ((the_arity_of av) . k) by A2, A6, MSAFREE2:11;
then A8: q1 . k in (FreeSort the Sorts of SCS) . ((the_arity_of av) /. k) by A7, A5, PARTFUN1:def_6;
now__::_thesis:_not_(the_arity_of_av)_/._k_<>_w
assume  (the_arity_of av) /. k <> w ; ::_thesis: contradiction
then  (FreeSort the Sorts of SCS) . ((the_arity_of av) /. k) misses (FreeSort the Sorts of SCS) . w by MSAFREE:12;
then  ((FreeSort the Sorts of SCS) . ((the_arity_of av) /. k)) /\ ((FreeSort the Sorts of SCS) . w) = {} by XBOOLE_0:def_7;
hence  contradiction by A4, A5, A8, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  w = (the_arity_of (action_at v)) /. k ; ::_thesis: verum
end;
end;

registration
let IIG be non empty non void Circuit-like monotonic ManySortedSign ;
let SCS be non-empty finite-yielding MSAlgebra over IIG;
let v be Vertex of IIG;
cluster  ->  Relation-like Function-like non empty finite for Element of the Sorts of (FreeEnv SCS) . v;
coherence
 for b1 being Element of the Sorts of (FreeEnv SCS) . v holds
( b1 is finite & not b1 is empty & b1 is Function-like & b1 is Relation-like ) ;
end;

registration
let IIG be non empty non void Circuit-like monotonic ManySortedSign ;
let SCS be non-empty finite-yielding MSAlgebra over IIG;
let v be Vertex of IIG;
cluster  ->  DecoratedTree-like for Element of the Sorts of (FreeEnv SCS) . v;
coherence
 for b1 being Element of the Sorts of (FreeEnv SCS) . v holds b1 is DecoratedTree-like ;
end;

theorem Th6: :: CIRCUIT1:6
for IIG being non empty non void Circuit-like monotonic ManySortedSign
for SCS being non-empty finite-yielding MSAlgebra over IIG
for v, w being Vertex of IIG
for e1 being Element of the Sorts of (FreeEnv SCS) . v
for e2 being Element of the Sorts of (FreeEnv SCS) . w
for q1 being DTree-yielding FinSequence
for k1 being Element of NAT st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e1 = [(action_at v), the carrier of IIG] -tree q1 & k1 + 1 in dom q1 & q1 . (k1 + 1) in the Sorts of (FreeEnv SCS) . w holds
e1 with-replacement (<*k1*>,e2) in the Sorts of (FreeEnv SCS) . v
proof
set q99 = <*> NAT;
let IIG be non empty non void Circuit-like monotonic ManySortedSign ; ::_thesis: for SCS being non-empty finite-yielding MSAlgebra over IIG
for v, w being Vertex of IIG
for e1 being Element of the Sorts of (FreeEnv SCS) . v
for e2 being Element of the Sorts of (FreeEnv SCS) . w
for q1 being DTree-yielding FinSequence
for k1 being Element of NAT st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e1 = [(action_at v), the carrier of IIG] -tree q1 & k1 + 1 in dom q1 & q1 . (k1 + 1) in the Sorts of (FreeEnv SCS) . w holds
e1 with-replacement (<*k1*>,e2) in the Sorts of (FreeEnv SCS) . v
let SCS be non-empty finite-yielding MSAlgebra over IIG; ::_thesis: for v, w being Vertex of IIG
for e1 being Element of the Sorts of (FreeEnv SCS) . v
for e2 being Element of the Sorts of (FreeEnv SCS) . w
for q1 being DTree-yielding FinSequence
for k1 being Element of NAT st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e1 = [(action_at v), the carrier of IIG] -tree q1 & k1 + 1 in dom q1 & q1 . (k1 + 1) in the Sorts of (FreeEnv SCS) . w holds
e1 with-replacement (<*k1*>,e2) in the Sorts of (FreeEnv SCS) . v
let v, w be Vertex of IIG; ::_thesis: for e1 being Element of the Sorts of (FreeEnv SCS) . v
for e2 being Element of the Sorts of (FreeEnv SCS) . w
for q1 being DTree-yielding FinSequence
for k1 being Element of NAT st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e1 = [(action_at v), the carrier of IIG] -tree q1 & k1 + 1 in dom q1 & q1 . (k1 + 1) in the Sorts of (FreeEnv SCS) . w holds
e1 with-replacement (<*k1*>,e2) in the Sorts of (FreeEnv SCS) . v
let e1 be Element of the Sorts of (FreeEnv SCS) . v; ::_thesis: for e2 being Element of the Sorts of (FreeEnv SCS) . w
for q1 being DTree-yielding FinSequence
for k1 being Element of NAT st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e1 = [(action_at v), the carrier of IIG] -tree q1 & k1 + 1 in dom q1 & q1 . (k1 + 1) in the Sorts of (FreeEnv SCS) . w holds
e1 with-replacement (<*k1*>,e2) in the Sorts of (FreeEnv SCS) . v
let e2 be Element of the Sorts of (FreeEnv SCS) . w; ::_thesis: for q1 being DTree-yielding FinSequence
for k1 being Element of NAT st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e1 = [(action_at v), the carrier of IIG] -tree q1 & k1 + 1 in dom q1 & q1 . (k1 + 1) in the Sorts of (FreeEnv SCS) . w holds
e1 with-replacement (<*k1*>,e2) in the Sorts of (FreeEnv SCS) . v
let q1 be DTree-yielding FinSequence; ::_thesis: for k1 being Element of NAT st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e1 = [(action_at v), the carrier of IIG] -tree q1 & k1 + 1 in dom q1 & q1 . (k1 + 1) in the Sorts of (FreeEnv SCS) . w holds
e1 with-replacement (<*k1*>,e2) in the Sorts of (FreeEnv SCS) . v
let k1 be Element of NAT ; ::_thesis: ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e1 = [(action_at v), the carrier of IIG] -tree q1 & k1 + 1 in dom q1 & q1 . (k1 + 1) in the Sorts of (FreeEnv SCS) . w implies e1 with-replacement (<*k1*>,e2) in the Sorts of (FreeEnv SCS) . v )
set k = k1 + 1;
set eke = e1 with-replacement (<*k1*>,e2);
assume that
A1: v in (InnerVertices IIG) \ (SortsWithConstants IIG) and
A2: e1 = [(action_at v), the carrier of IIG] -tree q1 and
A3: k1 + 1 in dom q1 and
A4: q1 . (k1 + 1) in the Sorts of (FreeEnv SCS) . w ; ::_thesis: e1 with-replacement (<*k1*>,e2) in the Sorts of (FreeEnv SCS) . v
reconsider O = [: the carrier' of IIG,{ the carrier of IIG}:] \/ (Union (coprod the Sorts of SCS)) as non empty set ;
reconsider R = REL the Sorts of SCS as Relation of O,(O *) ;
A5: DTConMSA the Sorts of SCS = DTConstrStr(# O,R #) by MSAFREE:def_8;
then reconsider TSDT = TS (DTConMSA the Sorts of SCS) as Subset of (FinTrees O) ;
 for x being set st x in TSDT holds
x is DecoratedTree of O ;
then reconsider TSDT = TSDT as DTree-set of O by TREES_3:def_6;
reconsider av = action_at v as OperSymbol of IIG ;
reconsider e19 = e1 as DecoratedTree ;
 ex p9 being DTree-yielding FinSequence st
( p9 = q1 & dom e19 = tree (doms p9) ) by A2, TREES_4:def_4;
then reconsider m = <*k1*> as Element of dom e1 by A3, PRE_CIRC:13;
reconsider m9 = m as FinSequence of NAT ;
consider qq being DTree-yielding FinSequence such that
A6: e1 with-replacement (m9,e2) = [av, the carrier of IIG] -tree qq and
A7: len qq = len q1 and
A8: qq . (k1 + 1) = e2 and
A9: for i being Element of NAT st i in dom q1 & i <> k1 + 1 holds
qq . i = q1 . i by A2, PRE_CIRC:15;
 ( NonTerminals (DTConMSA the Sorts of SCS) = [: the carrier' of IIG,{ the carrier of IIG}:] & the carrier of IIG in { the carrier of IIG} ) by MSAFREE:6, TARSKI:def_1;
then reconsider nt = [av, the carrier of IIG] as NonTerminal of (DTConMSA the Sorts of SCS) by ZFMISC_1:87;
A10: FreeEnv SCS = MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #) by MSAFREE:def_14;
then A11: the Sorts of (FreeEnv SCS) . v = FreeSort ( the Sorts of SCS,v) by MSAFREE:def_11;
then A12: e1 in TS (DTConMSA the Sorts of SCS) by TARSKI:def_3;
 e1 . {} = nt by A2, TREES_4:def_4;
then  ex p9 being FinSequence of TS (DTConMSA the Sorts of SCS) st
( e1 = nt -tree p9 & nt ==> roots p9 ) by A12, DTCONSTR:10;
then reconsider q19 = q1 as FinSequence of TS (DTConMSA the Sorts of SCS) by A2, TREES_4:15;
 the Sorts of (FreeEnv SCS) . w = FreeSort ( the Sorts of SCS,w) by A10, MSAFREE:def_11;
then A13: e2 in FreeSort ( the Sorts of SCS,w) ;
then  e2 in  {  a9 where a9 is Element of TS (DTConMSA the Sorts of SCS) : ( ex x being set st
( x in the Sorts of SCS . w & a9 = root-tree [x,w] ) or ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a9 . {} & the_result_sort_of o = w ) )  }  by MSAFREE:def_10;
then consider aa being Element of TS (DTConMSA the Sorts of SCS) such that
A14: aa = e2 and
A15: ( ex x being set st
( x in the Sorts of SCS . w & aa = root-tree [x,w] ) or ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = aa . {} & the_result_sort_of o = w ) ) ;
A16: dom qq = dom q1 by A7, FINSEQ_3:29;
 rng qq c= TS (DTConMSA the Sorts of SCS)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng qq or y in TS (DTConMSA the Sorts of SCS) )
assume  y in rng qq ; ::_thesis: y in TS (DTConMSA the Sorts of SCS)
then consider x being set  such that
A17: x in dom qq and
A18: y = qq . x by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A17;
percases ( x = k1 + 1 or x <> k1 + 1 ) ;
suppose x = k1 + 1 ; ::_thesis: y in TS (DTConMSA the Sorts of SCS)
hence  y in TS (DTConMSA the Sorts of SCS) by A8, A14, A18; ::_thesis: verum
end;
suppose x <> k1 + 1 ; ::_thesis: y in TS (DTConMSA the Sorts of SCS)
then  qq . x = q19 . x by A9, A16, A17;
hence  y in TS (DTConMSA the Sorts of SCS) by A16, A17, A18, FINSEQ_2:11; ::_thesis: verum
end;
end;
end;
then reconsider q9 = qq as FinSequence of TSDT by FINSEQ_1:def_4;
reconsider rq = roots q9 as FinSequence of O ;
reconsider rq = rq as Element of O * by FINSEQ_1:def_11;
A19: dom rq = dom qq by TREES_3:def_18;
A20: v in InnerVertices IIG by A1, XBOOLE_0:def_5;
then A21: the Sorts of (FreeEnv SCS) . (the_result_sort_of av) = the Sorts of (FreeEnv SCS) . v by MSAFREE2:def_7;
then A22: len q1 = len (the_arity_of av) by A2, MSAFREE2:10;
then A23: dom rq = dom (the_arity_of av) by A7, A19, FINSEQ_3:29;
A24: for x being set st x in dom rq holds
( ( rq . x in [: the carrier' of IIG,{ the carrier of IIG}:] implies for o1 being OperSymbol of IIG st [o1, the carrier of IIG] = rq . x holds
the_result_sort_of o1 = (the_arity_of av) . x ) & ( rq . x in Union (coprod the Sorts of SCS) implies rq . x in coprod (((the_arity_of av) . x), the Sorts of SCS) ) )
proof
 the carrier of IIG in { the carrier of IIG} by TARSKI:def_1;
then  [av, the carrier of IIG] in [: the carrier' of IIG,{ the carrier of IIG}:] by ZFMISC_1:87;
then reconsider av9 = [av, the carrier of IIG] as Symbol of (DTConMSA the Sorts of SCS) by A5, XBOOLE_0:def_3;
reconsider q19 = q19 as FinSequence of TSDT ;
let x be set ; ::_thesis: ( x in dom rq implies ( ( rq . x in [: the carrier' of IIG,{ the carrier of IIG}:] implies for o1 being OperSymbol of IIG st [o1, the carrier of IIG] = rq . x holds
the_result_sort_of o1 = (the_arity_of av) . x ) & ( rq . x in Union (coprod the Sorts of SCS) implies rq . x in coprod (((the_arity_of av) . x), the Sorts of SCS) ) ) )
reconsider b = roots q19 as Element of ([: the carrier' of IIG,{ the carrier of IIG}:] \/ (Union (coprod the Sorts of SCS))) * by FINSEQ_1:def_11;
reconsider b = b as FinSequence ;
assume A25: x in dom rq ; ::_thesis: ( ( rq . x in [: the carrier' of IIG,{ the carrier of IIG}:] implies for o1 being OperSymbol of IIG st [o1, the carrier of IIG] = rq . x holds
the_result_sort_of o1 = (the_arity_of av) . x ) & ( rq . x in Union (coprod the Sorts of SCS) implies rq . x in coprod (((the_arity_of av) . x), the Sorts of SCS) ) )
then reconsider x9 = x as Element of NAT ;
A26: (the_arity_of av) /. x9 = (the_arity_of av) . x9 by A23, A25, PARTFUN1:def_6;
A27: dom q1 = dom (the_arity_of av) by A22, FINSEQ_3:29;
 for n being Nat st n in dom q1 holds
q1 . n in FreeSort ( the Sorts of SCS,((the_arity_of av) /. n))
proof
let n be Nat; ::_thesis: ( n in dom q1 implies q1 . n in FreeSort ( the Sorts of SCS,((the_arity_of av) /. n)) )
assume  n in dom q1 ; ::_thesis: q1 . n in FreeSort ( the Sorts of SCS,((the_arity_of av) /. n))
then  ( q1 . n in the Sorts of (FreeEnv SCS) . ((the_arity_of av) . n) & (the_arity_of av) . n = (the_arity_of av) /. n ) by A2, A21, A27, MSAFREE2:11, PARTFUN1:def_6;
hence  q1 . n in FreeSort ( the Sorts of SCS,((the_arity_of av) /. n)) by A10, MSAFREE:def_11; ::_thesis: verum
end;
then A28: q19 in (((FreeSort the Sorts of SCS) #) * the Arity of IIG) . av by A27, MSAFREE:9;
 Sym (av, the Sorts of SCS) = [av, the carrier of IIG] by MSAFREE:def_9;
then  av9 ==> b by A28, MSAFREE:10;
then A29: ( dom (roots q1) = dom q1 & [av9,b] in R ) by A5, LANG1:def_1, TREES_3:def_18;
A30: (the_arity_of av) /. (k1 + 1) = w by A2, A3, A4, A20, Th5;
A31: ex T being DecoratedTree st
( T = qq . x9 & rq . x9 = T . {} ) by A19, A25, TREES_3:def_18;
A32: ex T9 being DecoratedTree st
( T9 = q1 . x9 & (roots q1) . x9 = T9 . {} ) by A16, A19, A25, TREES_3:def_18;
thus  ( rq . x in [: the carrier' of IIG,{ the carrier of IIG}:] implies for o1 being OperSymbol of IIG st [o1, the carrier of IIG] = rq . x holds
the_result_sort_of o1 = (the_arity_of av) . x ) ::_thesis: ( rq . x in Union (coprod the Sorts of SCS) implies rq . x in coprod (((the_arity_of av) . x), the Sorts of SCS) )
proof
assume A33: rq . x in [: the carrier' of IIG,{ the carrier of IIG}:] ; ::_thesis: for o1 being OperSymbol of IIG st [o1, the carrier of IIG] = rq . x holds
the_result_sort_of o1 = (the_arity_of av) . x
let o1 be OperSymbol of IIG; ::_thesis: ( [o1, the carrier of IIG] = rq . x implies the_result_sort_of o1 = (the_arity_of av) . x )
assume A34: [o1, the carrier of IIG] = rq . x ; ::_thesis: the_result_sort_of o1 = (the_arity_of av) . x
percases ( x9 = k1 + 1 or x9 <> k1 + 1 ) ;
supposeA35: x9 = k1 + 1 ; ::_thesis: the_result_sort_of o1 = (the_arity_of av) . x
now__::_thesis:_(_(_ex_xx_being_set_st_
(_xx_in_the_Sorts_of_SCS_._w_&_aa_=_root-tree_[xx,w]_)_&_contradiction_)_or_(_ex_o_being_OperSymbol_of_IIG_st_
(_[o,_the_carrier_of_IIG]_=_aa_._{}_&_the_result_sort_of_o_=_w_)_&_the_result_sort_of_o1_=_(the_arity_of_av)_._x_)_)
percases ( ex xx being set st
( xx in the Sorts of SCS . w & aa = root-tree [xx,w] ) or ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = aa . {} & the_result_sort_of o = w ) ) by A15;
case ex xx being set st
( xx in the Sorts of SCS . w & aa = root-tree [xx,w] ) ; ::_thesis: contradiction
then consider xx being set  such that
 xx in the Sorts of SCS . w and
A36: aa = root-tree [xx,w] ;
 [o1, the carrier of IIG] = [xx,w] by A8, A14, A31, A34, A35, A36, TREES_4:3;
then A37: the carrier of IIG = w by XTUPLE_0:1;
 for X being set holds not X in X ;
hence  contradiction by A37; ::_thesis: verum
end;
case ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = aa . {} & the_result_sort_of o = w ) ; ::_thesis: the_result_sort_of o1 = (the_arity_of av) . x
hence  the_result_sort_of o1 = (the_arity_of av) . x by A8, A14, A26, A31, A30, A34, A35, XTUPLE_0:1; ::_thesis: verum
end;
end;
end;
hence  the_result_sort_of o1 = (the_arity_of av) . x ; ::_thesis: verum
end;
suppose x9 <> k1 + 1 ; ::_thesis: the_result_sort_of o1 = (the_arity_of av) . x
then  (roots q1) . x9 = [o1, the carrier of IIG] by A9, A16, A19, A25, A31, A32, A34;
hence  the_result_sort_of o1 = (the_arity_of av) . x by A16, A19, A25, A29, A33, A34, MSAFREE1:3; ::_thesis: verum
end;
end;
end;
thus  ( rq . x in Union (coprod the Sorts of SCS) implies rq . x in coprod (((the_arity_of av) . x), the Sorts of SCS) ) ::_thesis: verum
proof
assume A38: rq . x in Union (coprod the Sorts of SCS) ; ::_thesis: rq . x in coprod (((the_arity_of av) . x), the Sorts of SCS)
then  rq . x in Terminals (DTConMSA the Sorts of SCS) by MSAFREE:6;
then consider s1 being SortSymbol of IIG, x99 being set  such that
A39: ( x99 in the Sorts of SCS . s1 & rq . x = [x99,s1] ) by MSAFREE:7;
percases ( x9 = k1 + 1 or x9 <> k1 + 1 ) ;
supposeA40: x9 = k1 + 1 ; ::_thesis: rq . x in coprod (((the_arity_of av) . x), the Sorts of SCS)
reconsider rqx = rq . x9 as Terminal of (DTConMSA the Sorts of SCS) by A38, MSAFREE:6;
 aa = root-tree rqx by A8, A14, A31, A40, DTCONSTR:9;
then  aa in  {  a99 where a99 is Element of TS (DTConMSA the Sorts of SCS) : ( ex x999 being set st
( x999 in the Sorts of SCS . s1 & a99 = root-tree [x999,s1] ) or ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a99 . {} & the_result_sort_of o = s1 ) )  }  by A39;
then A41: aa in FreeSort ( the Sorts of SCS,s1) by MSAFREE:def_10;
A42: e2 in (FreeSort the Sorts of SCS) . w by A13, MSAFREE:def_11;
now__::_thesis:_not_w_<>_s1
assume  w <> s1 ; ::_thesis: contradiction
then  (FreeSort the Sorts of SCS) . w misses (FreeSort the Sorts of SCS) . s1 by MSAFREE:12;
then A43: ((FreeSort the Sorts of SCS) . w) /\ ((FreeSort the Sorts of SCS) . s1) = {} by XBOOLE_0:def_7;
 e2 in (FreeSort the Sorts of SCS) . s1 by A14, A41, MSAFREE:def_11;
hence  contradiction by A42, A43, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  rq . x in coprod (((the_arity_of av) . x), the Sorts of SCS) by A26, A30, A39, A40, MSAFREE:def_2; ::_thesis: verum
end;
suppose x9 <> k1 + 1 ; ::_thesis: rq . x in coprod (((the_arity_of av) . x), the Sorts of SCS)
then  rq . x9 = (roots q1) . x9 by A9, A16, A19, A25, A31, A32;
hence  rq . x in coprod (((the_arity_of av) . x), the Sorts of SCS) by A16, A19, A25, A29, A38, MSAFREE1:3; ::_thesis: verum
end;
end;
end;
end;
 len rq = len qq by A19, FINSEQ_3:29;
then  [nt,(roots qq)] in REL the Sorts of SCS by A7, A22, A24, MSAFREE:5;
then  nt ==> roots qq by A5, LANG1:def_1;
then reconsider q9 = q9 as SubtreeSeq of nt by DTCONSTR:def_6;
 e1 with-replacement (<*k1*>,e2) = nt -tree q9 by A6;
then reconsider eke9 = e1 with-replacement (<*k1*>,e2) as Element of TS (DTConMSA the Sorts of SCS) ;
 <*> NAT in (dom e1) with-replacement (m9,(dom e2)) by TREES_1:22;
then  ( ( not m9 is_a_prefix_of <*> NAT & (e1 with-replacement (<*k1*>,e2)) . (<*> NAT) = e1 . (<*> NAT) ) or ex r being FinSequence of NAT st
( r in dom e2 & <*> NAT = m9 ^ r & (e1 with-replacement (<*k1*>,e2)) . (<*> NAT) = e2 . r ) ) by TREES_2:def_11;
then A44: (e1 with-replacement (<*k1*>,e2)) . {} = [av, the carrier of IIG] by A2, TREES_4:def_4;
now__::_thesis:_ex_av,_o_being_OperSymbol_of_IIG_st_
(_[o,_the_carrier_of_IIG]_=_(e1_with-replacement_(<*k1*>,e2))_._{}_&_the_result_sort_of_o_=_v_)
take av = av; ::_thesis: ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = (e1 with-replacement (<*k1*>,e2)) . {} & the_result_sort_of o = v )
 the_result_sort_of av = v by A20, MSAFREE2:def_7;
hence  ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = (e1 with-replacement (<*k1*>,e2)) . {} & the_result_sort_of o = v ) by A44; ::_thesis: verum
end;
then  eke9 in  {  a99 where a99 is Element of TS (DTConMSA the Sorts of SCS) : ( ex x being set st
( x in the Sorts of SCS . v & a99 = root-tree [x,v] ) or ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a99 . {} & the_result_sort_of o = v ) )  }  ;
then reconsider eke9 = eke9 as Element of the Sorts of (FreeEnv SCS) . v by A11, MSAFREE:def_10;
 eke9 in the Sorts of (FreeEnv SCS) . v ;
hence  e1 with-replacement (<*k1*>,e2) in the Sorts of (FreeEnv SCS) . v ; ::_thesis: verum
end;

theorem Th7: :: CIRCUIT1:7
for IIG being non empty non void Circuit-like monotonic ManySortedSign
for A being non-empty finite-yielding MSAlgebra over IIG
for v being Element of IIG
for e being Element of the Sorts of (FreeEnv A) . v st 1 < card e holds
ex o being OperSymbol of IIG st e . {} = [o, the carrier of IIG]
proof
let IIG be non empty non void Circuit-like monotonic ManySortedSign ; ::_thesis: for A being non-empty finite-yielding MSAlgebra over IIG
for v being Element of IIG
for e being Element of the Sorts of (FreeEnv A) . v st 1 < card e holds
ex o being OperSymbol of IIG st e . {} = [o, the carrier of IIG]
let A be non-empty finite-yielding MSAlgebra over IIG; ::_thesis: for v being Element of IIG
for e being Element of the Sorts of (FreeEnv A) . v st 1 < card e holds
ex o being OperSymbol of IIG st e . {} = [o, the carrier of IIG]
let v be Element of IIG; ::_thesis: for e being Element of the Sorts of (FreeEnv A) . v st 1 < card e holds
ex o being OperSymbol of IIG st e . {} = [o, the carrier of IIG]
let e be Element of the Sorts of (FreeEnv A) . v; ::_thesis: ( 1 < card e implies ex o being OperSymbol of IIG st e . {} = [o, the carrier of IIG] )
set X = the Sorts of A;
assume A1: 1 < card e ; ::_thesis: ex o being OperSymbol of IIG st e . {} = [o, the carrier of IIG]
A2: ( (FreeSort the Sorts of A) . v = FreeSort ( the Sorts of A,v) & FreeSort ( the Sorts of A,v) =  {  a where a is Element of TS (DTConMSA the Sorts of A) : ( ex x being set st
( x in the Sorts of A . v & a = root-tree [x,v] ) or ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a . {} & the_result_sort_of o = v ) )  }  ) by MSAFREE:def_10, MSAFREE:def_11;
 ( e in the Sorts of (FreeMSA the Sorts of A) . v & FreeMSA the Sorts of A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #) ) by MSAFREE:def_14;
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 A2;
hence  ex o being OperSymbol of IIG st e . {} = [o, the carrier of IIG] by A1, PRE_CIRC:19; ::_thesis: verum
end;

theorem :: CIRCUIT1:8
for IIG being non empty non void Circuit-like ManySortedSign
for SCS being non-empty Circuit of IIG
for s being State of SCS
for o being OperSymbol of IIG holds (Den (o,SCS)) . (o depends_on_in s) in the Sorts of SCS . (the_result_sort_of o)
proof
let IIG be non empty non void Circuit-like ManySortedSign ; ::_thesis: for SCS being non-empty Circuit of IIG
for s being State of SCS
for o being OperSymbol of IIG holds (Den (o,SCS)) . (o depends_on_in s) in the Sorts of SCS . (the_result_sort_of o)
let SCS be non-empty Circuit of IIG; ::_thesis: for s being State of SCS
for o being OperSymbol of IIG holds (Den (o,SCS)) . (o depends_on_in s) in the Sorts of SCS . (the_result_sort_of o)
let s be State of SCS; ::_thesis: for o being OperSymbol of IIG holds (Den (o,SCS)) . (o depends_on_in s) in the Sorts of SCS . (the_result_sort_of o)
let o be OperSymbol of IIG; ::_thesis: (Den (o,SCS)) . (o depends_on_in s) in the Sorts of SCS . (the_result_sort_of o)
A1: dom the ResultSort of IIG = the carrier' of IIG by FUNCT_2:def_1;
Result (o,SCS) = ( the Sorts of SCS * the ResultSort of IIG) . o by MSUALG_1:def_5
.= the Sorts of SCS . ( the ResultSort of IIG . o) by A1, FUNCT_1:13
.= the Sorts of SCS . (the_result_sort_of o) by MSUALG_1:def_2 ;
hence  (Den (o,SCS)) . (o depends_on_in s) in the Sorts of SCS . (the_result_sort_of o) by FUNCT_2:5; ::_thesis: verum
end;

theorem Th9: :: CIRCUIT1:9
for IIG being non empty non void Circuit-like monotonic ManySortedSign
for A being non-empty Circuit of IIG
for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v st e . {} = [(action_at v), the carrier of IIG] holds
ex p being DTree-yielding FinSequence st e = [(action_at v), the carrier of IIG] -tree p
proof
let IIG be non empty non void Circuit-like monotonic ManySortedSign ; ::_thesis: for A being non-empty Circuit of IIG
for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v st e . {} = [(action_at v), the carrier of IIG] holds
ex p being DTree-yielding FinSequence st e = [(action_at v), the carrier of IIG] -tree p
let A be non-empty Circuit of IIG; ::_thesis: for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v st e . {} = [(action_at v), the carrier of IIG] holds
ex p being DTree-yielding FinSequence st e = [(action_at v), the carrier of IIG] -tree p
let v be Vertex of IIG; ::_thesis: for e being Element of the Sorts of (FreeEnv A) . v st e . {} = [(action_at v), the carrier of IIG] holds
ex p being DTree-yielding FinSequence st e = [(action_at v), the carrier of IIG] -tree p
let e be Element of the Sorts of (FreeEnv A) . v; ::_thesis: ( e . {} = [(action_at v), the carrier of IIG] implies ex p being DTree-yielding FinSequence st e = [(action_at v), the carrier of IIG] -tree p )
assume A1: e . {} = [(action_at v), the carrier of IIG] ; ::_thesis: ex p being DTree-yielding FinSequence st e = [(action_at v), the carrier of IIG] -tree p
set X = the Sorts of A;
 ( NonTerminals (DTConMSA the Sorts of A) = [: the carrier' of IIG,{ the carrier of IIG}:] & the carrier of IIG in { the carrier of IIG} ) by MSAFREE:6, TARSKI:def_1;
then reconsider nt = [(action_at v), the carrier of IIG] as NonTerminal of (DTConMSA the Sorts of A) by ZFMISC_1:87;
 ( FreeMSA the Sorts of A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #) & e in the Sorts of (FreeEnv A) . v ) by MSAFREE:def_14;
then  e in FreeSort ( the Sorts of A,v) by MSAFREE:def_11;
then reconsider tsg = e as Element of TS (DTConMSA the Sorts of A) ;
consider ts being FinSequence of TS (DTConMSA the Sorts of A) such that
A2: tsg = nt -tree ts and
 nt ==> roots ts by A1, DTCONSTR:10;
take  ts ; ::_thesis: e = [(action_at v), the carrier of IIG] -tree ts
thus  e = [(action_at v), the carrier of IIG] -tree ts by A2; ::_thesis: verum
end;

begin

registration
let IIG be non empty non void monotonic ManySortedSign ;
let A be non-empty finite-yielding MSAlgebra over IIG;
let v be SortSymbol of IIG;
cluster the Sorts of (FreeEnv A) . v ->  finite ;
coherence
 the Sorts of (FreeEnv A) . v is finite
proof
 the Sorts of A is V31() by MSAFREE2:def_11;
then  FreeEnv A is finitely-generated by MSAFREE2:8;
then  FreeEnv A is finite-yielding by MSAFREE2:def_13;
then  the Sorts of (FreeEnv A) is V31() by MSAFREE2:def_11;
hence  the Sorts of (FreeEnv A) . v is finite ; ::_thesis: verum
end;
end;

defpred S1[ set ] means verum;

definition
let IIG be non empty non void Circuit-like monotonic ManySortedSign ;
let A be non-empty finite-yielding MSAlgebra over IIG;
let v be SortSymbol of IIG;
func size (v,A) ->  Nat means :Def4: :: CIRCUIT1:def 4
 ex s being non empty finite Subset of NAT st
( s =  {  (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum  }  & it = max s );
existence
 ex b1 being Nat ex s being non empty finite Subset of NAT st
( s =  {  (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum  }  & b1 = max s )
proof
deffunc H1( Element of the Sorts of (FreeEnv A) . v) ->  Element of omega = card $1;
set s =  {  H1(t) where t is Element of the Sorts of (FreeEnv A) . v : S1[t]  }  ;
set t = the Element of the Sorts of (FreeEnv A) . v;
A1: card the Element of the Sorts of (FreeEnv A) . v in  {  H1(t) where t is Element of the Sorts of (FreeEnv A) . v : S1[t]  }  ;
A2:  {  H1(t) where t is Element of the Sorts of (FreeEnv A) . v : S1[t]  }  is Subset of NAT from DOMAIN_1:sch_8();
  {  H1(t) where t is Element of the Sorts of (FreeEnv A) . v : S1[t]  }  is finite from PRE_CIRC:sch_1();
then reconsider s =  {  H1(t) where t is Element of the Sorts of (FreeEnv A) . v : S1[t]  }  as non empty finite Subset of NAT by A1, A2;
take  max s ; ::_thesis: ex s being non empty finite Subset of NAT st
( s =  {  (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum  }  & max s = max s )
take  s ; ::_thesis: ( s =  {  (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum  }  & max s = max s )
thus  ( s =  {  (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum  }  & max s = max s ) ; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being Nat st ex s being non empty finite Subset of NAT st
( s =  {  (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum  }  & b1 = max s ) & ex s being non empty finite Subset of NAT st
( s =  {  (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum  }  & b2 = max s ) holds
b1 = b2;
;
end;

:: deftheorem Def4 defines size CIRCUIT1:def_4_:_
 for IIG being non empty non void Circuit-like monotonic ManySortedSign
for A being non-empty finite-yielding MSAlgebra over IIG
for v being SortSymbol of IIG
for b4 being Nat holds
( b4 = size (v,A) iff ex s being non empty finite Subset of NAT st
( s =  {  (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum  }  & b4 = max s ) );

theorem Th10: :: CIRCUIT1:10
for IIG being non empty non void Circuit-like monotonic ManySortedSign
for A being non-empty finite-yielding MSAlgebra over IIG
for v being Element of IIG holds
( size (v,A) = 1 iff v in (InputVertices IIG) \/ (SortsWithConstants IIG) )
proof
let IIG be non empty non void Circuit-like monotonic ManySortedSign ; ::_thesis: for A being non-empty finite-yielding MSAlgebra over IIG
for v being Element of IIG holds
( size (v,A) = 1 iff v in (InputVertices IIG) \/ (SortsWithConstants IIG) )
let A be non-empty finite-yielding MSAlgebra over IIG; ::_thesis: for v being Element of IIG holds
( size (v,A) = 1 iff v in (InputVertices IIG) \/ (SortsWithConstants IIG) )
let v be Element of IIG; ::_thesis: ( size (v,A) = 1 iff v in (InputVertices IIG) \/ (SortsWithConstants IIG) )
consider s being non empty finite Subset of NAT such that
A1: s =  {  (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum  }  and
A2: size (v,A) = max s by Def4;
reconsider Y = s as non empty finite real-membered set ;
 max Y in  {  (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum  }  by A1, XXREAL_2:def_8;
then consider e being Element of the Sorts of (FreeEnv A) . v such that
A3: card e = max Y ;
A4: FreeEnv A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #) by MSAFREE:def_14;
then  ( e in the Sorts of (FreeEnv A) . v & the Sorts of (FreeEnv A) . v = FreeSort ( the Sorts of A,v) ) by MSAFREE:def_11;
then A5: 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;
thus  ( size (v,A) = 1 implies v in (InputVertices IIG) \/ (SortsWithConstants IIG) ) ::_thesis: ( v in (InputVertices IIG) \/ (SortsWithConstants IIG) implies size (v,A) = 1 )
proof
assume A6: size (v,A) = 1 ; ::_thesis: v in (InputVertices IIG) \/ (SortsWithConstants IIG)
now__::_thesis:_v_in_(InputVertices_IIG)_\/_(SortsWithConstants_IIG)
assume A7: not v in (InputVertices IIG) \/ (SortsWithConstants IIG) ; ::_thesis: contradiction
then  not v in SortsWithConstants IIG by XBOOLE_0:def_3;
then  not v in  {  v9 where v9 is SortSymbol of IIG : v9 is with_const_op  }  by MSAFREE2:def_1;
then A8: not v is with_const_op ;
A9: the carrier of IIG = (InputVertices IIG) \/ (InnerVertices IIG) by XBOOLE_1:45;
 not v in InputVertices IIG by A7, XBOOLE_0:def_3;
then  v in InnerVertices IIG by A9, XBOOLE_0:def_3;
then consider x being set  such that
A10: x in dom the ResultSort of IIG and
A11: v = the ResultSort of IIG . x by FUNCT_1:def_3;
reconsider o = x as OperSymbol of IIG by A10;
percases ( not the Arity of IIG . o = {} or not the ResultSort of IIG . o = v ) by A8, MSUALG_2:def_1;
suppose not the Arity of IIG . o = {} ; ::_thesis: contradiction
then A12: the_arity_of o <> {} by MSUALG_1:def_1;
reconsider O = [: the carrier' of IIG,{ the carrier of IIG}:] \/ (Union (coprod the Sorts of A)) as non empty set ;
reconsider R = REL the Sorts of A as Relation of O,(O *) ;
 the carrier of IIG in { the carrier of IIG} by TARSKI:def_1;
then A13: [o, the carrier of IIG] in [: the carrier' of IIG,{ the carrier of IIG}:] by ZFMISC_1:87;
 DTConMSA the Sorts of A = DTConstrStr(# O,R #) by MSAFREE:def_8;
then reconsider o9 = [o, the carrier of IIG] as Symbol of (DTConMSA the Sorts of A) by A13, XBOOLE_0:def_3;
 o9 in NonTerminals (DTConMSA the Sorts of A) by A13, MSAFREE:6;
then consider p being FinSequence of TS (DTConMSA the Sorts of A) such that
A14: o9 ==> roots p by DTCONSTR:def_5;
reconsider op = o9 -tree p as Element of TS (DTConMSA the Sorts of A) by A14, DTCONSTR:def_1;
reconsider e1 = op as finite DecoratedTree ;
reconsider co = card e1 as real number ;
A15: op . {} = o9 by TREES_4:def_4;
now__::_thesis:_ex_o,_o_being_OperSymbol_of_IIG_st_
(_[o,_the_carrier_of_IIG]_=_op_._{}_&_the_result_sort_of_o_=_v_)
take o = o; ::_thesis: ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = op . {} & the_result_sort_of o = v )
 the_result_sort_of o = v by A11, MSUALG_1:def_2;
hence  ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = op . {} & the_result_sort_of o = v ) by A15; ::_thesis: verum
end;
then  op in  {  a9 where a9 is Element of TS (DTConMSA the Sorts of A) : ( ex x9 being set st
( x9 in the Sorts of A . v & a9 = root-tree [x9,v] ) or ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a9 . {} & the_result_sort_of o = v ) )  }  ;
then A16: op in FreeSort ( the Sorts of A,v) by MSAFREE:def_10;
A17: the Sorts of (FreeEnv A) . (the_result_sort_of o) = (FreeSort the Sorts of A) . v by A4, A11, MSUALG_1:def_2
.= FreeSort ( the Sorts of A,v) by MSAFREE:def_11 ;
then reconsider e1 = e1 as Element of the Sorts of (FreeEnv A) . v by A11, A16, MSUALG_1:def_2;
 len p = len (the_arity_of o) by A16, A17, MSAFREE2:10;
then  p <> {} by A12;
then  rng p <> {} ;
then A18: 1 in dom p by FINSEQ_3:32;
 ( ex q being DTree-yielding FinSequence st
( p = q & dom op = tree (doms q) ) & 0 + 1 = 1 ) by TREES_4:def_4;
then A19: <*0*> in dom op by A18, PRE_CIRC:13;
then consider i being Element of NAT , T being DecoratedTree, q being Node of T such that
A20: ( i < len p & T = p . (i + 1) & <*0*> = <*i*> ^ q ) by TREES_4:11;
 op . <*0*> = T . q by A20, TREES_4:12;
then A21: [<*0*>,(T . q)] in op by A19, FUNCT_1:1;
 {} in dom op by TREES_1:22;
then  [{},o9] in op by A15, FUNCT_1:1;
then A22: {[{},o9],[<*0*>,(T . q)]} c= op by A21, ZFMISC_1:32;
 e1 in the Sorts of (FreeEnv A) . v ;
then A23: co in Y by A1;
 [{},o9] <> [<*0*>,(T . q)] by XTUPLE_0:1;
then  card {[{},o9],[<*0*>,(T . q)]} = 2 by CARD_2:57;
then  2 <= co by A22, NAT_1:43;
then  co > size (v,A) by A6, XXREAL_0:2;
hence  contradiction by A2, A23, XXREAL_2:def_8; ::_thesis: verum
end;
suppose not the ResultSort of IIG . o = v ; ::_thesis: contradiction
hence  contradiction by A11; ::_thesis: verum
end;
end;
end;
hence  v in (InputVertices IIG) \/ (SortsWithConstants IIG) ; ::_thesis: verum
end;
consider a being Element of TS (DTConMSA the Sorts of A) such that
A24: a = e and
A25: ( 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 A5;
assume A26: v in (InputVertices IIG) \/ (SortsWithConstants IIG) ; ::_thesis: size (v,A) = 1
percases ( v in InputVertices IIG or v in SortsWithConstants IIG ) by A26, XBOOLE_0:def_3;
suppose v in InputVertices IIG ; ::_thesis: size (v,A) = 1
then consider x being set  such that
 x in the Sorts of A . v and
A27: a = root-tree [x,v] by A25, MSAFREE2:2;
root-tree [x,v] = {{}} --> [x,v] by TREES_1:29, TREES_4:def_2
.= [:{{}},{[x,v]}:] by FUNCOP_1:def_2
.= {[{},[x,v]]} by ZFMISC_1:29 ;
hence  size (v,A) = 1 by A2, A3, A24, A27, CARD_1:30; ::_thesis: verum
end;
suppose v in SortsWithConstants IIG ; ::_thesis: size (v,A) = 1
then  v in  {  v9 where v9 is SortSymbol of IIG : v9 is with_const_op  }  by MSAFREE2:def_1;
then consider v9 being SortSymbol of IIG such that
A28: v9 = v and
A29: v9 is with_const_op ;
consider o being OperSymbol of IIG such that
A30: the Arity of IIG . o = {} and
A31: the ResultSort of IIG . o = v9 by A29, MSUALG_2:def_1;
now__::_thesis:_size_(v,A)_=_1
percases ( ex x being set st
( x in the Sorts of A . v & a = root-tree [x,v] ) or ex o9 being OperSymbol of IIG st
( [o9, the carrier of IIG] = a . {} & the_result_sort_of o9 = v ) ) by A25;
suppose ex x being set st
( x in the Sorts of A . v & a = root-tree [x,v] ) ; ::_thesis: size (v,A) = 1
then consider x being set  such that
 x in the Sorts of A . v and
A32: a = root-tree [x,v] ;
 root-tree [x,v] = {[{},[x,v]]} by TREES_4:6;
hence  size (v,A) = 1 by A2, A3, A24, A32, CARD_1:30; ::_thesis: verum
end;
suppose ex o9 being OperSymbol of IIG st
( [o9, the carrier of IIG] = a . {} & the_result_sort_of o9 = v ) ; ::_thesis: size (v,A) = 1
then consider o9 being OperSymbol of IIG such that
A33: [o9, the carrier of IIG] = a . {} and
A34: the_result_sort_of o9 = v ;
 the_result_sort_of o9 = the_result_sort_of o by A28, A31, A34, MSUALG_1:def_2;
then A35: o9 = o by MSAFREE2:def_6;
 ( NonTerminals (DTConMSA the Sorts of A) = [: the carrier' of IIG,{ the carrier of IIG}:] & the carrier of IIG in { the carrier of IIG} ) by MSAFREE:6, TARSKI:def_1;
then reconsider nt = [o9, the carrier of IIG] as NonTerminal of (DTConMSA the Sorts of A) by ZFMISC_1:87;
consider ts being FinSequence of TS (DTConMSA the Sorts of A) such that
A36: a = nt -tree ts and
 nt ==> roots ts by A33, DTCONSTR:10;
reconsider ts = ts as DTree-yielding FinSequence ;
len ts = len (the_arity_of o9) by A24, A34, A36, MSAFREE2:10
.= len {} by A30, A35, MSUALG_1:def_1
.= 0 ;
then  ts = {} ;
then a = root-tree nt by A36, TREES_4:20
.= {[{},nt]} by TREES_4:6 ;
hence  size (v,A) = 1 by A2, A3, A24, CARD_1:30; ::_thesis: verum
end;
end;
end;
hence  size (v,A) = 1 ; ::_thesis: verum
end;
end;
end;

theorem :: CIRCUIT1:11
for IIG being non empty non void Circuit-like monotonic ManySortedSign
for SCS being non-empty finite-yielding MSAlgebra over IIG
for v, w being Vertex of IIG
for e1 being Element of the Sorts of (FreeEnv SCS) . v
for e2 being Element of the Sorts of (FreeEnv SCS) . w
for q1 being DTree-yielding FinSequence st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e1 = size (v,SCS) & e1 = [(action_at v), the carrier of IIG] -tree q1 & e2 in rng q1 holds
card e2 = size (w,SCS)
proof
let IIG be non empty non void Circuit-like monotonic ManySortedSign ; ::_thesis: for SCS being non-empty finite-yielding MSAlgebra over IIG
for v, w being Vertex of IIG
for e1 being Element of the Sorts of (FreeEnv SCS) . v
for e2 being Element of the Sorts of (FreeEnv SCS) . w
for q1 being DTree-yielding FinSequence st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e1 = size (v,SCS) & e1 = [(action_at v), the carrier of IIG] -tree q1 & e2 in rng q1 holds
card e2 = size (w,SCS)
let SCS be non-empty finite-yielding MSAlgebra over IIG; ::_thesis: for v, w being Vertex of IIG
for e1 being Element of the Sorts of (FreeEnv SCS) . v
for e2 being Element of the Sorts of (FreeEnv SCS) . w
for q1 being DTree-yielding FinSequence st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e1 = size (v,SCS) & e1 = [(action_at v), the carrier of IIG] -tree q1 & e2 in rng q1 holds
card e2 = size (w,SCS)
let v, w be Vertex of IIG; ::_thesis: for e1 being Element of the Sorts of (FreeEnv SCS) . v
for e2 being Element of the Sorts of (FreeEnv SCS) . w
for q1 being DTree-yielding FinSequence st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e1 = size (v,SCS) & e1 = [(action_at v), the carrier of IIG] -tree q1 & e2 in rng q1 holds
card e2 = size (w,SCS)
let e1 be Element of the Sorts of (FreeEnv SCS) . v; ::_thesis: for e2 being Element of the Sorts of (FreeEnv SCS) . w
for q1 being DTree-yielding FinSequence st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e1 = size (v,SCS) & e1 = [(action_at v), the carrier of IIG] -tree q1 & e2 in rng q1 holds
card e2 = size (w,SCS)
let e2 be Element of the Sorts of (FreeEnv SCS) . w; ::_thesis: for q1 being DTree-yielding FinSequence st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e1 = size (v,SCS) & e1 = [(action_at v), the carrier of IIG] -tree q1 & e2 in rng q1 holds
card e2 = size (w,SCS)
let q1 be DTree-yielding FinSequence; ::_thesis: ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e1 = size (v,SCS) & e1 = [(action_at v), the carrier of IIG] -tree q1 & e2 in rng q1 implies card e2 = size (w,SCS) )
assume that
A1: v in (InnerVertices IIG) \ (SortsWithConstants IIG) and
A2: card e1 = size (v,SCS) and
A3: e1 = [(action_at v), the carrier of IIG] -tree q1 and
A4: e2 in rng q1 ; ::_thesis: card e2 = size (w,SCS)
consider sw being non empty finite Subset of NAT such that
A5: sw =  {  (card t) where t is Element of the Sorts of (FreeEnv SCS) . w : verum  }  and
A6: size (w,SCS) = max sw by Def4;
reconsider Y = sw as non empty finite real-membered set ;
reconsider m = max Y as real number ;
 m in  {  (card t) where t is Element of the Sorts of (FreeEnv SCS) . w : verum  }  by A5, XXREAL_2:def_8;
then consider e3 being Element of the Sorts of (FreeEnv SCS) . w such that
A7: card e3 = m ;
 card e2 in Y by A5;
then A8: card e2 <= max Y by XXREAL_2:def_8;
reconsider e39 = e3 as DecoratedTree ;
reconsider e19 = e1 as DecoratedTree ;
reconsider q19 = q1 as Function ;
consider k being set  such that
A9: k in dom q19 and
A10: e2 = q19 . k by A4, FUNCT_1:def_3;
 k in dom q1 by A9;
then reconsider kN = k as Element of NAT ;
reconsider k1 = kN - 1 as Element of NAT by A9, FINSEQ_3:26;
A11: k1 + 1 = kN ;
 ex p being DTree-yielding FinSequence st
( p = q1 & dom e19 = tree (doms p) ) by A3, TREES_4:def_4;
then reconsider k9 = <*k1*> as Element of dom e1 by A9, A11, PRE_CIRC:13;
A12: kN <= len q1 by A9, FINSEQ_3:25;
 k1 < kN by A11, XREAL_1:29;
then  k1 < len q1 by A12, XXREAL_0:2;
then A13: e1 | k9 = e2 by A3, A10, A11, TREES_4:def_4;
assume  card e2 <> size (w,SCS) ; ::_thesis: contradiction
then  card e2 < max Y by A6, A8, XXREAL_0:1;
then  ( (card (e1 with-replacement (k9,e3))) + (card (e1 | k9)) = (card e1) + (card e3) & (card e1) + (card (e1 | k9)) < (card e1) + (card e3) ) by A7, A13, PRE_CIRC:18, XREAL_1:6;
then A14: card e1 < card (e1 with-replacement (k9,e3)) by XREAL_1:6;
reconsider k99 = k9 as FinSequence of NAT ;
reconsider eke = e19 with-replacement (k99,e39) as DecoratedTree ;
reconsider eke = eke as Element of the Sorts of (FreeEnv SCS) . v by A1, A3, A9, A10, A11, Th6;
consider sv being non empty finite Subset of NAT such that
A15: sv =  {  (card t) where t is Element of the Sorts of (FreeEnv SCS) . v : verum  }  and
A16: size (v,SCS) = max sv by Def4;
reconsider Z = sv as non empty finite real-membered set ;
 card eke in Z by A15;
hence  contradiction by A2, A16, A14, XXREAL_2:def_8; ::_thesis: verum
end;

theorem Th12: :: CIRCUIT1:12
for IIG being non empty non void Circuit-like monotonic ManySortedSign
for A being non-empty finite-yielding MSAlgebra over IIG
for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e = size (v,A) holds
ex q being DTree-yielding FinSequence st 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 finite-yielding MSAlgebra over IIG
for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e = size (v,A) holds
ex q being DTree-yielding FinSequence st e = [(action_at v), the carrier of IIG] -tree q
let A be non-empty finite-yielding MSAlgebra over IIG; ::_thesis: for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e = size (v,A) holds
ex q being DTree-yielding FinSequence st 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 st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e = size (v,A) holds
ex q being DTree-yielding FinSequence st e = [(action_at v), the carrier of IIG] -tree q
let e be Element of the Sorts of (FreeEnv A) . v; ::_thesis: ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e = size (v,A) implies ex q being DTree-yielding FinSequence st e = [(action_at v), the carrier of IIG] -tree q )
assume that
A1: v in (InnerVertices IIG) \ (SortsWithConstants IIG) and
A2: card e = size (v,A) ; ::_thesis: ex q being DTree-yielding FinSequence st e = [(action_at v), the carrier of IIG] -tree q
A3: not v in SortsWithConstants IIG by A1, XBOOLE_0:def_5;
 InputVertices IIG misses InnerVertices IIG by XBOOLE_1:79;
then A4: (InputVertices IIG) /\ (InnerVertices IIG) = {} by XBOOLE_0:def_7;
 v in InnerVertices IIG by A1, XBOOLE_0:def_5;
then  not v in InputVertices IIG by A4, XBOOLE_0:def_4;
then  not v in (InputVertices IIG) \/ (SortsWithConstants IIG) by A3, XBOOLE_0:def_3;
then A5: card e <> 1 by A2, Th10;
reconsider e9 = e as non empty finite set ;
 FreeEnv A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #) by MSAFREE:def_14;
then  the Sorts of (FreeEnv A) . v = FreeSort ( the Sorts of A,v) by MSAFREE:def_11;
then  e in FreeSort ( the Sorts of A,v) ;
then A6: 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;
 1 <= card e9 by NAT_1:14;
then  1 < card e9 by A5, XXREAL_0:1;
then consider o being OperSymbol of IIG such that
A7: e . {} = [o, the carrier of IIG] by Th7;
 ( NonTerminals (DTConMSA the Sorts of A) = [: the carrier' of IIG,{ the carrier of IIG}:] & the carrier of IIG in { the carrier of IIG} ) by MSAFREE:6, TARSKI:def_1;
then reconsider nt = [o, the carrier of IIG] as NonTerminal of (DTConMSA the Sorts of A) by ZFMISC_1:87;
consider a being Element of TS (DTConMSA the Sorts of A) such that
A8: a = e and
A9: ( 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;
consider x being set  such that
A10: ( ( x in the Sorts of A . v & a = root-tree [x,v] ) or ex o9 being OperSymbol of IIG st
( [o9, the carrier of IIG] = a . {} & the_result_sort_of o9 = v ) ) by A9;
consider ts being FinSequence of TS (DTConMSA the Sorts of A) such that
A11: a = nt -tree ts and
 nt ==> roots ts by A8, A7, DTCONSTR:10;
reconsider q = ts as DTree-yielding FinSequence ;
take  q ; ::_thesis: e = [(action_at v), the carrier of IIG] -tree q
A12: v in InnerVertices IIG by A1, XBOOLE_0:def_5;
now__::_thesis:_not_a_=_root-tree_[x,v]
assume  a = root-tree [x,v] ; ::_thesis: contradiction
then  [o, the carrier of IIG] = [x,v] by A8, A7, TREES_4:3;
then A13: the carrier of IIG = v by XTUPLE_0:1;
 for X being set holds not X in X ;
hence  contradiction by A13; ::_thesis: verum
end;
then consider o9 being OperSymbol of IIG such that
A14: [o9, the carrier of IIG] = a . {} and
A15: the_result_sort_of o9 = v by A10;
o = o9 by A8, A7, A14, XTUPLE_0:1
.= action_at v by A15, A12, MSAFREE2:def_7 ;
hence  e = [(action_at v), the carrier of IIG] -tree q by A8, A11; ::_thesis: verum
end;

theorem :: CIRCUIT1:13
for IIG being non empty non void Circuit-like monotonic ManySortedSign
for A being non-empty finite-yielding MSAlgebra over IIG
for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e = size (v,A) holds
ex o being OperSymbol of IIG st e . {} = [o, the carrier of IIG]
proof
let IIG be non empty non void Circuit-like monotonic ManySortedSign ; ::_thesis: for A being non-empty finite-yielding MSAlgebra over IIG
for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e = size (v,A) holds
ex o being OperSymbol of IIG st e . {} = [o, the carrier of IIG]
let A be non-empty finite-yielding MSAlgebra over IIG; ::_thesis: for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e = size (v,A) holds
ex o being OperSymbol of IIG st e . {} = [o, 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 (InnerVertices IIG) \ (SortsWithConstants IIG) & card e = size (v,A) holds
ex o being OperSymbol of IIG st e . {} = [o, the carrier of IIG]
let e be Element of the Sorts of (FreeEnv A) . v; ::_thesis: ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e = size (v,A) implies ex o being OperSymbol of IIG st e . {} = [o, the carrier of IIG] )
assume  ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e = size (v,A) ) ; ::_thesis: ex o being OperSymbol of IIG st e . {} = [o, the carrier of IIG]
then A1: ex q being DTree-yielding FinSequence st e = [(action_at v), the carrier of IIG] -tree q by Th12;
take  action_at v ; ::_thesis: e . {} = [(action_at v), the carrier of IIG]
thus  e . {} = [(action_at v), the carrier of IIG] by A1, TREES_4:def_4; ::_thesis: verum
end;

definition
let S be non empty non void ManySortedSign ;
let A be non-empty finite-yielding MSAlgebra over S;
let v be SortSymbol of S;
let e be Element of the Sorts of (FreeEnv A) . v;
func depth e ->  Element of NAT  means :Def5: :: CIRCUIT1:def 5
 ex e9 being Element of the Sorts of (FreeMSA the Sorts of A) . v st
( e = e9 & it = depth e9 );
existence
 ex b1 being Element of NAT ex e9 being Element of the Sorts of (FreeMSA the Sorts of A) . v st
( e = e9 & b1 = depth e9 )
proof
reconsider e9 = e as Element of the Sorts of (FreeMSA the Sorts of A) . v ;
reconsider d = depth e9 as Element of NAT by ORDINAL1:def_12;
take  d ; ::_thesis: ex e9 being Element of the Sorts of (FreeMSA the Sorts of A) . v st
( e = e9 & d = depth e9 )
take  e9 ; ::_thesis: ( e = e9 & d = depth e9 )
thus  ( e = e9 & d = depth e9 ) ; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being Element of NAT st ex e9 being Element of the Sorts of (FreeMSA the Sorts of A) . v st
( e = e9 & b1 = depth e9 ) & ex e9 being Element of the Sorts of (FreeMSA the Sorts of A) . v st
( e = e9 & b2 = depth e9 ) holds
b1 = b2;
;
end;

:: deftheorem Def5 defines depth CIRCUIT1:def_5_:_
 for S being non empty non void ManySortedSign
for A being non-empty finite-yielding MSAlgebra over S
for v being SortSymbol of S
for e being Element of the Sorts of (FreeEnv A) . v
for b5 being Element of NAT holds
( b5 = depth e iff ex e9 being Element of the Sorts of (FreeMSA the Sorts of A) . v st
( e = e9 & b5 = depth e9 ) );

theorem Th14: :: CIRCUIT1:14
for IIG being non empty non void Circuit-like monotonic ManySortedSign
for A being non-empty finite-yielding MSAlgebra over IIG
for v, w being Element of IIG st v in InnerVertices IIG & w in rng (the_arity_of (action_at v)) holds
size (w,A) < size (v,A)
proof
let IIG be non empty non void Circuit-like monotonic ManySortedSign ; ::_thesis: for A being non-empty finite-yielding MSAlgebra over IIG
for v, w being Element of IIG st v in InnerVertices IIG & w in rng (the_arity_of (action_at v)) holds
size (w,A) < size (v,A)
let A be non-empty finite-yielding MSAlgebra over IIG; ::_thesis: for v, w being Element of IIG st v in InnerVertices IIG & w in rng (the_arity_of (action_at v)) holds
size (w,A) < size (v,A)
let v, w be Element of IIG; ::_thesis: ( v in InnerVertices IIG & w in rng (the_arity_of (action_at v)) implies size (w,A) < size (v,A) )
assume that
A1: v in InnerVertices IIG and
A2: w in rng (the_arity_of (action_at v)) ; ::_thesis: size (w,A) < size (v,A)
reconsider av = action_at v as OperSymbol of IIG ;
consider x being set  such that
A3: x in dom (the_arity_of av) and
A4: w = (the_arity_of av) . x by A2, FUNCT_1:def_3;
reconsider k = x as Element of NAT by A3;
reconsider k1 = k - 1 as Element of NAT by A3, FINSEQ_3:26;
A5: k1 + 1 = k ;
reconsider o = <*k1*> as FinSequence of NAT ;
consider sv being non empty finite Subset of NAT such that
A6: sv =  {  (card tv) where tv is Element of the Sorts of (FreeEnv A) . v : verum  }  and
A7: size (v,A) = max sv by Def4;
reconsider Yv = sv as non empty finite real-membered set ;
 max Yv in Yv by XXREAL_2:def_8;
then consider tv being Element of the Sorts of (FreeEnv A) . v such that
A8: card tv = max Yv by A6;
now__::_thesis:_not_v_in_SortsWithConstants_IIG
assume  v in SortsWithConstants IIG ; ::_thesis: contradiction
then  v in  {  v9 where v9 is SortSymbol of IIG : v9 is with_const_op  }  by MSAFREE2:def_1;
then consider v9 being SortSymbol of IIG such that
A9: v9 = v and
A10: v9 is with_const_op ;
consider oo being OperSymbol of IIG such that
A11: the Arity of IIG . oo = {} and
A12: the ResultSort of IIG . oo = v9 by A10, MSUALG_2:def_1;
the_result_sort_of oo = v by A9, A12, MSUALG_1:def_2
.= the_result_sort_of av by A1, MSAFREE2:def_7 ;
then A13: av = oo by MSAFREE2:def_6;
reconsider aoo = the Arity of IIG . oo as FinSequence ;
 dom aoo = {} by A11;
hence  contradiction by A3, A13, MSUALG_1:def_1; ::_thesis: verum
end;
then A14: v in (InnerVertices IIG) \ (SortsWithConstants IIG) by A1, XBOOLE_0:def_5;
then consider p being DTree-yielding FinSequence such that
A15: tv = [av, the carrier of IIG] -tree p by A7, A8, Th12;
A16: the Sorts of (FreeEnv A) . v = the Sorts of (FreeEnv A) . (the_result_sort_of av) by A1, MSAFREE2:def_7;
then  len p = len (the_arity_of av) by A15, MSAFREE2:10;
then A17: k in dom p by A3, FINSEQ_3:29;
reconsider e1 = tv as finite DecoratedTree ;
reconsider de1 = dom e1 as finite Tree ;
consider sw being non empty finite Subset of NAT such that
A18: sw =  {  (card tw) where tw is Element of the Sorts of (FreeEnv A) . w : verum  }  and
A19: size (w,A) = max sw by Def4;
reconsider Yw = sw as non empty finite real-membered set ;
 max Yw in Yw by XXREAL_2:def_8;
then consider tw being Element of the Sorts of (FreeEnv A) . w such that
A20: card tw = max Yw by A18;
reconsider e2 = tw as finite DecoratedTree ;
reconsider de2 = dom e2 as finite Tree ;
 ex p9 being DTree-yielding FinSequence st
( p9 = p & dom e1 = tree (doms p9) ) by A15, TREES_4:def_4;
then reconsider o = o as Element of dom e1 by A17, A5, PRE_CIRC:13;
reconsider eoe = e1 with-replacement (o,e2) as finite Function ;
reconsider o = o as Element of de1 ;
reconsider deoe = dom eoe as finite Tree ;
A21: card (de1 | o) < card de1 by PRE_CIRC:16;
 dom eoe = de1 with-replacement (o,de2) by TREES_2:def_11;
then  (card deoe) + (card (de1 | o)) = (card de1) + (card de2) by PRE_CIRC:17;
then  (card (de1 | o)) + (card de2) < (card deoe) + (card (de1 | o)) by A21, XREAL_1:6;
then  card de2 < card deoe by XREAL_1:6;
then A22: card e2 < card deoe by CARD_1:62;
 p . k in the Sorts of (FreeEnv A) . ((the_arity_of av) . k) by A3, A15, A16, MSAFREE2:11;
then reconsider eoe = eoe as Element of the Sorts of (FreeEnv A) . v by A4, A14, A15, A17, A5, Th6;
 card eoe in Yv by A6;
then  card eoe <= size (v,A) by A7, XXREAL_2:def_8;
then  card deoe <= size (v,A) by CARD_1:62;
hence  size (w,A) < size (v,A) by A19, A20, A22, XXREAL_0:2; ::_thesis: verum
end;

theorem Th15: :: CIRCUIT1:15
for IIG being non empty non void Circuit-like monotonic ManySortedSign
for A being non-empty finite-yielding MSAlgebra over IIG
for v being SortSymbol of IIG holds size (v,A) > 0
proof
let IIG be non empty non void Circuit-like monotonic ManySortedSign ; ::_thesis: for A being non-empty finite-yielding MSAlgebra over IIG
for v being SortSymbol of IIG holds size (v,A) > 0
let A be non-empty finite-yielding MSAlgebra over IIG; ::_thesis: for v being SortSymbol of IIG holds size (v,A) > 0
let v be SortSymbol of IIG; ::_thesis: size (v,A) > 0
consider s being non empty finite Subset of NAT such that
A1: s =  {  (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum  }  and
A2: size (v,A) = max s by Def4;
reconsider Y = s as non empty finite real-membered set ;
 max Y in  {  (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum  }  by A1, XXREAL_2:def_8;
then  ex t being Element of the Sorts of (FreeEnv A) . v st card t = max Y ;
hence  size (v,A) > 0 by A2; ::_thesis: verum
end;

theorem :: CIRCUIT1:16
for IIG being non empty non void Circuit-like monotonic ManySortedSign
for A being non-empty Circuit of IIG
for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v
for p being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(action_at v), the carrier of IIG] -tree p & ( for k being Element of NAT st k in dom p holds
ex ek being Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k) st
( ek = p . k & card ek = size (((the_arity_of (action_at v)) /. k),A) ) ) holds
card e = size (v,A)
proof
let IIG be non empty non void Circuit-like monotonic ManySortedSign ; ::_thesis: for A being non-empty Circuit of IIG
for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v
for p being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(action_at v), the carrier of IIG] -tree p & ( for k being Element of NAT st k in dom p holds
ex ek being Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k) st
( ek = p . k & card ek = size (((the_arity_of (action_at v)) /. k),A) ) ) holds
card e = size (v,A)
let A be non-empty Circuit of IIG; ::_thesis: for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v
for p being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(action_at v), the carrier of IIG] -tree p & ( for k being Element of NAT st k in dom p holds
ex ek being Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k) st
( ek = p . k & card ek = size (((the_arity_of (action_at v)) /. k),A) ) ) holds
card e = size (v,A)
let v be Vertex of IIG; ::_thesis: for e being Element of the Sorts of (FreeEnv A) . v
for p being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(action_at v), the carrier of IIG] -tree p & ( for k being Element of NAT st k in dom p holds
ex ek being Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k) st
( ek = p . k & card ek = size (((the_arity_of (action_at v)) /. k),A) ) ) holds
card e = size (v,A)
let e be Element of the Sorts of (FreeEnv A) . v; ::_thesis: for p being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(action_at v), the carrier of IIG] -tree p & ( for k being Element of NAT st k in dom p holds
ex ek being Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k) st
( ek = p . k & card ek = size (((the_arity_of (action_at v)) /. k),A) ) ) holds
card e = size (v,A)
let p be DTree-yielding FinSequence; ::_thesis: ( v in InnerVertices IIG & e = [(action_at v), the carrier of IIG] -tree p & ( for k being Element of NAT st k in dom p holds
ex ek being Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k) st
( ek = p . k & card ek = size (((the_arity_of (action_at v)) /. k),A) ) ) implies card e = size (v,A) )
assume that
A1: v in InnerVertices IIG and
A2: e = [(action_at v), the carrier of IIG] -tree p and
A3: for k being Element of NAT st k in dom p holds
ex ek being Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k) st
( ek = p . k & card ek = size (((the_arity_of (action_at v)) /. k),A) ) ; ::_thesis: card e = size (v,A)
consider s being non empty finite Subset of NAT such that
A4: s =  {  (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum  }  and
A5: size (v,A) = max s by Def4;
reconsider S = s as non empty finite real-membered set ;
A6: now__::_thesis:_for_r_being_ext-real_number_st_r_in_S_holds_
r_<=_card_e
reconsider e9 = e as finite set ;
let r be ext-real number ; ::_thesis: ( r in S implies b1 <= card e )
A7: 1 <= card e9 by NAT_1:14;
assume  r in S ; ::_thesis: b1 <= card e
then consider t being Element of the Sorts of (FreeEnv A) . v such that
A8: r = card t by A4;
 FreeEnv A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #) by MSAFREE:def_14;
then  the Sorts of (FreeEnv A) . v = FreeSort ( the Sorts of A,v) by MSAFREE:def_11;
then  t in FreeSort ( the Sorts of A,v) ;
then  t in  {  a9 where a9 is Element of TS (DTConMSA the Sorts of A) : ( ex x being set st
( x in the Sorts of A . v & a9 = root-tree [x,v] ) or ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a9 . {} & the_result_sort_of o = v ) )  }  by MSAFREE:def_10;
then consider a9 being Element of TS (DTConMSA the Sorts of A) such that
A9: a9 = t and
A10: ( ex x being set st
( x in the Sorts of A . v & a9 = root-tree [x,v] ) or ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a9 . {} & the_result_sort_of o = v ) ) ;
percases ( ex x being set st
( x in the Sorts of A . v & a9 = root-tree [x,v] ) or ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a9 . {} & the_result_sort_of o = v ) ) by A10;
suppose ex x being set st
( x in the Sorts of A . v & a9 = root-tree [x,v] ) ; ::_thesis: b1 <= card e
then consider x being set  such that
 x in the Sorts of A . v and
A11: a9 = root-tree [x,v] ;
 root-tree [x,v] = {[{},[x,v]]} by TREES_4:6;
hence  r <= card e by A7, A8, A9, A11, CARD_1:30; ::_thesis: verum
end;
suppose ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a9 . {} & the_result_sort_of o = v ) ; ::_thesis: b1 <= card e
then  a9 . {} = [(action_at v), the carrier of IIG] by A1, MSAFREE2:def_7;
then consider q being DTree-yielding FinSequence such that
A12: t = [(action_at v), the carrier of IIG] -tree q by A9, Th9;
deffunc H1( Nat) ->  set = p +* (q | (Seg $1));
consider T being FinSequence such that
A13: len T = len p and
A14: for k being Nat st k in dom T holds
T . k = H1(k) from FINSEQ_1:sch_2();
A15: dom T = dom p by A13, FINSEQ_3:29;
A16: the_result_sort_of (action_at v) = v by A1, MSAFREE2:def_7;
A17: dom p = Seg (len p) by FINSEQ_1:def_3;
now__::_thesis:_r_<=_card_e
percases ( len q = 0 or len q <> 0 ) ;
suppose len q = 0 ; ::_thesis: r <= card e
then  q = {} ;
then  t = root-tree [(action_at v), the carrier of IIG] by A12, TREES_4:20;
hence  r <= card e by A7, A8, PRE_CIRC:19; ::_thesis: verum
end;
supposeA18: len q <> 0 ; ::_thesis: r <= card e
defpred S2[ Element of NAT ] means ( $1 in dom p implies for qk being DTree-yielding FinSequence st qk = T . $1 holds
for tk being finite set st tk = [(action_at v), the carrier of IIG] -tree qk holds
card tk <= card e );
A19: len p = len (the_arity_of (action_at v)) by A2, A16, MSAFREE2:10;
then A20: len p = len q by A12, A16, MSAFREE2:10;
then A21: 1 + 0 <= len p by A18, NAT_1:14;
A22: dom p = dom q by A20, FINSEQ_3:29;
A23: dom p = dom (the_arity_of (action_at v)) by A19, FINSEQ_3:29;
A24: now__::_thesis:_for_k_being_Element_of_NAT_st_S2[k]_holds_
S2[k_+_1]
let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] )
assume A25: S2[k] ; ::_thesis: S2[k + 1]
thus  S2[k + 1] ::_thesis: verum
proof
reconsider tree0 = [(action_at v), the carrier of IIG] -tree p as finite DecoratedTree by A2;
assume A26: k + 1 in dom p ; ::_thesis: for qk being DTree-yielding FinSequence st qk = T . (k + 1) holds
for tk being finite set st tk = [(action_at v), the carrier of IIG] -tree qk holds
card tk <= card e
let qk1 be DTree-yielding FinSequence; ::_thesis: ( qk1 = T . (k + 1) implies for tk being finite set st tk = [(action_at v), the carrier of IIG] -tree qk1 holds
card tk <= card e )
assume A27: qk1 = T . (k + 1) ; ::_thesis: for tk being finite set st tk = [(action_at v), the carrier of IIG] -tree qk1 holds
card tk <= card e
let tk1 be finite set ; ::_thesis: ( tk1 = [(action_at v), the carrier of IIG] -tree qk1 implies card tk1 <= card e )
assume A28: tk1 = [(action_at v), the carrier of IIG] -tree qk1 ; ::_thesis: card tk1 <= card e
then reconsider treek1 = tk1 as finite DecoratedTree ;
percases ( k = 0 or k <> 0 ) ;
supposeA29: k = 0 ; ::_thesis: card tk1 <= card e
set v1 = (the_arity_of (action_at v)) /. 1;
A30: 1 in dom p by A21, FINSEQ_3:25;
then consider e1 being Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. 1) such that
A31: e1 = p . 1 and
A32: card e1 = size (((the_arity_of (action_at v)) /. 1),A) by A3;
 1 in Seg 1 by FINSEQ_1:3;
then A33: 1 in dom (q | (Seg 1)) by A22, A30, RELAT_1:57;
A34: 1 in dom (the_arity_of (action_at v)) by A19, A21, FINSEQ_3:25;
then  q . 1 in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) . 1) by A12, A16, MSAFREE2:11;
then reconsider T1 = q . 1 as Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. 1) by A34, PARTFUN1:def_6;
reconsider Tx = p . 1 as finite DecoratedTree by A31;
 ( {} is Element of dom Tx & <*0*> = <*0*> ^ {} ) by FINSEQ_1:34, TREES_1:22;
then reconsider w0 = <*0*> as Element of dom tree0 by A21, TREES_4:11;
consider q0 being DTree-yielding FinSequence such that
A35: e with-replacement (w0,T1) = [(action_at v), the carrier of IIG] -tree q0 and
A36: len q0 = len p and
A37: q0 . (0 + 1) = T1 and
A38: for i being Element of NAT st i in dom p & i <> 0 + 1 holds
q0 . i = p . i by A2, PRE_CIRC:15;
A39: 1 in dom p by A21, FINSEQ_3:25;
then A40: qk1 . 1 = (p +* (q | (Seg 1))) . 1 by A14, A15, A27, A29
.= (q | (Seg 1)) . 1 by A33, FUNCT_4:13
.= q . 1 by FINSEQ_1:3, FUNCT_1:49 ;
A41: now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_q0_holds_
q0_._k_=_qk1_._k
let k be Nat; ::_thesis: ( 1 <= k & k <= len q0 implies q0 . b1 = qk1 . b1 )
assume  ( 1 <= k & k <= len q0 ) ; ::_thesis: q0 . b1 = qk1 . b1
then A42: k in dom p by A36, FINSEQ_3:25;
percases ( k = 1 or k <> 1 ) ;
suppose k = 1 ; ::_thesis: q0 . b1 = qk1 . b1
hence  q0 . k = qk1 . k by A40, A37; ::_thesis: verum
end;
supposeA43: k <> 1 ; ::_thesis: qk1 . b1 = q0 . b1
A44: dom (q | (Seg 1)) = (dom q) /\ (Seg 1) by RELAT_1:61;
 not k in Seg 1 by A43, FINSEQ_1:2, TARSKI:def_1;
then A45: not k in dom (q | (Seg 1)) by A44, XBOOLE_0:def_4;
thus qk1 . k = (p +* (q | (Seg 1))) . k by A14, A15, A27, A29, A39
.= p . k by A45, FUNCT_4:11
.= q0 . k by A38, A42, A43 ; ::_thesis: verum
end;
end;
end;
dom qk1 = dom (p +* (q | (Seg 1))) by A14, A15, A27, A29, A39
.= (dom p) \/ (dom (q | (Seg 1))) by FUNCT_4:def_1
.= (dom p) \/ ((dom q) /\ (Seg 1)) by RELAT_1:61
.= dom p by A22, XBOOLE_1:22 ;
then  len qk1 = len p by FINSEQ_3:29;
then  treek1 = tree0 with-replacement (w0,T1) by A2, A28, A35, A36, A41, FINSEQ_1:14;
then A46: (card treek1) + (card (tree0 | w0)) = (card tree0) + (card T1) by PRE_CIRC:18;
consider s1 being non empty finite Subset of NAT such that
A47: s1 =  {  (card t1) where t1 is Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. 1) : verum  }  and
A48: card e1 = max s1 by A32, Def4;
reconsider S1 = s1 as non empty finite real-membered set ;
 card T1 in S1 by A47;
then A49: card T1 <= card e1 by A48, XXREAL_2:def_8;
 tree0 | w0 = e1 by A21, A31, TREES_4:def_4;
hence  card tk1 <= card e by A2, A49, A46, XREAL_1:8; ::_thesis: verum
end;
supposeA50: k <> 0 ; ::_thesis: card tk1 <= card e
A51: k + 1 <= len p by A26, FINSEQ_3:25;
then A52: k < len p by NAT_1:13;
set v1 = (the_arity_of (action_at v)) /. (k + 1);
 ( not k + 1 in Seg k & dom (q | (Seg k)) = (dom q) /\ (Seg k) ) by FINSEQ_3:8, RELAT_1:61;
then A53: not k + 1 in dom (q | (Seg k)) by XBOOLE_0:def_4;
 k + 1 >= 1 by NAT_1:11;
then A54: k + 1 in dom (the_arity_of (action_at v)) by A19, A51, FINSEQ_3:25;
then  p . (k + 1) in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) . (k + 1)) by A2, A16, MSAFREE2:11;
then reconsider T1 = p . (k + 1) as Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. (k + 1)) by A54, PARTFUN1:def_6;
 k + 1 in Seg (k + 1) by FINSEQ_1:3;
then A55: k + 1 in dom (q | (Seg (k + 1))) by A22, A26, RELAT_1:57;
A56: k >= 1 by A50, NAT_1:14;
then A57: k in dom p by A52, FINSEQ_3:25;
then  T . k = p +* (q | (Seg k)) by A14, A15;
then reconsider qk = T . k as Function ;
A58: dom qk = dom (p +* (q | (Seg k))) by A14, A15, A57
.= (dom p) \/ (dom (q | (Seg k))) by FUNCT_4:def_1
.= (dom p) \/ ((dom q) /\ (Seg k)) by RELAT_1:61
.= dom p by A22, XBOOLE_1:22 ;
then  dom qk = Seg (len p) by FINSEQ_1:def_3;
then reconsider qk = qk as FinSequence by FINSEQ_1:def_2;
A59: for x being set st x in dom qk holds
qk . x is finite DecoratedTree
proof
let x be set ; ::_thesis: ( x in dom qk implies qk . x is finite DecoratedTree )
assume A60: x in dom qk ; ::_thesis: qk . x is finite DecoratedTree
then reconsider n = x as Element of NAT ;
set v1 = (the_arity_of (action_at v)) /. n;
 ( qk . n = q . n or qk . n = p . n )
proof
percases ( n <= k or n > k ) ;
supposeA61: n <= k ; ::_thesis: ( qk . n = q . n or qk . n = p . n )
 n >= 1 by A60, FINSEQ_3:25;
then A62: n in Seg k by A61, FINSEQ_1:1;
 dom (q | (Seg k)) = (dom q) /\ (Seg k) by RELAT_1:61;
then A63: n in dom (q | (Seg k)) by A22, A58, A60, A62, XBOOLE_0:def_4;
qk . n = (p +* (q | (Seg k))) . n by A14, A15, A57
.= (q | (Seg k)) . n by A63, FUNCT_4:13
.= q . n by A63, FUNCT_1:47 ;
hence  ( qk . n = q . n or qk . n = p . n ) ; ::_thesis: verum
end;
supposeA64: n > k ; ::_thesis: ( qk . n = q . n or qk . n = p . n )
A65: dom (q | (Seg k)) = (dom q) /\ (Seg k) by RELAT_1:61;
 not n in Seg k by A64, FINSEQ_1:1;
then A66: not n in dom (q | (Seg k)) by A65, XBOOLE_0:def_4;
qk . n = (p +* (q | (Seg k))) . n by A14, A15, A57
.= p . n by A66, FUNCT_4:11 ;
hence  ( qk . n = q . n or qk . n = p . n ) ; ::_thesis: verum
end;
end;
end;
then  qk . n in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) . n) by A2, A12, A16, A23, A58, A60, MSAFREE2:11;
then reconsider T1 = qk . n as Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. n) by A23, A58, A60, PARTFUN1:def_6;
 T1 in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. n) ;
hence  qk . x is finite DecoratedTree ; ::_thesis: verum
end;
then  for x being set st x in dom qk holds
qk . x is DecoratedTree ;
then reconsider qk = qk as DTree-yielding FinSequence by TREES_3:24;
A67: len qk = len p by A58, FINSEQ_3:29;
A68: qk . (k + 1) = (p +* (q | (Seg k))) . (k + 1) by A14, A15, A57
.= p . (k + 1) by A53, FUNCT_4:11 ;
now__::_thesis:_for_x_being_set_st_x_in_dom_(doms_qk)_holds_
(doms_qk)_._x_is_finite_Tree
let x be set ; ::_thesis: ( x in dom (doms qk) implies (doms qk) . x is finite Tree )
assume  x in dom (doms qk) ; ::_thesis: (doms qk) . x is finite Tree
then A69: x in dom qk by TREES_3:37;
then reconsider T1 = qk . x as finite DecoratedTree by A59;
 dom T1 is finite Tree ;
hence  (doms qk) . x is finite Tree by A69, FUNCT_6:22; ::_thesis: verum
end;
then reconsider qkf = doms qk as FinTree-yielding FinSequence by TREES_3:23;
 ( tree qkf is finite & ex q being DTree-yielding FinSequence st
( qk = q & dom ([(action_at v), the carrier of IIG] -tree qk) = tree (doms q) ) ) by TREES_4:def_4;
then reconsider tk = [(action_at v), the carrier of IIG] -tree qk as finite DecoratedTree by FINSET_1:10;
consider e1 being Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. (k + 1)) such that
A70: e1 = p . (k + 1) and
A71: card e1 = size (((the_arity_of (action_at v)) /. (k + 1)),A) by A3, A26;
 T1 in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. (k + 1)) ;
then reconsider Tx = qk . (k + 1) as finite DecoratedTree by A68;
 (the_arity_of (action_at v)) /. (k + 1) = (the_arity_of (action_at v)) . (k + 1) by A54, PARTFUN1:def_6;
then reconsider T1 = q . (k + 1) as Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. (k + 1)) by A12, A16, A54, MSAFREE2:11;
A72: ( {} is Element of dom Tx & <*k*> = <*k*> ^ {} ) by FINSEQ_1:34, TREES_1:22;
then  <*k*> in dom tk by A52, A67, TREES_4:11;
then consider q0 being DTree-yielding FinSequence such that
A73: tk with-replacement (<*k*>,T1) = [(action_at v), the carrier of IIG] -tree q0 and
A74: len q0 = len qk and
A75: q0 . (k + 1) = T1 and
A76: for i being Element of NAT st i in dom qk & i <> k + 1 holds
q0 . i = qk . i by PRE_CIRC:15;
A77: qk1 . (k + 1) = (p +* (q | (Seg (k + 1)))) . (k + 1) by A14, A15, A26, A27
.= (q | (Seg (k + 1))) . (k + 1) by A55, FUNCT_4:13
.= q . (k + 1) by FINSEQ_1:3, FUNCT_1:49 ;
A78: now__::_thesis:_for_n_being_Nat_st_1_<=_n_&_n_<=_len_q0_holds_
q0_._n_=_qk1_._n
let n be Nat; ::_thesis: ( 1 <= n & n <= len q0 implies q0 . b1 = qk1 . b1 )
assume that
A79: 1 <= n and
A80: n <= len q0 ; ::_thesis: q0 . b1 = qk1 . b1
A81: n in dom qk by A74, A79, A80, FINSEQ_3:25;
percases ( n = k + 1 or n > k + 1 or n < k + 1 ) by XXREAL_0:1;
suppose n = k + 1 ; ::_thesis: q0 . b1 = qk1 . b1
hence  q0 . n = qk1 . n by A77, A75; ::_thesis: verum
end;
supposeA82: n > k + 1 ; ::_thesis: qk1 . b1 = q0 . b1
 k + 1 >= k by NAT_1:11;
then  n > k by A82, XXREAL_0:2;
then A83: not n in Seg k by FINSEQ_1:1;
 dom (q | (Seg k)) = (dom q) /\ (Seg k) by RELAT_1:61;
then A84: not n in dom (q | (Seg k)) by A83, XBOOLE_0:def_4;
A85: dom (q | (Seg (k + 1))) = (dom q) /\ (Seg (k + 1)) by RELAT_1:61;
 not n in Seg (k + 1) by A82, FINSEQ_1:1;
then A86: not n in dom (q | (Seg (k + 1))) by A85, XBOOLE_0:def_4;
thus qk1 . n = (p +* (q | (Seg (k + 1)))) . n by A14, A15, A26, A27
.= p . n by A86, FUNCT_4:11
.= (p +* (q | (Seg k))) . n by A84, FUNCT_4:11
.= qk . n by A14, A15, A57
.= q0 . n by A76, A81, A82 ; ::_thesis: verum
end;
supposeA87: n < k + 1 ; ::_thesis: qk1 . b1 = q0 . b1
A88: n in dom q by A20, A67, A74, A79, A80, FINSEQ_3:25;
 n <= k by A87, NAT_1:13;
then A89: n in Seg k by A79, FINSEQ_1:1;
 dom (q | (Seg k)) = (dom q) /\ (Seg k) by RELAT_1:61;
then A90: n in dom (q | (Seg k)) by A88, A89, XBOOLE_0:def_4;
A91: dom (q | (Seg (k + 1))) = (dom q) /\ (Seg (k + 1)) by RELAT_1:61;
 n in Seg (k + 1) by A79, A87, FINSEQ_1:1;
then A92: n in dom (q | (Seg (k + 1))) by A88, A91, XBOOLE_0:def_4;
thus qk1 . n = (p +* (q | (Seg (k + 1)))) . n by A14, A15, A26, A27
.= (q | (Seg (k + 1))) . n by A92, FUNCT_4:13
.= q . n by A92, FUNCT_1:47
.= (q | (Seg k)) . n by A90, FUNCT_1:47
.= (p +* (q | (Seg k))) . n by A90, FUNCT_4:13
.= qk . n by A14, A15, A57
.= q0 . n by A76, A81, A87 ; ::_thesis: verum
end;
end;
end;
 k < len qk by A52, A58, FINSEQ_3:29;
then reconsider w0 = <*k*> as Element of dom tk by A72, TREES_4:11;
dom qk1 = dom (p +* (q | (Seg (k + 1)))) by A14, A15, A26, A27
.= (dom p) \/ (dom (q | (Seg (k + 1)))) by FUNCT_4:def_1
.= (dom p) \/ ((dom q) /\ (Seg (k + 1))) by RELAT_1:61
.= dom p by A22, XBOOLE_1:22 ;
then  len qk1 = len p by FINSEQ_3:29;
then  treek1 = tk with-replacement (w0,T1) by A28, A67, A73, A74, A78, FINSEQ_1:14;
then A93: (card treek1) + (card (tk | w0)) = (card tk) + (card T1) by PRE_CIRC:18;
consider s1 being non empty finite Subset of NAT such that
A94: s1 =  {  (card t1) where t1 is Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. (k + 1)) : verum  }  and
A95: card e1 = max s1 by A71, Def4;
reconsider S1 = s1 as non empty finite real-membered set ;
 card T1 in S1 by A94;
then A96: card T1 <= card e1 by A95, XXREAL_2:def_8;
 tk | w0 = e1 by A52, A70, A68, A67, TREES_4:def_4;
then A97: card tk1 <= card tk by A96, A93, XREAL_1:8;
 card tk <= card e by A25, A56, A52, FINSEQ_3:25;
hence  card tk1 <= card e by A97, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
end;
A98: S2[ 0 ] by FINSEQ_3:25;
A99: for k being Element of NAT holds S2[k] from NAT_1:sch_1(A98, A24);
 dom p = Seg (len p) by FINSEQ_1:def_3;
then A100: dom p = dom q by A20, FINSEQ_1:def_3;
A101: len p in dom p by A21, FINSEQ_3:25;
then T . (len p) = p +* (q | (dom p)) by A14, A15, A17
.= p +* q by A100, RELAT_1:69
.= q by A22, FUNCT_4:19 ;
hence  r <= card e by A8, A12, A99, A101; ::_thesis: verum
end;
end;
end;
hence  r <= card e ; ::_thesis: verum
end;
end;
end;
 card e in S by A4;
hence  card e = size (v,A) by A5, A6, XXREAL_2:def_8; ::_thesis: verum
end;

begin

definition
let S be non empty non void monotonic ManySortedSign ;
let A be non-empty finite-yielding MSAlgebra over S;
let v be SortSymbol of S;
func depth (v,A) ->  Nat means :Def6: :: CIRCUIT1:def 6
 ex s being non empty finite Subset of NAT st
( s =  {  (depth t) where t is Element of the Sorts of (FreeEnv A) . v : verum  }  & it = max s );
existence
 ex b1 being Nat ex s being non empty finite Subset of NAT st
( s =  {  (depth t) where t is Element of the Sorts of (FreeEnv A) . v : verum  }  & b1 = max s )
proof
deffunc H1( Element of the Sorts of (FreeEnv A) . v) ->  Element of NAT = depth $1;
set s =  {  H1(t) where t is Element of the Sorts of (FreeEnv A) . v : S1[t]  }  ;
set t = the Element of the Sorts of (FreeEnv A) . v;
A1: depth the Element of the Sorts of (FreeEnv A) . v in  {  H1(t) where t is Element of the Sorts of (FreeEnv A) . v : S1[t]  }  ;
A2:  {  H1(t) where t is Element of the Sorts of (FreeEnv A) . v : S1[t]  }  is Subset of NAT from DOMAIN_1:sch_8();
  {  H1(t) where t is Element of the Sorts of (FreeEnv A) . v : S1[t]  }  is finite from PRE_CIRC:sch_1();
then reconsider s =  {  H1(t) where t is Element of the Sorts of (FreeEnv A) . v : S1[t]  }  as non empty finite Subset of NAT by A1, A2;
take  max s ; ::_thesis: ex s being non empty finite Subset of NAT st
( s =  {  (depth t) where t is Element of the Sorts of (FreeEnv A) . v : verum  }  & max s = max s )
take  s ; ::_thesis: ( s =  {  (depth t) where t is Element of the Sorts of (FreeEnv A) . v : verum  }  & max s = max s )
thus  ( s =  {  (depth t) where t is Element of the Sorts of (FreeEnv A) . v : verum  }  & max s = max s ) ; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being Nat st ex s being non empty finite Subset of NAT st
( s =  {  (depth t) where t is Element of the Sorts of (FreeEnv A) . v : verum  }  & b1 = max s ) & ex s being non empty finite Subset of NAT st
( s =  {  (depth t) where t is Element of the Sorts of (FreeEnv A) . v : verum  }  & b2 = max s ) holds
b1 = b2;
;
end;

:: deftheorem Def6 defines depth CIRCUIT1:def_6_:_
 for S being non empty non void monotonic ManySortedSign
for A being non-empty finite-yielding MSAlgebra over S
for v being SortSymbol of S
for b4 being Nat holds
( b4 = depth (v,A) iff ex s being non empty finite Subset of NAT st
( s =  {  (depth t) where t is Element of the Sorts of (FreeEnv A) . v : verum  }  & b4 = max s ) );

definition
let IIG be non empty finite non void Circuit-like monotonic ManySortedSign ;
let A be non-empty Circuit of IIG;
func depth A ->  Nat means :Def7: :: CIRCUIT1:def 7
 ex Ds being non empty finite Subset of NAT st
( Ds =  {  (depth (v,A)) where v is Element of IIG : v in the carrier of IIG  }  & it = max Ds );
existence
 ex b1 being Nat ex Ds being non empty finite Subset of NAT st
( Ds =  {  (depth (v,A)) where v is Element of IIG : v in the carrier of IIG  }  & b1 = max Ds )
proof
deffunc H1( Element of IIG) ->  Nat = depth ($1,A);
set Ds =  {  H1(v) where v is Element of IIG : v in the carrier of IIG  }  ;
A1:  {  H1(v) where v is Element of IIG : v in the carrier of IIG  }  is natural-membered
proof
let e be number ; :: according to MEMBERED:def_6 ::_thesis: ( not e in  {  H1(v) where v is Element of IIG : v in the carrier of IIG  }  or e is natural )
assume  e in  {  H1(v) where v is Element of IIG : v in the carrier of IIG  }  ; ::_thesis: e is natural
then  ex v being Element of IIG st
( e = depth (v,A) & v in the carrier of IIG ) ;
hence  e is natural ; ::_thesis: verum
end;
set v = the Element of IIG;
A2: depth ( the Element of IIG,A) in  {  H1(v) where v is Element of IIG : v in the carrier of IIG  }  ;
A3: the carrier of IIG is finite ;
  {  H1(v) where v is Element of IIG : v in the carrier of IIG  }  is finite from FRAENKEL:sch_21(A3);
then reconsider Ds =  {  H1(v) where v is Element of IIG : v in the carrier of IIG  }  as non empty finite Subset of NAT by A1, A2, MEMBERED:6;
take  max Ds ; ::_thesis: ex Ds being non empty finite Subset of NAT st
( Ds =  {  (depth (v,A)) where v is Element of IIG : v in the carrier of IIG  }  & max Ds = max Ds )
take  Ds ; ::_thesis: ( Ds =  {  (depth (v,A)) where v is Element of IIG : v in the carrier of IIG  }  & max Ds = max Ds )
thus  ( Ds =  {  (depth (v,A)) where v is Element of IIG : v in the carrier of IIG  }  & max Ds = max Ds ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Nat st ex Ds being non empty finite Subset of NAT st
( Ds =  {  (depth (v,A)) where v is Element of IIG : v in the carrier of IIG  }  & b1 = max Ds ) & ex Ds being non empty finite Subset of NAT st
( Ds =  {  (depth (v,A)) where v is Element of IIG : v in the carrier of IIG  }  & b2 = max Ds ) holds
b1 = b2 ;
end;

:: deftheorem Def7 defines depth CIRCUIT1:def_7_:_
 for IIG being non empty finite non void Circuit-like monotonic ManySortedSign
for A being non-empty Circuit of IIG
for b3 being Nat holds
( b3 = depth A iff ex Ds being non empty finite Subset of NAT st
( Ds =  {  (depth (v,A)) where v is Element of IIG : v in the carrier of IIG  }  & b3 = max Ds ) );

theorem :: CIRCUIT1:17
for IIG being non empty finite non void Circuit-like monotonic ManySortedSign
for A being non-empty Circuit of IIG
for v being Vertex of IIG holds depth (v,A) <= depth A
proof
let IIG be non empty finite non void Circuit-like monotonic ManySortedSign ; ::_thesis: for A being non-empty Circuit of IIG
for v being Vertex of IIG holds depth (v,A) <= depth A
let A be non-empty Circuit of IIG; ::_thesis: for v being Vertex of IIG holds depth (v,A) <= depth A
let v be Vertex of IIG; ::_thesis: depth (v,A) <= depth A
consider Ds being non empty finite Subset of NAT such that
A1: Ds =  {  (depth (v9,A)) where v9 is Element of IIG : v9 in the carrier of IIG  }  and
A2: depth A = max Ds by Def7;
reconsider Y = Ds as non empty finite real-membered set ;
 depth (v,A) in Y by A1;
hence  depth (v,A) <= depth A by A2, XXREAL_2:def_8; ::_thesis: verum
end;

theorem Th18: :: CIRCUIT1:18
for IIG being non empty non void Circuit-like monotonic ManySortedSign
for A being non-empty Circuit of IIG
for v being Vertex of IIG holds
( depth (v,A) = 0 iff ( v in InputVertices IIG or v in SortsWithConstants IIG ) )
proof
let IIG be non empty non void Circuit-like monotonic ManySortedSign ; ::_thesis: for A being non-empty Circuit of IIG
for v being Vertex of IIG holds
( depth (v,A) = 0 iff ( v in InputVertices IIG or v in SortsWithConstants IIG ) )
let A be non-empty Circuit of IIG; ::_thesis: for v being Vertex of IIG holds
( depth (v,A) = 0 iff ( v in InputVertices IIG or v in SortsWithConstants IIG ) )
let v be Vertex of IIG; ::_thesis: ( depth (v,A) = 0 iff ( v in InputVertices IIG or v in SortsWithConstants IIG ) )
consider s being non empty finite Subset of NAT such that
A1: s =  {  (depth t) where t is Element of the Sorts of (FreeEnv A) . v : verum  }  and
A2: depth (v,A) = max s by Def6;
reconsider Y = s as non empty finite real-membered set ;
A3: max Y in  {  (depth t) where t is Element of the Sorts of (FreeEnv A) . v : verum  }  by A1, XXREAL_2:def_8;
consider ss being non empty finite Subset of NAT such that
A4: ss =  {  (card tt) where tt is Element of the Sorts of (FreeEnv A) . v : verum  }  and
A5: size (v,A) = max ss by Def4;
reconsider YY = ss as non empty finite real-membered set ;
consider t being Element of the Sorts of (FreeEnv A) . v such that
A6: depth t = max Y by A3;
reconsider t99 = t as Function ;
consider t2 being Element of the Sorts of (FreeMSA the Sorts of A) . v such that
A7: t = t2 and
A8: depth t = depth t2 by Def5;
consider dt being finite DecoratedTree, t9 being finite Tree such that
A9: ( dt = t2 & t9 = dom dt ) and
A10: depth t2 = height t9 by MSAFREE2:def_14;
consider p being FinSequence of NAT  such that
A11: p in t9 and
A12: len p = height t9 by TREES_1:def_12;
consider y99 being set  such that
A13: [p,y99] in t99 by A7, A9, A11, XTUPLE_0:def_12;
thus  ( not depth (v,A) = 0 or v in InputVertices IIG or v in SortsWithConstants IIG ) ::_thesis: ( ( v in InputVertices IIG or v in SortsWithConstants IIG ) implies depth (v,A) = 0 )
proof
assume A14: depth (v,A) = 0 ; ::_thesis: ( v in InputVertices IIG or v in SortsWithConstants IIG )
A15: for kk being ext-real number st kk in YY holds
kk <= 1
proof
let kk be ext-real number ; ::_thesis: ( kk in YY implies kk <= 1 )
assume  kk in YY ; ::_thesis: kk <= 1
then consider tt being Element of the Sorts of (FreeEnv A) . v such that
A16: card tt = kk by A4;
consider tiv being Element of the Sorts of (FreeMSA the Sorts of A) . v such that
A17: ( tt = tiv & depth tt = depth tiv ) by Def5;
 depth tt in Y by A1;
then A18: depth tt = 0 by A2, A14, XXREAL_2:def_8;
A19: ex dt9 being finite DecoratedTree ex t999 being finite Tree st
( dt9 = tiv & t999 = dom dt9 & depth tiv = height t999 ) by MSAFREE2:def_14;
then  rng tt = {(tt . {})} by A18, A17, FUNCT_1:4, TREES_1:29, TREES_1:43;
then  tt = {[{},(tt . {})]} by A18, A17, A19, PRE_CIRC:1, TREES_1:29, TREES_1:43;
hence  kk <= 1 by A16, CARD_1:30; ::_thesis: verum
end;
 rng t99 = {(t . {})} by A2, A6, A7, A8, A9, A10, A14, FUNCT_1:4, TREES_1:29, TREES_1:43;
then  t99 = {[{},(t . {})]} by A2, A6, A7, A8, A9, A10, A14, PRE_CIRC:1, TREES_1:29, TREES_1:43;
then  card t = 1 by CARD_1:30;
then  1 in YY by A4;
then  size (v,A) = 1 by A5, A15, XXREAL_2:def_8;
then  v in (InputVertices IIG) \/ (SortsWithConstants IIG) by Th10;
hence  ( v in InputVertices IIG or v in SortsWithConstants IIG ) by XBOOLE_0:def_3; ::_thesis: verum
end;
 card t in NAT ;
then reconsider ct = card t as Real ;
 {} in dom t by TREES_1:22;
then consider y being set  such that
A20: [{},y] in t99 by XTUPLE_0:def_12;
A21: card t in ss by A4;
assume  ( v in InputVertices IIG or v in SortsWithConstants IIG ) ; ::_thesis: depth (v,A) = 0
then  v in (InputVertices IIG) \/ (SortsWithConstants IIG) by XBOOLE_0:def_3;
then  size (v,A) = 1 by Th10;
then  ct <= 1 by A5, A21, XXREAL_2:def_8;
then  ( card t <= 0 or card t = 0 + 1 ) by NAT_1:8;
then consider x being set  such that
A22: t = {x} by CARD_2:42;
 x = [{},y] by A22, A20, TARSKI:def_1;
then  [p,y99] = [{},y] by A22, A13, TARSKI:def_1;
then  p = {} by XTUPLE_0:1;
hence  depth (v,A) = 0 by A2, A6, A8, A10, A12; ::_thesis: verum
end;

theorem :: CIRCUIT1:19
for IIG being non empty non void Circuit-like monotonic ManySortedSign
for A being non-empty finite-yielding MSAlgebra over IIG
for v, v1 being SortSymbol of IIG st v in InnerVertices IIG & v1 in rng (the_arity_of (action_at v)) holds
depth (v1,A) < depth (v,A)
proof
let IIG be non empty non void Circuit-like monotonic ManySortedSign ; ::_thesis: for A being non-empty finite-yielding MSAlgebra over IIG
for v, v1 being SortSymbol of IIG st v in InnerVertices IIG & v1 in rng (the_arity_of (action_at v)) holds
depth (v1,A) < depth (v,A)
let A be non-empty finite-yielding MSAlgebra over IIG; ::_thesis: for v, v1 being SortSymbol of IIG st v in InnerVertices IIG & v1 in rng (the_arity_of (action_at v)) holds
depth (v1,A) < depth (v,A)
let v, v1 be SortSymbol of IIG; ::_thesis: ( v in InnerVertices IIG & v1 in rng (the_arity_of (action_at v)) implies depth (v1,A) < depth (v,A) )
assume that
A1: v in InnerVertices IIG and
A2: v1 in rng (the_arity_of (action_at v)) ; ::_thesis: depth (v1,A) < depth (v,A)
 size (v1,A) > 0 by Th15;
then A3: 0 + 1 <= size (v1,A) by NAT_1:13;
 size (v1,A) < size (v,A) by A1, A2, Th14;
then A4: not v in (InputVertices IIG) \/ (SortsWithConstants IIG) by A3, Th10;
then A5: not v in SortsWithConstants IIG by XBOOLE_0:def_3;
then A6: v in (InnerVertices IIG) \ (SortsWithConstants IIG) by A1, XBOOLE_0:def_5;
consider s1 being non empty finite Subset of NAT such that
A7: s1 =  {  (depth t1) where t1 is Element of the Sorts of (FreeEnv A) . v1 : verum  }  and
A8: depth (v1,A) = max s1 by Def6;
reconsider Y1 = s1 as non empty finite real-membered set ;
 max Y1 in  {  (depth t1) where t1 is Element of the Sorts of (FreeEnv A) . v1 : verum  }  by A7, XXREAL_2:def_8;
then consider t1 being Element of the Sorts of (FreeEnv A) . v1 such that
A9: depth t1 = max Y1 ;
reconsider av = action_at v as OperSymbol of IIG ;
consider s being non empty finite Subset of NAT such that
A10: s =  {  (depth t) where t is Element of the Sorts of (FreeEnv A) . v : verum  }  and
A11: depth (v,A) = max s by Def6;
consider x being set  such that
A12: x in dom (the_arity_of av) and
A13: v1 = (the_arity_of av) . x by A2, FUNCT_1:def_3;
reconsider Y = s as non empty finite real-membered set ;
 max Y in  {  (depth t) where t is Element of the Sorts of (FreeEnv A) . v : verum  }  by A10, XXREAL_2:def_8;
then consider t being Element of the Sorts of (FreeEnv A) . v such that
A14: depth t = max Y ;
 FreeEnv A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #) by MSAFREE:def_14;
then  the Sorts of (FreeEnv A) . v = FreeSort ( the Sorts of A,v) by MSAFREE:def_11;
then  t in FreeSort ( the Sorts of A,v) ;
then A15: t 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;
reconsider k = x as Element of NAT by A12;
reconsider k1 = k - 1 as Element of NAT by A12, FINSEQ_3:26;
reconsider f = <*k1*> as FinSequence of NAT ;
A16: k1 + 1 = k ;
reconsider tft = t with-replacement (f,t1) as DecoratedTree ;
consider e9 being Element of the Sorts of (FreeMSA the Sorts of A) . v1 such that
A17: t1 = e9 and
A18: depth t1 = depth e9 by Def5;
consider dt19 being finite DecoratedTree, t19 being finite Tree such that
A19: ( dt19 = e9 & t19 = dom dt19 ) and
A20: depth e9 = height t19 by MSAFREE2:def_14;
consider a being Element of TS (DTConMSA the Sorts of A) such that
A21: a = t and
A22: ( 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 A15;
A23: not v in InputVertices IIG by A4, XBOOLE_0:def_3;
now__::_thesis:_for_x_being_set_holds_
(_not_x_in_the_Sorts_of_A_._v_or_not_a_=_root-tree_[x,v]_)
given x being set  such that  x in the Sorts of A . v and
A24: a = root-tree [x,v] ; ::_thesis: contradiction
consider e9 being Element of the Sorts of (FreeMSA the Sorts of A) . v such that
A25: ( t = e9 & depth t = depth e9 ) by Def5;
 ex dta being finite DecoratedTree ex ta being finite Tree st
( dta = e9 & ta = dom dta & depth e9 = height ta ) by MSAFREE2:def_14;
then  depth t = 0 by A21, A24, A25, TREES_1:42, TREES_4:3;
hence  contradiction by A11, A14, A23, A5, Th18; ::_thesis: verum
end;
then consider o being OperSymbol of IIG such that
A26: [o, the carrier of IIG] = a . {} and
A27: the_result_sort_of o = v by A22;
 ( NonTerminals (DTConMSA the Sorts of A) = [: the carrier' of IIG,{ the carrier of IIG}:] & the carrier of IIG in { the carrier of IIG} ) by MSAFREE:6, TARSKI:def_1;
then reconsider o9 = [o, the carrier of IIG] as NonTerminal of (DTConMSA the Sorts of A) by ZFMISC_1:87;
consider q being FinSequence of TS (DTConMSA the Sorts of A) such that
A28: a = o9 -tree q and
 o9 ==> roots q by A26, DTCONSTR:10;
consider q9 being DTree-yielding FinSequence such that
A29: q = q9 and
A30: dom a = tree (doms q9) by A28, TREES_4:def_4;
A31: t = [av, the carrier of IIG] -tree q9 by A1, A21, A27, A28, A29, MSAFREE2:def_7;
A32: o = av by A1, A27, MSAFREE2:def_7;
then A33: len q9 = len (the_arity_of av) by A21, A27, A28, A29, MSAFREE2:10;
then A34: k in dom q9 by A12, FINSEQ_3:29;
A35: dom q9 = dom (the_arity_of av) by A33, FINSEQ_3:29;
then consider qq being DTree-yielding FinSequence such that
A36: t with-replacement (f,t1) = o9 -tree qq and
A37: len qq = len q9 and
 qq . (k1 + 1) = t1 and
 for i being Element of NAT st i in dom q9 & i <> k1 + 1 holds
qq . i = q9 . i by A21, A28, A29, A30, A12, PRE_CIRC:13, PRE_CIRC:15;
A38: k in dom qq by A12, A33, A37, FINSEQ_3:29;
 q9 . k in the Sorts of (FreeEnv A) . v1 by A21, A27, A28, A29, A12, A13, A32, MSAFREE2:11;
then reconsider tft = tft as Element of the Sorts of (FreeEnv A) . v by A6, A34, A16, A31, Th6;
reconsider dtft = depth tft as Real ;
 dtft in Y by A10;
then A39: dtft <= depth t by A14, XXREAL_2:def_8;
consider e9 being Element of the Sorts of (FreeMSA the Sorts of A) . v such that
A40: tft = e9 and
A41: depth tft = depth e9 by Def5;
consider dttft being finite DecoratedTree, ttft being finite Tree such that
A42: ( dttft = e9 & ttft = dom dttft ) and
A43: depth e9 = height ttft by MSAFREE2:def_14;
 ex qq9 being DTree-yielding FinSequence st
( qq = qq9 & dom tft = tree (doms qq9) ) by A36, TREES_4:def_4;
then reconsider f9 = f as Element of ttft by A16, A40, A42, A38, PRE_CIRC:13;
 <*k1*> in tree (doms q9) by A12, A35, A16, PRE_CIRC:13;
then  dom tft = (dom t) with-replacement (f,(dom t1)) by A21, A30, TREES_2:def_11;
then  ( f9 <> {} & ttft | f = t19 ) by A17, A19, A21, A30, A34, A16, A40, A42, PRE_CIRC:13, TREES_1:33;
hence  depth (v1,A) < depth (v,A) by A11, A14, A8, A9, A18, A20, A39, A41, A43, TREES_1:48, XXREAL_0:2; ::_thesis: verum
end;