circuit1.miz



    begin

    definition

      let S be non void Circuit-like non empty ManySortedSign;

      mode Circuit of S is finite-yielding MSAlgebra over S;

    end

    reserve IIG for Circuit-like non void non empty ManySortedSign;

    definition

      let IIG;

      let SCS be non-empty Circuit of IIG;

      :: CIRCUIT1:def1

      func Set-Constants SCS -> ManySortedSet of ( SortsWithConstants IIG) means

      : Def1: for x be Vertex of IIG st x in ( dom it ) holds (it . x) in ( Constants (SCS,x));

      existence

      proof

        defpred P[ object, object] means ex v be Vertex of IIG st v = $1 & $2 in ( Constants (SCS,v));

        set SW = ( SortsWithConstants IIG);

         A1:

        now

          let i be object;

          

           A2: SW = { v where v be SortSymbol of IIG : v is with_const_op } by MSAFREE2:def 1;

          assume

           A3: i in SW;

          then

          reconsider x = i as Vertex of IIG;

          consider v be Vertex of IIG such that

           A4: v = x and

           A5: v is with_const_op by A3, A2;

          consider o be 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 = y as Element of (the Sorts of SCS . v) by A7;

          reconsider y as object;

          take y;

          ex A be non empty set st A = (the Sorts of SCS . v) & ( Constants (SCS,v)) = { a where a be Element of A : ex o be 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 P[i, y];

        end;

        consider f be ManySortedSet of SW such that

         A9: for i be object st i in SW holds P[i, (f . i)] from PBOOLE:sch 3( A1);

        take f;

        let x be Vertex of IIG;

        assume x in ( dom f);

        then x in SW;

        then P[x, (f . x)] by A9;

        hence thesis;

      end;

      correctness

      proof

        let it1,it2 be ManySortedSet of ( SortsWithConstants IIG);

        assume

         A10: for x be Vertex of IIG st x in ( dom it1) holds (it1 . x) in ( Constants (SCS,x));

        assume

         A11: for x be Vertex of IIG st x in ( dom it2) holds (it2 . x) in ( Constants (SCS,x));

        now

          let i be object;

          

           A12: ( dom the Arity of IIG) = the carrier' of IIG by FUNCT_2:def 1;

          assume

           A13: i in ( SortsWithConstants IIG);

          then

          reconsider v = i as Vertex of IIG;

          

           A14: ex A be non empty set st A = (the Sorts of SCS . v) & ( Constants (SCS,v)) = { a where a be Element of A : ex o be 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 be Element of (the Sorts of SCS . v) such that

           A15: (it2 . v) = a2 and

           A16: ex o be 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 be 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 be Element of (the Sorts of SCS . v) such that

           A20: (it1 . v) = a1 and

           A21: ex o be 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 be 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 be object 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 be object 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;

        end;

        hence it1 = it2 by PBOOLE: 3;

      end;

    end

    theorem :: CIRCUIT1:1

    for IIG holds for SCS be non-empty Circuit of IIG, v be Vertex of IIG, e be 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;

      let SCS be non-empty Circuit of IIG, v be Vertex of IIG, e be Element of (the Sorts of SCS . v);

      assume that

       A1: v in ( SortsWithConstants IIG) and

       A2: e in ( Constants (SCS,v));

      

       A3: ex A be non empty set st A = (the Sorts of SCS . v) & ( Constants (SCS,v)) = { a where a be Element of A : ex o be 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 be Element of (the Sorts of SCS . v) st a = e & ex o be 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 be 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 be Element of (the Sorts of SCS . v) st a = (( Set-Constants SCS) . v) & ex o be 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 be 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 be object 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 be object 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 thesis by A11, A15, A13, A10, TARSKI:def 1;

    end;

    definition

      let IIG;

      let CS be Circuit of IIG;

      mode InputFuncs of CS is ManySortedFunction of (( InputVertices IIG) --> NAT ) qua ManySortedSet of ( InputVertices IIG), (the Sorts of CS | ( InputVertices IIG)) qua ManySortedSet of ( InputVertices IIG);

    end

    theorem :: CIRCUIT1:2

    

     Th2: for IIG holds for SCS be non-empty Circuit of IIG, InpFs be InputFuncs of SCS, n be Nat st IIG is with_input_V holds (( commute InpFs) . n) is InputValues of SCS

    proof

      let IIG;

      let SCS be non-empty Circuit of IIG, InpFs be InputFuncs of SCS, n be Nat;

      reconsider A = ( InputVertices IIG) as Subset of IIG;

      reconsider SS = the Sorts of SCS as non-empty ManySortedSet of the carrier of IIG;

      assume IIG is with_input_V;

      then

      reconsider A as non empty Subset of IIG;

      reconsider SI = (SS | A) as ManySortedSet of A;

      reconsider SI as non-empty ManySortedSet of A;

      reconsider n as Element of NAT by ORDINAL1:def 12;

      consider ivm be ManySortedSet of A such that

       A1: ivm = (( commute InpFs) . n) and

       A2: ivm in SI by PRE_CIRC: 7;

      now

        let v be Vertex of IIG;

        assume

         A3: v in ( InputVertices IIG);

        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;

      end;

      hence thesis by A1, MSAFREE2:def 5;

    end;

    definition

      let IIG;

      let SCS be non-empty Circuit of IIG, InpFs be InputFuncs of SCS, n be Nat;

      :: CIRCUIT1:def2

      func n -th_InputValues InpFs -> InputValues of SCS equals (( commute InpFs) . n);

      coherence by A1, Th2;

      correctness ;

    end

    definition

      let IIG;

      let SCS be Circuit of IIG;

      mode State of SCS is Element of ( product the Sorts of SCS);

    end

    theorem :: CIRCUIT1:3

    for IIG holds for SCS be non-empty Circuit of IIG, s be State of SCS holds ( dom s) = the carrier of IIG by PARTFUN1:def 2;

    theorem :: CIRCUIT1:4

    for IIG holds for SCS be non-empty Circuit of IIG, s be State of SCS, v be Vertex of IIG holds (s . v) in (the Sorts of SCS . v)

    proof

      let IIG;

      let SCS be non-empty Circuit of IIG, s be State of SCS, v be Vertex of IIG;

      ( dom the Sorts of SCS) = the carrier of IIG & ex g be Function st s = g & ( dom g) = ( dom the Sorts of SCS) & for x be object 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 thesis;

    end;

    definition

      let IIG;

      let SCS be non-empty Circuit of IIG, s be State of SCS, o be OperSymbol of IIG;

      :: CIRCUIT1:def3

      func o depends_on_in s -> Element of ( Args (o,SCS)) equals (s * ( the_arity_of o));

      coherence

      proof

        ( Args (o,SCS)) = ( product (the Sorts of SCS * ( the_arity_of o))) by PRALG_2: 3;

        hence thesis by CARD_3: 83;

      end;

      correctness ;

    end

    reserve IIG for monotonic Circuit-like non void non empty ManySortedSign;

    theorem :: CIRCUIT1:5

    

     Th5: for IIG holds for SCS be finite-yielding non-empty MSAlgebra over IIG, v,w be Vertex of IIG, e1 be Element of (the Sorts of ( FreeEnv SCS) . v), q1 be DTree-yielding FinSequence st v in ( InnerVertices IIG) & e1 = ( [( action_at v), the carrier of IIG] -tree q1) holds for k be 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;

      let SCS be finite-yielding non-empty MSAlgebra over IIG, v,w be Vertex of IIG, e1 be Element of (the Sorts of ( FreeEnv SCS) . v), q1 be DTree-yielding FinSequence;

      assume that

       A1: v in ( InnerVertices IIG) and

       A2: e1 = ( [( action_at v), the carrier of IIG] -tree q1);

      thus for k be 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

        reconsider av = ( action_at v) as OperSymbol of IIG;

        let k be Element of NAT ;

        assume that

         A3: k in ( dom q1) and

         A4: (q1 . k) in (the Sorts of ( FreeEnv SCS) . w);

        

         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

          assume (( the_arity_of av) /. k) <> w;

          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;

        end;

        hence thesis;

      end;

    end;

    registration

      let IIG;

      let SCS be finite-yielding non-empty MSAlgebra over IIG, v be Vertex of IIG;

      cluster -> finite non empty Function-like Relation-like for Element of (the Sorts of ( FreeEnv SCS) . v);

      coherence ;

    end

    registration

      let IIG;

      let SCS be finite-yielding non-empty MSAlgebra over IIG, v be Vertex of IIG;

      cluster -> DecoratedTree-like for Element of (the Sorts of ( FreeEnv SCS) . v);

      coherence ;

    end

    theorem :: CIRCUIT1:6

    

     Th6: for IIG holds for SCS be finite-yielding non-empty MSAlgebra over IIG, v,w be Vertex of IIG, e1 be Element of (the Sorts of ( FreeEnv SCS) . v), e2 be Element of (the Sorts of ( FreeEnv SCS) . w), q1 be DTree-yielding FinSequence, k1 be 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;

      let SCS be finite-yielding non-empty MSAlgebra over IIG, v,w be Vertex of IIG, e1 be Element of (the Sorts of ( FreeEnv SCS) . v), e2 be Element of (the Sorts of ( FreeEnv SCS) . w), q1 be DTree-yielding FinSequence, k1 be Element of NAT ;

      set k = (k1 + 1), 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: k in ( dom q1) and

       A4: (q1 . k) in (the Sorts of ( FreeEnv SCS) . w);

      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 be object st x in TSDT holds x is DecoratedTree of O;

      then

      reconsider 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 be 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 be 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 be Nat st i in ( dom q1) holds (i <> (k1 + 1) implies (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 be 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 be Element of ( TS ( DTConMSA the Sorts of SCS)) : (ex x be set st x in (the Sorts of SCS . w) & a9 = ( root-tree [x, w])) or ex o be OperSymbol of IIG st [o, the carrier of IIG] = (a9 . {} ) & ( the_result_sort_of o) = w } by MSAFREE:def 10;

      then

      consider aa be Element of ( TS ( DTConMSA the Sorts of SCS)) such that

       A14: aa = e2 and

       A15: (ex x be set st x in (the Sorts of SCS . w) & aa = ( root-tree [x, w])) or ex o be 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 object;

        assume y in ( rng qq);

        then

        consider x be object such that

         A17: x in ( dom qq) and

         A18: y = (qq . x) by FUNCT_1:def 3;

        reconsider x as Element of NAT by A17;

        per cases ;

          suppose x = (k1 + 1);

          hence thesis by A8, A14, A18;

        end;

          suppose x <> (k1 + 1);

          then (qq . x) = (q19 . x) by A9, A16, A17;

          hence thesis by A16, A17, A18, FINSEQ_2: 11;

        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 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 be set st x in ( dom rq) holds ((rq . x) in [:the carrier' of IIG, {the carrier of IIG}:] implies for o1 be 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 as FinSequence of TSDT;

        let x be set;

        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 as FinSequence;

        assume

         A25: x in ( dom rq);

        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 be 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;

          assume n in ( dom q1);

          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 thesis by A10, MSAFREE:def 11;

        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) /. k) = w by A2, A3, A4, A20, Th5;

        

         A31: ex T be DecoratedTree st T = (qq . x9) & (rq . x9) = (T . {} ) by A19, A25, TREES_3:def 18;

        

         A32: ex T9 be 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 be OperSymbol of IIG st [o1, the carrier of IIG] = (rq . x) holds ( the_result_sort_of o1) = (( the_arity_of av) . x)

        proof

          assume

           A33: (rq . x) in [:the carrier' of IIG, {the carrier of IIG}:];

          let o1 be OperSymbol of IIG;

          assume

           A34: [o1, the carrier of IIG] = (rq . x);

          per cases ;

            suppose

             A35: x9 = (k1 + 1);

            now

              per cases by A15;

                case ex xx be set st xx in (the Sorts of SCS . w) & aa = ( root-tree [xx, w]);

                then

                consider xx be 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 be set holds not X in X;

                hence contradiction by A37;

              end;

                case ex o be OperSymbol of IIG st [o, the carrier of IIG] = (aa . {} ) & ( the_result_sort_of o) = w;

                hence thesis by A8, A14, A26, A31, A30, A34, A35, XTUPLE_0: 1;

              end;

            end;

            hence thesis;

          end;

            suppose x9 <> (k1 + 1);

            then (( roots q1) . x9) = [o1, the carrier of IIG] by A9, A16, A19, A25, A31, A32, A34;

            hence thesis by A16, A19, A25, A29, A33, A34, MSAFREE1: 3;

          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))

        proof

          assume

           A38: (rq . x) in ( Union ( coprod the Sorts of SCS));

          then (rq . x) in ( Terminals ( DTConMSA the Sorts of SCS)) by MSAFREE: 6;

          then

          consider s1 be SortSymbol of IIG, x99 be set such that

           A39: x99 in (the Sorts of SCS . s1) & (rq . x) = [x99, s1] by MSAFREE: 7;

          per cases ;

            suppose

             A40: x9 = (k1 + 1);

            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 be Element of ( TS ( DTConMSA the Sorts of SCS)) : (ex x999 be set st x999 in (the Sorts of SCS . s1) & a99 = ( root-tree [x999, s1])) or ex o be 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

              assume w <> s1;

              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;

            end;

            hence thesis by A26, A30, A39, A40, MSAFREE:def 2;

          end;

            suppose x9 <> (k1 + 1);

            then (rq . x9) = (( roots q1) . x9) by A9, A16, A19, A25, A31, A32;

            hence thesis by A16, A19, A25, A29, A38, MSAFREE1: 3;

          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 as SubtreeSeq of nt by DTCONSTR:def 6;

      eke = (nt -tree q9) by A6;

      then

      reconsider eke9 = eke as Element of ( TS ( DTConMSA the Sorts of SCS));

      q99 in (( dom e1) with-replacement (m9,( dom e2))) by TREES_1: 22;

      then not m9 is_a_prefix_of q99 & (eke . q99) = (e1 . q99) or ex r be FinSequence of NAT st r in ( dom e2) & q99 = (m9 ^ r) & (eke . q99) = (e2 . r) by TREES_2:def 11;

      then

       A44: (eke . {} ) = [av, the carrier of IIG] by A2, TREES_4:def 4;

      now

        take av;

        ( the_result_sort_of av) = v by A20, MSAFREE2:def 7;

        hence ex o be OperSymbol of IIG st [o, the carrier of IIG] = (eke . {} ) & ( the_result_sort_of o) = v by A44;

      end;

      then eke9 in { a99 where a99 be Element of ( TS ( DTConMSA the Sorts of SCS)) : (ex x be set st x in (the Sorts of SCS . v) & a99 = ( root-tree [x, v])) or ex o be OperSymbol of IIG st [o, the carrier of IIG] = (a99 . {} ) & ( the_result_sort_of o) = v };

      then

      reconsider eke9 as Element of (the Sorts of ( FreeEnv SCS) . v) by A11, MSAFREE:def 10;

      eke9 in (the Sorts of ( FreeEnv SCS) . v);

      hence thesis;

    end;

    theorem :: CIRCUIT1:7

    

     Th7: for IIG holds for A be finite-yielding non-empty MSAlgebra over IIG, v be Element of IIG, e be Element of (the Sorts of ( FreeEnv A) . v) st 1 < ( card e) holds ex o be OperSymbol of IIG st (e . {} ) = [o, the carrier of IIG]

    proof

      let IIG;

      let A be finite-yielding non-empty MSAlgebra over IIG, v be Element of IIG, e be Element of (the Sorts of ( FreeEnv A) . v);

      set X = the Sorts of A;

      assume

       A1: 1 < ( card e);

      

       A2: (( FreeSort X) . v) = ( FreeSort (X,v)) & ( FreeSort (X,v)) = { a where a be Element of ( TS ( DTConMSA X)) : (ex x be set st x in (X . v) & a = ( root-tree [x, v])) or ex o be 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 X) . v) & ( FreeMSA X) = MSAlgebra (# ( FreeSort X), ( FreeOper X) #) by MSAFREE:def 14;

      then ex a be Element of ( TS ( DTConMSA X)) st a = e & ((ex x be set st x in (X . v) & a = ( root-tree [x, v])) or ex o be OperSymbol of IIG st [o, the carrier of IIG] = (a . {} ) & ( the_result_sort_of o) = v) by A2;

      hence thesis by A1, PRE_CIRC: 19;

    end;

    theorem :: CIRCUIT1:8

    for IIG be non void Circuit-like non empty ManySortedSign holds for SCS be non-empty Circuit of IIG, s be State of SCS, o be 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 void Circuit-like non empty ManySortedSign;

      let SCS be non-empty Circuit of IIG, s be State of SCS, o be OperSymbol of IIG;

      

       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 thesis by FUNCT_2: 5;

    end;

    theorem :: CIRCUIT1:9

    

     Th9: for IIG holds for A be non-empty Circuit of IIG, v be Vertex of IIG, e be Element of (the Sorts of ( FreeEnv A) . v) st (e . {} ) = [( action_at v), the carrier of IIG] holds ex p be DTree-yielding FinSequence st e = ( [( action_at v), the carrier of IIG] -tree p)

    proof

      let IIG;

      let A be non-empty Circuit of IIG, v be Vertex of IIG, e be Element of (the Sorts of ( FreeEnv A) . v) such that

       A1: (e . {} ) = [( action_at v), the carrier of IIG];

      set X = the Sorts of A;

      ( NonTerminals ( DTConMSA X)) = [: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 X) by ZFMISC_1: 87;

      ( FreeMSA X) = MSAlgebra (# ( FreeSort X), ( FreeOper X) #) & e in (the Sorts of ( FreeEnv A) . v) by MSAFREE:def 14;

      then e in ( FreeSort (X,v)) by MSAFREE:def 11;

      then

      reconsider tsg = e as Element of ( TS ( DTConMSA X));

      consider ts be FinSequence of ( TS ( DTConMSA X)) such that

       A2: tsg = (nt -tree ts) and nt ==> ( roots ts) by A1, DTCONSTR: 10;

      take ts;

      thus thesis by A2;

    end;

    begin

    registration

      let IIG be monotonic non void non empty ManySortedSign;

      let A be finite-yielding non-empty MSAlgebra over IIG;

      let v be SortSymbol of IIG;

      cluster (the Sorts of ( FreeEnv A) . v) -> finite;

      coherence

      proof

        the Sorts of A is finite-yielding 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 finite-yielding;

        hence thesis;

      end;

    end

    defpred P[ set] means not contradiction;

    definition

      let IIG;

      let A be finite-yielding non-empty MSAlgebra over IIG;

      let v be SortSymbol of IIG;

      :: CIRCUIT1:def4

      func size (v,A) -> Nat means

      : Def4: ex s be finite non empty Subset of NAT st s = the set of all ( card t) where t be Element of (the Sorts of ( FreeEnv A) . v) & it = ( max s);

      existence

      proof

        deffunc F( Element of (the Sorts of ( FreeEnv A) . v)) = ( card $1);

        set s = { F(t) where t be Element of (the Sorts of ( FreeEnv A) . v) : P[t] };

        set t = the Element of (the Sorts of ( FreeEnv A) . v);

        

         A1: ( card t) in s;

        

         A2: s is Subset of NAT from DOMAIN_1:sch 8;

        s is finite from PRE_CIRC:sch 1;

        then

        reconsider s as finite non empty Subset of NAT by A1, A2;

        reconsider m = ( max s) as Nat by TARSKI: 1;

        take m, s;

        thus thesis;

      end;

      correctness ;

    end

    theorem :: CIRCUIT1:10

    

     Th10: for IIG holds for A be finite-yielding non-empty MSAlgebra over IIG, v be Element of IIG holds ( size (v,A)) = 1 iff v in (( InputVertices IIG) \/ ( SortsWithConstants IIG))

    proof

      let IIG;

      let A be finite-yielding non-empty MSAlgebra over IIG, v be Element of IIG;

      consider s be finite non empty Subset of NAT such that

       A1: s = the set of all ( card t) where t be Element of (the Sorts of ( FreeEnv A) . v) and

       A2: ( size (v,A)) = ( max s) by Def4;

      reconsider Y = s as finite non empty real-membered set;

      ( max Y) in the set of all ( card t) where t be Element of (the Sorts of ( FreeEnv A) . v) by A1, XXREAL_2:def 8;

      then

      consider e be 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 be Element of ( TS ( DTConMSA the Sorts of A)) : (ex x be set st x in (the Sorts of A . v) & a = ( root-tree [x, v])) or ex o be 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))

      proof

        assume

         A6: ( size (v,A)) = 1;

        now

          assume

           A7: not v in (( InputVertices IIG) \/ ( SortsWithConstants IIG));

          then not v in ( SortsWithConstants IIG) by XBOOLE_0:def 3;

          then not v in { v9 where v9 be 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 be object 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;

          per cases by A8, MSUALG_2:def 1;

            suppose not (the Arity of IIG . o) = {} ;

            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 be 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;

            

             A15: (op . {} ) = o9 by TREES_4:def 4;

            now

              take o;

              ( the_result_sort_of o) = v by A11, MSUALG_1:def 2;

              hence ex o be OperSymbol of IIG st [o, the carrier of IIG] = (op . {} ) & ( the_result_sort_of o) = v by A15;

            end;

            then op in { a9 where a9 be Element of ( TS ( DTConMSA the Sorts of A)) : (ex x9 be set st x9 in (the Sorts of A . v) & a9 = ( root-tree [x9, v])) or ex o be 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 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 be 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 be Nat, T be DecoratedTree, q be 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;

          end;

            suppose not (the ResultSort of IIG . o) = v;

            hence contradiction by A11;

          end;

        end;

        hence thesis;

      end;

      consider a be Element of ( TS ( DTConMSA the Sorts of A)) such that

       A24: a = e and

       A25: (ex x be set st x in (the Sorts of A . v) & a = ( root-tree [x, v])) or ex o be 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));

      per cases by A26, XBOOLE_0:def 3;

        suppose v in ( InputVertices IIG);

        then

        consider x be 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 thesis by A2, A3, A24, A27, CARD_1: 30;

      end;

        suppose v in ( SortsWithConstants IIG);

        then v in { v9 where v9 be SortSymbol of IIG : v9 is with_const_op } by MSAFREE2:def 1;

        then

        consider v9 be SortSymbol of IIG such that

         A28: v9 = v and

         A29: v9 is with_const_op;

        consider o be 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

          per cases by A25;

            suppose ex x be set st x in (the Sorts of A . v) & a = ( root-tree [x, v]);

            then

            consider x be 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 thesis by A2, A3, A24, A32, CARD_1: 30;

          end;

            suppose ex o9 be OperSymbol of IIG st [o9, the carrier of IIG] = (a . {} ) & ( the_result_sort_of o9) = v;

            then

            consider o9 be 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 be 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 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 thesis by A2, A3, A24, CARD_1: 30;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: CIRCUIT1:11

    for IIG holds for SCS be finite-yielding non-empty MSAlgebra over IIG, v,w be Vertex of IIG, e1 be Element of (the Sorts of ( FreeEnv SCS) . v), e2 be Element of (the Sorts of ( FreeEnv SCS) . w), q1 be 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;

      let SCS be finite-yielding non-empty MSAlgebra over IIG, v,w be Vertex of IIG, e1 be Element of (the Sorts of ( FreeEnv SCS) . v), e2 be Element of (the Sorts of ( FreeEnv SCS) . w), q1 be DTree-yielding FinSequence;

      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);

      consider sw be finite non empty Subset of NAT such that

       A5: sw = the set of all ( card t) where t be Element of (the Sorts of ( FreeEnv SCS) . w) and

       A6: ( size (w,SCS)) = ( max sw) by Def4;

      reconsider Y = sw as finite non empty real-membered set;

      reconsider m = ( max Y) as Real;

      m in the set of all ( card t) where t be Element of (the Sorts of ( FreeEnv SCS) . w) by A5, XXREAL_2:def 8;

      then

      consider e3 be 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 be object 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 be 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));

      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 as Element of (the Sorts of ( FreeEnv SCS) . v) by A1, A3, A9, A10, A11, Th6;

      consider sv be finite non empty Subset of NAT such that

       A15: sv = the set of all ( card t) where t be Element of (the Sorts of ( FreeEnv SCS) . v) and

       A16: ( size (v,SCS)) = ( max sv) by Def4;

      reconsider Z = sv as finite non empty real-membered set;

      ( card eke) in Z by A15;

      hence contradiction by A2, A16, A14, XXREAL_2:def 8;

    end;

    theorem :: CIRCUIT1:12

    

     Th12: for IIG holds for A be finite-yielding non-empty MSAlgebra over IIG, v be Vertex of IIG, e be Element of (the Sorts of ( FreeEnv A) . v) st v in (( InnerVertices IIG) \ ( SortsWithConstants IIG)) & ( card e) = ( size (v,A)) holds ex q be DTree-yielding FinSequence st e = ( [( action_at v), the carrier of IIG] -tree q)

    proof

      let IIG;

      let A be finite-yielding non-empty MSAlgebra over IIG, v be Vertex of IIG, e be Element of (the Sorts of ( FreeEnv A) . v);

      assume that

       A1: v in (( InnerVertices IIG) \ ( SortsWithConstants IIG)) and

       A2: ( card e) = ( size (v,A));

      

       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 finite non empty 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 be Element of ( TS ( DTConMSA the Sorts of A)) : (ex x be set st x in (the Sorts of A . v) & a = ( root-tree [x, v])) or ex o be 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 be 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 be Element of ( TS ( DTConMSA the Sorts of A)) such that

       A8: a = e and

       A9: (ex x be set st x in (the Sorts of A . v) & a = ( root-tree [x, v])) or ex o be OperSymbol of IIG st [o, the carrier of IIG] = (a . {} ) & ( the_result_sort_of o) = v by A6;

      consider x be set such that

       A10: x in (the Sorts of A . v) & a = ( root-tree [x, v]) or ex o9 be OperSymbol of IIG st [o9, the carrier of IIG] = (a . {} ) & ( the_result_sort_of o9) = v by A9;

      consider ts be 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;

      

       A12: v in ( InnerVertices IIG) by A1, XBOOLE_0:def 5;

      now

        assume a = ( root-tree [x, v]);

        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 be set holds not X in X;

        hence contradiction by A13;

      end;

      then

      consider o9 be 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 thesis by A8, A11;

    end;

    theorem :: CIRCUIT1:13

    for IIG holds for A be finite-yielding non-empty MSAlgebra over IIG, v be Vertex of IIG, e be Element of (the Sorts of ( FreeEnv A) . v) st v in (( InnerVertices IIG) \ ( SortsWithConstants IIG)) & ( card e) = ( size (v,A)) holds ex o be OperSymbol of IIG st (e . {} ) = [o, the carrier of IIG]

    proof

      let IIG;

      let A be finite-yielding non-empty MSAlgebra over IIG, v be Vertex of IIG, e be Element of (the Sorts of ( FreeEnv A) . v);

      assume v in (( InnerVertices IIG) \ ( SortsWithConstants IIG)) & ( card e) = ( size (v,A));

      then

       A1: ex q be DTree-yielding FinSequence st e = ( [( action_at v), the carrier of IIG] -tree q) by Th12;

      take ( action_at v);

      thus thesis by A1, TREES_4:def 4;

    end;

    definition

      let S be non void non empty ManySortedSign, A be finite-yielding non-empty MSAlgebra over S, v be SortSymbol of S, e be Element of (the Sorts of ( FreeEnv A) . v);

      :: CIRCUIT1:def5

      func depth e -> Element of NAT means

      : Def5: ex e9 be Element of (the Sorts of ( FreeMSA the Sorts of A) . v) st e = e9 & it = ( depth e9);

      existence

      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, e9;

        thus thesis;

      end;

      correctness ;

    end

    theorem :: CIRCUIT1:14

    

     Th14: for IIG holds for A be finite-yielding non-empty MSAlgebra over IIG, v,w be 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;

      let A be finite-yielding non-empty MSAlgebra over IIG, v,w be Element of IIG;

      assume that

       A1: v in ( InnerVertices IIG) and

       A2: w in ( rng ( the_arity_of ( action_at v)));

      reconsider av = ( action_at v) as OperSymbol of IIG;

      consider x be object 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 be finite non empty Subset of NAT such that

       A6: sv = the set of all ( card tv) where tv be Element of (the Sorts of ( FreeEnv A) . v) and

       A7: ( size (v,A)) = ( max sv) by Def4;

      reconsider Yv = sv as finite non empty real-membered set;

      ( max Yv) in Yv by XXREAL_2:def 8;

      then

      consider tv be Element of (the Sorts of ( FreeEnv A) . v) such that

       A8: ( card tv) = ( max Yv) by A6;

      now

        assume v in ( SortsWithConstants IIG);

        then v in { v9 where v9 be SortSymbol of IIG : v9 is with_const_op } by MSAFREE2:def 1;

        then

        consider v9 be SortSymbol of IIG such that

         A9: v9 = v and

         A10: v9 is with_const_op;

        consider oo be 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;

      end;

      then

       A14: v in (( InnerVertices IIG) \ ( SortsWithConstants IIG)) by A1, XBOOLE_0:def 5;

      then

      consider p be 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 be finite non empty Subset of NAT such that

       A18: sw = the set of all ( card tw) where tw be Element of (the Sorts of ( FreeEnv A) . w) and

       A19: ( size (w,A)) = ( max sw) by Def4;

      reconsider Yw = sw as finite non empty real-membered set;

      ( max Yw) in Yw by XXREAL_2:def 8;

      then

      consider tw be 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 be DTree-yielding FinSequence st p9 = p & ( dom e1) = ( tree ( doms p9)) by A15, TREES_4:def 4;

      then

      reconsider o as Element of ( dom e1) by A17, A5, PRE_CIRC: 13;

      reconsider eoe = (e1 with-replacement (o,e2)) as finite Function;

      reconsider 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 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 thesis by A19, A20, A22, XXREAL_0: 2;

    end;

    theorem :: CIRCUIT1:15

    

     Th15: for IIG holds for A be finite-yielding non-empty MSAlgebra over IIG, v be SortSymbol of IIG holds ( size (v,A)) > 0

    proof

      let IIG;

      let A be finite-yielding non-empty MSAlgebra over IIG, v be SortSymbol of IIG;

      consider s be finite non empty Subset of NAT such that

       A1: s = the set of all ( card t) where t be Element of (the Sorts of ( FreeEnv A) . v) and

       A2: ( size (v,A)) = ( max s) by Def4;

      reconsider Y = s as finite non empty real-membered set;

      ( max Y) in the set of all ( card t) where t be Element of (the Sorts of ( FreeEnv A) . v) by A1, XXREAL_2:def 8;

      then ex t be Element of (the Sorts of ( FreeEnv A) . v) st ( card t) = ( max Y);

      hence thesis by A2;

    end;

    theorem :: CIRCUIT1:16

    for IIG holds for A be non-empty Circuit of IIG, v be Vertex of IIG, e be Element of (the Sorts of ( FreeEnv A) . v), p be DTree-yielding FinSequence st v in ( InnerVertices IIG) & e = ( [( action_at v), the carrier of IIG] -tree p) & for k be Element of NAT st k in ( dom p) holds ex ek be 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;

      let A be non-empty Circuit of IIG, v be Vertex of IIG, e be Element of (the Sorts of ( FreeEnv A) . v), p be DTree-yielding FinSequence such that

       A1: v in ( InnerVertices IIG) and

       A2: e = ( [( action_at v), the carrier of IIG] -tree p) and

       A3: for k be Element of NAT st k in ( dom p) holds ex ek be 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));

      consider s be finite non empty Subset of NAT such that

       A4: s = the set of all ( card t) where t be Element of (the Sorts of ( FreeEnv A) . v) and

       A5: ( size (v,A)) = ( max s) by Def4;

      reconsider S = s as finite non empty real-membered set;

       A6:

      now

        reconsider e9 = e as finite set;

        let r be ExtReal;

        

         A7: 1 <= ( card e9) by NAT_1: 14;

        assume r in S;

        then

        consider t be 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 be Element of ( TS ( DTConMSA the Sorts of A)) : (ex x be set st x in (the Sorts of A . v) & a9 = ( root-tree [x, v])) or ex o be OperSymbol of IIG st [o, the carrier of IIG] = (a9 . {} ) & ( the_result_sort_of o) = v } by MSAFREE:def 10;

        then

        consider a9 be Element of ( TS ( DTConMSA the Sorts of A)) such that

         A9: a9 = t and

         A10: (ex x be set st x in (the Sorts of A . v) & a9 = ( root-tree [x, v])) or ex o be OperSymbol of IIG st [o, the carrier of IIG] = (a9 . {} ) & ( the_result_sort_of o) = v;

        per cases by A10;

          suppose ex x be set st x in (the Sorts of A . v) & a9 = ( root-tree [x, v]);

          then

          consider x be 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;

        end;

          suppose ex o be OperSymbol of IIG st [o, the carrier of IIG] = (a9 . {} ) & ( the_result_sort_of o) = v;

          then (a9 . {} ) = [( action_at v), the carrier of IIG] by A1, MSAFREE2:def 7;

          then

          consider q be DTree-yielding FinSequence such that

           A12: t = ( [( action_at v), the carrier of IIG] -tree q) by A9, Th9;

          deffunc F( Nat) = (p +* (q | ( Seg $1)));

          consider T be FinSequence such that

           A13: ( len T) = ( len p) and

           A14: for k be Nat st k in ( dom T) holds (T . k) = F(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

            per cases ;

              suppose ( len q) = 0 ;

              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;

            end;

              suppose

               A18: ( len q) <> 0 ;

              defpred P[ Nat] means $1 in ( dom p) implies for qk be DTree-yielding FinSequence st qk = (T . $1) holds for tk be 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

                let k be Nat;

                assume

                 A25: P[k];

                thus P[(k + 1)]

                proof

                  reconsider tree0 = ( [( action_at v), the carrier of IIG] -tree p) as finite DecoratedTree by A2;

                  assume

                   A26: (k + 1) in ( dom p);

                  let qk1 be DTree-yielding FinSequence such that

                   A27: qk1 = (T . (k + 1));

                  let tk1 be finite set;

                  assume

                   A28: tk1 = ( [( action_at v), the carrier of IIG] -tree qk1);

                  then

                  reconsider treek1 = tk1 as finite DecoratedTree;

                  per cases ;

                    suppose

                     A29: k = 0 ;

                    set v1 = (( the_arity_of ( action_at v)) /. 1);

                    

                     A30: 1 in ( dom p) by A21, FINSEQ_3: 25;

                    then

                    consider e1 be Element of (the Sorts of ( FreeEnv A) . v1) such that

                     A31: e1 = (p . 1) and

                     A32: ( card e1) = ( size (v1,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) . v1) 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 be 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 be 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

                      let k be Nat;

                      assume 1 <= k & k <= ( len q0);

                      then

                       A42: k in ( dom p) by A36, FINSEQ_3: 25;

                      per cases ;

                        suppose k = 1;

                        hence (q0 . k) = (qk1 . k) by A40, A37;

                      end;

                        suppose

                         A43: k <> 1;

                        

                         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;

                      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 be finite non empty Subset of NAT such that

                     A47: s1 = the set of all ( card t1) where t1 be Element of (the Sorts of ( FreeEnv A) . v1) and

                     A48: ( card e1) = ( max s1) by A32, Def4;

                    reconsider S1 = s1 as finite non empty 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 thesis by A2, A49, A46, XREAL_1: 8;

                  end;

                    suppose

                     A50: k <> 0 ;

                    

                     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) . v1) 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 as FinSequence by FINSEQ_1:def 2;

                    

                     A59: for x be set st x in ( dom qk) holds (qk . x) is finite DecoratedTree

                    proof

                      let x be set;

                      assume

                       A60: x in ( dom qk);

                      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

                        per cases ;

                          suppose

                           A61: n <= k;

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

                        end;

                          suppose

                           A64: n > k;

                          

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

                        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) . v1) by A23, A58, A60, PARTFUN1:def 6;

                      T1 in (the Sorts of ( FreeEnv A) . v1);

                      hence thesis;

                    end;

                    then for x be object st x in ( dom qk) holds (qk . x) is DecoratedTree;

                    then

                    reconsider 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

                      let x be object;

                      assume x in ( dom ( doms qk));

                      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;

                    end;

                    then

                    reconsider qkf = ( doms qk) as FinTree-yielding FinSequence by TREES_3: 23;

                    ( tree qkf) is finite & ex q be 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 be Element of (the Sorts of ( FreeEnv A) . v1) such that

                     A70: e1 = (p . (k + 1)) and

                     A71: ( card e1) = ( size (v1,A)) by A3, A26;

                    T1 in (the Sorts of ( FreeEnv A) . v1);

                    then

                    reconsider Tx = (qk . (k + 1)) as finite DecoratedTree by A68;

                    v1 = (( 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) . v1) by A12, A16, A54, MSAFREE2: 11;

                    

                     A72: k in NAT by ORDINAL1:def 12;

                    

                     A73: {} 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 be DTree-yielding FinSequence such that

                     A74: (tk with-replacement ( <*k*>,T1)) = ( [( action_at v), the carrier of IIG] -tree q0) and

                     A75: ( len q0) = ( len qk) and

                     A76: (q0 . (k + 1)) = T1 and

                     A77: for i be Nat st i in ( dom qk) & i <> (k + 1) holds (q0 . i) = (qk . i) by PRE_CIRC: 15, A72;

                    

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

                     A79:

                    now

                      let n be Nat;

                      assume that

                       A80: 1 <= n and

                       A81: n <= ( len q0);

                      

                       A82: n in ( dom qk) by A75, A80, A81, FINSEQ_3: 25;

                      per cases by XXREAL_0: 1;

                        suppose n = (k + 1);

                        hence (q0 . n) = (qk1 . n) by A78, A76;

                      end;

                        suppose

                         A83: n > (k + 1);

                        (k + 1) >= k by NAT_1: 11;

                        then n > k by A83, XXREAL_0: 2;

                        then

                         A84: not n in ( Seg k) by FINSEQ_1: 1;

                        ( dom (q | ( Seg k))) = (( dom q) /\ ( Seg k)) by RELAT_1: 61;

                        then

                         A85: not n in ( dom (q | ( Seg k))) by A84, XBOOLE_0:def 4;

                        

                         A86: ( dom (q | ( Seg (k + 1)))) = (( dom q) /\ ( Seg (k + 1))) by RELAT_1: 61;

                         not n in ( Seg (k + 1)) by A83, FINSEQ_1: 1;

                        then

                         A87: not n in ( dom (q | ( Seg (k + 1)))) by A86, XBOOLE_0:def 4;

                        

                        thus (qk1 . n) = ((p +* (q | ( Seg (k + 1)))) . n) by A14, A15, A26, A27

                        .= (p . n) by A87, FUNCT_4: 11

                        .= ((p +* (q | ( Seg k))) . n) by A85, FUNCT_4: 11

                        .= (qk . n) by A14, A15, A57

                        .= (q0 . n) by A77, A82, A83;

                      end;

                        suppose

                         A88: n < (k + 1);

                        

                         A89: n in ( dom q) by A20, A67, A75, A80, A81, FINSEQ_3: 25;

                        n <= k by A88, NAT_1: 13;

                        then

                         A90: n in ( Seg k) by A80, FINSEQ_1: 1;

                        ( dom (q | ( Seg k))) = (( dom q) /\ ( Seg k)) by RELAT_1: 61;

                        then

                         A91: n in ( dom (q | ( Seg k))) by A89, A90, XBOOLE_0:def 4;

                        

                         A92: ( dom (q | ( Seg (k + 1)))) = (( dom q) /\ ( Seg (k + 1))) by RELAT_1: 61;

                        n in ( Seg (k + 1)) by A80, A88, FINSEQ_1: 1;

                        then

                         A93: n in ( dom (q | ( Seg (k + 1)))) by A89, A92, XBOOLE_0:def 4;

                        

                        thus (qk1 . n) = ((p +* (q | ( Seg (k + 1)))) . n) by A14, A15, A26, A27

                        .= ((q | ( Seg (k + 1))) . n) by A93, FUNCT_4: 13

                        .= (q . n) by A93, FUNCT_1: 47

                        .= ((q | ( Seg k)) . n) by A91, FUNCT_1: 47

                        .= ((p +* (q | ( Seg k))) . n) by A91, FUNCT_4: 13

                        .= (qk . n) by A14, A15, A57

                        .= (q0 . n) by A77, A82, A88;

                      end;

                    end;

                    k < ( len qk) by A52, A58, FINSEQ_3: 29;

                    then

                    reconsider w0 = <*k*> as Element of ( dom tk) by A73, 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, A74, A75, A79, FINSEQ_1: 14;

                    then

                     A94: (( card treek1) + ( card (tk | w0))) = (( card tk) + ( card T1)) by PRE_CIRC: 18;

                    consider s1 be finite non empty Subset of NAT such that

                     A95: s1 = the set of all ( card t1) where t1 be Element of (the Sorts of ( FreeEnv A) . v1) and

                     A96: ( card e1) = ( max s1) by A71, Def4;

                    reconsider S1 = s1 as finite non empty real-membered set;

                    ( card T1) in S1 by A95;

                    then

                     A97: ( card T1) <= ( card e1) by A96, XXREAL_2:def 8;

                    (tk | w0) = e1 by A52, A70, A68, A67, TREES_4:def 4;

                    then

                     A98: ( card tk1) <= ( card tk) by A97, A94, XREAL_1: 8;

                    ( card tk) <= ( card e) by A25, A56, A52, FINSEQ_3: 25;

                    hence thesis by A98, XXREAL_0: 2;

                  end;

                end;

              end;

              

               A99: P[ 0 ] by FINSEQ_3: 25;

              

               A100: for k be Nat holds P[k] from NAT_1:sch 2( A99, A24);

              ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3;

              then

               A101: ( dom p) = ( dom q) by A20, FINSEQ_1:def 3;

              

               A102: ( 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 A101

              .= q by A22, FUNCT_4: 19;

              hence r <= ( card e) by A8, A12, A100, A102;

            end;

          end;

          hence r <= ( card e);

        end;

      end;

      ( card e) in S by A4;

      hence thesis by A5, A6, XXREAL_2:def 8;

    end;

    begin

    definition

      let S be monotonic non void non empty ManySortedSign, A be finite-yielding non-empty MSAlgebra over S, v be SortSymbol of S;

      :: CIRCUIT1:def6

      func depth (v,A) -> Nat means

      : Def6: ex s be finite non empty Subset of NAT st s = the set of all ( depth t) where t be Element of (the Sorts of ( FreeEnv A) . v) & it = ( max s);

      existence

      proof

        deffunc F( Element of (the Sorts of ( FreeEnv A) . v)) = ( depth $1);

        set s = { F(t) where t be Element of (the Sorts of ( FreeEnv A) . v) : P[t] };

        set t = the Element of (the Sorts of ( FreeEnv A) . v);

        

         A1: ( depth t) in s;

        

         A2: s is Subset of NAT from DOMAIN_1:sch 8;

        s is finite from PRE_CIRC:sch 1;

        then

        reconsider s as finite non empty Subset of NAT by A1, A2;

        reconsider m = ( max s) as Nat by TARSKI: 1;

        take m, s;

        thus thesis;

      end;

      correctness ;

    end

    definition

      let IIG be finite monotonic Circuit-like non void non empty ManySortedSign, A be non-empty Circuit of IIG;

      :: CIRCUIT1:def7

      func depth A -> Nat means

      : Def7: ex Ds be finite non empty Subset of NAT st Ds = { ( depth (v,A)) where v be Element of IIG : v in the carrier of IIG } & it = ( max Ds);

      existence

      proof

        deffunc F( Element of IIG) = ( depth ($1,A));

        set Ds = { F(v) where v be Element of IIG : v in the carrier of IIG };

        

         A1: Ds is natural-membered

        proof

          let e be object;

          assume e in Ds;

          then ex v be Element of IIG st e = ( depth (v,A)) & v in the carrier of IIG;

          hence thesis;

        end;

        set v = the Element of IIG;

        

         A2: ( depth (v,A)) in Ds;

        

         A3: the carrier of IIG is finite;

        Ds is finite from FRAENKEL:sch 21( A3);

        then

        reconsider Ds as finite non empty Subset of NAT by A1, A2, MEMBERED: 6;

        reconsider m = ( max Ds) as Nat by TARSKI: 1;

        take m, Ds;

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: CIRCUIT1:17

    for IIG be finite monotonic Circuit-like non void non empty ManySortedSign, A be non-empty Circuit of IIG, v be Vertex of IIG holds ( depth (v,A)) <= ( depth A)

    proof

      let IIG be finite monotonic Circuit-like non void non empty ManySortedSign, A be non-empty Circuit of IIG, v be Vertex of IIG;

      consider Ds be finite non empty Subset of NAT such that

       A1: Ds = { ( depth (v9,A)) where v9 be Element of IIG : v9 in the carrier of IIG } and

       A2: ( depth A) = ( max Ds) by Def7;

      reconsider Y = Ds as finite non empty real-membered set;

      ( depth (v,A)) in Y by A1;

      hence thesis by A2, XXREAL_2:def 8;

    end;

    theorem :: CIRCUIT1:18

    

     Th18: for IIG holds for A be non-empty Circuit of IIG, v be Vertex of IIG holds ( depth (v,A)) = 0 iff v in ( InputVertices IIG) or v in ( SortsWithConstants IIG)

    proof

      let IIG;

      let A be non-empty Circuit of IIG, v be Vertex of IIG;

      consider s be finite non empty Subset of NAT such that

       A1: s = the set of all ( depth t) where t be Element of (the Sorts of ( FreeEnv A) . v) and

       A2: ( depth (v,A)) = ( max s) by Def6;

      reconsider Y = s as finite non empty real-membered set;

      

       A3: ( max Y) in the set of all ( depth t) where t be Element of (the Sorts of ( FreeEnv A) . v) by A1, XXREAL_2:def 8;

      consider ss be finite non empty Subset of NAT such that

       A4: ss = the set of all ( card tt) where tt be Element of (the Sorts of ( FreeEnv A) . v) and

       A5: ( size (v,A)) = ( max ss) by Def4;

      reconsider YY = ss as finite non empty real-membered set;

      consider t be Element of (the Sorts of ( FreeEnv A) . v) such that

       A6: ( depth t) = ( max Y) by A3;

      reconsider t99 = t as Function;

      consider t2 be 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 be finite DecoratedTree, t9 be finite Tree such that

       A9: dt = t2 & t9 = ( dom dt) and

       A10: ( depth t2) = ( height t9) by MSAFREE2:def 14;

      consider p be FinSequence of NAT such that

       A11: p in t9 and

       A12: ( len p) = ( height t9) by TREES_1:def 12;

      consider y99 be object such that

       A13: [p, y99] in t99 by A7, A9, A11, XTUPLE_0:def 12;

      thus ( depth (v,A)) = 0 implies v in ( InputVertices IIG) or v in ( SortsWithConstants IIG)

      proof

        assume

         A14: ( depth (v,A)) = 0 ;

        

         A15: for kk be ExtReal st kk in YY holds kk <= 1

        proof

          let kk be ExtReal;

          assume kk in YY;

          then

          consider tt be Element of (the Sorts of ( FreeEnv A) . v) such that

           A16: ( card tt) = kk by A4;

          consider tiv be 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 be finite DecoratedTree, t999 be 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, RELAT_1: 189, TREES_1: 29, TREES_1: 43;

          hence thesis by A16, CARD_1: 30;

        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, RELAT_1: 189, 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 thesis by XBOOLE_0:def 3;

      end;

      reconsider ct = ( card t) as Real;

       {} in ( dom t) by TREES_1: 22;

      then

      consider y be object 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);

      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 be object 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 thesis by A2, A6, A8, A10, A12;

    end;

    theorem :: CIRCUIT1:19

    for IIG holds for A be finite-yielding non-empty MSAlgebra over IIG, v,v1 be 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;

      let A be finite-yielding non-empty MSAlgebra over IIG, v,v1 be SortSymbol of IIG;

      assume that

       A1: v in ( InnerVertices IIG) and

       A2: v1 in ( rng ( the_arity_of ( action_at v)));

      ( 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 be finite non empty Subset of NAT such that

       A7: s1 = the set of all ( depth t1) where t1 be Element of (the Sorts of ( FreeEnv A) . v1) and

       A8: ( depth (v1,A)) = ( max s1) by Def6;

      reconsider Y1 = s1 as finite non empty real-membered set;

      ( max Y1) in the set of all ( depth t1) where t1 be Element of (the Sorts of ( FreeEnv A) . v1) by A7, XXREAL_2:def 8;

      then

      consider t1 be 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 be finite non empty Subset of NAT such that

       A10: s = the set of all ( depth t) where t be Element of (the Sorts of ( FreeEnv A) . v) and

       A11: ( depth (v,A)) = ( max s) by Def6;

      consider x be object 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 finite non empty real-membered set;

      ( max Y) in the set of all ( depth t) where t be Element of (the Sorts of ( FreeEnv A) . v) by A10, XXREAL_2:def 8;

      then

      consider t be 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 be Element of ( TS ( DTConMSA the Sorts of A)) : (ex x be set st x in (the Sorts of A . v) & a = ( root-tree [x, v])) or ex o be 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 be 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 be finite DecoratedTree, t19 be finite Tree such that

       A19: dt19 = e9 & t19 = ( dom dt19) and

       A20: ( depth e9) = ( height t19) by MSAFREE2:def 14;

      consider a be Element of ( TS ( DTConMSA the Sorts of A)) such that

       A21: a = t and

       A22: (ex x be set st x in (the Sorts of A . v) & a = ( root-tree [x, v])) or ex o be 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

        given x be set such that x in (the Sorts of A . v) and

         A24: a = ( root-tree [x, v]);

        consider e9 be Element of (the Sorts of ( FreeMSA the Sorts of A) . v) such that

         A25: t = e9 & ( depth t) = ( depth e9) by Def5;

        ex dta be finite DecoratedTree, ta be 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;

      end;

      then

      consider o be 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 be 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 be 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 be 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 be 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 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 be 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 be finite DecoratedTree, ttft be finite Tree such that

       A42: dttft = e9 & ttft = ( dom dttft) and

       A43: ( depth e9) = ( height ttft) by MSAFREE2:def 14;

      ex qq9 be 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 thesis by A11, A14, A8, A9, A18, A20, A39, A41, A43, TREES_1: 48, XXREAL_0: 2;

    end;