circuit2.miz



    begin

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

    

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

    theorem :: CIRCUIT2:1

    

     Th1: for X be non-empty ManySortedSet of the carrier of IIG, H be ManySortedFunction of ( FreeMSA X), ( FreeMSA X), HH be Function-yielding Function, v be SortSymbol of IIG, p be DTree-yielding FinSequence, t be Element of (the Sorts of ( FreeMSA X) . v) st v in ( InnerVertices IIG) & t = ( [( action_at v), the carrier of IIG] -tree p) & H is_homomorphism (( FreeMSA X),( FreeMSA X)) & HH = (H * ( the_arity_of ( action_at v))) holds ex HHp be DTree-yielding FinSequence st HHp = (HH .. p) & ((H . v) . t) = ( [( action_at v), the carrier of IIG] -tree HHp)

    proof

      let X be non-empty ManySortedSet of the carrier of IIG, H be ManySortedFunction of ( FreeMSA X), ( FreeMSA X), HH be Function-yielding Function, v be SortSymbol of IIG, p be DTree-yielding FinSequence, t be Element of (the Sorts of ( FreeMSA X) . v) such that

       A1: v in ( InnerVertices IIG) and

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

       A3: H is_homomorphism (( FreeMSA X),( FreeMSA X)) and

       A4: HH = (H * ( the_arity_of ( action_at v)));

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

      

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

      then ( len p) = ( len ( the_arity_of av)) by A2, MSAFREE2: 10;

      then

       A6: ( dom p) = ( dom ( the_arity_of av)) by FINSEQ_3: 29;

      

       A7: ( rng ( the_arity_of av)) c= the carrier of IIG by FINSEQ_1:def 4;

      then

       A8: ( rng ( the_arity_of av)) c= ( dom H) by PARTFUN1:def 2;

      then

       A9: ( dom ( the_arity_of av)) = ( dom HH) by A4, RELAT_1: 27;

      

       A10: ( FreeMSA X) = MSAlgebra (# ( FreeSort X), ( FreeOper X) #) by MSAFREE:def 14;

      then (the Sorts of ( FreeMSA X) . v) = ( FreeSort (X,v)) by MSAFREE:def 11;

      then ( [av, the carrier of IIG] -tree p) in ( FreeSort (X,v)) by A2;

      then

       A11: ( [av, the carrier of IIG] -tree p) in { a where a 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;

      reconsider HHp = (HH .. p) as Function;

      

       A12: ( dom HHp) = (( dom HH) /\ ( dom p)) by PRALG_1:def 19

      .= ( dom HH) by A6, A9;

      (H * ( the_arity_of av)) is FinSequence by A8, FINSEQ_1: 16;

      then ex n be Nat st ( dom HH) = ( Seg n) by A4, FINSEQ_1:def 2;

      then

      reconsider HHp as FinSequence by A12, FINSEQ_1:def 2;

       A13:

      now

        reconsider HH9 = HH as FinSequence by A4, A8, FINSEQ_1: 16;

        let x9 be object;

        set x = (HHp . x9);

        reconsider g = (HH . x9) as Function;

        assume

         A14: x9 in ( dom HHp);

        then

        reconsider k = x9 as Element of NAT ;

        

         A15: x = (g . (p . k)) by A14, PRALG_1:def 19;

        ( len HH9) = ( len ( the_arity_of av)) by A4, A8, FINSEQ_2: 29;

        then

         A16: ( dom HH9) = ( dom ( the_arity_of av)) by FINSEQ_3: 29;

        then

        reconsider s = (( the_arity_of av) . k) as SortSymbol of IIG by A12, A14, FINSEQ_2: 11;

        g = (H . s) by A4, A12, A14, A16, FUNCT_1: 13;

        then x in (the Sorts of ( FreeMSA X) . s) by A2, A12, A5, A14, A16, A15, FUNCT_2: 5, MSAFREE2: 11;

        hence x is DecoratedTree;

      end;

      set f = (the Sorts of ( FreeMSA X) * ( the_arity_of av));

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

      

      then

       A17: (((the Sorts of ( FreeMSA X) # ) * the Arity of IIG) . av) = ((the Sorts of ( FreeMSA X) # ) . (the Arity of IIG . av)) by FUNCT_1: 13

      .= ((the Sorts of ( FreeMSA X) # ) . ( the_arity_of av)) by MSUALG_1:def 1

      .= ( product (the Sorts of ( FreeMSA X) * ( the_arity_of av))) by FINSEQ_2:def 5;

      reconsider HHp as DTree-yielding FinSequence by A13, TREES_3: 24;

      consider a be Element of ( TS ( DTConMSA X)) such that

       A18: a = ( [av, the carrier of IIG] -tree p) and

       A19: (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 A11;

      consider x9 be set such that

       A20: x9 in (X . v) & a = ( root-tree [x9, v]) or ex o be OperSymbol of IIG st [o, the carrier of IIG] = (a . {} ) & ( the_result_sort_of o) = v by A19;

      ( dom the Sorts of ( FreeMSA X)) = the carrier of IIG by PARTFUN1:def 2;

      then

       A21: ( dom f) = ( dom ( the_arity_of av)) by A7, RELAT_1: 27;

      now

        let x be object;

        assume

         A22: x in ( dom f);

        then

        reconsider n = x as Element of NAT by A21;

        (( the_arity_of av) . x) in ( rng ( the_arity_of av)) by A21, A22, FUNCT_1:def 3;

        then

        reconsider s = (( the_arity_of av) . x) as SortSymbol of IIG by A7;

        n in ( dom ( the_arity_of av)) & ((the Sorts of ( FreeMSA X) * ( the_arity_of av)) . x) = (the Sorts of ( FreeMSA X) . s) by A21, A22, FUNCT_1: 13;

        hence (p . x) in (f . x) by A2, A5, MSAFREE2: 11;

      end;

      then p in (((the Sorts of ( FreeMSA X) # ) * the Arity of IIG) . av) by A17, A21, A6, CARD_3:def 5;

      then

      reconsider x = p as Element of ( Args (av,( FreeMSA X))) by MSUALG_1:def 4;

      

       A23: (a . {} ) = [av, the carrier of IIG] by A18, TREES_4:def 4;

      reconsider Hx = (H # x) as Function;

       A24:

      now

        let x9 be set;

        assume

         A25: x9 in ( dom HH);

        then

        reconsider n = x9 as Element of NAT by A9;

        (( the_arity_of av) . n) in ( rng ( the_arity_of av)) by A9, A25, FUNCT_1:def 3;

        then

        reconsider s = (( the_arity_of av) . n) as SortSymbol of IIG by A7;

        (Hx . n) = ((H . (( the_arity_of av) /. n)) . (p . n)) by A9, A6, A25, MSUALG_3:def 6

        .= ((H . s) . (p . n)) by A9, A25, PARTFUN1:def 6;

        hence (Hx . x9) = ((HH . x9) . (p . x9)) by A4, A9, A25, FUNCT_1: 13;

      end;

      

       AA: ( dom Hx) = ( dom HH) by A9, MSUALG_3: 6

      .= (( dom HH) /\ ( dom p)) by A12, PRALG_1:def 19;

      then

       A26: HHp = Hx by PRALG_1:def 19, AA, A24, A6, A9;

      now

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

        then

         A27: (a . {} ) = [x9, v] by TREES_4: 3;

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

        then the carrier of IIG = v by A27, XTUPLE_0: 1;

        hence contradiction by Lm1;

      end;

      then

      consider o be OperSymbol of IIG such that

       A28: [o, the carrier of IIG] = (a . {} ) and ( the_result_sort_of o) = v by A20;

      the carrier of IIG in {the carrier of IIG} by TARSKI:def 1;

      then [o, the carrier of IIG] in [:the carrier' of IIG, {the carrier of IIG}:] by ZFMISC_1: 87;

      then

      reconsider nt = [o, the carrier of IIG] as NonTerminal of ( DTConMSA X) by MSAFREE: 6;

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

       A29: a = (nt -tree ts) and

       A30: nt ==> ( roots ts) by A28, DTCONSTR: 10;

      take HHp;

      thus HHp = (HH .. p);

      

       A31: ( Sym (av,X)) = [av, the carrier of IIG] by MSAFREE:def 9;

      now

        let x be object;

        reconsider g = (HH . x) as Function;

        assume

         A32: x in ( dom f);

        then

         aa: x in ( dom (the Sorts of ( FreeMSA X) * ( the_arity_of av)));

        ( dom (the Sorts of ( FreeMSA X) * ( the_arity_of av))) c= ( dom ( the_arity_of av)) by RELAT_1: 25;

        then

         A33: (HHp . x) = (g . (p . x)) by A32, A9, A12, PRALG_1:def 19;

        (( the_arity_of av) . x) in ( rng ( the_arity_of av)) by A21, A32, FUNCT_1:def 3;

        then

        reconsider s = (( the_arity_of av) . x) as SortSymbol of IIG by A7;

        

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

        ((the Sorts of ( FreeMSA X) * ( the_arity_of av)) . x) = (the Sorts of ( FreeMSA X) . s) & g = (H . s) by A4, A21, A32, FUNCT_1: 13;

        hence (HHp . x) in (f . x) by A2, A21, A32, A34, A33, FUNCT_2: 5, MSAFREE2: 11;

      end;

      then

       A35: HHp in (((( FreeSort X) # ) * the Arity of IIG) . av) by A12, A17, A21, A9, A10, CARD_3:def 5;

      then

      reconsider HHp9 = HHp as FinSequence of ( TS ( DTConMSA X)) by MSAFREE: 8;

      

       A36: ( Sym (av,X)) ==> ( roots HHp9) by A35, MSAFREE: 10;

      reconsider p9 = p as FinSequence of ( TS ( DTConMSA X)) by A18, A29, TREES_4: 15;

      ts = p by A18, A29, TREES_4: 15;

      then

       A37: (( DenOp (av,X)) . p9) = t by A2, A28, A23, A30, A31, MSAFREE:def 12;

      ( Den (av,( FreeMSA X))) = (( FreeOper X) . av) by A10, MSUALG_1:def 6

      .= ( DenOp (av,X)) by MSAFREE:def 13;

      

      hence ((H . v) . t) = (( DenOp (av,X)) . HHp) by A3, A5, A37, A26, MSUALG_3:def 7

      .= ( [( action_at v), the carrier of IIG] -tree HHp) by A31, A36, MSAFREE:def 12;

    end;

    definition

      let IIG;

      let SCS be non-empty Circuit of IIG, s be State of SCS, iv be InputValues of SCS;

      :: original: +*

      redefine

      func s +* iv -> State of SCS ;

      coherence

      proof

        

         A1: ( dom iv) = ( InputVertices IIG) by PARTFUN1:def 2;

        then ( dom the Sorts of SCS) = the carrier of IIG & for x be set st x in ( dom iv) holds (iv . x) in (the Sorts of SCS . x) by MSAFREE2:def 5, PARTFUN1:def 2;

        hence thesis by A1, PRE_CIRC: 6;

      end;

    end

    definition

      let IIG;

      let A be non-empty Circuit of IIG, iv be InputValues of A;

      :: CIRCUIT2:def1

      func Fix_inp iv -> ManySortedFunction of ( FreeGen the Sorts of A), the Sorts of ( FreeEnv A) means

      : Def1: for v be Vertex of IIG holds (v in ( InputVertices IIG) implies (it . v) = (( FreeGen (v,the Sorts of A)) --> ( root-tree [(iv . v), v]))) & (v in ( SortsWithConstants IIG) implies (it . v) = (( FreeGen (v,the Sorts of A)) --> ( root-tree [( action_at v), the carrier of IIG]))) & (v in (( InnerVertices IIG) \ ( SortsWithConstants IIG)) implies (it . v) = ( id ( FreeGen (v,the Sorts of A))));

      existence

      proof

        defpred P[ object, object] means ex v be Vertex of IIG st v = $1 & ($1 in ( InputVertices IIG) implies $2 = (( FreeGen (v,the Sorts of A)) --> ( root-tree [(iv . v), v]))) & ($1 in ( SortsWithConstants IIG) implies $2 = (( FreeGen (v,the Sorts of A)) --> ( root-tree [( action_at v), the carrier of IIG]))) & ($1 in (( InnerVertices IIG) \ ( SortsWithConstants IIG)) implies $2 = ( id ( FreeGen (v,the Sorts of A))));

         A1:

        now

          let i be object;

          assume

           A2: i in the carrier of IIG;

          then

          reconsider v = i as Vertex of IIG;

          v in (( InputVertices IIG) \/ ( InnerVertices IIG)) by A2, XBOOLE_1: 45;

          then

           A3: v in ( InputVertices IIG) or v in ( InnerVertices IIG) by XBOOLE_0:def 3;

          

           A4: ((( InnerVertices IIG) \ ( SortsWithConstants IIG)) \/ ( SortsWithConstants IIG)) = ( InnerVertices IIG) by MSAFREE2: 3, XBOOLE_1: 45;

          thus ex j be object st P[i, j]

          proof

            per cases by A4, A3, XBOOLE_0:def 3;

              suppose

               A5: v in ( InputVertices IIG);

              reconsider j = (( FreeGen (v,the Sorts of A)) --> ( root-tree [(iv . v), v])) as set;

              take j, v;

              thus v = i;

              thus i in ( InputVertices IIG) implies j = (( FreeGen (v,the Sorts of A)) --> ( root-tree [(iv . v), v]));

              thus i in ( SortsWithConstants IIG) implies j = (( FreeGen (v,the Sorts of A)) --> ( root-tree [( action_at v), the carrier of IIG])) by A5, MSAFREE2: 4, XBOOLE_0: 3;

              

               A6: (( InnerVertices IIG) \ ( SortsWithConstants IIG)) c= ( InnerVertices IIG) & ( InputVertices IIG) misses ( InnerVertices IIG) by XBOOLE_1: 36, XBOOLE_1: 79;

              assume i in (( InnerVertices IIG) \ ( SortsWithConstants IIG));

              hence thesis by A5, A6, XBOOLE_0: 3;

            end;

              suppose

               A7: v in ( SortsWithConstants IIG);

              reconsider j = (( FreeGen (v,the Sorts of A)) --> ( root-tree [( action_at v), the carrier of IIG])) as set;

              take j, v;

              thus v = i;

              thus i in ( InputVertices IIG) implies j = (( FreeGen (v,the Sorts of A)) --> ( root-tree [(iv . v), v])) by A7, MSAFREE2: 4, XBOOLE_0: 3;

              thus i in ( SortsWithConstants IIG) implies j = (( FreeGen (v,the Sorts of A)) --> ( root-tree [( action_at v), the carrier of IIG]));

              

               A8: (( InnerVertices IIG) \ ( SortsWithConstants IIG)) misses ( SortsWithConstants IIG) by XBOOLE_1: 79;

              assume i in (( InnerVertices IIG) \ ( SortsWithConstants IIG));

              hence thesis by A7, A8, XBOOLE_0: 3;

            end;

              suppose

               A9: v in (( InnerVertices IIG) \ ( SortsWithConstants IIG));

              reconsider j = ( id ( FreeGen (v,the Sorts of A))) as set;

              take j, v;

              thus v = i;

              hereby

                

                 A10: (( InnerVertices IIG) \ ( SortsWithConstants IIG)) c= ( InnerVertices IIG) & ( InputVertices IIG) misses ( InnerVertices IIG) by XBOOLE_1: 36, XBOOLE_1: 79;

                assume i in ( InputVertices IIG);

                hence j = (( FreeGen (v,the Sorts of A)) --> ( root-tree [(iv . v), v])) by A9, A10, XBOOLE_0: 3;

              end;

              thus i in ( SortsWithConstants IIG) implies j = (( FreeGen (v,the Sorts of A)) --> ( root-tree [( action_at v), the carrier of IIG])) by A9, XBOOLE_0: 3, XBOOLE_1: 79;

              assume i in (( InnerVertices IIG) \ ( SortsWithConstants IIG));

              thus thesis;

            end;

          end;

        end;

        consider M be ManySortedSet of the carrier of IIG such that

         A11: for i be object st i in the carrier of IIG holds P[i, (M . i)] from PBOOLE:sch 3( A1);

         A12:

        now

          let i be object;

          

           A13: ((( InnerVertices IIG) \ ( SortsWithConstants IIG)) \/ ( SortsWithConstants IIG)) = ( InnerVertices IIG) by MSAFREE2: 3, XBOOLE_1: 45;

          assume

           A14: i in the carrier of IIG;

          then

          reconsider v = i as Vertex of IIG;

          v in (( InputVertices IIG) \/ ( InnerVertices IIG)) by A14, XBOOLE_1: 45;

          then

           A15: v in ( InputVertices IIG) or v in ( InnerVertices IIG) by XBOOLE_0:def 3;

          

           A16: ( FreeGen (v,the Sorts of A)) = (( FreeGen the Sorts of A) . v) by MSAFREE:def 16;

          

           A17: ( FreeEnv A) = MSAlgebra (# ( FreeSort the Sorts of A), ( FreeOper the Sorts of A) #) by MSAFREE:def 14;

          per cases by A13, A15, XBOOLE_0:def 3;

            suppose

             A18: v in ( InputVertices IIG);

            then (iv . v) in (the Sorts of A . v) by MSAFREE2:def 5;

            then

             A19: ( root-tree [(iv . v), v]) in ( FreeGen (v,the Sorts of A)) by MSAFREE:def 15;

             P[v, (M . v)] by A11;

            hence (M . i) is Function of (( FreeGen the Sorts of A) . i), (the Sorts of ( FreeEnv A) . i) by A16, A17, A18, A19, FUNCOP_1: 45;

          end;

            suppose

             A20: v in ( SortsWithConstants IIG);

            reconsider sy = ( Sym (( action_at v),the Sorts of A)) as NonTerminal of ( DTConMSA the Sorts of A);

            set p = ( <*> ( TS ( DTConMSA the Sorts of A)));

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

            

             A21: ( SortsWithConstants IIG) c= ( InnerVertices IIG) by MSAFREE2: 3;

            v in { s where s be SortSymbol of IIG : s is with_const_op } by A20, MSAFREE2:def 1;

            then ex s be SortSymbol of IIG st v = s & s is with_const_op;

            then

            consider o be OperSymbol of IIG such that

             A22: (the Arity of IIG . o) = {} and

             A23: (the ResultSort of IIG . o) = v by MSUALG_2:def 1;

            

             A24: for n be Nat st n in ( dom p) holds (p . n) in ( FreeSort (the Sorts of A,(( the_arity_of o) /. n) qua SortSymbol of IIG));

            p = ( the_arity_of o) by A22, MSUALG_1:def 1;

            then

             A25: p in (((( FreeSort the Sorts of A) # ) * the Arity of IIG) . o) by A24, MSAFREE: 9;

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

            then o = ( action_at v) by A20, A21, MSAFREE2:def 7;

            then sy ==> ( roots p) by A25, MSAFREE: 10;

            then {} = ( <*> (IIG -Terms the Sorts of A)) & p is SubtreeSeq of ( Sym (( action_at v),the Sorts of A)) by DTCONSTR:def 6;

            then e = ( [( action_at v), the carrier of IIG] -tree {} ) & {} is ArgumentSeq of sy by MSATERM:def 2, TREES_4: 20;

            then e in (IIG -Terms the Sorts of A) by MSATERM: 1;

            then

            reconsider e as Element of ( TS ( DTConMSA the Sorts of A)) by MSATERM:def 1;

            (e . {} ) = [( action_at v), the carrier of IIG] & ( the_result_sort_of ( action_at v)) = v by A20, A21, MSAFREE2:def 7, TREES_4: 3;

            then 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 };

            then e in ( FreeSort (the Sorts of A,v)) by MSAFREE:def 10;

            then

             A26: e in (the Sorts of ( FreeEnv A) . v) by A17, MSAFREE:def 11;

             P[v, (M . v)] by A11;

            hence (M . i) is Function of (( FreeGen the Sorts of A) . i), (the Sorts of ( FreeEnv A) . i) by A16, A20, A26, FUNCOP_1: 45;

          end;

            suppose

             A27: v in (( InnerVertices IIG) \ ( SortsWithConstants IIG));

            

             A28: ( dom ( id ( FreeGen (v,the Sorts of A)))) = ( FreeGen (v,the Sorts of A)) & ( rng ( id ( FreeGen (v,the Sorts of A)))) = ( FreeGen (v,the Sorts of A));

             P[v, (M . v)] by A11;

            hence (M . i) is Function of (( FreeGen the Sorts of A) . i), (the Sorts of ( FreeEnv A) . i) by A16, A17, A27, A28, FUNCT_2:def 1, RELSET_1: 4;

          end;

        end;

        now

          let i be object;

          assume i in ( dom M);

          then i in the carrier of IIG by PARTFUN1:def 2;

          hence (M . i) is Function by A12;

        end;

        then

        reconsider M as ManySortedFunction of the carrier of IIG by FUNCOP_1:def 6;

        reconsider M as ManySortedFunction of ( FreeGen the Sorts of A), the Sorts of ( FreeEnv A) by A12, PBOOLE:def 15;

        take M;

        let v be Vertex of IIG;

        hereby

          assume

           A29: v in ( InputVertices IIG);

           P[v, (M . v)] by A11;

          hence (M . v) = (( FreeGen (v,the Sorts of A)) --> ( root-tree [(iv . v), v])) by A29;

        end;

        hereby

          assume

           A30: v in ( SortsWithConstants IIG);

           P[v, (M . v)] by A11;

          hence (M . v) = (( FreeGen (v,the Sorts of A)) --> ( root-tree [( action_at v), the carrier of IIG])) by A30;

        end;

        assume

         A31: v in (( InnerVertices IIG) \ ( SortsWithConstants IIG));

         P[v, (M . v)] by A11;

        hence thesis by A31;

      end;

      uniqueness

      proof

        let M1,M2 be ManySortedFunction of ( FreeGen the Sorts of A), the Sorts of ( FreeEnv A) such that

         A32: for v be Vertex of IIG holds (v in ( InputVertices IIG) implies (M1 . v) = (( FreeGen (v,the Sorts of A)) --> ( root-tree [(iv . v), v]))) & (v in ( SortsWithConstants IIG) implies (M1 . v) = (( FreeGen (v,the Sorts of A)) --> ( root-tree [( action_at v), the carrier of IIG]))) & (v in (( InnerVertices IIG) \ ( SortsWithConstants IIG)) implies (M1 . v) = ( id ( FreeGen (v,the Sorts of A)))) and

         A33: for v be Vertex of IIG holds (v in ( InputVertices IIG) implies (M2 . v) = (( FreeGen (v,the Sorts of A)) --> ( root-tree [(iv . v), v]))) & (v in ( SortsWithConstants IIG) implies (M2 . v) = (( FreeGen (v,the Sorts of A)) --> ( root-tree [( action_at v), the carrier of IIG]))) & (v in (( InnerVertices IIG) \ ( SortsWithConstants IIG)) implies (M2 . v) = ( id ( FreeGen (v,the Sorts of A))));

        now

          let i be object;

          

           A34: ((( InnerVertices IIG) \ ( SortsWithConstants IIG)) \/ ( SortsWithConstants IIG)) = ( InnerVertices IIG) by MSAFREE2: 3, XBOOLE_1: 45;

          assume

           A35: i in the carrier of IIG;

          then

          reconsider v = i as Vertex of IIG;

          v in (( InputVertices IIG) \/ ( InnerVertices IIG)) by A35, XBOOLE_1: 45;

          then

           A36: v in ( InputVertices IIG) or v in ( InnerVertices IIG) by XBOOLE_0:def 3;

          per cases by A34, A36, XBOOLE_0:def 3;

            suppose

             A37: v in ( InputVertices IIG);

            then (M1 . v) = (( FreeGen (v,the Sorts of A)) --> ( root-tree [(iv . v), v])) by A32;

            hence (M1 . i) = (M2 . i) by A33, A37;

          end;

            suppose

             A38: v in ( SortsWithConstants IIG);

            then (M1 . v) = (( FreeGen (v,the Sorts of A)) --> ( root-tree [( action_at v), the carrier of IIG])) by A32;

            hence (M1 . i) = (M2 . i) by A33, A38;

          end;

            suppose

             A39: v in (( InnerVertices IIG) \ ( SortsWithConstants IIG));

            then (M1 . v) = ( id ( FreeGen (v,the Sorts of A))) by A32;

            hence (M1 . i) = (M2 . i) by A33, A39;

          end;

        end;

        hence M1 = M2;

      end;

    end

    definition

      let IIG;

      let A be non-empty Circuit of IIG, iv be InputValues of A;

      :: CIRCUIT2:def2

      func Fix_inp_ext iv -> ManySortedFunction of ( FreeEnv A), ( FreeEnv A) means

      : Def2: it is_homomorphism (( FreeEnv A),( FreeEnv A)) & ( Fix_inp iv) c= it ;

      existence

      proof

        reconsider G = ( FreeGen the Sorts of A) as free GeneratorSet of ( FreeEnv A) by MSAFREE: 16;

        consider h be ManySortedFunction of ( FreeEnv A), ( FreeEnv A) such that

         A1: h is_homomorphism (( FreeEnv A),( FreeEnv A)) and

         A2: (h || G) = ( Fix_inp iv) by MSAFREE:def 5;

        take h;

        thus h is_homomorphism (( FreeEnv A),( FreeEnv A)) by A1;

        let i be object;

        assume

         A3: i in the carrier of IIG;

        then

        reconsider hi = (h . i) as Function of (the Sorts of ( FreeEnv A) . i), (the Sorts of ( FreeEnv A) . i) by PBOOLE:def 15;

        (( Fix_inp iv) . i) = (hi | (G . i)) by A2, A3, MSAFREE:def 1;

        hence thesis by RELAT_1: 59;

      end;

      uniqueness

      proof

        let h1,h2 be ManySortedFunction of ( FreeEnv A), ( FreeEnv A) such that

         A4: h1 is_homomorphism (( FreeEnv A),( FreeEnv A)) and

         A5: ( Fix_inp iv) c= h1 and

         A6: h2 is_homomorphism (( FreeEnv A),( FreeEnv A)) and

         A7: ( Fix_inp iv) c= h2;

        reconsider f1 = h1, f2 = h2 as ManySortedFunction of ( FreeMSA the Sorts of A), ( FreeMSA the Sorts of A);

        now

          let i be set such that

           A8: i in the carrier of IIG;

          reconsider g = (f2 . i) as Function of (the Sorts of ( FreeMSA the Sorts of A) . i), (the Sorts of ( FreeMSA the Sorts of A) . i) by A8, PBOOLE:def 15;

          

           A9: (( Fix_inp iv) . i) c= g by A7, A8;

          reconsider Fi = (( Fix_inp iv) . i) as Function;

          Fi is Function of (( FreeGen the Sorts of A) . i), (the Sorts of ( FreeMSA the Sorts of A) . i) by A8, PBOOLE:def 15;

          then

           A10: ( dom Fi) = (( FreeGen the Sorts of A) . i) by A8, FUNCT_2:def 1;

          

           A11: (( Fix_inp iv) . i) c= (f1 . i) by A5, A8;

          

          thus ((f2 || ( FreeGen the Sorts of A)) . i) = (g | (( FreeGen the Sorts of A) . i)) by A8, MSAFREE:def 1

          .= (( Fix_inp iv) . i) by A10, A9, GRFUNC_1: 23

          .= ((f1 . i) | (( FreeGen the Sorts of A) . i)) by A10, A11, GRFUNC_1: 23;

        end;

        then (f1 || ( FreeGen the Sorts of A)) = (f2 || ( FreeGen the Sorts of A)) by MSAFREE:def 1;

        hence h1 = h2 by A4, A6, EXTENS_1: 14;

      end;

    end

    theorem :: CIRCUIT2:2

    

     Th2: for A be non-empty Circuit of IIG, iv be InputValues of A, v be Vertex of IIG, e be Element of (the Sorts of ( FreeEnv A) . v), x be set st v in (( InnerVertices IIG) \ ( SortsWithConstants IIG)) & e = ( root-tree [x, v]) holds ((( Fix_inp_ext iv) . v) . e) = e

    proof

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

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

       A2: e = ( root-tree [x, v]);

      

       A3: (e . {} ) = [x, v] by A2, TREES_4: 3;

       A4:

      now

        given o be OperSymbol of IIG such that

         A5: [o, the carrier of IIG] = (e . {} ) and ( the_result_sort_of o) = v;

        v = the carrier of IIG by A3, A5, XTUPLE_0: 1;

        hence contradiction by Lm1;

      end;

      set X = the Sorts of A;

      ( FreeEnv A) = MSAlgebra (# ( FreeSort the Sorts of A), ( FreeOper the Sorts of A) #) by MSAFREE:def 14;

      then e in (( FreeSort X) . v);

      then

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

      ( Fix_inp iv) c= ( Fix_inp_ext iv) by Def2;

      then

       A7: (( Fix_inp iv) . v) c= (( Fix_inp_ext iv) . v);

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

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

      then

       A8: e in ( FreeGen (v,the Sorts of A)) by A4, MSAFREE:def 15;

      then e in (( FreeGen the Sorts of A) . v) by MSAFREE:def 16;

      then e in ( dom (( Fix_inp iv) . v)) by FUNCT_2:def 1;

      

      hence ((( Fix_inp_ext iv) . v) . e) = ((( Fix_inp iv) . v) . e) by A7, GRFUNC_1: 2

      .= (( id ( FreeGen (v,the Sorts of A))) . e) by A1, Def1

      .= e by A8, FUNCT_1: 17;

    end;

    theorem :: CIRCUIT2:3

    

     Th3: for A be non-empty Circuit of IIG, iv be InputValues of A, v be Vertex of IIG, x be Element of (the Sorts of A . v) st v in ( InputVertices IIG) holds ((( Fix_inp_ext iv) . v) . ( root-tree [x, v])) = ( root-tree [(iv . v), v])

    proof

      let A be non-empty Circuit of IIG, iv be InputValues of A, v be Vertex of IIG, x be Element of (the Sorts of A . v);

      set e = ( root-tree [x, v]);

      assume

       A1: v in ( InputVertices IIG);

      

       A2: e in ( FreeGen (v,the Sorts of A)) by MSAFREE:def 15;

      ( Fix_inp iv) c= ( Fix_inp_ext iv) by Def2;

      then

       A3: (( Fix_inp iv) . v) c= (( Fix_inp_ext iv) . v);

      ( FreeEnv A) = MSAlgebra (# ( FreeSort the Sorts of A), ( FreeOper the Sorts of A) #) by MSAFREE:def 14;

      then

      reconsider e as Element of (the Sorts of ( FreeEnv A) . v) by A2;

      e in (( FreeGen the Sorts of A) . v) by A2, MSAFREE:def 16;

      then e in ( dom (( Fix_inp iv) . v)) by FUNCT_2:def 1;

      

      hence ((( Fix_inp_ext iv) . v) . ( root-tree [x, v])) = ((( Fix_inp iv) . v) . e) by A3, GRFUNC_1: 2

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

      .= ( root-tree [(iv . v), v]) by A2, FUNCOP_1: 7;

    end;

    theorem :: CIRCUIT2:4

    

     Th4: for A be non-empty Circuit of IIG, iv be InputValues of A, v be Vertex of IIG, e be Element of (the Sorts of ( FreeEnv A) . v), p,q be DTree-yielding FinSequence st v in ( InnerVertices IIG) & e = ( [( action_at v), the carrier of IIG] -tree p) & ( dom p) = ( dom q) & for k be Element of NAT st k in ( dom p) holds (q . k) = ((( Fix_inp_ext iv) . (( the_arity_of ( action_at v)) /. k)) . (p . k)) holds ((( Fix_inp_ext iv) . v) . e) = ( [( action_at v), the carrier of IIG] -tree q)

    proof

      let A be non-empty Circuit of IIG, iv be InputValues of A, v be Vertex of IIG, e be Element of (the Sorts of ( FreeEnv A) . v), p,q 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: ( dom p) = ( dom q) and

       A4: for k be Element of NAT st k in ( dom p) holds (q . k) = ((( Fix_inp_ext iv) . (( the_arity_of ( action_at v)) /. k)) . (p . k));

      set o = ( action_at v);

      

       A5: ( the_result_sort_of o) = v by A1, MSAFREE2:def 7;

      then

       A6: ( len p) = ( len ( the_arity_of o)) by A2, MSAFREE2: 10;

       A7:

      now

        let k be Nat;

        assume

         A8: k in ( dom q);

        then

         A9: k in ( dom ( the_arity_of o)) by A3, A6, FINSEQ_3: 29;

        then (p . k) in (the Sorts of ( FreeEnv A) . (( the_arity_of o) . k)) by A2, A5, MSAFREE2: 11;

        then

         A10: (p . k) in (the Sorts of ( FreeEnv A) . (( the_arity_of o) /. k)) by A9, PARTFUN1:def 6;

        (q . k) = ((( Fix_inp_ext iv) . (( the_arity_of o) /. k)) . (p . k)) by A3, A4, A8;

        hence (q . k) in (the Sorts of ( FreeEnv A) . (( the_arity_of o) /. k)) by A10, FUNCT_2: 5;

      end;

       A11:

      now

        let k be Nat;

        assume k in ( dom p);

        then

         A12: k in ( dom ( the_arity_of o)) by A6, FINSEQ_3: 29;

        then (p . k) in (the Sorts of ( FreeEnv A) . (( the_arity_of o) . k)) by A2, A5, MSAFREE2: 11;

        hence (p . k) in (the Sorts of ( FreeEnv A) . (( the_arity_of o) /. k)) by A12, PARTFUN1:def 6;

      end;

      then

      reconsider x = p as Element of ( Args (o,( FreeEnv A))) by A6, MSAFREE2: 5;

      

       A13: ( FreeEnv A) = MSAlgebra (# ( FreeSort the Sorts of A), ( FreeOper the Sorts of A) #) by MSAFREE:def 14;

      then

       A14: ( Args (o,( FreeEnv A))) = (((( FreeSort the Sorts of A) # ) * the Arity of IIG) . o) by MSUALG_1:def 4;

      then

      reconsider pp = p as FinSequence of ( TS ( DTConMSA the Sorts of A)) by A6, A11, MSAFREE: 8, MSAFREE2: 5;

      p in ( Args (o,( FreeEnv A))) by A6, A11, MSAFREE2: 5;

      then

       A15: ( Sym (o,the Sorts of A)) ==> ( roots pp) by A14, MSAFREE: 10;

      

       A16: ( len q) = ( len ( the_arity_of o)) by A3, A6, FINSEQ_3: 29;

      then

      reconsider y = q as Element of ( Args (o,( FreeEnv A))) by A7, MSAFREE2: 5;

      

       A17: ( Fix_inp_ext iv) is_homomorphism (( FreeEnv A),( FreeEnv A)) by Def2;

      reconsider qq = q as FinSequence of ( TS ( DTConMSA the Sorts of A)) by A14, A16, A7, MSAFREE: 8, MSAFREE2: 5;

      q in ( Args (o,( FreeEnv A))) by A16, A7, MSAFREE2: 5;

      then

       A18: ( Sym (o,the Sorts of A)) ==> ( roots qq) by A14, MSAFREE: 10;

      for k be Nat st k in ( dom p) holds (q . k) = ((( Fix_inp_ext iv) . (( the_arity_of ( action_at v)) /. k)) . (p . k)) by A4;

      then

       A19: y = (( Fix_inp_ext iv) # x) by MSUALG_3:def 6;

      e = (( Sym (( action_at v),the Sorts of A)) -tree pp) by A2, MSAFREE:def 9

      .= (( DenOp (( action_at v),the Sorts of A)) . x) by A15, MSAFREE:def 12

      .= ((the Charact of ( FreeEnv A) . o) . x) by A13, MSAFREE:def 13

      .= (( Den (( action_at v),( FreeEnv A))) . x) by MSUALG_1:def 6;

      

      hence ((( Fix_inp_ext iv) . v) . e) = (( Den (( action_at v),( FreeEnv A))) . q) by A5, A19, A17, MSUALG_3:def 7

      .= ((( FreeOper the Sorts of A) . o) . q) by A13, MSUALG_1:def 6

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

      .= (( Sym (( action_at v),the Sorts of A)) -tree qq) by A18, MSAFREE:def 12

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

    end;

    theorem :: CIRCUIT2:5

    

     Th5: for A be non-empty Circuit of IIG, iv be InputValues of A, v be Vertex of IIG, e be Element of (the Sorts of ( FreeEnv A) . v) st v in ( SortsWithConstants IIG) holds ((( Fix_inp_ext iv) . v) . e) = ( root-tree [( action_at v), the carrier of IIG])

    proof

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

      set X = the Sorts of A;

      assume

       A1: v in ( SortsWithConstants IIG);

      

       A2: ( FreeEnv A) = MSAlgebra (# ( FreeSort the Sorts of A), ( FreeOper the Sorts of A) #) by MSAFREE:def 14;

      then e in (( FreeSort the Sorts of A) . v);

      then e in ( FreeSort (the Sorts of A,v)) by MSAFREE:def 11;

      then e in { a where a 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;

      then

       A3: ex a be Element of ( TS ( DTConMSA X)) st e = a & ((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);

      per cases by A3;

        suppose

         A4: ex x be set st x in (X . v) & e = ( root-tree [x, v]);

        ( Fix_inp iv) c= ( Fix_inp_ext iv) by Def2;

        then

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

        

         A6: e in ( FreeGen (v,the Sorts of A)) by A4, MSAFREE:def 15;

        then e in (( FreeGen the Sorts of A) . v) by MSAFREE:def 16;

        then e in ( dom (( Fix_inp iv) . v)) by FUNCT_2:def 1;

        

        hence ((( Fix_inp_ext iv) . v) . e) = ((( Fix_inp iv) . v) . e) by A5, GRFUNC_1: 2

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

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

      end;

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

        then

        consider o9 be OperSymbol of IIG such that

         A7: [o9, the carrier of IIG] = (e . {} ) and

         A8: ( the_result_sort_of o9) = v;

        

         A9: ( SortsWithConstants IIG) c= ( InnerVertices IIG) by MSAFREE2: 3;

        then o9 = ( action_at v) by A1, A8, MSAFREE2:def 7;

        then

        consider q be DTree-yielding FinSequence such that

         A10: e = ( [( action_at v), the carrier of IIG] -tree q) by A7, CIRCUIT1: 9;

        v in { s where s be SortSymbol of IIG : s is with_const_op } by A1, MSAFREE2:def 1;

        then ex s be SortSymbol of IIG st v = s & s is with_const_op;

        then

        consider o be OperSymbol of IIG such that

         A11: (the Arity of IIG . o) = {} and

         A12: (the ResultSort of IIG . o) = v by MSUALG_2:def 1;

        

         A13: ( Fix_inp_ext iv) is_homomorphism (( FreeEnv A),( FreeEnv A)) by Def2;

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

        then

         A14: o = ( action_at v) by A1, A9, MSAFREE2:def 7;

        ( action_at v) in the carrier' of IIG;

        then

         A15: ( action_at v) in ( dom the Arity of IIG) by FUNCT_2:def 1;

        

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

        .= ((the Sorts of ( FreeEnv A) # ) . ( <*> the carrier of IIG)) by A11, A14, A15, FUNCT_1: 13

        .= { {} } by PRE_CIRC: 2;

        then

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

        

         A17: x = (( Fix_inp_ext iv) # x) by A16, TARSKI:def 1;

        

         A18: ( Args (( action_at v),( FreeEnv A))) = (((( FreeSort the Sorts of A) # ) * the Arity of IIG) . o) by A2, A14, MSUALG_1:def 4;

        then

        reconsider p = x as FinSequence of ( TS ( DTConMSA the Sorts of A)) by MSAFREE: 8;

        

         A19: ( Sym (( action_at v),the Sorts of A)) ==> ( roots p) by A14, A18, MSAFREE: 10;

        

         A20: ( the_result_sort_of ( action_at v)) = v by A1, A9, MSAFREE2:def 7;

        

        then ( len q) = ( len ( the_arity_of ( action_at v))) by A10, MSAFREE2: 10

        .= ( len {} ) by A11, A14, MSUALG_1:def 1

        .= 0 ;

        then q = {} ;

        then

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

        (( Den (( action_at v),( FreeEnv A))) . x) = ((( FreeOper the Sorts of A) . ( action_at v)) . x) by A2, MSUALG_1:def 6

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

        .= (( Sym (( action_at v),the Sorts of A)) -tree p) by A19, MSAFREE:def 12

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

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

        hence thesis by A20, A17, A13, A21, MSUALG_3:def 7;

      end;

    end;

    theorem :: CIRCUIT2:6

    

     Th6: for A be non-empty Circuit of IIG, iv be InputValues of A, v be Vertex of IIG, e,e1 be Element of (the Sorts of ( FreeEnv A) . v), t,t1 be DecoratedTree st t = e & t1 = e1 & e1 = ((( Fix_inp_ext iv) . v) . e) holds ( dom t) = ( dom t1)

    proof

      let A be non-empty Circuit of IIG, iv be InputValues of A, v be Vertex of IIG, e,e1 be Element of (the Sorts of ( FreeEnv A) . v), t,t1 be DecoratedTree;

      set X = the Sorts of A;

      set FX = the Sorts of ( FreeEnv A);

      defpred P[ Nat] means for v be Vertex of IIG, e,e1 be Element of (FX . v), t,t1 be DecoratedTree st t = e & t1 = e1 & ( depth (v,A)) <= $1 & e1 = ((( Fix_inp_ext iv) . v) . e) holds ( dom t) = ( dom t1);

      reconsider k = ( depth (v,A)) as Element of NAT by ORDINAL1:def 12;

      

       A1: ( depth (v,A)) <= k;

      

       A2: ( FreeMSA X) = MSAlgebra (# ( FreeSort X), ( FreeOper X) #) by MSAFREE:def 14;

      

       A3: for k be Nat st P[k] holds P[(k + 1)]

      proof

        

         A4: ((( InnerVertices IIG) \ ( SortsWithConstants IIG)) \/ ( SortsWithConstants IIG)) = ( InnerVertices IIG) by MSAFREE2: 3, XBOOLE_1: 45;

        let k be Nat;

        assume

         A5: P[k];

        let v be Vertex of IIG, e,e1 be Element of (FX . v), t,t1 be DecoratedTree;

        assume that

         A6: t = e and

         A7: t1 = e1 and

         A8: ( depth (v,A)) <= (k + 1) and

         A9: e1 = ((( Fix_inp_ext iv) . v) . e);

        

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

        (( InputVertices IIG) \/ ( InnerVertices IIG)) = the carrier of IIG by XBOOLE_1: 45;

        then

         A11: v in ( InputVertices IIG) or v in ( InnerVertices IIG) by XBOOLE_0:def 3;

        e in (FX . v) & (( FreeSort X) . v) = ( FreeSort (X,v)) by MSAFREE:def 11;

        then

        consider a be Element of ( TS ( DTConMSA X)) such that

         A12: a = e and

         A13: (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, A10;

        per cases by A13, A11, A4, XBOOLE_0:def 3;

          suppose

           A14: v in ( InputVertices IIG);

          then

           A15: ((( Fix_inp_ext iv) . v) . a) = ( root-tree [(iv . v), v]) by A13, Th3, MSAFREE2: 2;

          

          thus ( dom t) = { {} } by A6, A12, A13, A14, MSAFREE2: 2, TREES_1: 29, TREES_4: 3

          .= ( dom t1) by A7, A9, A12, A15, TREES_1: 29, TREES_4: 3;

        end;

          suppose v in (( InnerVertices IIG) \ ( SortsWithConstants IIG)) & ex x be set st x in (X . v) & a = ( root-tree [x, v]);

          hence thesis by A6, A7, A9, A12, Th2;

        end;

          suppose that

           A16: v in ( SortsWithConstants IIG) and

           A17: ex x be set st x in (X . v) & a = ( root-tree [x, v]);

          

           A18: ((( Fix_inp_ext iv) . v) . a) = ( root-tree [( action_at v), the carrier of IIG]) by A12, A16, Th5;

          

          thus ( dom t) = { {} } by A6, A12, A17, TREES_1: 29, TREES_4: 3

          .= ( dom t1) by A7, A9, A12, A18, TREES_1: 29, TREES_4: 3;

        end;

          suppose that

           A19: v in ( InnerVertices IIG) and

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

          consider o be OperSymbol of IIG such that

           A21: [o, the carrier of IIG] = (a . {} ) and

           A22: ( the_result_sort_of o) = v by A20;

          

           A23: o = ( action_at v) by A19, A22, MSAFREE2:def 7;

          then

          consider p be DTree-yielding FinSequence such that

           A24: e = ( [( action_at v), the carrier of IIG] -tree p) by A12, A21, CIRCUIT1: 9;

          deffunc F( Nat) = ((( Fix_inp_ext iv) . (( the_arity_of ( action_at v)) /. $1)) . (p . $1));

          consider q be FinSequence such that

           A25: ( len q) = ( len p) and

           A26: for k be Nat st k in ( dom q) holds (q . k) = F(k) from FINSEQ_1:sch 2;

          

           A27: ( dom p) = ( dom q) by A25, FINSEQ_3: 29;

          ( len p) = ( len ( the_arity_of ( action_at v))) by A22, A23, A24, MSAFREE2: 10;

          then

           A28: ( dom p) = ( dom ( the_arity_of ( action_at v))) by FINSEQ_3: 29;

           A29:

          now

            let x be object;

            assume

             A30: x in ( dom q);

            then

            reconsider i = x as Element of NAT ;

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

            v1 = (( the_arity_of o) . i) by A23, A28, A27, A30, PARTFUN1:def 6;

            then

            reconsider ee = (p . i) as Element of (FX . v1) by A22, A23, A24, A28, A27, A30, MSAFREE2: 11;

            reconsider fv1 = (( Fix_inp_ext iv) . v1) as Function of (FX . v1), (FX . v1);

            (q . i) = (fv1 . ee) by A26, A30;

            hence (q . x) is DecoratedTree;

          end;

          

           A31: for k be Element of NAT st k in ( dom q) holds (q . k) = F(k) by A26;

          reconsider q as DTree-yielding FinSequence by A29, TREES_3: 24;

          

           A32: ((( Fix_inp_ext iv) . v) . e) = ( [( action_at v), the carrier of IIG] -tree q) by A19, A24, A31, A27, Th4;

          

           A33: ( dom ( doms p)) = ( dom p) by TREES_3: 37;

           A34:

          now

            let i be Nat;

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

            reconsider fv1 = (( Fix_inp_ext iv) . v1) as Function of (FX . v1), (FX . v1);

            assume

             A35: i in ( dom ( doms p));

            then v1 = (( the_arity_of o) . i) by A23, A28, A33, PARTFUN1:def 6;

            then

            reconsider ee = (p . i) as Element of (FX . v1) by A22, A23, A24, A28, A33, A35, MSAFREE2: 11;

            (q . i) = (fv1 . ee) by A26, A33, A27, A35;

            then

            reconsider ee1 = (q . i) as Element of (FX . v1);

            v1 in ( rng ( the_arity_of ( action_at v))) by A28, A33, A35, PARTFUN2: 2;

            then ( depth (v1,A)) < (k + 1) by A8, A19, CIRCUIT1: 19, XXREAL_0: 2;

            then

             A36: ( depth (v1,A)) <= k by NAT_1: 13;

            (q . i) = ((( Fix_inp_ext iv) . v1) . (p . i)) by A26, A33, A27, A35;

            then ( dom ee) = ( dom ee1) by A5, A36;

            

            hence (( doms p) . i) = ( dom ee1) by A33, A35, FUNCT_6: 22

            .= (( doms q) . i) by A33, A27, A35, FUNCT_6: 22;

          end;

          ( dom q) = ( dom ( doms q)) by TREES_3: 37;

          then ( doms p) = ( doms q) by A27, A34, FINSEQ_1: 13, TREES_3: 37;

          

          hence ( dom t) = ( tree ( doms q)) by A6, A24, TREES_4: 10

          .= ( dom t1) by A7, A9, A32, TREES_4: 10;

        end;

      end;

      

       A37: P[ 0 ]

      proof

        let v be Vertex of IIG, e,e1 be Element of (FX . v), t,t1 be DecoratedTree such that

         A38: t = e and

         A39: t1 = e1 and

         A40: ( depth (v,A)) <= 0 and

         A41: e1 = ((( Fix_inp_ext iv) . v) . e);

        

         A42: ( depth (v,A)) = 0 by A40, NAT_1: 3;

        

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

        e in (FX . v) & (( FreeSort X) . v) = ( FreeSort (X,v)) by MSAFREE:def 11;

        then

        consider a be Element of ( TS ( DTConMSA X)) such that

         A44: a = e and

         A45: (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, A43;

        per cases by A42, A45, CIRCUIT1: 18;

          suppose

           A46: v in ( InputVertices IIG);

          then

           A47: ((( Fix_inp_ext iv) . v) . a) = ( root-tree [(iv . v), v]) by A45, Th3, MSAFREE2: 2;

          

          thus ( dom t) = { {} } by A38, A44, A45, A46, MSAFREE2: 2, TREES_1: 29, TREES_4: 3

          .= ( dom t1) by A39, A41, A44, A47, TREES_1: 29, TREES_4: 3;

        end;

          suppose that

           A48: v in ( SortsWithConstants IIG) and

           A49: ex x be set st x in (X . v) & a = ( root-tree [x, v]);

          

           A50: ((( Fix_inp_ext iv) . v) . a) = ( root-tree [( action_at v), the carrier of IIG]) by A44, A48, Th5;

          

          thus ( dom t) = { {} } by A38, A44, A49, TREES_1: 29, TREES_4: 3

          .= ( dom t1) by A39, A41, A44, A50, TREES_1: 29, TREES_4: 3;

        end;

          suppose that

           A51: v in ( SortsWithConstants IIG) and

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

          

           A53: ((( Fix_inp_ext iv) . v) . a) = ( root-tree [( action_at v), the carrier of IIG]) by A44, A51, Th5;

          consider o be OperSymbol of IIG such that

           A54: [o, the carrier of IIG] = (a . {} ) and

           A55: ( the_result_sort_of o) = v by A52;

          

           A56: ( SortsWithConstants IIG) c= ( InnerVertices IIG) by MSAFREE2: 3;

          then o = ( action_at v) by A51, A55, MSAFREE2:def 7;

          then

          consider p be DTree-yielding FinSequence such that

           A57: a = ( [( action_at v), the carrier of IIG] -tree p) by A44, A54, CIRCUIT1: 9;

          v in { s where s be SortSymbol of IIG : s is with_const_op } by A51, MSAFREE2:def 1;

          then ex s be SortSymbol of IIG st v = s & s is with_const_op;

          then

          consider o9 be OperSymbol of IIG such that

           A58: (the Arity of IIG . o9) = {} and

           A59: (the ResultSort of IIG . o9) = v by MSUALG_2:def 1;

          

           A60: ( the_result_sort_of o9) = v by A59, MSUALG_1:def 2;

          then

           A61: o9 = ( action_at v) by A51, A56, MSAFREE2:def 7;

          

          then ( len p) = ( len ( the_arity_of o9)) by A44, A60, A57, MSAFREE2: 10

          .= ( len {} ) by A58, MSUALG_1:def 1

          .= 0 ;

          then p = {} ;

          then a = ( root-tree [o9, the carrier of IIG]) by A61, A57, TREES_4: 20;

          

          hence ( dom t) = { {} } by A38, A44, TREES_1: 29, TREES_4: 3

          .= ( dom t1) by A39, A41, A44, A53, TREES_1: 29, TREES_4: 3;

        end;

      end;

      for k be Nat holds P[k] from NAT_1:sch 2( A37, A3);

      hence thesis by A1;

    end;

    theorem :: CIRCUIT2:7

    

     Th7: for A be non-empty Circuit of IIG, iv be InputValues of A, v be Vertex of IIG, e,e1 be Element of (the Sorts of ( FreeEnv A) . v) st e1 = ((( Fix_inp_ext iv) . v) . e) holds ( card e) = ( card e1)

    proof

      let A be non-empty Circuit of IIG, iv be InputValues of A, v be Vertex of IIG, e,e1 be Element of (the Sorts of ( FreeEnv A) . v);

      assume e1 = ((( Fix_inp_ext iv) . v) . e);

      then ( dom e) = ( dom e1) by Th6;

      

      hence ( card e) = ( card ( dom e1)) by CARD_1: 62

      .= ( card e1) by CARD_1: 62;

    end;

    definition

      let IIG;

      let SCS be non-empty Circuit of IIG, v be Vertex of IIG, iv be InputValues of SCS;

      :: CIRCUIT2:def3

      func IGTree (v,iv) -> Element of (the Sorts of ( FreeEnv SCS) . v) means

      : Def3: ex e be Element of (the Sorts of ( FreeEnv SCS) . v) st ( card e) = ( size (v,SCS)) & it = ((( Fix_inp_ext iv) . v) . e);

      existence

      proof

        reconsider SFv = (the Sorts of ( FreeEnv SCS) . v) as non empty set;

        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 SCS) . v) and

         A2: ( size (v,SCS)) = ( max s) by CIRCUIT1:def 4;

        ( size (v,SCS)) in s by A2, XXREAL_2:def 8;

        then

        consider e be Element of (the Sorts of ( FreeEnv SCS) . v) such that

         A3: ( size (v,SCS)) = ( card e) by A1;

        reconsider Fiev = (( Fix_inp_ext iv) . v) as Function of SFv, SFv;

        reconsider e9 = e as Element of SFv;

        reconsider IT = (Fiev . e9) as Element of SFv;

        reconsider IT as Element of (the Sorts of ( FreeEnv SCS) . v);

        take IT, e;

        thus ( card e) = ( size (v,SCS)) by A3;

        thus thesis;

      end;

      uniqueness

      proof

        defpred P[ Nat] means ex v be Vertex of IIG, it1,it2 be Element of (the Sorts of ( FreeEnv SCS) . v) st ( size (v,SCS)) = $1 & (ex e1 be Element of (the Sorts of ( FreeEnv SCS) . v) st ( card e1) = ( size (v,SCS)) & it1 = ((( Fix_inp_ext iv) . v) . e1)) & (ex e2 be Element of (the Sorts of ( FreeEnv SCS) . v) st ( card e2) = ( size (v,SCS)) & it2 = ((( Fix_inp_ext iv) . v) . e2)) & it1 <> it2;

        let it1,it2 be Element of (the Sorts of ( FreeEnv SCS) . v);

        now

          assume

           A4: ex n be Nat st P[n];

          consider n be Nat such that

           A5: P[n] and

           A6: for k be Nat st P[k] holds n <= k from NAT_1:sch 5( A4);

          consider v be Vertex of IIG, it1,it2 be Element of (the Sorts of ( FreeEnv SCS) . v) such that

           A7: ( size (v,SCS)) = n and

           A8: ex e1 be Element of (the Sorts of ( FreeEnv SCS) . v) st ( card e1) = ( size (v,SCS)) & it1 = ((( Fix_inp_ext iv) . v) . e1) and

           A9: ex e2 be Element of (the Sorts of ( FreeEnv SCS) . v) st ( card e2) = ( size (v,SCS)) & it2 = ((( Fix_inp_ext iv) . v) . e2) and

           A10: it1 <> it2 by A5;

          consider e2 be Element of (the Sorts of ( FreeEnv SCS) . v) such that

           A11: ( card e2) = ( size (v,SCS)) and

           A12: it2 = ((( Fix_inp_ext iv) . v) . e2) by A9;

          consider e1 be Element of (the Sorts of ( FreeEnv SCS) . v) such that

           A13: ( card e1) = ( size (v,SCS)) and

           A14: it1 = ((( Fix_inp_ext iv) . v) . e1) by A8;

          per cases ;

            suppose

             A15: v in ( InputVertices IIG);

            then

             A16: ex x2 be Element of (the Sorts of SCS . v) st e2 = ( root-tree [x2, v]) by MSAFREE2: 9;

            ex x1 be Element of (the Sorts of SCS . v) st e1 = ( root-tree [x1, v]) by A15, MSAFREE2: 9;

            

            then it1 = ( root-tree [(iv . v), v]) by A14, A15, Th3

            .= it2 by A12, A15, A16, Th3;

            hence contradiction by A10;

          end;

            suppose

             A17: v in ( SortsWithConstants IIG);

            

            then it1 = ( root-tree [( action_at v), the carrier of IIG]) by A14, Th5

            .= it2 by A12, A17, Th5;

            hence contradiction by A10;

          end;

            suppose that

             A18: not v in ( InputVertices IIG) and

             A19: not v in ( SortsWithConstants IIG);

            set Ht = (( Fix_inp_ext iv) * ( the_arity_of ( action_at v)));

            (( InputVertices IIG) \/ ( InnerVertices IIG)) = the carrier of IIG by XBOOLE_1: 45;

            then

             A20: v in ( InnerVertices IIG) by A18, XBOOLE_0:def 3;

            then

             A21: v in (( InnerVertices IIG) \ ( SortsWithConstants IIG)) by A19, XBOOLE_0:def 5;

            then

            consider q1 be DTree-yielding FinSequence such that

             A22: e1 = ( [( action_at v), the carrier of IIG] -tree q1) by A13, CIRCUIT1: 12;

            ( [( action_at v), the carrier of IIG] -tree q1) in (the Sorts of ( FreeEnv SCS) . v) by A22;

            then ( [( action_at v), the carrier of IIG] -tree q1) in (the Sorts of ( FreeEnv SCS) . ( the_result_sort_of ( action_at v))) by A20, MSAFREE2:def 7;

            then

             B2: ( len q1) = ( len ( the_arity_of ( action_at v))) by MSAFREE2: 10;

            consider q2 be DTree-yielding FinSequence such that

             A23: e2 = ( [( action_at v), the carrier of IIG] -tree q2) by A11, A21, CIRCUIT1: 12;

            ( [( action_at v), the carrier of IIG] -tree q2) in (the Sorts of ( FreeEnv SCS) . v) by A23;

            then

             A24: ( [( action_at v), the carrier of IIG] -tree q2) in (the Sorts of ( FreeEnv SCS) . ( the_result_sort_of ( action_at v))) by A20, MSAFREE2:def 7;

            then

             B1: ( len q2) = ( len ( the_arity_of ( action_at v))) by MSAFREE2: 10;

            then

             B3: ( dom q1) = ( dom q2) by B2, FINSEQ_3: 29;

            set acv = ( action_at v);

            

             B4: ( dom q2) = ( dom ( the_arity_of acv)) by FINSEQ_3: 29, B1;

            

             A25: ( Fix_inp_ext iv) is_homomorphism (( FreeEnv SCS),( FreeEnv SCS)) by Def2;

            then

            consider p1 be DTree-yielding FinSequence such that

             A26: p1 = (Ht .. q1) and

             A27: it1 = ( [( action_at v), the carrier of IIG] -tree p1) by A14, A20, A22, Th1;

            consider p2 be DTree-yielding FinSequence such that

             A28: p2 = (Ht .. q2) and

             A29: it2 = ( [( action_at v), the carrier of IIG] -tree p2) by A12, A20, A23, A25, Th1;

            ( rng ( the_arity_of acv)) c= the carrier of IIG by FINSEQ_1:def 4;

            then ( rng ( the_arity_of acv)) c= ( dom ( Fix_inp_ext iv)) by PARTFUN1:def 2;

            then

             A33: ( dom ( the_arity_of ( action_at v))) = ( dom Ht) by RELAT_1: 27;

            

             A30: ( dom p1) = (( dom Ht) /\ ( dom q1)) by A26, PRALG_1:def 19

            .= ( dom Ht) by A33, B4, B3;

            

             a30: ( dom p2) = (( dom Ht) /\ ( dom q2)) by A28, PRALG_1:def 19

            .= ( dom Ht) by A33, B4;

            then ( len p1) = ( len p2) by A30, FINSEQ_3: 29;

            then

            consider i be Nat such that

             A31: i in ( dom p1) and

             A32: (p1 . i) <> (p2 . i) by A10, A27, A29, FINSEQ_2: 9;

            reconsider w = (( the_arity_of acv) . i) as Vertex of IIG by A30, A31, A33, FINSEQ_2: 11;

            ( [acv, the carrier of IIG] -tree q1) in (the Sorts of ( FreeEnv SCS) . v) by A22;

            then

             A34: ( [acv, the carrier of IIG] -tree q1) in (the Sorts of ( FreeEnv SCS) . ( the_result_sort_of acv)) by A20, MSAFREE2:def 7;

            then

            reconsider E1 = (q1 . i), E2 = (q2 . i) as Element of (the Sorts of ( FreeEnv SCS) . w) by A30, A33, A31, A24, MSAFREE2: 11;

            

             B2: ( len q1) = ( len ( the_arity_of acv)) by A34, MSAFREE2: 10;

            ( [acv, the carrier of IIG] -tree p2) in (the Sorts of ( FreeEnv SCS) . v) by A29;

            then

             A35: ( [acv, the carrier of IIG] -tree p2) in (the Sorts of ( FreeEnv SCS) . ( the_result_sort_of acv)) by A20, MSAFREE2:def 7;

            ( [acv, the carrier of IIG] -tree p1) in (the Sorts of ( FreeEnv SCS) . v) by A27;

            then ( [acv, the carrier of IIG] -tree p1) in (the Sorts of ( FreeEnv SCS) . ( the_result_sort_of acv)) by A20, MSAFREE2:def 7;

            then

            reconsider It1 = (p1 . i), It2 = (p2 . i) as Element of (the Sorts of ( FreeEnv SCS) . w) by A30, A33, A31, A35, MSAFREE2: 11;

            reconsider Hti = (Ht . i) as Function;

            

             A36: Hti = (( Fix_inp_ext iv) . (( the_arity_of acv) . i)) by A30, A31, FUNCT_1: 12;

            then

             A37: It2 = ((( Fix_inp_ext iv) . w) . E2) by a30, A28, A30, A31, PRALG_1:def 19;

            i in ( dom q2) by B1, A30, A33, A31, FINSEQ_3: 29;

            then E2 in ( rng q2) by FUNCT_1:def 3;

            then

             A38: ( card E2) = ( size (w,SCS)) by A11, A21, A23, CIRCUIT1: 11;

            i in ( dom q1) by B2, A30, A33, A31, FINSEQ_3: 29;

            then E1 in ( rng q1) by FUNCT_1:def 3;

            then

             A39: ( card E1) = ( size (w,SCS)) by A13, A21, A22, CIRCUIT1: 11;

            

             A40: w in ( rng ( the_arity_of ( action_at v))) by A30, A33, A31, FUNCT_1:def 3;

            It1 = ((( Fix_inp_ext iv) . w) . E1) by A26, A31, A36, PRALG_1:def 19;

            hence contradiction by A6, A7, A20, A32, A39, A38, A37, A40, CIRCUIT1: 14;

          end;

        end;

        hence thesis;

      end;

    end

    theorem :: CIRCUIT2:8

    

     Th8: for SCS be non-empty Circuit of IIG, v be Vertex of IIG, iv be InputValues of SCS holds ( IGTree (v,iv)) = ((( Fix_inp_ext iv) . v) . ( IGTree (v,iv)))

    proof

      let SCS be non-empty Circuit of IIG, v be Vertex of IIG, iv be InputValues of SCS;

      reconsider igt = ( IGTree (v,iv)) as Element of (the Sorts of ( FreeEnv SCS) . v);

      ex e be Element of (the Sorts of ( FreeEnv SCS) . v) st ( card e) = ( size (v,SCS)) & ( IGTree (v,iv)) = ((( Fix_inp_ext iv) . v) . e) by Def3;

      then ( card igt) = ( size (v,SCS)) by Th7;

      hence thesis by Def3;

    end;

    theorem :: CIRCUIT2:9

    

     Th9: for SCS be non-empty Circuit of IIG, v be Vertex of IIG, iv be InputValues of SCS, p be DTree-yielding FinSequence st v in ( InnerVertices IIG) & ( dom p) = ( dom ( the_arity_of ( action_at v))) & for k be Element of NAT st k in ( dom p) holds (p . k) = ( IGTree ((( the_arity_of ( action_at v)) /. k),iv)) holds ( IGTree (v,iv)) = ( [( action_at v), the carrier of IIG] -tree p)

    proof

      let SCS be non-empty Circuit of IIG, v be Vertex of IIG, iv be InputValues of SCS, p be DTree-yielding FinSequence;

      assume that

       A1: v in ( InnerVertices IIG) and

       A2: ( dom p) = ( dom ( the_arity_of ( action_at v))) and

       A3: for k be Element of NAT st k in ( dom p) holds (p . k) = ( IGTree ((( the_arity_of ( action_at v)) /. k),iv));

      set U1 = ( FreeEnv SCS);

      set o = ( action_at v);

       A4:

      now

        let k be Nat;

        assume k in ( dom p);

        then (p . k) = ( IGTree ((( the_arity_of o) /. k),iv)) by A3;

        hence (p . k) in (the Sorts of U1 . (( the_arity_of o) /. k));

      end;

      ( len p) = ( len ( the_arity_of o)) by A2, FINSEQ_3: 29;

      then

      reconsider p99 = p as Element of ( Args (o,U1)) by A4, MSAFREE2: 5;

      set X = the Sorts of SCS;

      

       A5: ( dom the ResultSort of IIG) = the carrier' of IIG by FUNCT_2:def 1;

      

       A6: ( Result (o,U1)) = ((the Sorts of U1 * the ResultSort of IIG) . o) by MSUALG_1:def 5

      .= (the Sorts of U1 . (the ResultSort of IIG . o)) by A5, FUNCT_1: 13;

      

       A7: U1 = MSAlgebra (# ( FreeSort X), ( FreeOper X) #) & ( Args (o,U1)) = (((the Sorts of U1 # ) * the Arity of IIG) . o) by MSAFREE:def 14, MSUALG_1:def 4;

      then

      reconsider p9 = p99 as FinSequence of ( TS ( DTConMSA X)) by MSAFREE: 8;

      U1 = MSAlgebra (# ( FreeSort X), ( FreeOper X) #) by MSAFREE:def 14;

      

      then

       A8: ( Den (o,U1)) = (( FreeOper X) . o) by MSUALG_1:def 6

      .= ( DenOp (o,X)) by MSAFREE:def 13;

      ( Sym (o,X)) ==> ( roots p9) by A7, MSAFREE: 10;

      

      then

       A9: (( Den (o,U1)) . p) = (( Sym (o,X)) -tree p9) by A8, MSAFREE:def 12

      .= ( [o, the carrier of IIG] -tree p9) by MSAFREE:def 9;

      (the ResultSort of IIG . o) = ( the_result_sort_of o) by MSUALG_1:def 2

      .= v by A1, MSAFREE2:def 7;

      then

      reconsider t = ( [( action_at v), the carrier of IIG] -tree p) as Element of (the Sorts of ( FreeMSA X) . v) by A9, A6, FUNCT_2: 5;

      now

        let k be Element of NAT ;

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

        assume k in ( dom p);

        then

         A10: (p . k) = ( IGTree (v1,iv)) by A3;

        then

        reconsider ek = (p . k) as Element of (the Sorts of ( FreeEnv SCS) . v1);

        take ek;

        thus ek = (p . k);

        ex e1 be Element of (the Sorts of ( FreeMSA X) . v1) st ( card e1) = ( size (v1,SCS)) & ek = ((( Fix_inp_ext iv) . v1) . e1) by A10, Def3;

        hence ( card ek) = ( size (v1,SCS)) by Th7;

      end;

      then

       A11: ( card t) = ( size (v,SCS)) by A1, CIRCUIT1: 16;

      now

        let k be Element of NAT ;

        assume k in ( dom p);

        then (p . k) = ( IGTree ((( the_arity_of ( action_at v)) /. k),iv)) by A3;

        hence (p . k) = ((( Fix_inp_ext iv) . (( the_arity_of ( action_at v)) /. k)) . (p . k)) by Th8;

      end;

      then ( [( action_at v), the carrier of IIG] -tree p) = ((( Fix_inp_ext iv) . v) . t) by A1, Th4;

      hence thesis by A11, Def3;

    end;

    definition

      let IIG;

      let SCS be non-empty Circuit of IIG, v be Vertex of IIG, iv be InputValues of SCS;

      :: CIRCUIT2:def4

      func IGValue (v,iv) -> Element of (the Sorts of SCS . v) equals ((( Eval SCS) . v) . ( IGTree (v,iv)));

      coherence ;

    end

    theorem :: CIRCUIT2:10

    

     Th10: for SCS be non-empty Circuit of IIG, v be Vertex of IIG, iv be InputValues of SCS st v in ( InputVertices IIG) holds ( IGValue (v,iv)) = (iv . v)

    proof

      let SCS be non-empty Circuit of IIG, v be Vertex of IIG, iv be InputValues of SCS;

      set X = the Sorts of SCS;

      

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

      assume

       A2: v in ( InputVertices IIG);

      then

       A3: (iv . v) in (the Sorts of SCS . v) by MSAFREE2:def 5;

      then ( root-tree [(iv . v), v]) in ( FreeGen (v,the Sorts of SCS)) by MSAFREE:def 15;

      then ( root-tree [(iv . v), v]) in (( FreeSort the Sorts of SCS) . v);

      then

       A4: ( root-tree [(iv . v), v]) in ( FreeSort (the Sorts of SCS,v)) by MSAFREE:def 11;

      consider e be Element of (the Sorts of ( FreeEnv SCS) . v) such that ( card e) = ( size (v,SCS)) and

       A5: ( IGTree (v,iv)) = ((( Fix_inp_ext iv) . v) . e) by Def3;

      e in (the Sorts of ( FreeMSA 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 A1;

      then

       A6: e in ( FreeGen (v,the Sorts of SCS)) by A2, MSAFREE:def 15, MSAFREE2: 2;

      ( Fix_inp iv) c= ( Fix_inp_ext iv) by Def2;

      then

       A7: (( Fix_inp iv) . v) c= (( Fix_inp_ext iv) . v);

      

       A8: (( Fix_inp iv) . v) = (( FreeGen (v,the Sorts of SCS)) --> ( root-tree [(iv . v), v])) by A2, Def1;

      then e in ( dom (( Fix_inp iv) . v)) by A6;

      then ((( Fix_inp iv) . v) . e) = ((( Fix_inp_ext iv) . v) . e) by A7, GRFUNC_1: 2;

      

      hence ( IGValue (v,iv)) = ((( Eval SCS) . v) . ( root-tree [(iv . v), v])) by A5, A6, A8, FUNCOP_1: 7

      .= (iv . v) by A3, A4, MSAFREE2:def 9;

    end;

    theorem :: CIRCUIT2:11

    

     Th11: for SCS be non-empty Circuit of IIG, v be Vertex of IIG, iv be InputValues of SCS st v in ( SortsWithConstants IIG) holds ( IGValue (v,iv)) = (( Set-Constants SCS) . v)

    proof

      reconsider p = {} as DTree-yielding FinSequence;

      let SCS be non-empty Circuit of IIG, v be Vertex of IIG, iv be InputValues of SCS;

      assume

       A1: v in ( SortsWithConstants IIG);

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

      

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

      set X = the Sorts of SCS;

      set F = ( Eval SCS);

      

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

      

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

      set o = ( action_at v);

      

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

      then

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

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

      then

      consider x9 be SortSymbol of IIG such that

       A7: x9 = v and

       A8: x9 is with_const_op by A1;

      consider o1 be OperSymbol of IIG such that

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

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

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

      then

       A11: o = o1 by A1, A5, A7, A10, MSAFREE2:def 7;

      

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

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

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

      then

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

      reconsider Fx = (F # x) as Element of ( Args (o,SCS));

      F is_homomorphism (( FreeEnv SCS),SCS) by MSAFREE2:def 9;

      then

       A13: ((F . ( the_result_sort_of o)) . (( Den (o,( FreeEnv SCS))) . x)) = (( Den (o,SCS)) . Fx) by MSUALG_3:def 7;

      

       A14: ( FreeMSA X) = MSAlgebra (# ( FreeSort X), ( FreeOper X) #) by MSAFREE:def 14;

      

      then

       A15: ( Den (o,( FreeEnv SCS))) = (( FreeOper X) . o) by MSUALG_1:def 6

      .= ( DenOp (o,X)) by MSAFREE:def 13;

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

      then

       A16: p in (((( FreeSort X) # ) * the Arity of IIG) . o) by A14, MSUALG_1:def 4;

      then

      reconsider p9 = {} as FinSequence of ( TS ( DTConMSA X)) by MSAFREE: 8;

      ( Sym (o,X)) ==> ( roots p9) by A16, MSAFREE: 10;

      

      then

       A17: (( Den (o,( FreeEnv SCS))) . {} ) = (( Sym (o,X)) -tree p) by A15, MSAFREE:def 12

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

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

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

      then

       A18: e in ( rng ( Den (o,SCS))) by A6, A17, A13, FUNCT_1:def 3;

      ( 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 A4, FUNCT_1: 13;

      then

      reconsider e as Element of (the Sorts of SCS . v) by A6, A17, A13, MSUALG_1:def 2;

      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

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

      ex e be Element of (the Sorts of ( FreeEnv SCS) . v) st ( card e) = ( size (v,SCS)) & ( IGTree (v,iv)) = ((( Fix_inp_ext iv) . v) . e) by Def3;

      

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

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

    end;

    begin

    definition

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

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

      :: CIRCUIT2:def5

      func Following s -> State of SCS means

      : Def5: for v be Vertex of IIG holds (v in ( InputVertices IIG) implies (it . v) = (s . v)) & (v in ( InnerVertices IIG) implies (it . v) = (( Den (( action_at v),SCS)) . (( action_at v) depends_on_in s)));

      existence

      proof

        deffunc G( Vertex of IIG) = (( Den (( action_at $1),SCS)) . (( action_at $1) depends_on_in s));

        deffunc F( set) = (s . $1);

        defpred P[ set] means $1 in ( InputVertices IIG);

        consider f be ManySortedSet of the carrier of IIG such that

         A1: for v be Vertex of IIG st v in the carrier of IIG holds ( P[v] implies (f . v) = F(v)) & ( not P[v] implies (f . v) = G(v)) from PRE_CIRC:sch 2;

         A2:

        now

          let x be object;

          assume x in ( dom the Sorts of SCS);

          then

          reconsider v = x as Vertex of IIG by PARTFUN1:def 2;

          per cases ;

            suppose v in ( InputVertices IIG);

            then (f . v) = (s . v) by A1;

            hence (f . x) in (the Sorts of SCS . x) by CIRCUIT1: 4;

          end;

            suppose

             A3: not v in ( InputVertices IIG);

            v in the carrier of IIG;

            then v in (( InputVertices IIG) \/ ( InnerVertices IIG)) by XBOOLE_1: 45;

            then v in ( InnerVertices IIG) by A3, XBOOLE_0:def 3;

            then

             A4: ( the_result_sort_of ( action_at v)) = v by MSAFREE2:def 7;

            (f . x) = (( Den (( action_at v),SCS)) . (( action_at v) depends_on_in s)) by A1, A3;

            hence (f . x) in (the Sorts of SCS . x) by A4, CIRCUIT1: 8;

          end;

        end;

        ( dom f) = the carrier of IIG & ( dom the Sorts of SCS) = the carrier of IIG by PARTFUN1:def 2;

        then

        reconsider f as State of SCS by A2, CARD_3:def 5;

        take f;

        let v be Vertex of IIG;

        thus v in ( InputVertices IIG) implies (f . v) = (s . v) by A1;

        

         A5: ( InputVertices IIG) misses ( InnerVertices IIG) by XBOOLE_1: 79;

        assume v in ( InnerVertices IIG);

        then not v in ( InputVertices IIG) by A5, XBOOLE_0: 3;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let it1,it2 be State of SCS such that

         A6: for v be Vertex of IIG holds (v in ( InputVertices IIG) implies (it1 . v) = (s . v)) & (v in ( InnerVertices IIG) implies (it1 . v) = (( Den (( action_at v),SCS)) . (( action_at v) depends_on_in s))) and

         A7: for v be Vertex of IIG holds (v in ( InputVertices IIG) implies (it2 . v) = (s . v)) & (v in ( InnerVertices IIG) implies (it2 . v) = (( Den (( action_at v),SCS)) . (( action_at v) depends_on_in s)));

        assume

         A8: it1 <> it2;

        ( dom it2) = the carrier of IIG by CIRCUIT1: 3;

        then

        consider x be object such that

         A9: x in ( dom it1) and

         A10: (it1 . x) <> (it2 . x) by A8, CIRCUIT1: 3, FUNCT_1: 2;

        reconsider v = x as Vertex of IIG by A9, CIRCUIT1: 3;

        

         A11: v in ( InnerVertices IIG) implies (it1 . v) = (( Den (( action_at v),SCS)) . (( action_at v) depends_on_in s)) by A6;

        ( dom it1) = the carrier of IIG by CIRCUIT1: 3;

        then v in (( InputVertices IIG) \/ ( InnerVertices IIG)) by A9, XBOOLE_1: 45;

        then

         A12: v in ( InputVertices IIG) or v in ( InnerVertices IIG) by XBOOLE_0:def 3;

        v in ( InputVertices IIG) implies (it1 . v) = (s . v) by A6;

        hence contradiction by A7, A10, A12, A11;

      end;

    end

    theorem :: CIRCUIT2:12

    

     Th12: for SCS be non-empty Circuit of IIG, s be State of SCS, iv be InputValues of SCS st iv c= s holds iv c= ( Following s)

    proof

      let SCS be non-empty Circuit of IIG, s be State of SCS, iv be InputValues of SCS such that

       A1: iv c= s;

      now

        ( dom s) = the carrier of IIG by CIRCUIT1: 3

        .= ( dom ( Following s)) by CIRCUIT1: 3;

        hence ( dom iv) c= ( dom ( Following s)) by A1, RELAT_1: 11;

        let x be object such that

         A2: x in ( dom iv);

        

         A3: ( dom iv) = ( InputVertices IIG) by PARTFUN1:def 2;

        then

        reconsider v = x as Vertex of IIG by A2;

        (iv . v) = (s . v) by A1, A2, GRFUNC_1: 2;

        hence (iv . x) = (( Following s) . x) by A2, A3, Def5;

      end;

      hence thesis by GRFUNC_1: 2;

    end;

    definition

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

      let SCS be non-empty Circuit of IIG;

      let IT be State of SCS;

      :: CIRCUIT2:def6

      attr IT is stable means IT = ( Following IT);

    end

    definition

      let IIG;

      let SCS be non-empty Circuit of IIG, s be State of SCS, iv be InputValues of SCS;

      :: CIRCUIT2:def7

      func Following (s,iv) -> State of SCS equals ( Following (s +* iv));

      coherence ;

    end

    definition

      let IIG;

      let SCS be non-empty Circuit of IIG, InpFs be InputFuncs of SCS, s be State of SCS;

      :: CIRCUIT2:def8

      func InitialComp (s,InpFs) -> State of SCS equals ((s +* ( 0 -th_InputValues InpFs)) +* ( Set-Constants SCS));

      coherence

      proof

        set sc = ( Set-Constants SCS);

        

         A1: ( dom sc) = ( SortsWithConstants IIG) by PARTFUN1:def 2;

         A2:

        now

          let x be set;

          assume

           A3: x in ( dom sc);

          then

          reconsider v = x as Vertex of IIG by A1;

          (sc . x) in ( Constants (SCS,v)) by A3, CIRCUIT1:def 1;

          hence (sc . x) in (the Sorts of SCS . x);

        end;

        ( dom the Sorts of SCS) = the carrier of IIG by PARTFUN1:def 2;

        hence thesis by A1, A2, PRE_CIRC: 6;

      end;

    end

    definition

      let IIG;

      let SCS be non-empty Circuit of IIG, InpFs be InputFuncs of SCS, s be State of SCS;

      :: CIRCUIT2:def9

      func Computation (s,InpFs) -> sequence of ( product the Sorts of SCS) means

      : Def9: (it . 0 ) = ( InitialComp (s,InpFs)) & for i be Nat holds (it . (i + 1)) = ( Following ((it . i),((i + 1) -th_InputValues InpFs)));

      correctness

      proof

        deffunc F( Nat, State of SCS) = ( Following ($2,(($1 + 1) -th_InputValues InpFs)));

        thus (ex IT be sequence of ( product the Sorts of SCS) st (IT . 0 ) = ( InitialComp (s,InpFs)) & for i be Nat holds (IT . (i + 1)) = F(i,.)) & for IT1,IT2 be sequence of ( product the Sorts of SCS) st ((IT1 . 0 ) = ( InitialComp (s,InpFs)) & for i be Nat holds (IT1 . (i + 1)) = F(i,.)) & ((IT2 . 0 ) = ( InitialComp (s,InpFs)) & for i be Nat holds (IT2 . (i + 1)) = F(i,.)) holds IT1 = IT2 from PRE_CIRC:sch 3;

      end;

    end

    reserve SCS for non-empty Circuit of IIG;

    reserve s for State of SCS;

    reserve iv for InputValues of SCS;

    theorem :: CIRCUIT2:13

    

     Th13: for k be Nat st for v be Vertex of IIG st ( depth (v,SCS)) <= k holds (s . v) = ( IGValue (v,iv)) holds for v1 be Vertex of IIG st ( depth (v1,SCS)) <= (k + 1) holds (( Following s) . v1) = ( IGValue (v1,iv))

    proof

      let k be Nat such that

       A1: for v be Vertex of IIG st ( depth (v,SCS)) <= k holds (s . v) = ( IGValue (v,iv));

      let v be Vertex of IIG such that

       A2: ( depth (v,SCS)) <= (k + 1);

      v in the carrier of IIG;

      then

       A3: v in (( InputVertices IIG) \/ ( InnerVertices IIG)) by XBOOLE_1: 45;

      per cases by A3, XBOOLE_0:def 3;

        suppose

         A4: v in ( InputVertices IIG);

        then

         A5: ( depth (v,SCS)) = 0 by CIRCUIT1: 18;

        

        thus (( Following s) . v) = (s . v) by A4, Def5

        .= ( IGValue (v,iv)) by A1, A5, NAT_1: 2;

      end;

        suppose

         A6: v in ( InnerVertices IIG);

        set F = ( Eval SCS);

        set X = the Sorts of SCS;

        set U1 = ( FreeEnv SCS);

        set o = ( action_at v);

        set taofo = ( the_arity_of o);

        deffunc F( Nat) = ( IGTree ((taofo /. $1) qua Vertex of IIG,iv));

        consider p be FinSequence such that

         A7: ( len p) = ( len ( the_arity_of o)) and

         A8: for k be Nat st k in ( dom p) holds (p . k) = F(k) from FINSEQ_1:sch 2;

        

         A9: for k be Element of NAT st k in ( dom p) holds (p . k) = F(k) by A8;

         A10:

        now

          let k be Nat;

          assume k in ( dom p);

          then (p . k) = ( IGTree ((taofo /. k),iv)) by A8;

          hence (p . k) in (the Sorts of U1 . (( the_arity_of o) /. k));

        end;

        U1 = MSAlgebra (# ( FreeSort X), ( FreeOper X) #) by MSAFREE:def 14;

        

        then

         A11: ( Den (o,U1)) = (( FreeOper X) . o) by MSUALG_1:def 6

        .= ( DenOp (o,X)) by MSAFREE:def 13;

        reconsider ods = (o depends_on_in s) as Function;

        

         A12: F is_homomorphism (U1,SCS) by MSAFREE2:def 9;

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

        

        then

         A13: (((the Sorts of SCS # ) * the Arity of IIG) . o) = ((the Sorts of SCS # ) . (the Arity of IIG . o)) by FUNCT_1: 13

        .= ((the Sorts of SCS # ) . ( the_arity_of o)) by MSUALG_1:def 1

        .= ( product (the Sorts of SCS * ( the_arity_of o))) by FINSEQ_2:def 5;

        

         A14: ( dom p) = ( dom ( the_arity_of o)) by A7, FINSEQ_3: 29;

        reconsider p as Element of ( Args (o,U1)) by A7, A10, MSAFREE2: 5;

        

         A15: U1 = MSAlgebra (# ( FreeSort X), ( FreeOper X) #) & ( Args (o,U1)) = (((the Sorts of U1 # ) * the Arity of IIG) . o) by MSAFREE:def 14, MSUALG_1:def 4;

        then

        reconsider p9 = p as FinSequence of ( TS ( DTConMSA X)) by MSAFREE: 8;

        ( Sym (o,X)) ==> ( roots p9) by A15, MSAFREE: 10;

        

        then

         A16: (( Den (o,U1)) . p) = (( Sym (o,X)) -tree p9) by A11, MSAFREE:def 12

        .= ( [o, the carrier of IIG] -tree p9) by MSAFREE:def 9

        .= ( IGTree (v,iv)) by A6, A9, A14, Th9;

        reconsider Fp = (F # p) as Function;

        

         A17: ( Args (o,SCS)) = (((the Sorts of SCS # ) * the Arity of IIG) . o) by MSUALG_1:def 4;

        now

          ( dom the Sorts of SCS) = the carrier of IIG & ( rng ( the_arity_of o)) c= the carrier of IIG by FINSEQ_1:def 4, PARTFUN1:def 2;

          

          hence ( dom ( the_arity_of o)) = ( dom (the Sorts of SCS * ( the_arity_of o))) by RELAT_1: 27

          .= ( dom Fp) by A13, A17, CARD_3: 9;

          ( dom s) = the carrier of IIG & ( rng ( the_arity_of o)) c= the carrier of IIG by CIRCUIT1: 3, FINSEQ_1:def 4;

          

          hence ( dom ( the_arity_of o)) = ( dom (s * ( the_arity_of o))) by RELAT_1: 27

          .= ( dom ods) by CIRCUIT1:def 3;

          let x be object;

          reconsider v1 = (( the_arity_of o) /. x) as Element of IIG;

          assume

           A18: x in ( dom ( the_arity_of o));

          then

          reconsider x9 = x as Element of NAT ;

          

           A19: v1 = (( the_arity_of o) . x9) by A18, PARTFUN1:def 6;

          then v1 in ( rng ( the_arity_of o)) by A18, FUNCT_1:def 3;

          then ( depth (v1,SCS)) < (k + 1) by A2, A6, CIRCUIT1: 19, XXREAL_0: 2;

          then

           A20: ( depth (v1,SCS)) <= k by NAT_1: 13;

          

          thus (Fp . x) = ((F . v1) . (p9 . x9)) by A14, A18, MSUALG_3:def 6

          .= ( IGValue (v1,iv)) by A8, A14, A18

          .= (s . v1) by A1, A20

          .= ((s * ( the_arity_of o)) . x) by A18, A19, FUNCT_1: 13

          .= (ods . x) by CIRCUIT1:def 3;

        end;

        then (F # p) = (o depends_on_in s) by FUNCT_1: 2;

        

        hence (( Following s) . v) = (( Den (o,SCS)) . (F # p)) by A6, Def5

        .= ((F . ( the_result_sort_of o)) . (( Den (o,U1)) . p)) by A12, MSUALG_3:def 7

        .= ( IGValue (v,iv)) by A6, A16, MSAFREE2:def 7;

      end;

    end;

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

    reserve SCS for non-empty Circuit of IIG;

    reserve InpFs for InputFuncs of SCS;

    reserve s for State of SCS;

    reserve iv for InputValues of SCS;

    theorem :: CIRCUIT2:14

    

     Th14: ( commute InpFs) is constant & ( InputVertices IIG) is non empty implies for s, iv st iv = (( commute InpFs) . 0 ) holds for k be Nat holds iv c= (( Computation (s,InpFs)) . k)

    proof

      assume that

       A1: ( commute InpFs) is constant and

       A2: ( InputVertices IIG) is non empty;

      

       A3: ( dom ( commute InpFs)) = NAT by A2, PRE_CIRC: 5;

      let s, iv;

      assume

       A4: iv = (( commute InpFs) . 0 );

      let k be Nat;

      

       A5: k in NAT by ORDINAL1:def 12;

      IIG is with_input_V by A2;

      

      then

       A6: (k -th_InputValues InpFs) = (( commute InpFs) . k) by CIRCUIT1:def 2

      .= iv by A1, A4, A3, FUNCT_1:def 10, A5;

      set Ck = (( Computation (s,InpFs)) . k);

      ( dom iv) = ( InputVertices IIG) & ( dom ( Set-Constants SCS)) = ( SortsWithConstants IIG) by PARTFUN1:def 2;

      then

       A7: ( dom iv) misses ( dom ( Set-Constants SCS)) by MSAFREE2: 4;

      per cases by NAT_1: 6;

        suppose

         A8: k = 0 ;

        

        then Ck = ( InitialComp (s,InpFs)) by Def9

        .= ((s +* ( 0 -th_InputValues InpFs)) +* ( Set-Constants SCS));

        hence thesis by A6, A7, A8, FUNCT_4: 25, FUNCT_4: 124;

      end;

        suppose ex n be Nat st k = (n + 1);

        then

        consider n be Nat such that

         A9: k = (n + 1);

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

        reconsider Cn = (( Computation (s,InpFs)) . n) as State of SCS;

        Ck = ( Following (Cn,(k -th_InputValues InpFs))) by A9, Def9

        .= ( Following (Cn +* iv)) by A6;

        hence thesis by Th12, FUNCT_4: 25;

      end;

    end;

    theorem :: CIRCUIT2:15

    for n be Element of NAT st ( commute InpFs) is constant & ( InputVertices IIG) is non empty & (( Computation (s,InpFs)) . n) is stable holds for m be Nat st n <= m holds (( Computation (s,InpFs)) . n) = (( Computation (s,InpFs)) . m)

    proof

      let n be Element of NAT such that

       A1: ( commute InpFs) is constant and

       A2: ( InputVertices IIG) is non empty and

       A3: (( Computation (s,InpFs)) . n) is stable;

      defpred P[ Nat] means n <= $1 implies (( Computation (s,InpFs)) . n) = (( Computation (s,InpFs)) . $1);

       A4:

      now

        let m be Nat;

        assume

         A5: P[m];

        thus P[(m + 1)]

        proof

          

           A6: IIG is with_input_V by A2;

          then

          reconsider iv = (( commute InpFs) . 0 ) as InputValues of SCS by CIRCUIT1: 2;

          reconsider Ckm = (( Computation (s,InpFs)) . m) as State of SCS;

          

           A7: ( dom ( commute InpFs)) = NAT by A2, PRE_CIRC: 5;

          ((m + 1) -th_InputValues InpFs) = (( commute InpFs) . (m + 1)) by A6, CIRCUIT1:def 2

          .= iv by A1, A7, FUNCT_1:def 10;

          then

           A8: ((m + 1) -th_InputValues InpFs) c= (( Computation (s,InpFs)) . m) by A1, A2, Th14;

          assume

           A9: n <= (m + 1);

          per cases by A9, NAT_1: 8;

            suppose n <= m;

            

            hence (( Computation (s,InpFs)) . n) = ( Following Ckm) by A3, A5

            .= ( Following ((( Computation (s,InpFs)) . m),((m + 1) -th_InputValues InpFs))) by A8, FUNCT_4: 98

            .= (( Computation (s,InpFs)) . (m + 1)) by Def9;

          end;

            suppose n = (m + 1);

            hence thesis;

          end;

        end;

      end;

      

       A10: P[ 0 ] by NAT_1: 3;

      thus for m be Nat holds P[m] from NAT_1:sch 2( A10, A4);

    end;

    theorem :: CIRCUIT2:16

    

     Th16: ( commute InpFs) is constant & ( InputVertices IIG) is non empty implies for s, iv st iv = (( commute InpFs) . 0 ) holds for k be Nat, v be Vertex of IIG st ( depth (v,SCS)) <= k holds ((( Computation (s,InpFs)) . k) qua Element of ( product the Sorts of SCS) . v) = ( IGValue (v,iv))

    proof

      assume that

       A1: ( commute InpFs) is constant and

       A2: ( InputVertices IIG) is non empty;

      let s, iv;

      assume

       A3: iv = (( commute InpFs) . 0 );

      defpred P[ Nat] means for v be Vertex of IIG st ( depth (v,SCS)) <= $1 holds ((( Computation (s,InpFs)) . $1) qua State of SCS . v) = ( IGValue (v,iv));

      

       A4: IIG is with_input_V by A2;

      

       A5: P[ 0 ]

      proof

        let v be Vertex of IIG;

        assume ( depth (v,SCS)) <= 0 ;

        then

         A6: ( depth (v,SCS)) = 0 by NAT_1: 3;

        

         A7: (( Computation (s,InpFs)) . 0 ) = ( InitialComp (s,InpFs)) by Def9

        .= ((s +* ( 0 -th_InputValues InpFs)) +* ( Set-Constants SCS));

        per cases by A6, CIRCUIT1: 18;

          suppose

           A8: v in ( InputVertices IIG);

          

           A9: ( dom ( 0 -th_InputValues InpFs)) = ( InputVertices IIG) by PARTFUN1:def 2;

          ( InputVertices IIG) misses ( SortsWithConstants IIG) by MSAFREE2: 4;

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

          then not v in ( dom ( Set-Constants SCS)) by PARTFUN1:def 2;

          

          hence ((( Computation (s,InpFs)) . 0 ) qua Element of ( product the Sorts of SCS) . v) = ((s +* ( 0 -th_InputValues InpFs)) . v) by A7, FUNCT_4: 11

          .= (( 0 -th_InputValues InpFs) . v) by A8, A9, FUNCT_4: 13

          .= (iv . v) by A4, A3, CIRCUIT1:def 2

          .= ( IGValue (v,iv)) by A8, Th10;

        end;

          suppose

           A10: v in ( SortsWithConstants IIG);

          then v in ( dom ( Set-Constants SCS)) by PARTFUN1:def 2;

          

          hence ((( Computation (s,InpFs)) . 0 ) qua Element of ( product the Sorts of SCS) . v) = (( Set-Constants SCS) . v) by A7, FUNCT_4: 13

          .= ( IGValue (v,iv)) by A10, Th11;

        end;

      end;

      

       A11: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        reconsider Ck = (( Computation (s,InpFs)) . k) as State of SCS;

        assume

         A12: P[k];

        let v be Vertex of IIG such that

         A13: ( depth (v,SCS)) <= (k + 1);

        

         A14: ( dom ( commute InpFs)) = NAT by A2, PRE_CIRC: 5;

        

         A15: ((k + 1) -th_InputValues InpFs) = (( commute InpFs) . (k + 1)) by A4, CIRCUIT1:def 2

        .= (( commute InpFs) . 0 ) by A1, A14, FUNCT_1:def 10;

        

         A16: iv c= Ck by A1, A2, A3, Th14;

        

        thus ((( Computation (s,InpFs)) . (k + 1)) qua State of SCS . v) = (( Following (Ck,((k + 1) -th_InputValues InpFs))) . v) by Def9

        .= (( Following Ck) . v) by A3, A15, A16, FUNCT_4: 98

        .= ( IGValue (v,iv)) by A12, A13, Th13;

      end;

      thus for k be Nat holds P[k] from NAT_1:sch 2( A5, A11);

    end;

    theorem :: CIRCUIT2:17

    

     Th17: ( commute InpFs) is constant & ( InputVertices IIG) is non empty & iv = (( commute InpFs) . 0 ) implies for s be State of SCS, v be Vertex of IIG, n be Element of NAT st n = ( depth SCS) holds ((( Computation (s,InpFs)) . n) qua State of SCS . v) = ( IGValue (v,iv))

    proof

      assume

       A1: ( commute InpFs) is constant & ( InputVertices IIG) is non empty & iv = (( commute InpFs) . 0 );

      let s be State of SCS, v be Vertex of IIG;

      

       A2: ( depth (v,SCS)) <= ( depth SCS) by CIRCUIT1: 17;

      let n be Element of NAT ;

      assume n = ( depth SCS);

      hence thesis by A1, A2, Th16;

    end;

    theorem :: CIRCUIT2:18

    ( commute InpFs) is constant & ( InputVertices IIG) is non empty implies for s be State of SCS, n be Element of NAT st n = ( depth SCS) holds (( Computation (s,InpFs)) . n) is stable

    proof

      assume that

       A1: ( commute InpFs) is constant and

       A2: ( InputVertices IIG) is non empty;

      

       A3: ( dom ( commute InpFs)) = NAT by A2, PRE_CIRC: 5;

      

       A4: IIG is with_input_V by A2;

      then

      reconsider iv = (( commute InpFs) . 0 ) as InputValues of SCS by CIRCUIT1: 2;

      let s be State of SCS, n be Element of NAT such that

       A5: n = ( depth SCS);

      reconsider Cn = (( Computation (s,InpFs)) . n) as State of SCS;

      

       A6: iv c= Cn by A1, A2, Th14;

      

       A7: ((n + 1) -th_InputValues InpFs) = (( commute InpFs) . (n + 1)) by A4, CIRCUIT1:def 2

      .= (( commute InpFs) . 0 ) by A1, A3, FUNCT_1:def 10;

      reconsider Cn1 = (( Computation (s,InpFs)) . (n + 1)) as State of SCS;

      now

        thus the carrier of IIG = ( dom Cn) by CIRCUIT1: 3;

        thus the carrier of IIG = ( dom Cn1) by CIRCUIT1: 3;

        let x be object;

        assume x in the carrier of IIG;

        then

        reconsider x9 = x as Vertex of IIG;

        

         A8: ( depth (x9,SCS)) <= n by A5, CIRCUIT1: 17;

        then (Cn . x9) = ( IGValue (x9,iv)) by A1, A2, Th16;

        hence (Cn . x) = (Cn1 . x) by A1, A2, A8, Th16, NAT_1: 12;

      end;

      

      hence (( Computation (s,InpFs)) . n) = (( Computation (s,InpFs)) . (n + 1))

      .= ( Following (Cn,((n + 1) -th_InputValues InpFs))) by Def9

      .= ( Following (( Computation (s,InpFs)) . n)) by A7, A6, FUNCT_4: 98;

    end;

    theorem :: CIRCUIT2:19

    ( commute InpFs) is constant & ( InputVertices IIG) is non empty implies for s1,s2 be State of SCS holds (( Computation (s1,InpFs)) . ( depth SCS)) = (( Computation (s2,InpFs)) . ( depth SCS))

    proof

      assume that

       A1: ( commute InpFs) is constant and

       A2: ( InputVertices IIG) is non empty;

      IIG is with_input_V by A2;

      then

      reconsider iv = (( commute InpFs) . 0 ) as InputValues of SCS by CIRCUIT1: 2;

      reconsider dSCS = ( depth SCS) as Element of NAT by ORDINAL1:def 12;

      let s1,s2 be State of SCS;

      reconsider Cs1 = (( Computation (s1,InpFs)) . dSCS) as State of SCS;

      reconsider Cs2 = (( Computation (s2,InpFs)) . dSCS) as State of SCS;

      now

        thus the carrier of IIG = ( dom Cs1) by CIRCUIT1: 3;

        thus the carrier of IIG = ( dom Cs2) by CIRCUIT1: 3;

        let x be object;

        assume x in the carrier of IIG;

        then

        reconsider x9 = x as Vertex of IIG;

        (Cs1 . x9) = ( IGValue (x9,iv)) by A1, A2, Th17;

        hence (Cs1 . x) = (Cs2 . x) by A1, A2, Th17;

      end;

      hence thesis;

    end;