circtrm1.miz



    begin

    theorem :: CIRCTRM1:1

    

     Th1: for S be non empty non void ManySortedSign holds for A be non-empty MSAlgebra over S holds for V be Variables of A holds for t be Term of S, V, T be c-Term of A, V st T = t holds ( the_sort_of T) = ( the_sort_of t)

    proof

      let S be non empty non void ManySortedSign;

      let A be non-empty MSAlgebra over S;

      let V be Variables of A;

      defpred P[ set] means for t9 be Term of S, V, T be c-Term of A, V st t9 = $1 & T = t9 holds ( the_sort_of T) = ( the_sort_of t9);

      

       A1: for s be SortSymbol of S, v be Element of (V . s) holds P[( root-tree [v, s])]

      proof

        let s be SortSymbol of S, v be Element of (V . s);

        let t be Term of S, V, T be c-Term of A, V;

        assume that

         A2: t = ( root-tree [v, s]) and

         A3: T = t;

        ( the_sort_of t) = s by A2, MSATERM: 14;

        hence thesis by A2, A3, MSATERM: 16;

      end;

      

       A4: for o be OperSymbol of S, p be ArgumentSeq of ( Sym (o,V)) st for t9 be Term of S, V st t9 in ( rng p) holds P[t9] holds P[( [o, the carrier of S] -tree p)]

      proof

        let o be OperSymbol of S;

        let p be ArgumentSeq of ( Sym (o,V));

        assume for t9 be Term of S, V st t9 in ( rng p) holds for t be Term of S, V, T be c-Term of A, V st t = t9 & T = t holds ( the_sort_of T) = ( the_sort_of t);

        let t be Term of S, V, T be c-Term of A, V;

        assume t = ( [o, the carrier of S] -tree p);

        then

         A5: (t . {} ) = [o, the carrier of S] by TREES_4:def 4;

        then ( the_sort_of t) = ( the_result_sort_of o) by MSATERM: 17;

        hence thesis by A5, MSATERM: 17;

      end;

      for t be Term of S, V holds P[t] from MSATERM:sch 1( A1, A4);

      hence thesis;

    end;

    definition

      let S be non empty non void ManySortedSign;

      let V be non-empty ManySortedSet of the carrier of S;

      let X be non empty Subset of (S -Terms V);

      :: CIRCTRM1:def1

      func X -CircuitStr -> non empty strict ManySortedSign equals ManySortedSign (# ( Subtrees X), ( [:the carrier' of S, {the carrier of S}:] -Subtrees X), ( [:the carrier' of S, {the carrier of S}:] -ImmediateSubtrees X), ( incl ( [:the carrier' of S, {the carrier of S}:] -Subtrees X)) #);

      correctness ;

    end

    registration

      let S be non empty non void ManySortedSign;

      let V be non-empty ManySortedSet of the carrier of S;

      let X be non empty Subset of (S -Terms V);

      cluster (X -CircuitStr ) -> unsplit;

      coherence ;

    end

    reserve S for non empty non void ManySortedSign,

V for non-empty ManySortedSet of the carrier of S,

A for non-empty MSAlgebra over S,

X for non empty Subset of (S -Terms V),

t for Element of X;

    theorem :: CIRCTRM1:2

    (X -CircuitStr ) is void iff for t be Element of X holds t is root & not (t . {} ) in [:the carrier' of S, {the carrier of S}:] by TREES_9: 25;

    theorem :: CIRCTRM1:3

    

     Th3: X is SetWithCompoundTerm of S, V iff (X -CircuitStr ) is non void

    proof

      hereby

        assume X is SetWithCompoundTerm of S, V;

        then

        consider t be CompoundTerm of S, V such that

         A1: t in X by MSATERM:def 7;

        (t . {} ) in [:the carrier' of S, {the carrier of S}:] by MSATERM:def 6;

        hence (X -CircuitStr ) is non void by A1, TREES_9: 25;

      end;

      assume (X -CircuitStr ) is non void;

      then

      consider t such that

       A2: not t is root or (t . {} ) in [:the carrier' of S, {the carrier of S}:] by TREES_9: 25;

      t is CompoundTerm of S, V by A2, MSATERM: 28, MSATERM:def 6;

      hence thesis by MSATERM:def 7;

    end;

    registration

      let S be non empty non void ManySortedSign;

      let V be non-empty ManySortedSet of the carrier of S;

      let X be SetWithCompoundTerm of S, V;

      cluster (X -CircuitStr ) -> non void;

      coherence by Th3;

    end

    theorem :: CIRCTRM1:4

    

     Th4: (for v be Vertex of (X -CircuitStr ) holds v is Term of S, V) & for s be set st s in the carrier' of (X -CircuitStr ) holds s is CompoundTerm of S, V

    proof

      set C = [:the carrier' of S, {the carrier of S}:];

      hereby

        let v be Vertex of (X -CircuitStr );

        consider t be Element of X, p be Node of t such that

         A1: v = (t | p) by TREES_9: 19;

        thus v is Term of S, V by A1;

      end;

      let s be set;

      assume s in the carrier' of (X -CircuitStr );

      then

      consider t be Element of X, p be Node of t such that

       A2: s = (t | p) and

       A3: not p in ( Leaves ( dom t)) or (t . p) in C by TREES_9: 24;

      reconsider s as Term of S, V by A2;

      reconsider e = {} as Node of (t | p) by TREES_1: 22;

      

       A4: ( dom (t | p)) = (( dom t) qua Tree | p qua FinSequence of NAT ) by TREES_2:def 10;

      p = (p ^ e) by FINSEQ_1: 34;

      then

       A5: (t . p) = (s . e) by A2, A4, TREES_2:def 10;

      p in ( Leaves ( dom t)) iff s is root by A2, TREES_9: 6;

      hence thesis by A3, A5, MSATERM: 28, MSATERM:def 6;

    end;

    theorem :: CIRCTRM1:5

    

     Th5: for t be Vertex of (X -CircuitStr ) holds t in the carrier' of (X -CircuitStr ) iff t is CompoundTerm of S, V

    proof

      let t be Vertex of (X -CircuitStr );

      thus t in the carrier' of (X -CircuitStr ) implies t is CompoundTerm of S, V by Th4;

      set C = [:the carrier' of S, {the carrier of S}:];

      consider tt be Element of X, p be Node of tt such that

       A1: t = (tt | p) by TREES_9: 19;

      assume t is CompoundTerm of S, V;

      then

      reconsider t9 = t as CompoundTerm of S, V;

      

       A2: (t9 . {} ) in C by MSATERM:def 6;

      

       A3: (p ^ ( <*> NAT )) = p by FINSEQ_1: 34;

       {} in (( dom tt) | p) by TREES_1: 22;

      then (tt . p) in C by A1, A2, A3, TREES_2:def 10;

      hence thesis by A1, TREES_9: 24;

    end;

    registration

      let S, V;

      let X be SetWithCompoundTerm of S, V, g be Gate of (X -CircuitStr );

      cluster ( the_arity_of g) -> DTree-yielding;

      coherence ;

    end

    registration

      let S be non empty non void ManySortedSign;

      let V be non-empty ManySortedSet of the carrier of S;

      let X be non empty Subset of (S -Terms V);

      cluster -> finite Function-like Relation-like for Vertex of (X -CircuitStr );

      coherence by Th4;

    end

    registration

      let S be non empty non void ManySortedSign;

      let V be non-empty ManySortedSet of the carrier of S;

      let X be non empty Subset of (S -Terms V);

      cluster -> DecoratedTree-like for Vertex of (X -CircuitStr );

      coherence ;

    end

    registration

      let S be non empty non void ManySortedSign;

      let V be non-empty ManySortedSet of the carrier of S;

      let X be SetWithCompoundTerm of S, V;

      cluster -> finite Function-like Relation-like for Gate of (X -CircuitStr );

      coherence by Th4;

    end

    registration

      let S be non empty non void ManySortedSign;

      let V be non-empty ManySortedSet of the carrier of S;

      let X be SetWithCompoundTerm of S, V;

      cluster -> DecoratedTree-like for Gate of (X -CircuitStr );

      coherence ;

    end

    theorem :: CIRCTRM1:6

    

     Th6: for X1,X2 be non empty Subset of (S -Terms V) holds the Arity of (X1 -CircuitStr ) tolerates the Arity of (X2 -CircuitStr ) & the ResultSort of (X1 -CircuitStr ) tolerates the ResultSort of (X2 -CircuitStr )

    proof

      let t1,t2 be non empty Subset of (S -Terms V);

      set C = [:the carrier' of S, {the carrier of S}:];

      

       A1: ( dom (C -ImmediateSubtrees t1)) = (C -Subtrees t1) by FUNCT_2:def 1;

      

       A2: ( dom (C -ImmediateSubtrees t2)) = (C -Subtrees t2) by FUNCT_2:def 1;

      hereby

        let x be object;

        assume

         A3: x in (( dom the Arity of (t1 -CircuitStr )) /\ ( dom the Arity of (t2 -CircuitStr )));

        then

         A4: x in ( dom the Arity of (t1 -CircuitStr )) by XBOOLE_0:def 4;

        

         A5: x in ( dom the Arity of (t2 -CircuitStr )) by A3, XBOOLE_0:def 4;

        reconsider u = x as Element of ( Subtrees t1) by A1, A4;

        ((C -ImmediateSubtrees t1) . x) in (( Subtrees t1) * ) by A1, A4, FUNCT_2: 5;

        then

        reconsider y1 = (the Arity of (t1 -CircuitStr ) . x) as FinSequence of ( Subtrees t1) by FINSEQ_1:def 11;

        (the Arity of (t2 -CircuitStr ) . x) in (( Subtrees t2) * ) by A2, A5, FUNCT_2: 5;

        then

        reconsider y2 = (the Arity of (t2 -CircuitStr ) . x) as FinSequence of ( Subtrees t2) by FINSEQ_1:def 11;

        

         A6: (for t be Element of t1 holds t is finite) & for t be Element of t2 holds t is finite;

        then

         A7: u = ((u . {} ) -tree y1) by A1, A4, TREES_9:def 13;

        u = ((u . {} ) -tree y2) by A2, A5, A6, TREES_9:def 13;

        hence (the Arity of (t1 -CircuitStr ) . x) = (the Arity of (t2 -CircuitStr ) . x) by A7, TREES_4: 15;

      end;

      let x be object;

      assume

       A8: x in (( dom the ResultSort of (t1 -CircuitStr )) /\ ( dom the ResultSort of (t2 -CircuitStr )));

      then

       A9: x in ( dom the ResultSort of (t1 -CircuitStr )) by XBOOLE_0:def 4;

      

       A10: x in ( dom the ResultSort of (t2 -CircuitStr )) by A8, XBOOLE_0:def 4;

      

      thus (the ResultSort of (t1 -CircuitStr ) . x) = x by A9, FUNCT_1: 18

      .= (the ResultSort of (t2 -CircuitStr ) . x) by A10, FUNCT_1: 18;

    end;

    registration

      let X,Y be constituted-DTrees set;

      cluster (X \/ Y) -> constituted-DTrees;

      coherence by TREES_3: 9;

    end

    theorem :: CIRCTRM1:7

    

     Th7: for X1,X2 be constituted-DTrees non empty set holds ( Subtrees (X1 \/ X2)) = (( Subtrees X1) \/ ( Subtrees X2))

    proof

      let X1,X2 be constituted-DTrees non empty set;

      hereby

        let x be object;

        assume x in ( Subtrees (X1 \/ X2));

        then

        consider t be Element of (X1 \/ X2), n be Node of t such that

         A1: x = (t | n) by TREES_9: 19;

        t in X1 or t in X2 by XBOOLE_0:def 3;

        then x in ( Subtrees X1) or x in ( Subtrees X2) by A1, TREES_9: 19;

        hence x in (( Subtrees X1) \/ ( Subtrees X2)) by XBOOLE_0:def 3;

      end;

      let x be object;

      assume

       A2: x in (( Subtrees X1) \/ ( Subtrees X2));

      per cases by A2, XBOOLE_0:def 3;

        suppose x in ( Subtrees X1);

        then

        consider t be Element of X1, n be Node of t such that

         A3: x = (t | n) by TREES_9: 19;

        t is Element of (X1 \/ X2) by XBOOLE_0:def 3;

        hence thesis by A3, TREES_9: 19;

      end;

        suppose x in ( Subtrees X2);

        then

        consider t be Element of X2, n be Node of t such that

         A4: x = (t | n) by TREES_9: 19;

        t is Element of (X1 \/ X2) by XBOOLE_0:def 3;

        hence thesis by A4, TREES_9: 19;

      end;

    end;

    theorem :: CIRCTRM1:8

    

     Th8: for X1,X2 be constituted-DTrees non empty set, C be set holds (C -Subtrees (X1 \/ X2)) = ((C -Subtrees X1) \/ (C -Subtrees X2))

    proof

      let X1,X2 be constituted-DTrees non empty set, C be set;

      hereby

        let x be object;

        assume x in (C -Subtrees (X1 \/ X2));

        then

        consider t be Element of (X1 \/ X2), n be Node of t such that

         A1: x = (t | n) and

         A2: not n in ( Leaves ( dom t)) or (t . n) in C by TREES_9: 24;

        t in X1 or t in X2 by XBOOLE_0:def 3;

        then x in (C -Subtrees X1) or x in (C -Subtrees X2) by A1, A2, TREES_9: 24;

        hence x in ((C -Subtrees X1) \/ (C -Subtrees X2)) by XBOOLE_0:def 3;

      end;

      let x be object;

      assume

       A3: x in ((C -Subtrees X1) \/ (C -Subtrees X2));

      per cases by A3, XBOOLE_0:def 3;

        suppose x in (C -Subtrees X1);

        then

        consider t be Element of X1, n be Node of t such that

         A4: x = (t | n) and

         A5: not n in ( Leaves ( dom t)) or (t . n) in C by TREES_9: 24;

        t is Element of (X1 \/ X2) by XBOOLE_0:def 3;

        hence thesis by A4, A5, TREES_9: 24;

      end;

        suppose x in (C -Subtrees X2);

        then

        consider t be Element of X2, n be Node of t such that

         A6: x = (t | n) and

         A7: not n in ( Leaves ( dom t)) or (t . n) in C by TREES_9: 24;

        t is Element of (X1 \/ X2) by XBOOLE_0:def 3;

        hence thesis by A6, A7, TREES_9: 24;

      end;

    end;

    theorem :: CIRCTRM1:9

    

     Th9: for X1,X2 be constituted-DTrees non empty set st (for t be Element of X1 holds t is finite) & (for t be Element of X2 holds t is finite) holds for C be set holds (C -ImmediateSubtrees (X1 \/ X2)) = ((C -ImmediateSubtrees X1) +* (C -ImmediateSubtrees X2))

    proof

      let X1,X2 be constituted-DTrees non empty set such that

       A1: for t be Element of X1 holds t is finite and

       A2: for t be Element of X2 holds t is finite;

       A3:

      now

        let t be Element of (X1 \/ X2);

        t in X1 or t in X2 by XBOOLE_0:def 3;

        hence t is finite by A1, A2;

      end;

      let C be set;

      set X = (X1 \/ X2);

      set f = (C -ImmediateSubtrees (X1 \/ X2));

      set f1 = (C -ImmediateSubtrees X1);

      set f2 = (C -ImmediateSubtrees X2);

      

       A4: ( dom f) = (C -Subtrees X) by FUNCT_2:def 1;

      

       A5: ( dom f1) = (C -Subtrees X1) by FUNCT_2:def 1;

      

       A6: ( dom f2) = (C -Subtrees X2) by FUNCT_2:def 1;

      

       A7: (C -Subtrees X) = ((C -Subtrees X1) \/ (C -Subtrees X2)) by Th8;

      now

        let x be object;

        assume

         A8: x in (( dom f1) \/ ( dom f2));

        then

        reconsider t = x as Element of ( Subtrees X) by A5, A6, A7;

        (f . x) in (( Subtrees X) * ) by A5, A6, A7, A8, FUNCT_2: 5;

        then

        reconsider p = (f . x) as FinSequence of ( Subtrees X) by FINSEQ_1:def 11;

        hereby

          assume

           A9: x in ( dom f2);

          then (f2 . x) in (( Subtrees X2) * ) by A6, FUNCT_2: 5;

          then

          reconsider p2 = (f2 . x) as FinSequence of ( Subtrees X2) by FINSEQ_1:def 11;

          

           A10: t = ((t . {} ) -tree p) by A3, A5, A6, A7, A8, TREES_9:def 13;

          t = ((t . {} ) -tree p2) by A2, A6, A9, TREES_9:def 13;

          hence (f . x) = (f2 . x) by A10, TREES_4: 15;

        end;

        assume not x in ( dom f2);

        then

         A11: x in ( dom f1) by A8, XBOOLE_0:def 3;

        then (f1 . x) in (( Subtrees X1) * ) by A5, FUNCT_2: 5;

        then

        reconsider p1 = (f1 . x) as FinSequence of ( Subtrees X1) by FINSEQ_1:def 11;

        

         A12: t = ((t . {} ) -tree p) by A3, A5, A6, A7, A8, TREES_9:def 13;

        t = ((t . {} ) -tree p1) by A1, A5, A11, TREES_9:def 13;

        hence (f . x) = (f1 . x) by A12, TREES_4: 15;

      end;

      hence thesis by A4, A5, A6, A7, FUNCT_4:def 1;

    end;

    theorem :: CIRCTRM1:10

    

     Th10: for X1,X2 be non empty Subset of (S -Terms V) holds ((X1 \/ X2) -CircuitStr ) = ((X1 -CircuitStr ) +* (X2 -CircuitStr ))

    proof

      let X1,X2 be non empty Subset of (S -Terms V);

      set X = (X1 \/ X2);

      set C = [:the carrier' of S, {the carrier of S}:];

      

       A1: ( Subtrees X) = (( Subtrees X1) \/ ( Subtrees X2)) by Th7;

      

       A2: (C -Subtrees X) = ((C -Subtrees X1) \/ (C -Subtrees X2)) by Th8;

      (for t be Element of X1 holds t is finite) & for t be Element of X2 holds t is finite;

      then

       A3: (C -ImmediateSubtrees X) = ((C -ImmediateSubtrees X1) +* (C -ImmediateSubtrees X2)) by Th9;

      ( id (C -Subtrees X)) = (( id (C -Subtrees X1)) +* ( id (C -Subtrees X2))) by A2, FUNCT_4: 22;

      hence thesis by A1, A2, A3, CIRCCOMB:def 2;

    end;

    theorem :: CIRCTRM1:11

    

     Th11: for x be set holds x in ( InputVertices (X -CircuitStr )) iff x in ( Subtrees X) & ex s be SortSymbol of S, v be Element of (V . s) st x = ( root-tree [v, s])

    proof

      set G = (X -CircuitStr );

      let x be set;

      hereby

        assume

         A1: x in ( InputVertices (X -CircuitStr ));

        then

         A2: not x in the carrier' of G by XBOOLE_0:def 5;

        thus x in ( Subtrees X) by A1;

        reconsider t = x as Term of S, V by A1, Th4;

        (ex s be SortSymbol of S, v be Element of (V . s) st (t . {} ) = [v, s]) or (t . {} ) in [:the carrier' of S, {the carrier of S}:] by MSATERM: 2;

        then (ex s be SortSymbol of S, v be Element of (V . s) st (t . {} ) = [v, s]) or t is CompoundTerm of S, V by MSATERM:def 6;

        then

        consider s be SortSymbol of S, v be Element of (V . s) such that

         A3: (t . {} ) = [v, s] by A1, A2, Th5;

        take s;

        reconsider v as Element of (V . s);

        take v;

        thus x = ( root-tree [v, s]) by A3, MSATERM: 5;

      end;

      assume

       A4: x in ( Subtrees X);

      given s be SortSymbol of S, v be Element of (V . s) such that

       A5: x = ( root-tree [v, s]);

      assume not thesis;

      then x in the carrier' of G by A4, XBOOLE_0:def 5;

      then

      reconsider t = x as CompoundTerm of S, V by Th4;

      (t . {} ) = [v, s] by A5, TREES_4: 3;

      then [v, s] in [:the carrier' of S, {the carrier of S}:] by MSATERM:def 6;

      then s = the carrier of S by ZFMISC_1: 106;

      then s in s;

      hence contradiction;

    end;

    theorem :: CIRCTRM1:12

    

     Th12: for X be SetWithCompoundTerm of S, V, g be Gate of (X -CircuitStr ) holds g = ((g . {} ) -tree ( the_arity_of g))

    proof

      let X be SetWithCompoundTerm of S, V;

      let g be Gate of (X -CircuitStr );

      for t be Element of X holds t is finite;

      hence thesis by TREES_9:def 13;

    end;

    begin

    definition

      let S be non empty non void ManySortedSign;

      let V be non-empty ManySortedSet of the carrier of S;

      let X be non empty Subset of (S -Terms V);

      let v be Vertex of (X -CircuitStr );

      let A be MSAlgebra over S;

      :: CIRCTRM1:def2

      func the_sort_of (v,A) -> set means

      : Def2: for u be Term of S, V st u = v holds it = (the Sorts of A . ( the_sort_of u));

      uniqueness

      proof

        let S1,S2 be set;

        reconsider u = v as Term of S, V by Th4;

        assume

         A1: not thesis;

        then S1 = (the Sorts of A . ( the_sort_of u));

        hence thesis by A1;

      end;

      existence

      proof

        reconsider u = v as Term of S, V by Th4;

        take (the Sorts of A . ( the_sort_of u));

        thus thesis;

      end;

    end

    registration

      let S be non empty non void ManySortedSign;

      let V be non-empty ManySortedSet of the carrier of S;

      let X be non empty Subset of (S -Terms V);

      let v be Vertex of (X -CircuitStr );

      let A be non-empty MSAlgebra over S;

      cluster ( the_sort_of (v,A)) -> non empty;

      coherence

      proof

        reconsider u = v as Term of S, V by Th4;

        ( the_sort_of (v,A)) = (the Sorts of A . ( the_sort_of u)) by Def2;

        hence thesis;

      end;

    end

    definition

      let S be non empty non void ManySortedSign;

      let V be non-empty ManySortedSet of the carrier of S;

      let X be non empty Subset of (S -Terms V);

      assume

       A1: X is SetWithCompoundTerm of S, V;

      let o be Gate of (X -CircuitStr );

      let A be MSAlgebra over S;

      :: CIRCTRM1:def3

      func the_action_of (o,A) -> Function means

      : Def3: for X9 be SetWithCompoundTerm of S, V st X9 = X holds for o9 be Gate of (X9 -CircuitStr ) st o9 = o holds it = (the Charact of A . ((o9 . {} ) `1 ));

      uniqueness

      proof

        let f1,f2 be Function;

        reconsider X9 = X as SetWithCompoundTerm of S, V by A1;

        reconsider o9 = o as Gate of (X9 -CircuitStr );

        assume

         A2: not thesis;

        then f1 = (the Charact of A . ((o9 . {} ) `1 ));

        hence thesis by A2;

      end;

      existence

      proof

        reconsider X9 = X as SetWithCompoundTerm of S, V by A1;

        reconsider o9 = o as Gate of (X9 -CircuitStr );

        take (the Charact of A . ((o9 . {} ) `1 ));

        thus thesis;

      end;

    end

    scheme :: CIRCTRM1:sch1

    MSFuncEx { I() -> non empty set , A,B() -> non-empty ManySortedSet of I() , P[ object, object, object] } :

ex f be ManySortedFunction of A(), B() st for i be Element of I(), a be Element of (A() . i) holds P[i, a, ((f . i) . a)]

      provided

       A1: for i be Element of I(), a be Element of (A() . i) holds ex b be Element of (B() . i) st P[i, a, b];

      defpred R[ object, object] means ex g be Function of (A() . $1), (B() . $1) st $2 = g & for a be set st a in (A() . $1) holds P[$1, a, (g . a)];

      

       A2: for i be object st i in I() holds ex y be object st R[i, y]

      proof

        let i be object;

        assume i in I();

        then

        reconsider ii = i as Element of I();

        defpred RR[ object, object] means P[i, $1, $2];

        

         A3: for a be object st a in (A() . i) holds ex b be object st b in (B() . i) & RR[a, b]

        proof

          let a be object;

          assume a in (A() . i);

          then ex b be Element of (B() . ii) st P[i, a, b] by A1;

          hence thesis;

        end;

        consider g be Function such that

         A4: ( dom g) = (A() . i) & ( rng g) c= (B() . i) and

         A5: for a be object st a in (A() . i) holds RR[a, (g . a)] from FUNCT_1:sch 6( A3);

        take y = g;

        reconsider g as Function of (A() . i), (B() . i) by A4, FUNCT_2: 2;

        take g;

        thus y = g & for a be set st a in (A() . i) holds P[i, a, (g . a)] by A5;

      end;

      consider f be Function such that

       A6: ( dom f) = I() and

       A7: for i be object st i in I() holds R[i, (f . i)] from CLASSES1:sch 1( A2);

      reconsider f as ManySortedSet of I() by A6, PARTFUN1:def 2, RELAT_1:def 18;

      f is ManySortedFunction of A(), B()

      proof

        let i be object;

        assume i in I();

        then ex g be Function of (A() . i), (B() . i) st (f . i) = g & for a be set st a in (A() . i) holds P[i, a, (g . a)] by A7;

        hence thesis;

      end;

      then

      reconsider f as ManySortedFunction of A(), B();

      take f;

      let i be Element of I(), a be Element of (A() . i);

      ex g be Function of (A() . i), (B() . i) st (f . i) = g & for a be set st a in (A() . i) holds P[i, a, (g . a)] by A7;

      hence thesis;

    end;

    definition

      let S be non empty non void ManySortedSign;

      let V be non-empty ManySortedSet of the carrier of S;

      let X be non empty Subset of (S -Terms V);

      let A be MSAlgebra over S;

      :: CIRCTRM1:def4

      func X -CircuitSorts A -> ManySortedSet of the carrier of (X -CircuitStr ) means

      : Def4: for v be Vertex of (X -CircuitStr ) holds (it . v) = ( the_sort_of (v,A));

      uniqueness

      proof

        let S1,S2 be ManySortedSet of the carrier of (X -CircuitStr ) such that

         A1: for v be Vertex of (X -CircuitStr ) holds (S1 . v) = ( the_sort_of (v,A)) and

         A2: for v be Vertex of (X -CircuitStr ) holds (S2 . v) = ( the_sort_of (v,A));

        now

          let x be object;

          assume x in the carrier of (X -CircuitStr );

          then

          reconsider v = x as Vertex of (X -CircuitStr );

          

          thus (S1 . x) = ( the_sort_of (v,A)) by A1

          .= (S2 . x) by A2;

        end;

        hence thesis;

      end;

      existence

      proof

        deffunc f( Vertex of (X -CircuitStr )) = ( the_sort_of ($1,A));

        thus ex f be ManySortedSet of the carrier of (X -CircuitStr ) st for d be Element of (X -CircuitStr ) holds (f . d) = f(d) from PBOOLE:sch 5;

      end;

    end

    registration

      let S be non empty non void ManySortedSign;

      let V be non-empty ManySortedSet of the carrier of S;

      let X be non empty Subset of (S -Terms V);

      let A be non-empty MSAlgebra over S;

      cluster (X -CircuitSorts A) -> non-empty;

      coherence

      proof

        let i be object;

        assume i in the carrier of (X -CircuitStr );

        then

        reconsider i as Vertex of (X -CircuitStr );

        ((X -CircuitSorts A) . i) = ( the_sort_of (i,A)) by Def4;

        hence thesis;

      end;

    end

    theorem :: CIRCTRM1:13

    

     Th13: for X be SetWithCompoundTerm of S, V, g be Gate of (X -CircuitStr ) holds for o be OperSymbol of S st (g . {} ) = [o, the carrier of S] holds ((X -CircuitSorts A) * ( the_arity_of g)) = (the Sorts of A * ( the_arity_of o))

    proof

      let t be SetWithCompoundTerm of S, V, g be Gate of (t -CircuitStr );

      set X = t;

      reconsider f = g as CompoundTerm of S, V by Th4;

      reconsider ag = ( the_arity_of g) as FinSequence of ( Subtrees t);

      

       A1: g = ((f . {} ) -tree ag) by Th12;

      let o be OperSymbol of S;

      assume (g . {} ) = [o, the carrier of S];

      then

      consider a be ArgumentSeq of ( Sym (o,V)) such that

       A2: f = ( [o, the carrier of S] -tree a) by MSATERM: 10;

      

       A3: ( len a) = ( len ( the_arity_of o)) by MSATERM: 22;

      

       A4: a = ag by A1, A2, TREES_4: 15;

      

       A5: ( dom ( the_arity_of o)) = ( Seg ( len a)) by A3, FINSEQ_1:def 3;

      

       A6: ( dom ( the_arity_of g)) = ( Seg ( len a)) by A4, FINSEQ_1:def 3;

      

       A7: ( rng ( the_arity_of g)) c= the carrier of (t -CircuitStr ) by FINSEQ_1:def 4;

      

       A8: ( rng ( the_arity_of o)) c= the carrier of S by FINSEQ_1:def 4;

      

       A9: ( dom (X -CircuitSorts A)) = the carrier of (X -CircuitStr ) by PARTFUN1:def 2;

      

       A10: ( dom the Sorts of A) = the carrier of S by PARTFUN1:def 2;

      

       A11: ( dom ((X -CircuitSorts A) * ( the_arity_of g))) = ( Seg ( len a)) by A6, A7, A9, RELAT_1: 27;

      

       A12: ( dom (the Sorts of A * ( the_arity_of o))) = ( Seg ( len a)) by A5, A8, A10, RELAT_1: 27;

      now

        let i be object;

        assume

         A13: i in ( Seg ( len a));

        then

        reconsider j = i as Element of NAT ;

        (ag . i) in ( rng ( the_arity_of g)) by A6, A13, FUNCT_1:def 3;

        then

        reconsider v = (ag . j) as Vertex of (t -CircuitStr ) by A7;

        (( the_arity_of o) . i) in ( rng ( the_arity_of o)) by A5, A13, FUNCT_1:def 3;

        then

        reconsider s = (( the_arity_of o) . j) as SortSymbol of S by A8;

        reconsider u = v as Term of S, V by A4, A6, A13, MSATERM: 22;

        

         A14: ( the_sort_of u) = s by A4, A6, A13, MSATERM: 23;

        

         A15: (((t -CircuitSorts A) * ( the_arity_of g)) . i) = ((t -CircuitSorts A) . v) by A11, A13, FUNCT_1: 12;

        

         A16: ((the Sorts of A * ( the_arity_of o)) . i) = (the Sorts of A . s) by A12, A13, FUNCT_1: 12;

        

        thus (((t -CircuitSorts A) * ( the_arity_of g)) . i) = ( the_sort_of (v,A)) by A15, Def4

        .= ((the Sorts of A * ( the_arity_of o)) . i) by A14, A16, Def2;

      end;

      hence thesis by A11, A12, FUNCT_1: 2;

    end;

    definition

      let S be non empty non void ManySortedSign;

      let V be non-empty ManySortedSet of the carrier of S;

      let X be non empty Subset of (S -Terms V);

      let A be non-empty MSAlgebra over S;

      :: CIRCTRM1:def5

      func X -CircuitCharact A -> ManySortedFunction of (((X -CircuitSorts A) # ) * the Arity of (X -CircuitStr )), ((X -CircuitSorts A) * the ResultSort of (X -CircuitStr )) means

      : Def5: for g be Gate of (X -CircuitStr ) st g in the carrier' of (X -CircuitStr ) holds (it . g) = ( the_action_of (g,A));

      uniqueness

      proof

        let C1,C2 be ManySortedFunction of (((X -CircuitSorts A) # ) * the Arity of (X -CircuitStr )), ((X -CircuitSorts A) * the ResultSort of (X -CircuitStr )) such that

         A1: for o be Gate of (X -CircuitStr ) st o in the carrier' of (X -CircuitStr ) holds (C1 . o) = ( the_action_of (o,A)) and

         A2: for o be Gate of (X -CircuitStr ) st o in the carrier' of (X -CircuitStr ) holds (C2 . o) = ( the_action_of (o,A));

        now

          let x be object;

          assume

           A3: x in the carrier' of (X -CircuitStr );

          then

          reconsider o = x as Gate of (X -CircuitStr );

          (C1 . o) = ( the_action_of (o,A)) by A1, A3;

          hence (C1 . x) = (C2 . x) by A2, A3;

        end;

        hence thesis;

      end;

      existence

      proof

        defpred P[ object, object] means ex g be Gate of (X -CircuitStr ) st g = $1 & $2 = ( the_action_of (g,A));

         A4:

        now

          let x be object;

          assume x in the carrier' of (X -CircuitStr );

          then

          reconsider g = x as Gate of (X -CircuitStr );

          reconsider y = ( the_action_of (g,A)) as object;

          take y;

          thus P[x, y];

        end;

        consider CHARACT be ManySortedSet of the carrier' of (X -CircuitStr ) such that

         A5: for x be object st x in the carrier' of (X -CircuitStr ) holds P[x, (CHARACT . x)] from PBOOLE:sch 3( A4);

        

         A6: ( dom CHARACT) = the carrier' of (X -CircuitStr ) by PARTFUN1:def 2;

        CHARACT is Function-yielding

        proof

          let x be object;

          assume x in ( dom CHARACT);

          then ex g be Gate of (X -CircuitStr ) st g = x & (CHARACT . x) = ( the_action_of (g,A)) by A5, A6;

          hence thesis;

        end;

        then

        reconsider CHARACT as ManySortedFunction of the carrier' of (X -CircuitStr );

        CHARACT is ManySortedFunction of (((X -CircuitSorts A) # ) * the Arity of (X -CircuitStr )), ((X -CircuitSorts A) * the ResultSort of (X -CircuitStr ))

        proof

          let i be object;

          assume

           A7: i in the carrier' of (X -CircuitStr );

          then not (X -CircuitStr ) is void;

          then

          reconsider X9 = X as SetWithCompoundTerm of S, V by Th3;

          reconsider g = i as Gate of (X9 -CircuitStr ) by A7;

          ( the_result_sort_of g) = g;

          then

          reconsider v = g as Vertex of (X9 -CircuitStr );

          reconsider I = i as CompoundTerm of S, V by A7, Th4;

          (I . {} ) in [:the carrier' of S, {the carrier of S}:] by MSATERM:def 6;

          then

          consider o,y be object such that

           A8: o in the carrier' of S and

           A9: y in {the carrier of S} and

           A10: (I . {} ) = [o, y] by ZFMISC_1: 84;

          reconsider o as OperSymbol of S by A8;

          

           A11: o = ((I . {} ) `1 ) by A10;

          

           A12: y = the carrier of S by A9, TARSKI:def 1;

          ex g be Gate of (X -CircuitStr ) st g = i & (CHARACT . i) = ( the_action_of (g,A)) by A5, A7;

          

          then

           A13: (CHARACT . i) = ( the_action_of (g,A))

          .= (the Charact of A . o) by A11, Def3;

          

           A14: ((the Sorts of A * the ResultSort of S) . o) = (the Sorts of A . ( the_result_sort_of o)) by FUNCT_2: 15

          .= (the Sorts of A . ( the_sort_of I)) by A10, A12, MSATERM: 17;

          

           A15: (((X -CircuitSorts A) * the ResultSort of (X -CircuitStr )) . g) = ((X -CircuitSorts A) . ( the_result_sort_of g)) by FUNCT_2: 15

          .= ( the_sort_of (v,A)) by Def4

          .= (the Sorts of A . ( the_sort_of I)) by Def2;

          

           A16: ((((X -CircuitSorts A) # ) * the Arity of (X -CircuitStr )) . g) = (((X -CircuitSorts A) # ) . ( the_arity_of g)) by FUNCT_2: 15

          .= ( product ((X9 -CircuitSorts A) * ( the_arity_of g))) by FINSEQ_2:def 5

          .= ( product (the Sorts of A * ( the_arity_of o))) by A10, A12, Th13;

          (((the Sorts of A # ) * the Arity of S) . o) = ((the Sorts of A # ) . ( the_arity_of o)) by FUNCT_2: 15

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

          hence thesis by A13, A14, A15, A16, PBOOLE:def 15;

        end;

        then

        reconsider CHARACT as ManySortedFunction of (((X -CircuitSorts A) # ) * the Arity of (X -CircuitStr )), ((X -CircuitSorts A) * the ResultSort of (X -CircuitStr ));

        take CHARACT;

        let g be Gate of (X -CircuitStr );

        assume g in the carrier' of (X -CircuitStr );

        then ex h be Gate of (X -CircuitStr ) st h = g & (CHARACT . g) = ( the_action_of (h,A)) by A5;

        hence thesis;

      end;

    end

    definition

      let S be non empty non void ManySortedSign;

      let V be non-empty ManySortedSet of the carrier of S;

      let X be non empty Subset of (S -Terms V);

      let A be non-empty MSAlgebra over S;

      :: CIRCTRM1:def6

      func X -Circuit A -> non-empty strict MSAlgebra over (X -CircuitStr ) equals MSAlgebra (# (X -CircuitSorts A), (X -CircuitCharact A) #);

      correctness by MSUALG_1:def 3;

    end

    theorem :: CIRCTRM1:14

    for v be Vertex of (X -CircuitStr ) holds (the Sorts of (X -Circuit A) . v) = ( the_sort_of (v,A)) by Def4;

    theorem :: CIRCTRM1:15

    for A be finite-yielding non-empty MSAlgebra over S holds for X be SetWithCompoundTerm of S, V holds for g be OperSymbol of (X -CircuitStr ) holds ( Den (g,(X -Circuit A))) = ( the_action_of (g,A)) by Def5;

    theorem :: CIRCTRM1:16

    

     Th16: for A be finite-yielding non-empty MSAlgebra over S holds for X be SetWithCompoundTerm of S, V holds for g be OperSymbol of (X -CircuitStr ), o be OperSymbol of S st (g . {} ) = [o, the carrier of S] holds ( Den (g,(X -Circuit A))) = ( Den (o,A))

    proof

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

      let X be SetWithCompoundTerm of S, V;

      let g be OperSymbol of (X -CircuitStr ), o be OperSymbol of S;

      ( Den (g,(X -Circuit A))) = ( the_action_of (g,A)) by Def5

      .= (the Charact of A . ((g . {} ) `1 )) by Def3;

      hence thesis;

    end;

    theorem :: CIRCTRM1:17

    

     Th17: for A be finite-yielding non-empty MSAlgebra over S, X be non empty Subset of (S -Terms V) holds (X -Circuit A) is finite-yielding

    proof

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

      let t be non empty Subset of (S -Terms V);

      let i be object;

      assume i in the carrier of (t -CircuitStr );

      then

      reconsider i as Vertex of (t -CircuitStr );

      reconsider u = i as Term of S, V by Th4;

      

       A1: the Sorts of A is finite-yielding by MSAFREE2:def 11;

      (the Sorts of (t -Circuit A) . i) = ( the_sort_of (i,A)) by Def4

      .= (the Sorts of A . ( the_sort_of u)) by Def2;

      hence thesis by A1;

    end;

    registration

      let S be non empty non void ManySortedSign;

      let V be non-empty ManySortedSet of the carrier of S;

      let X be SetWithCompoundTerm of S, V;

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

      cluster (X -Circuit A) -> finite-yielding;

      coherence by Th17;

    end

    theorem :: CIRCTRM1:18

    

     Th18: for S be non empty non void ManySortedSign holds for V be non-empty ManySortedSet of the carrier of S holds for X1,X2 be SetWithCompoundTerm of S, V holds for A be non-empty MSAlgebra over S holds (X1 -Circuit A) tolerates (X2 -Circuit A)

    proof

      let S be non empty non void ManySortedSign;

      let V be non-empty ManySortedSet of the carrier of S;

      let X1,X2 be SetWithCompoundTerm of S, V;

      let A be non-empty MSAlgebra over S;

      thus the Arity of (X1 -CircuitStr ) tolerates the Arity of (X2 -CircuitStr ) & the ResultSort of (X1 -CircuitStr ) tolerates the ResultSort of (X2 -CircuitStr ) by Th6;

      thus the Sorts of (X1 -Circuit A) tolerates the Sorts of (X2 -Circuit A)

      proof

        let x be object;

        assume

         A1: x in (( dom the Sorts of (X1 -Circuit A)) /\ ( dom the Sorts of (X2 -Circuit A)));

        then

         A2: x in ( dom the Sorts of (X1 -Circuit A)) by XBOOLE_0:def 4;

        

         A3: x in ( dom the Sorts of (X2 -Circuit A)) by A1, XBOOLE_0:def 4;

        

         A4: x in the carrier of (X1 -CircuitStr ) by A2, PARTFUN1:def 2;

        reconsider v1 = x as Vertex of (X1 -CircuitStr ) by A2, PARTFUN1:def 2;

        reconsider v2 = x as Vertex of (X2 -CircuitStr ) by A3, PARTFUN1:def 2;

        reconsider t = x as Term of S, V by A4, Th4;

        

        thus (the Sorts of (X1 -Circuit A) . x) = ( the_sort_of (v1,A)) by Def4

        .= (the Sorts of A . ( the_sort_of t)) by Def2

        .= ( the_sort_of (v2,A)) by Def2

        .= (the Sorts of (X2 -Circuit A) . x) by Def4;

      end;

      let x be object;

      assume

       A5: x in (( dom the Charact of (X1 -Circuit A)) /\ ( dom the Charact of (X2 -Circuit A)));

      then

       A6: x in ( dom the Charact of (X1 -Circuit A)) by XBOOLE_0:def 4;

      

       A7: x in ( dom the Charact of (X2 -Circuit A)) by A5, XBOOLE_0:def 4;

      reconsider g1 = x as Gate of (X1 -CircuitStr ) by A6, PARTFUN1:def 2;

      reconsider g2 = x as Gate of (X2 -CircuitStr ) by A7, PARTFUN1:def 2;

      

      thus (the Charact of (X1 -Circuit A) . x) = ( the_action_of (g1,A)) by Def5

      .= (the Charact of A . ((g1 . {} ) `1 )) by Def3

      .= ( the_action_of (g2,A)) by Def3

      .= (the Charact of (X2 -Circuit A) . x) by Def5;

    end;

    theorem :: CIRCTRM1:19

    for S be non empty non void ManySortedSign holds for V be non-empty ManySortedSet of the carrier of S holds for X1,X2 be SetWithCompoundTerm of S, V holds for A be non-empty MSAlgebra over S holds ((X1 \/ X2) -Circuit A) = ((X1 -Circuit A) +* (X2 -Circuit A))

    proof

      let S be non empty non void ManySortedSign;

      let V be non-empty ManySortedSet of the carrier of S;

      let X1,X2 be SetWithCompoundTerm of S, V;

      consider t1 be CompoundTerm of S, V such that

       A1: t1 in X1 by MSATERM:def 7;

      t1 in (X1 \/ X2) by A1, XBOOLE_0:def 3;

      then

      reconsider X = (X1 \/ X2) as SetWithCompoundTerm of S, V by MSATERM:def 7;

      let A be non-empty MSAlgebra over S;

      set C1 = (X1 -Circuit A), C2 = (X2 -Circuit A), C = (X -Circuit A);

      

       A2: C1 tolerates C2 by Th18;

      then

       A3: the Sorts of C1 tolerates the Sorts of C2;

      

       A4: the Charact of C1 tolerates the Charact of C2 by A2;

      

       A5: the Sorts of (C1 +* C2) = (the Sorts of C1 +* the Sorts of C2) by A3, CIRCCOMB:def 4;

      

       A6: the Charact of (C1 +* C2) = (the Charact of C1 +* the Charact of C2) by A3, CIRCCOMB:def 4;

      

       A7: (X -CircuitStr ) = ((X1 -CircuitStr ) +* (X2 -CircuitStr )) by Th10;

      

       A8: C1 tolerates C by Th18;

      

       A9: C2 tolerates C by Th18;

      

       A10: the Sorts of C1 tolerates the Sorts of C by A8;

      

       A11: the Sorts of C2 tolerates the Sorts of C by A9;

      

       A12: the Charact of C1 tolerates the Charact of C by A8;

      

       A13: the Charact of C2 tolerates the Charact of C by A9;

      

       A14: ( dom the Sorts of (C1 +* C2)) = the carrier of (X -CircuitStr ) by A7, PARTFUN1:def 2;

      ( dom the Charact of (C1 +* C2)) = the carrier' of (X -CircuitStr ) by A7, PARTFUN1:def 2;

      then

       A15: ( dom the Charact of (C1 +* C2)) = ( dom the Charact of C) by PARTFUN1:def 2;

      

       A16: ( dom the Sorts of (C1 +* C2)) = ( dom the Sorts of C) by A14, PARTFUN1:def 2;

      

       A17: the Charact of (C1 +* C2) = the Charact of C by A4, A6, A12, A13, A15, FUNCT_4: 125, PARTFUN1: 55;

      the Sorts of (C1 +* C2) = the Sorts of C by A3, A5, A10, A11, A16, FUNCT_4: 125, PARTFUN1: 55;

      hence thesis by A17;

    end;

    begin

    reserve S for non empty non void ManySortedSign,

A for non-empty finite-yielding MSAlgebra over S,

V for Variables of A,

X for SetWithCompoundTerm of S, V;

    definition

      let S be non empty non void ManySortedSign;

      let A be non-empty MSAlgebra over S;

      let V be Variables of A;

      let t be DecoratedTree;

      let f be ManySortedFunction of V, the Sorts of A;

      :: CIRCTRM1:def7

      func t @ (f,A) -> set means

      : Def7: ex t9 be c-Term of A, V st t9 = t & it = (t9 @ f);

      correctness

      proof

        reconsider t9 = t as c-Term of A, V by A1, MSATERM: 27;

        (t9 @ f) = (t9 @ f);

        hence thesis;

      end;

    end

    definition

      let S be non empty non void ManySortedSign;

      let V be non-empty ManySortedSet of the carrier of S;

      let X be SetWithCompoundTerm of S, V;

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

      let s be State of (X -Circuit A);

      defpred P[ set, set, set] means ( root-tree [$2, $1]) in ( Subtrees X) implies $3 = (s . ( root-tree [$2, $1]));

      

       A1: for x be Vertex of S, v be Element of (V . x) holds ex a be Element of (the Sorts of A . x) st P[x, v, a]

      proof

        let x be Vertex of S, v be Element of (V . x);

        per cases ;

          suppose not ( root-tree [v, x]) in ( Subtrees X);

          hence thesis;

        end;

          suppose ( root-tree [v, x]) in ( Subtrees X);

          then

          reconsider a = ( root-tree [v, x]) as Vertex of (X -CircuitStr );

          reconsider t = a as Term of S, V by MSATERM: 4;

          

           A2: ( the_sort_of t) = x by MSATERM: 14;

          

           A3: ( the_sort_of (a,A)) = (the Sorts of A . ( the_sort_of t)) by Def2;

          ((X -CircuitSorts A) . a) = ( the_sort_of (a,A)) by Def4;

          then

          reconsider b = (s . a) as Element of (the Sorts of A . x) by A2, A3, CIRCUIT1: 4;

          take b;

          thus thesis;

        end;

      end;

      :: CIRCTRM1:def8

      mode CompatibleValuation of s -> ManySortedFunction of V, the Sorts of A means

      : Def8: for x be Vertex of S, v be Element of (V . x) st ( root-tree [v, x]) in ( Subtrees X) holds ((it . x) . v) = (s . ( root-tree [v, x]));

      existence

      proof

        thus ex f be ManySortedFunction of V, the Sorts of A st for x be Element of S, v be Element of (V . x) holds P[x, v, ((f . x) . v)] from MSFuncEx( A1);

      end;

    end

    theorem :: CIRCTRM1:20

    for s be State of (X -Circuit A) holds for f be CompatibleValuation of s, n be Element of NAT holds f is CompatibleValuation of ( Following (s,n))

    proof

      let s be State of (X -Circuit A);

      let f be CompatibleValuation of s, n be Element of NAT ;

      let x be Vertex of S, v be Element of (V . x);

      assume

       A1: ( root-tree [v, x]) in ( Subtrees X);

      then ( root-tree [v, x]) in ( InputVertices (X -CircuitStr )) by Th11;

      then s is_stable_at ( root-tree [v, x]) by FACIRC_1: 18;

      then (( Following (s,n)) . ( root-tree [v, x])) = (s . ( root-tree [v, x]));

      hence thesis by A1, Def8;

    end;

    registration

      let x be object;

      let S be non empty non void ManySortedSign;

      let V be non-empty ManySortedSet of the carrier of S;

      let p be FinSequence of (S -Terms V);

      cluster (x -tree p) -> finite;

      coherence

      proof

        reconsider q = ( doms p) as FinTree-yielding FinSequence;

        ( dom (x -tree p)) = ( tree q) by TREES_4: 10;

        hence thesis by FINSET_1: 10;

      end;

    end

    theorem :: CIRCTRM1:21

    

     Th21: for s be State of (X -Circuit A) holds for f be CompatibleValuation of s holds for t be Term of S, V st t in ( Subtrees X) holds ( Following (s,(1 + ( height ( dom t))))) is_stable_at t & (( Following (s,(1 + ( height ( dom t))))) . t) = (t @ (f,A))

    proof

      let q be State of (X -Circuit A);

      let f be CompatibleValuation of q;

      

       A1: (X -CircuitStr ) = ManySortedSign (# ( Subtrees X), ( [:the carrier' of S, {the carrier of S}:] -Subtrees X), ( [:the carrier' of S, {the carrier of S}:] -ImmediateSubtrees X), ( incl ( [:the carrier' of S, {the carrier of S}:] -Subtrees X)) #);

      defpred P[ finite DecoratedTree] means $1 in ( Subtrees X) implies ( Following (q,(1 + ( height ( dom $1))))) is_stable_at $1 & (( Following (q,(1 + ( height ( dom $1))))) . $1) = ($1 @ (f,A));

      

       A2: for s be SortSymbol of S, v be Element of (V . s) holds P[( root-tree [v, s])]

      proof

        let s be SortSymbol of S, v be Element of (V . s);

        assume

         A3: ( root-tree [v, s]) in ( Subtrees X);

        then

         A4: ( root-tree [v, s]) in ( InputVertices (X -CircuitStr )) by Th11;

        hence ( Following (q,(1 + ( height ( dom ( root-tree [v, s])))))) is_stable_at ( root-tree [v, s]) by FACIRC_1: 18;

        reconsider t = ( root-tree [v, s]) as c-Term of A, V by MSATERM: 8;

        

         A5: t is Term of S, V by MSATERM: 4;

        q is_stable_at ( root-tree [v, s]) by A4, FACIRC_1: 18;

        

        hence (( Following (q,(1 + ( height ( dom ( root-tree [v, s])))))) . ( root-tree [v, s])) = (q . ( root-tree [v, s]))

        .= ((f . s) . v) by A3, Def8

        .= ((v -term A) @ f) by MSATERM: 42

        .= (t @ f) by MSATERM:def 4

        .= (( root-tree [v, s]) @ (f,A)) by A5, Def7;

      end;

      

       A6: for o be OperSymbol of S, p be ArgumentSeq of ( Sym (o,V)) st for t be Term of S, V st t in ( rng p) holds P[t] holds P[( [o, the carrier of S] -tree p)]

      proof

        let o be OperSymbol of S, p be ArgumentSeq of ( Sym (o,V)) such that

         A7: for t be Term of S, V st t in ( rng p) & t in ( Subtrees X) holds ( Following (q,(1 + ( height ( dom t))))) is_stable_at t & (( Following (q,(1 + ( height ( dom t))))) . t) = (t @ (f,A)) and

         A8: ( [o, the carrier of S] -tree p) in ( Subtrees X);

        consider tt be Element of X, n be Node of tt such that

         A9: ( [o, the carrier of S] -tree p) = (tt | n) by A8, TREES_9: 19;

        

         A10: ( <*> NAT ) in (( dom tt) | n) by TREES_1: 22;

        (n ^ {} ) = n by FINSEQ_1: 34;

        

        then (tt . n) = ((tt | n) . {} ) by A10, TREES_2:def 10

        .= [o, the carrier of S] by A9, TREES_4:def 4;

        then (tt . n) in [:the carrier' of S, {the carrier of S}:] by ZFMISC_1: 106;

        then

        reconsider g = ( [o, the carrier of S] -tree p) as Gate of (X -CircuitStr ) by A9, TREES_9: 24;

        

         A11: ( the_result_sort_of g) = g;

        

         A12: (g . {} ) = [o, the carrier of S] by TREES_4:def 4;

        g = ((g . {} ) -tree ( the_arity_of g)) by Th12;

        then

         A13: ( the_arity_of g) = p by TREES_4: 15;

        

         A14: ( rng ( the_arity_of g)) c= ( Subtrees X) by FINSEQ_1:def 4;

        

         A15: ( dom ( [o, the carrier of S] -tree p)) = ( tree ( doms p)) by TREES_4: 10;

        now

          let x be set;

          assume

           A16: x in ( rng ( the_arity_of g));

          then

          reconsider t = x as Element of ( Subtrees X) by A14;

          reconsider t as Term of S, V by A1, Th4;

          consider z be object such that

           A17: z in ( dom p) and

           A18: t = (p . z) by A13, A16, FUNCT_1:def 3;

          

           A19: z in ( dom ( doms p)) by A17, A18, FUNCT_6: 22;

          (( doms p) . z) = ( dom t) by A17, A18, FUNCT_6: 22;

          then ( dom t) in ( rng ( doms p)) by A19, FUNCT_1:def 3;

          then ( height ( dom t)) < ( height ( tree ( doms p))) by TREES_3: 78;

          then (1 + ( height ( dom t))) <= ( height ( tree ( doms p))) by NAT_1: 13;

          then

          consider i be Nat such that

           A20: ( height ( tree ( doms p))) = ((1 + ( height ( dom t))) + i) by NAT_1: 10;

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

          ( Following (q,( height ( dom ( [o, the carrier of S] -tree p))))) = ( Following (( Following (q,(1 + ( height ( dom t))))),i)) by A15, A20, FACIRC_1: 13;

          hence ( Following (q,( height ( dom ( [o, the carrier of S] -tree p))))) is_stable_at x by A7, A13, A16, FACIRC_1: 17;

        end;

        then ( Following ( Following (q,( height ( dom ( [o, the carrier of S] -tree p)))))) is_stable_at ( [o, the carrier of S] -tree p) by A11, FACIRC_1: 19;

        hence ( Following (q,(1 + ( height ( dom ( [o, the carrier of S] -tree p)))))) is_stable_at ( [o, the carrier of S] -tree p) by FACIRC_1: 12;

        reconsider t = (( Sym (o,V)) -tree p) as c-Term of A, V by MSATERM: 27;

        

         A21: ( Sym (o,(the Sorts of A (\/) V))) = [o, the carrier of S] by MSAFREE:def 9;

        

         A22: ( Sym (o,V)) = [o, the carrier of S] by MSAFREE:def 9;

        

         A23: t = ( [o, the carrier of S] -tree p) by MSAFREE:def 9;

        deffunc f( set) = (( Following (q,( height ( dom t)))) . (p . $1));

        consider vp be FinSequence such that

         A24: ( len vp) = ( len p) and

         A25: for i be Nat st i in ( dom vp) holds (vp . i) = f(i) from FINSEQ_1:sch 2;

        

         A26: ( dom vp) = ( Seg ( len p)) by A24, FINSEQ_1:def 3;

        

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

        

         A28: ( dom p) = ( dom ( the_arity_of o)) by MSATERM: 22;

        now

          let i be Nat;

          assume

           A29: i in ( dom p);

          then

          reconsider t = (p . i) as Term of S, V by MSATERM: 22;

          reconsider t9 = t as c-Term of A, V by MSATERM: 27;

          take t9;

          ( the_sort_of t) = ( the_sort_of t9) by Th1;

          hence t9 = (p . i) & ( the_sort_of t9) = (( the_arity_of o) . i) by A29, MSATERM: 23;

        end;

        then

        reconsider p9 = p as ArgumentSeq of o, A, V by A28, MSATERM: 24;

        now

          let i be Nat;

          assume

           A30: i in ( dom p);

          let t be c-Term of A, V;

          assume

           A31: t = (p . i);

          then

           A32: t in ( rng p) by A30, FUNCT_1:def 3;

          then

          reconsider tt = t as Element of ( Subtrees X) by A13, A14;

          reconsider tt as Term of S, V by A1, Th4;

          

           A33: ( Following (q,(1 + ( height ( dom t))))) is_stable_at tt by A7, A32;

          

           A34: (( Following (q,(1 + ( height ( dom t))))) . tt) = (tt @ (f,A)) by A7, A32;

          

           A35: (vp . i) = (( Following (q,( height ( dom ( [o, the carrier of S] -tree p))))) . t) by A23, A25, A26, A27, A30, A31;

          

           A36: i in ( dom ( doms p)) by A30, A31, FUNCT_6: 22;

          (( doms p) . i) = ( dom t) by A30, A31, FUNCT_6: 22;

          then ( dom t) in ( rng ( doms p)) by A36, FUNCT_1:def 3;

          then ( height ( dom t)) < ( height ( tree ( doms p))) by TREES_3: 78;

          then (1 + ( height ( dom t))) <= ( height ( tree ( doms p))) by NAT_1: 13;

          then

          consider j be Nat such that

           A37: ( height ( tree ( doms p))) = ((1 + ( height ( dom t))) + j) by NAT_1: 10;

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

          ( Following (q,( height ( dom ( [o, the carrier of S] -tree p))))) = ( Following (( Following (q,(1 + ( height ( dom t))))),j)) by A15, A37, FACIRC_1: 13;

          then (( Following (q,( height ( dom ( [o, the carrier of S] -tree p))))) . t) = (( Following (q,(1 + ( height ( dom t))))) . t) by A33;

          hence (vp . i) = (t @ f) by A34, A35, Def7;

        end;

        then

         A38: ((( Sym (o,(the Sorts of A (\/) V))) -tree p9) qua c-Term of A, V @ f) = (( Den (o,A)) . vp) by A24, MSATERM: 43;

        now

          

           A39: ( rng p) c= the carrier of (X -CircuitStr ) by A13, FINSEQ_1:def 4;

          ( dom ( Following (q,( height ( dom t))))) = the carrier of (X -CircuitStr ) by CIRCUIT1: 3;

          hence ( dom (( Following (q,( height ( dom t)))) * p)) = ( dom p) by A39, RELAT_1: 27;

          let z be object;

          assume

           A40: z in ( Seg ( len p));

          then

          reconsider i = z as Element of NAT ;

          (vp . i) = (( Following (q,( height ( dom t)))) . (p . i)) by A25, A26, A40;

          hence (vp . z) = ((( Following (q,( height ( dom t)))) * p) . z) by A27, A40, FUNCT_1: 13;

        end;

        then

         A41: vp = (( Following (q,( height ( dom t)))) * ( the_arity_of g)) by A13, A26, A27, FUNCT_1: 2;

        ( Den (g,(X -Circuit A))) = ( Den (o,A)) by A12, Th16;

        then (( Den (o,A)) . vp) = (( Following ( Following (q,( height ( dom t))))) . t) by A11, A23, A41, FACIRC_1: 10;

        

        hence (( Following (q,(1 + ( height ( dom ( [o, the carrier of S] -tree p)))))) . ( [o, the carrier of S] -tree p)) = (t @ f) by A21, A22, A38, FACIRC_1: 12

        .= (( [o, the carrier of S] -tree p) @ (f,A)) by A22, Def7;

      end;

      thus for t be Term of S, V holds P[t] from MSATERM:sch 1( A2, A6);

    end;

    theorem :: CIRCTRM1:22

     not (ex t be Term of S, V, o be OperSymbol of S st t in ( Subtrees X) & (t . {} ) = [o, the carrier of S] & ( the_arity_of o) = {} ) implies for s be State of (X -Circuit A) holds for f be CompatibleValuation of s holds for t be Term of S, V st t in ( Subtrees X) holds ( Following (s,( height ( dom t)))) is_stable_at t & (( Following (s,( height ( dom t)))) . t) = (t @ (f,A))

    proof

      assume

       A1: not ex t be Term of S, V, o be OperSymbol of S st t in ( Subtrees X) & (t . {} ) = [o, the carrier of S] & ( the_arity_of o) = {} ;

      let q be State of (X -Circuit A);

      let f be CompatibleValuation of q;

      

       A2: (X -CircuitStr ) = ManySortedSign (# ( Subtrees X), ( [:the carrier' of S, {the carrier of S}:] -Subtrees X), ( [:the carrier' of S, {the carrier of S}:] -ImmediateSubtrees X), ( incl ( [:the carrier' of S, {the carrier of S}:] -Subtrees X)) #);

      defpred P[ finite DecoratedTree] means $1 in ( Subtrees X) implies ( Following (q,( height ( dom $1)))) is_stable_at $1 & (( Following (q,( height ( dom $1)))) . $1) = ($1 @ (f,A));

      

       A3: for s be SortSymbol of S, v be Element of (V . s) holds P[( root-tree [v, s])]

      proof

        let s be SortSymbol of S, v be Element of (V . s);

        assume

         A4: ( root-tree [v, s]) in ( Subtrees X);

        then ( root-tree [v, s]) in ( InputVertices (X -CircuitStr )) by Th11;

        hence ( Following (q,( height ( dom ( root-tree [v, s]))))) is_stable_at ( root-tree [v, s]) by FACIRC_1: 18;

        reconsider t = ( root-tree [v, s]) as c-Term of A, V by MSATERM: 8;

        

         A5: t is Term of S, V by MSATERM: 4;

        ( dom ( root-tree [v, s])) = ( elementary_tree 0 ) by TREES_4: 3;

        

        hence (( Following (q,( height ( dom ( root-tree [v, s]))))) . ( root-tree [v, s])) = (q . ( root-tree [v, s])) by FACIRC_1: 11, TREES_1: 42

        .= ((f . s) . v) by A4, Def8

        .= ((v -term A) @ f) by MSATERM: 42

        .= (t @ f) by MSATERM:def 4

        .= (( root-tree [v, s]) @ (f,A)) by A5, Def7;

      end;

      

       A6: for o be OperSymbol of S, p be ArgumentSeq of ( Sym (o,V)) st for t be Term of S, V st t in ( rng p) holds P[t] holds P[( [o, the carrier of S] -tree p)]

      proof

        let o be OperSymbol of S, p be ArgumentSeq of ( Sym (o,V)) such that

         A7: for t be Term of S, V st t in ( rng p) & t in ( Subtrees X) holds ( Following (q,( height ( dom t)))) is_stable_at t & (( Following (q,( height ( dom t)))) . t) = (t @ (f,A)) and

         A8: ( [o, the carrier of S] -tree p) in ( Subtrees X);

        consider tt be Element of X, n be Node of tt such that

         A9: ( [o, the carrier of S] -tree p) = (tt | n) by A8, TREES_9: 19;

        

         A10: ( <*> NAT ) in (( dom tt) | n) by TREES_1: 22;

        (n ^ {} ) = n by FINSEQ_1: 34;

        

        then (tt . n) = ((tt | n) . {} ) by A10, TREES_2:def 10

        .= [o, the carrier of S] by A9, TREES_4:def 4;

        then (tt . n) in [:the carrier' of S, {the carrier of S}:] by ZFMISC_1: 106;

        then

        reconsider g = ( [o, the carrier of S] -tree p) as Gate of (X -CircuitStr ) by A9, TREES_9: 24;

        

         A11: ( the_result_sort_of g) = g;

        

         A12: (g . {} ) = [o, the carrier of S] by TREES_4:def 4;

        g = ((g . {} ) -tree ( the_arity_of g)) by Th12;

        then

         A13: ( the_arity_of g) = p by TREES_4: 15;

        

         A14: ( rng ( the_arity_of g)) c= ( Subtrees X) by FINSEQ_1:def 4;

        

         A15: ( dom ( [o, the carrier of S] -tree p)) = ( tree ( doms p)) by TREES_4: 10;

        now

          assume ( height ( dom ( [o, the carrier of S] -tree p))) = 0 ;

          then ( [o, the carrier of S] -tree p) = ( root-tree [o, the carrier of S]) by A12, TREES_1: 43, TREES_4: 5;

          then p = {} by TREES_4: 17;

          then ( len p) = 0 ;

          then ( len ( the_arity_of o)) = 0 by MSATERM: 22;

          then

           A16: ( the_arity_of o) = {} ;

          g is Term of S, V by Th4;

          hence contradiction by A1, A8, A12, A16;

        end;

        then

        consider h be Nat such that

         A17: ( height ( dom ( [o, the carrier of S] -tree p))) = (h + 1) by NAT_1: 6;

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

        now

          let x be set;

          assume

           A18: x in ( rng ( the_arity_of g));

          then

          reconsider t = x as Element of ( Subtrees X) by A14;

          reconsider t as Term of S, V by A2, Th4;

          consider z be object such that

           A19: z in ( dom p) and

           A20: t = (p . z) by A13, A18, FUNCT_1:def 3;

          

           A21: z in ( dom ( doms p)) by A19, A20, FUNCT_6: 22;

          (( doms p) . z) = ( dom t) by A19, A20, FUNCT_6: 22;

          then ( dom t) in ( rng ( doms p)) by A21, FUNCT_1:def 3;

          then ( height ( dom t)) < ( height ( tree ( doms p))) by TREES_3: 78;

          then ( height ( dom t)) <= h by A15, A17, NAT_1: 13;

          then

          consider i be Nat such that

           A22: h = (( height ( dom t)) + i) by NAT_1: 10;

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

          ( Following (q,h)) = ( Following (( Following (q,( height ( dom t)))),i)) by A22, FACIRC_1: 13;

          hence ( Following (q,h)) is_stable_at x by A7, A13, A18, FACIRC_1: 17;

        end;

        then ( Following ( Following (q,h))) is_stable_at ( [o, the carrier of S] -tree p) by A11, FACIRC_1: 19;

        hence ( Following (q,( height ( dom ( [o, the carrier of S] -tree p))))) is_stable_at ( [o, the carrier of S] -tree p) by A17, FACIRC_1: 12;

        reconsider t = (( Sym (o,V)) -tree p) as c-Term of A, V by MSATERM: 27;

        

         A23: ( Sym (o,(the Sorts of A (\/) V))) = [o, the carrier of S] by MSAFREE:def 9;

        

         A24: ( Sym (o,V)) = [o, the carrier of S] by MSAFREE:def 9;

        

         A25: t = ( [o, the carrier of S] -tree p) by MSAFREE:def 9;

        deffunc f( set) = (( Following (q,h)) . (p . $1));

        consider vp be FinSequence such that

         A26: ( len vp) = ( len p) and

         A27: for i be Nat st i in ( dom vp) holds (vp . i) = f(i) from FINSEQ_1:sch 2;

        

         A28: ( dom vp) = ( Seg ( len p)) by A26, FINSEQ_1:def 3;

        

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

        

         A30: ( dom p) = ( dom ( the_arity_of o)) by MSATERM: 22;

        now

          let i be Nat;

          assume

           A31: i in ( dom p);

          then

          reconsider t = (p . i) as Term of S, V by MSATERM: 22;

          reconsider t9 = t as c-Term of A, V by MSATERM: 27;

          take t9;

          ( the_sort_of t) = ( the_sort_of t9) by Th1;

          hence t9 = (p . i) & ( the_sort_of t9) = (( the_arity_of o) . i) by A31, MSATERM: 23;

        end;

        then

        reconsider p9 = p as ArgumentSeq of o, A, V by A30, MSATERM: 24;

        now

          let i be Nat;

          assume

           A32: i in ( dom p);

          let t be c-Term of A, V;

          assume

           A33: t = (p . i);

          then

           A34: t in ( rng p) by A32, FUNCT_1:def 3;

          then

          reconsider tt = t as Element of ( Subtrees X) by A13, A14;

          reconsider tt as Term of S, V by A2, Th4;

          

           A35: ( Following (q,( height ( dom t)))) is_stable_at tt by A7, A34;

          

           A36: (( Following (q,( height ( dom t)))) . tt) = (tt @ (f,A)) by A7, A34;

          

           A37: (vp . i) = (( Following (q,h)) . t) by A27, A28, A29, A32, A33;

          

           A38: i in ( dom ( doms p)) by A32, A33, FUNCT_6: 22;

          (( doms p) . i) = ( dom t) by A32, A33, FUNCT_6: 22;

          then ( dom t) in ( rng ( doms p)) by A38, FUNCT_1:def 3;

          then ( height ( dom t)) < ( height ( tree ( doms p))) by TREES_3: 78;

          then ( height ( dom t)) <= h by A15, A17, NAT_1: 13;

          then

          consider j be Nat such that

           A39: h = (( height ( dom t)) + j) by NAT_1: 10;

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

          ( Following (q,h)) = ( Following (( Following (q,( height ( dom t)))),j)) by A39, FACIRC_1: 13;

          then (( Following (q,h)) . t) = (( Following (q,( height ( dom t)))) . t) by A35;

          hence (vp . i) = (t @ f) by A36, A37, Def7;

        end;

        then

         A40: ((( Sym (o,(the Sorts of A (\/) V))) -tree p9) qua c-Term of A, V @ f) = (( Den (o,A)) . vp) by A26, MSATERM: 43;

        now

          

           A41: ( rng p) c= the carrier of (X -CircuitStr ) by A13, FINSEQ_1:def 4;

          ( dom ( Following (q,h))) = the carrier of (X -CircuitStr ) by CIRCUIT1: 3;

          hence ( dom (( Following (q,h)) * p)) = ( dom p) by A41, RELAT_1: 27;

          let z be object;

          assume

           A42: z in ( Seg ( len p));

          then

          reconsider i = z as Element of NAT ;

          (vp . i) = (( Following (q,h)) . (p . i)) by A27, A28, A42;

          hence (vp . z) = ((( Following (q,h)) * p) . z) by A29, A42, FUNCT_1: 13;

        end;

        then

         A43: vp = (( Following (q,h)) * ( the_arity_of g)) by A13, A28, A29, FUNCT_1: 2;

        ( Den (g,(X -Circuit A))) = ( Den (o,A)) by A12, Th16;

        then (( Den (o,A)) . vp) = (( Following ( Following (q,h))) . t) by A11, A25, A43, FACIRC_1: 10;

        

        hence (( Following (q,( height ( dom ( [o, the carrier of S] -tree p))))) . ( [o, the carrier of S] -tree p)) = (t @ f) by A17, A23, A24, A40, FACIRC_1: 12

        .= (( [o, the carrier of S] -tree p) @ (f,A)) by A24, Def7;

      end;

      thus for t be Term of S, V holds P[t] from MSATERM:sch 1( A3, A6);

    end;

    begin

    definition

      let S1,S2 be non empty ManySortedSign;

      let f,g be Function;

      :: CIRCTRM1:def9

      pred S1,S2 are_equivalent_wrt f,g means f is one-to-one & g is one-to-one & (f,g) form_morphism_between (S1,S2) & ((f " ),(g " )) form_morphism_between (S2,S1);

    end

    theorem :: CIRCTRM1:23

    

     Th23: for S1,S2 be non empty ManySortedSign, f,g be Function st (S1,S2) are_equivalent_wrt (f,g) holds the carrier of S2 = (f .: the carrier of S1) & the carrier' of S2 = (g .: the carrier' of S1)

    proof

      let S1,S2 be non empty ManySortedSign, f,g be Function such that

       A1: f is one-to-one and

       A2: g is one-to-one and

       A3: (f,g) form_morphism_between (S1,S2) and

       A4: ((f " ),(g " )) form_morphism_between (S2,S1);

      

      thus the carrier of S2 = ( dom (f " )) by A4

      .= ( rng f) by A1, FUNCT_1: 33

      .= (f .: ( dom f)) by RELAT_1: 113

      .= (f .: the carrier of S1) by A3;

      

      thus the carrier' of S2 = ( dom (g " )) by A4

      .= ( rng g) by A2, FUNCT_1: 33

      .= (g .: ( dom g)) by RELAT_1: 113

      .= (g .: the carrier' of S1) by A3;

    end;

    theorem :: CIRCTRM1:24

    

     Th24: for S1,S2 be non empty ManySortedSign, f,g be Function st (S1,S2) are_equivalent_wrt (f,g) holds ( rng f) = the carrier of S2 & ( rng g) = the carrier' of S2

    proof

      let S1,S2 be non empty ManySortedSign, f,g be Function such that

       A1: f is one-to-one and

       A2: g is one-to-one and (f,g) form_morphism_between (S1,S2) and

       A3: ((f " ),(g " )) form_morphism_between (S2,S1);

      

      thus ( rng f) = ( dom (f " )) by A1, FUNCT_1: 33

      .= the carrier of S2 by A3;

      

      thus ( rng g) = ( dom (g " )) by A2, FUNCT_1: 33

      .= the carrier' of S2 by A3;

    end;

    theorem :: CIRCTRM1:25

    

     Th25: for S be non empty ManySortedSign holds (S,S) are_equivalent_wrt (( id the carrier of S),( id the carrier' of S))

    proof

      let S be non empty ManySortedSign;

      set f = ( id the carrier of S), g = ( id the carrier' of S);

      thus f is one-to-one;

      

       A1: (f " ) = f by FUNCT_1: 45;

      (g " ) = g by FUNCT_1: 45;

      hence thesis by A1, INSTALG1: 8;

    end;

    theorem :: CIRCTRM1:26

    

     Th26: for S1,S2 be non empty ManySortedSign, f,g be Function st (S1,S2) are_equivalent_wrt (f,g) holds (S2,S1) are_equivalent_wrt ((f " ),(g " ))

    proof

      let S1,S2 be non empty ManySortedSign, f,g be Function such that

       A1: f is one-to-one and

       A2: g is one-to-one and

       A3: (f,g) form_morphism_between (S1,S2) and

       A4: ((f " ),(g " )) form_morphism_between (S2,S1);

      thus (f " ) is one-to-one & (g " ) is one-to-one by A1, A2;

      ((f " ) " ) = f by A1, FUNCT_1: 43;

      hence thesis by A2, A3, A4, FUNCT_1: 43;

    end;

    theorem :: CIRCTRM1:27

    

     Th27: for S1,S2,S3 be non empty ManySortedSign, f1,g1,f2,g2 be Function st (S1,S2) are_equivalent_wrt (f1,g1) & (S2,S3) are_equivalent_wrt (f2,g2) holds (S1,S3) are_equivalent_wrt ((f2 * f1),(g2 * g1))

    proof

      let S1,S2,S3 be non empty ManySortedSign;

      let f1,g1,f2,g2 be Function such that

       A1: f1 is one-to-one and

       A2: g1 is one-to-one and

       A3: (f1,g1) form_morphism_between (S1,S2) and

       A4: ((f1 " ),(g1 " )) form_morphism_between (S2,S1) and

       A5: f2 is one-to-one and

       A6: g2 is one-to-one and

       A7: (f2,g2) form_morphism_between (S2,S3) and

       A8: ((f2 " ),(g2 " )) form_morphism_between (S3,S2);

      thus (f2 * f1) is one-to-one & (g2 * g1) is one-to-one by A1, A2, A5, A6;

      

       A9: ((f2 * f1) " ) = ((f1 " ) * (f2 " )) by A1, A5, FUNCT_1: 44;

      ((g2 * g1) " ) = ((g1 " ) * (g2 " )) by A2, A6, FUNCT_1: 44;

      hence thesis by A3, A4, A7, A8, A9, PUA2MSS1: 29;

    end;

    theorem :: CIRCTRM1:28

    

     Th28: for S1,S2 be non empty ManySortedSign, f,g be Function st (S1,S2) are_equivalent_wrt (f,g) holds (f .: ( InputVertices S1)) = ( InputVertices S2) & (f .: ( InnerVertices S1)) = ( InnerVertices S2)

    proof

      let S1,S2 be non empty ManySortedSign, f,g be Function such that

       A1: (S1,S2) are_equivalent_wrt (f,g);

      

       A2: f is one-to-one by A1;

      

       A3: (f,g) form_morphism_between (S1,S2) by A1;

      

       A4: ( rng g) = the carrier' of S2 by A1, Th24;

      

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

      

       A6: (f .: ( rng the ResultSort of S1)) = ( rng (f * the ResultSort of S1)) by RELAT_1: 127

      .= ( rng (the ResultSort of S2 * g)) by A3

      .= ( rng the ResultSort of S2) by A4, A5, RELAT_1: 28;

      

      thus (f .: ( InputVertices S1)) = ((f .: the carrier of S1) \ (f .: ( rng the ResultSort of S1))) by A2, FUNCT_1: 64

      .= ( InputVertices S2) by A1, A6, Th23;

      thus thesis by A6;

    end;

    definition

      let S1,S2 be non empty ManySortedSign;

      :: CIRCTRM1:def10

      pred S1,S2 are_equivalent means ex f,g be one-to-one Function st (S1,S2) are_equivalent_wrt (f,g);

      reflexivity

      proof

        let S be non empty ManySortedSign;

        take ( id the carrier of S), ( id the carrier' of S);

        thus thesis by Th25;

      end;

      symmetry by Th26;

    end

    theorem :: CIRCTRM1:29

    for S1,S2,S3 be non empty ManySortedSign st (S1,S2) are_equivalent & (S2,S3) are_equivalent holds (S1,S3) are_equivalent

    proof

      let S1,S2,S3 be non empty ManySortedSign;

      given f1,g1 be one-to-one Function such that

       A1: (S1,S2) are_equivalent_wrt (f1,g1);

      given f2,g2 be one-to-one Function such that

       A2: (S2,S3) are_equivalent_wrt (f2,g2);

      take (f2 * f1), (g2 * g1);

      thus thesis by A1, A2, Th27;

    end;

    definition

      let S1,S2 be non empty ManySortedSign;

      let f be Function;

      :: CIRCTRM1:def11

      pred f preserves_inputs_of S1,S2 means (f .: ( InputVertices S1)) c= ( InputVertices S2);

    end

    theorem :: CIRCTRM1:30

    

     Th30: for S1,S2 be non empty ManySortedSign holds for f,g be Function st (f,g) form_morphism_between (S1,S2) holds for v be Vertex of S1 holds (f . v) is Vertex of S2

    proof

      let S1,S2 be non empty ManySortedSign;

      let f,g be Function;

      assume that

       A1: ( dom f) = the carrier of S1 and ( dom g) = the carrier' of S1 and

       A2: ( rng f) c= the carrier of S2;

      now

        let v be Vertex of S1;

        (f . v) in ( rng f) by A1, FUNCT_1:def 3;

        hence (f . v) in the carrier of S2 by A2;

      end;

      hence thesis;

    end;

    theorem :: CIRCTRM1:31

    

     Th31: for S1,S2 be non empty non void ManySortedSign holds for f,g be Function st (f,g) form_morphism_between (S1,S2) holds for v be Gate of S1 holds (g . v) is Gate of S2

    proof

      let S1,S2 be non empty non void ManySortedSign;

      let f,g be Function;

      assume that ( dom f) = the carrier of S1 and

       A1: ( dom g) = the carrier' of S1 and ( rng f) c= the carrier of S2 and

       A2: ( rng g) c= the carrier' of S2;

      now

        let v be Gate of S1;

        (g . v) in ( rng g) by A1, FUNCT_1:def 3;

        hence (g . v) in the carrier' of S2 by A2;

      end;

      hence thesis;

    end;

    theorem :: CIRCTRM1:32

    

     Th32: for S1,S2 be non empty ManySortedSign holds for f,g be Function st (f,g) form_morphism_between (S1,S2) holds (f .: ( InnerVertices S1)) c= ( InnerVertices S2)

    proof

      let S1,S2 be non empty ManySortedSign;

      let f,g be Function;

      assume (f,g) form_morphism_between (S1,S2);

      then (f * the ResultSort of S1) = (the ResultSort of S2 * g);

      then (f .: ( InnerVertices S1)) = ( rng (the ResultSort of S2 * g)) by RELAT_1: 127;

      hence thesis by RELAT_1: 26;

    end;

    theorem :: CIRCTRM1:33

    

     Th33: for S1,S2 be Circuit-like non void non empty ManySortedSign holds for f,g be Function st (f,g) form_morphism_between (S1,S2) holds for v1 be Vertex of S1 st v1 in ( InnerVertices S1) holds for v2 be Vertex of S2 st v2 = (f . v1) holds ( action_at v2) = (g . ( action_at v1))

    proof

      let S1,S2 be Circuit-like non void non empty ManySortedSign;

      let f,g be Function such that

       A1: (f,g) form_morphism_between (S1,S2);

      let v1 be Vertex of S1 such that

       A2: v1 in ( InnerVertices S1);

      let v2 be Vertex of S2 such that

       A3: v2 = (f . v1);

      reconsider g1 = (g . ( action_at v1)) as Gate of S2 by A1, Th31;

      

       A4: ( dom g) = the carrier' of S1 by A1;

      

       A5: ( dom f) = the carrier of S1 by A1;

      

       A6: ( dom the ResultSort of S1) = the carrier' of S1 by FUNCT_2:def 1;

      

       A7: (f .: ( InnerVertices S1)) c= ( InnerVertices S2) by A1, Th32;

      

       A8: v2 in (f .: ( InnerVertices S1)) by A2, A3, A5, FUNCT_1:def 6;

      ( the_result_sort_of g1) = ((the ResultSort of S2 * g) . ( action_at v1)) by A4, FUNCT_1: 13

      .= ((f * the ResultSort of S1) . ( action_at v1)) by A1

      .= (f . ( the_result_sort_of ( action_at v1))) by A6, FUNCT_1: 13

      .= v2 by A2, A3, MSAFREE2:def 7;

      hence thesis by A7, A8, MSAFREE2:def 7;

    end;

    definition

      let S1,S2 be non empty ManySortedSign;

      let f,g be Function;

      let C1 be non-empty MSAlgebra over S1;

      let C2 be non-empty MSAlgebra over S2;

      :: CIRCTRM1:def12

      pred f,g form_embedding_of C1,C2 means f is one-to-one & g is one-to-one & (f,g) form_morphism_between (S1,S2) & the Sorts of C1 = (the Sorts of C2 * f) & the Charact of C1 = (the Charact of C2 * g);

    end

    theorem :: CIRCTRM1:34

    

     Th34: for S be non empty ManySortedSign holds for C be non-empty MSAlgebra over S holds (( id the carrier of S),( id the carrier' of S)) form_embedding_of (C,C)

    proof

      let S be non empty ManySortedSign;

      let C be non-empty MSAlgebra over S;

      thus ( id the carrier of S) is one-to-one;

      

       A1: ( dom the Sorts of C) = the carrier of S by PARTFUN1:def 2;

      ( dom the Charact of C) = the carrier' of S by PARTFUN1:def 2;

      hence thesis by A1, INSTALG1: 8, RELAT_1: 52;

    end;

    theorem :: CIRCTRM1:35

    

     Th35: for S1,S2,S3 be non empty ManySortedSign holds for f1,g1,f2,g2 be Function holds for C1 be non-empty MSAlgebra over S1 holds for C2 be non-empty MSAlgebra over S2 holds for C3 be non-empty MSAlgebra over S3 st (f1,g1) form_embedding_of (C1,C2) & (f2,g2) form_embedding_of (C2,C3) holds ((f2 * f1),(g2 * g1)) form_embedding_of (C1,C3) by PUA2MSS1: 29, RELAT_1: 36;

    definition

      let S1,S2 be non empty ManySortedSign;

      let f,g be Function;

      let C1 be non-empty MSAlgebra over S1;

      let C2 be non-empty MSAlgebra over S2;

      :: CIRCTRM1:def13

      pred C1,C2 are_similar_wrt f,g means (f,g) form_embedding_of (C1,C2) & ((f " ),(g " )) form_embedding_of (C2,C1);

    end

    theorem :: CIRCTRM1:36

    

     Th36: for S1,S2 be non empty ManySortedSign holds for f,g be Function holds for C1 be non-empty MSAlgebra over S1 holds for C2 be non-empty MSAlgebra over S2 st (C1,C2) are_similar_wrt (f,g) holds (S1,S2) are_equivalent_wrt (f,g)

    proof

      let S1,S2 be non empty ManySortedSign;

      let f,g be Function;

      let C1 be non-empty MSAlgebra over S1;

      let C2 be non-empty MSAlgebra over S2;

      assume that

       A1: f is one-to-one and

       A2: g is one-to-one and

       A3: (f,g) form_morphism_between (S1,S2) and the Sorts of C1 = (the Sorts of C2 * f) and the Charact of C1 = (the Charact of C2 * g) and (f " ) is one-to-one and (g " ) is one-to-one and

       A4: ((f " ),(g " )) form_morphism_between (S2,S1);

      thus thesis by A1, A2, A3, A4;

    end;

    theorem :: CIRCTRM1:37

    

     Th37: for S1,S2 be non empty ManySortedSign holds for f,g be Function holds for C1 be non-empty MSAlgebra over S1 holds for C2 be non-empty MSAlgebra over S2 holds (C1,C2) are_similar_wrt (f,g) iff (S1,S2) are_equivalent_wrt (f,g) & the Sorts of C1 = (the Sorts of C2 * f) & the Charact of C1 = (the Charact of C2 * g)

    proof

      let S1,S2 be non empty ManySortedSign;

      let f,g be Function;

      let C1 be non-empty MSAlgebra over S1;

      let C2 be non-empty MSAlgebra over S2;

      hereby

        assume

         A1: (C1,C2) are_similar_wrt (f,g);

        hence (S1,S2) are_equivalent_wrt (f,g) by Th36;

        (f,g) form_embedding_of (C1,C2) by A1;

        hence the Sorts of C1 = (the Sorts of C2 * f) & the Charact of C1 = (the Charact of C2 * g);

      end;

      assume that

       A2: f is one-to-one and

       A3: g is one-to-one and

       A4: (f,g) form_morphism_between (S1,S2) and

       A5: ((f " ),(g " )) form_morphism_between (S2,S1) and

       A6: the Sorts of C1 = (the Sorts of C2 * f) and

       A7: the Charact of C1 = (the Charact of C2 * g);

      thus f is one-to-one & g is one-to-one & (f,g) form_morphism_between (S1,S2) & the Sorts of C1 = (the Sorts of C2 * f) & the Charact of C1 = (the Charact of C2 * g) by A2, A3, A4, A6, A7;

      thus (f " ) is one-to-one & (g " ) is one-to-one by A2, A3;

      thus ((f " ),(g " )) form_morphism_between (S2,S1) by A5;

      ( dom (f " )) = the carrier of S2 by A5;

      then ( rng f) = the carrier of S2 by A2, FUNCT_1: 33;

      

      then (f * (f " )) = ( id the carrier of S2) by A2, FUNCT_1: 39

      .= ( id ( dom the Sorts of C2)) by PARTFUN1:def 2;

      

      hence the Sorts of C2 = (the Sorts of C2 * (f * (f " ))) by RELAT_1: 52

      .= (the Sorts of C1 * (f " )) by A6, RELAT_1: 36;

      ( dom (g " )) = the carrier' of S2 by A5;

      then ( rng g) = the carrier' of S2 by A3, FUNCT_1: 33;

      

      then (g * (g " )) = ( id the carrier' of S2) by A3, FUNCT_1: 39

      .= ( id ( dom the Charact of C2)) by PARTFUN1:def 2;

      

      hence the Charact of C2 = (the Charact of C2 * (g * (g " ))) by RELAT_1: 52

      .= (the Charact of C1 * (g " )) by A7, RELAT_1: 36;

    end;

    theorem :: CIRCTRM1:38

    for S be non empty ManySortedSign holds for C be non-empty MSAlgebra over S holds (C,C) are_similar_wrt (( id the carrier of S),( id the carrier' of S))

    proof

      let S be non empty ManySortedSign;

      let C be non-empty MSAlgebra over S;

      set f = ( id the carrier of S), g = ( id the carrier' of S);

      

       A1: (f " ) = f by FUNCT_1: 45;

      (g " ) = g by FUNCT_1: 45;

      hence (f,g) form_embedding_of (C,C) & ((f " ),(g " )) form_embedding_of (C,C) by A1, Th34;

    end;

    theorem :: CIRCTRM1:39

    

     Th39: for S1,S2 be non empty ManySortedSign holds for f,g be Function holds for C1 be non-empty MSAlgebra over S1 holds for C2 be non-empty MSAlgebra over S2 st (C1,C2) are_similar_wrt (f,g) holds (C2,C1) are_similar_wrt ((f " ),(g " ))

    proof

      let S1,S2 be non empty ManySortedSign;

      let f,g be Function;

      let C1 be non-empty MSAlgebra over S1;

      let C2 be non-empty MSAlgebra over S2;

      assume that

       A1: (f,g) form_embedding_of (C1,C2) and

       A2: ((f " ),(g " )) form_embedding_of (C2,C1);

      

       A3: f is one-to-one by A1;

      ((f " ) " ) = f by A3, FUNCT_1: 43;

      hence ((f " ),(g " )) form_embedding_of (C2,C1) & (((f " ) " ),((g " ) " )) form_embedding_of (C1,C2) by A1, A2, FUNCT_1: 43;

    end;

    theorem :: CIRCTRM1:40

    for S1,S2,S3 be non empty ManySortedSign holds for f1,g1,f2,g2 be Function holds for C1 be non-empty MSAlgebra over S1 holds for C2 be non-empty MSAlgebra over S2 holds for C3 be non-empty MSAlgebra over S3 st (C1,C2) are_similar_wrt (f1,g1) & (C2,C3) are_similar_wrt (f2,g2) holds (C1,C3) are_similar_wrt ((f2 * f1),(g2 * g1))

    proof

      let S1,S2,S3 be non empty ManySortedSign;

      let f1,g1,f2,g2 be Function;

      let C1 be non-empty MSAlgebra over S1;

      let C2 be non-empty MSAlgebra over S2;

      let C3 be non-empty MSAlgebra over S3;

      assume that

       A1: (f1,g1) form_embedding_of (C1,C2) and

       A2: ((f1 " ),(g1 " )) form_embedding_of (C2,C1) and

       A3: (f2,g2) form_embedding_of (C2,C3) and

       A4: ((f2 " ),(g2 " )) form_embedding_of (C3,C2);

      thus ((f2 * f1),(g2 * g1)) form_embedding_of (C1,C3) by A1, A3, Th35;

      

       A5: f1 is one-to-one by A1;

      

       A6: g1 is one-to-one by A1;

      

       A7: f2 is one-to-one by A3;

      

       A8: g2 is one-to-one by A3;

      

       A9: ((f2 * f1) " ) = ((f1 " ) * (f2 " )) by A5, A7, FUNCT_1: 44;

      ((g2 * g1) " ) = ((g1 " ) * (g2 " )) by A6, A8, FUNCT_1: 44;

      hence thesis by A2, A4, A9, Th35;

    end;

    definition

      let S1,S2 be non empty ManySortedSign;

      let C1 be non-empty MSAlgebra over S1;

      let C2 be non-empty MSAlgebra over S2;

      :: CIRCTRM1:def14

      pred C1,C2 are_similar means ex f,g be Function st (C1,C2) are_similar_wrt (f,g);

    end

    reserve G1,G2 for Circuit-like non void non empty ManySortedSign,

f,g for Function,

C1 for non-empty Circuit of G1,

C2 for non-empty Circuit of G2;

    theorem :: CIRCTRM1:41

    

     Th41: (f,g) form_embedding_of (C1,C2) implies ( dom f) = the carrier of G1 & ( rng f) c= the carrier of G2 & ( dom g) = the carrier' of G1 & ( rng g) c= the carrier' of G2

    proof

      assume that f is one-to-one and g is one-to-one and

       A1: ( dom f) = the carrier of G1 and

       A2: ( dom g) = the carrier' of G1 and

       A3: ( rng f) c= the carrier of G2 and

       A4: ( rng g) c= the carrier' of G2;

      thus thesis by A1, A2, A3, A4;

    end;

    theorem :: CIRCTRM1:42

    

     Th42: (f,g) form_embedding_of (C1,C2) implies for o1 be Gate of G1, o2 be Gate of G2 st o2 = (g . o1) holds ( Den (o2,C2)) = ( Den (o1,C1))

    proof

      assume that f is one-to-one and g is one-to-one and

       A1: (f,g) form_morphism_between (G1,G2) and the Sorts of C1 = (the Sorts of C2 * f) and

       A2: the Charact of C1 = (the Charact of C2 * g);

      let o1 be Gate of G1, o2 be Gate of G2 such that

       A3: o2 = (g . o1);

      ( dom g) = the carrier' of G1 by A1;

      hence thesis by A2, A3, FUNCT_1: 13;

    end;

    theorem :: CIRCTRM1:43

    

     Th43: (f,g) form_embedding_of (C1,C2) implies for o1 be Gate of G1, o2 be Gate of G2 st o2 = (g . o1) holds for s1 be State of C1, s2 be State of C2 st s1 = (s2 * f) holds (o2 depends_on_in s2) = (o1 depends_on_in s1)

    proof

      assume that f is one-to-one and g is one-to-one and

       A1: (f,g) form_morphism_between (G1,G2) and the Sorts of C1 = (the Sorts of C2 * f) and the Charact of C1 = (the Charact of C2 * g);

      let o1 be Gate of G1, o2 be Gate of G2 such that

       A2: o2 = (g . o1);

      let s1 be State of C1, s2 be State of C2 such that

       A3: s1 = (s2 * f);

      

      thus (o2 depends_on_in s2) = (s2 * ( the_arity_of o2)) by CIRCUIT1:def 3

      .= (s2 * (f * ( the_arity_of o1))) by A1, A2

      .= (s1 * ( the_arity_of o1)) by A3, RELAT_1: 36

      .= (o1 depends_on_in s1) by CIRCUIT1:def 3;

    end;

    theorem :: CIRCTRM1:44

    

     Th44: (f,g) form_embedding_of (C1,C2) implies for s be State of C2 holds (s * f) is State of C1

    proof

      set S1 = G1, S2 = G2;

      assume that f is one-to-one and g is one-to-one and

       A1: (f,g) form_morphism_between (S1,S2) and

       A2: the Sorts of C1 = (the Sorts of C2 * f) and the Charact of C1 = (the Charact of C2 * g);

      let s be State of C2;

      

       A3: ( dom the Sorts of C2) = the carrier of S2 by PARTFUN1:def 2;

      

       A4: ( dom the Sorts of C1) = the carrier of S1 by PARTFUN1:def 2;

      

       A5: ( dom s) = ( dom the Sorts of C2) by CARD_3: 9;

      

       A6: ( rng f) c= the carrier of S2 by A1;

      

       A7: ( dom f) = the carrier of S1 by A1;

      then

       A8: ( dom (s * f)) = the carrier of S1 by A3, A5, A6, RELAT_1: 27;

      now

        let x be object;

        assume

         A9: x in the carrier of S1;

        then

         A10: (f . x) in ( rng f) by A7, FUNCT_1:def 3;

        ((s * f) . x) = (s . (f . x)) by A7, A9, FUNCT_1: 13;

        then ((s * f) . x) in (the Sorts of C2 . (f . x)) by A3, A6, A10, CARD_3: 9;

        hence ((s * f) . x) in (the Sorts of C1 . x) by A2, A7, A9, FUNCT_1: 13;

      end;

      hence thesis by A4, A8, CARD_3: 9;

    end;

    theorem :: CIRCTRM1:45

    

     Th45: (f,g) form_embedding_of (C1,C2) implies for s2 be State of C2, s1 be State of C1 st s1 = (s2 * f) & for v be Vertex of G1 st v in ( InputVertices G1) holds s2 is_stable_at (f . v) holds ( Following s1) = (( Following s2) * f)

    proof

      assume

       A1: (f,g) form_embedding_of (C1,C2);

      then

       A2: (f,g) form_morphism_between (G1,G2);

      let s2 be State of C2, s1 be State of C1 such that

       A3: s1 = (s2 * f) and

       A4: for v be Vertex of G1 st v in ( InputVertices G1) holds s2 is_stable_at (f . v);

      reconsider s29 = (( Following s2) * f) as State of C1 by A1, Th44;

      

       A5: ( dom f) = the carrier of G1 by A2;

      now

        let v be Vertex of G1;

        

         A6: (s29 . v) = (( Following s2) . (f . v)) by A5, FUNCT_1: 13;

        reconsider fv = (f . v) as Vertex of G2 by A2, Th30;

        hereby

          assume v in ( InputVertices G1);

          then

           A7: s2 is_stable_at (f . v) by A4;

          ( Following (s2,1)) = ( Following s2) by FACIRC_1: 14;

          

          hence (s29 . v) = (s2 . (f . v)) by A6, A7

          .= (s1 . v) by A3, A5, FUNCT_1: 13;

        end;

        

         A8: (f .: ( InnerVertices G1)) c= ( InnerVertices G2) by A2, Th32;

        assume

         A9: v in ( InnerVertices G1);

        then

         A10: fv in (f .: ( InnerVertices G1)) by A5, FUNCT_1:def 6;

        

         A11: ( action_at fv) = (g . ( action_at v)) by A2, A9, Th33;

        

        thus (s29 . v) = (( Den (( action_at fv),C2)) . (( action_at fv) depends_on_in s2)) by A6, A8, A10, CIRCUIT2:def 5

        .= (( Den (( action_at v),C1)) . (( action_at fv) depends_on_in s2)) by A1, A11, Th42

        .= (( Den (( action_at v),C1)) . (( action_at v) depends_on_in s1)) by A1, A3, A11, Th43;

      end;

      hence thesis by CIRCUIT2:def 5;

    end;

    theorem :: CIRCTRM1:46

    

     Th46: (f,g) form_embedding_of (C1,C2) & f preserves_inputs_of (G1,G2) implies for s2 be State of C2, s1 be State of C1 st s1 = (s2 * f) holds ( Following s1) = (( Following s2) * f)

    proof

      assume that

       A1: (f,g) form_embedding_of (C1,C2) and

       A2: (f .: ( InputVertices G1)) c= ( InputVertices G2);

      let s2 be State of C2, s1 be State of C1 such that

       A3: s1 = (s2 * f);

      

       A4: ( dom f) = the carrier of G1 by A1, Th41;

      now

        let v be Vertex of G1;

        assume v in ( InputVertices G1);

        then (f . v) in (f .: ( InputVertices G1)) by A4, FUNCT_1:def 6;

        hence s2 is_stable_at (f . v) by A2, FACIRC_1: 18;

      end;

      hence thesis by A1, A3, Th45;

    end;

    theorem :: CIRCTRM1:47

    

     Th47: (f,g) form_embedding_of (C1,C2) & f preserves_inputs_of (G1,G2) implies for s2 be State of C2, s1 be State of C1 st s1 = (s2 * f) holds for n be Nat holds ( Following (s1,n)) = (( Following (s2,n)) * f)

    proof

      assume that

       A1: (f,g) form_embedding_of (C1,C2) and

       A2: f preserves_inputs_of (G1,G2);

      let s2 be State of C2, s1 be State of C1 such that

       A3: s1 = (s2 * f);

      defpred P[ Nat] means ( Following (s1,$1)) = (( Following (s2,$1)) * f);

      ( Following (s1, 0 )) = s1 by FACIRC_1: 11;

      then

       A4: P[ 0 ] by A3, FACIRC_1: 11;

       A5:

      now

        let n be Nat;

        assume P[n];

        then ( Following ( Following (s1,n))) = (( Following ( Following (s2,n))) * f) by A1, A2, Th46;

        

        then ( Following (s1,(n + 1))) = (( Following ( Following (s2,n))) * f) by FACIRC_1: 12

        .= (( Following (s2,(n + 1))) * f) by FACIRC_1: 12;

        hence P[(n + 1)];

      end;

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

    end;

    theorem :: CIRCTRM1:48

    (f,g) form_embedding_of (C1,C2) & f preserves_inputs_of (G1,G2) implies for s2 be State of C2, s1 be State of C1 st s1 = (s2 * f) holds s2 is stable implies s1 is stable by Th46;

    theorem :: CIRCTRM1:49

    

     Th49: (f,g) form_embedding_of (C1,C2) & f preserves_inputs_of (G1,G2) implies for s2 be State of C2, s1 be State of C1 st s1 = (s2 * f) holds for v1 be Vertex of G1 holds s1 is_stable_at v1 iff s2 is_stable_at (f . v1)

    proof

      assume that

       A1: (f,g) form_embedding_of (C1,C2) and

       A2: f preserves_inputs_of (G1,G2);

      let s2 be State of C2, s1 be State of C1 such that

       A3: s1 = (s2 * f);

      let v1 be Vertex of G1;

      

       A4: (f,g) form_morphism_between (G1,G2) by A1;

      then

       A5: ( dom f) = the carrier of G1;

      reconsider v2 = (f . v1) as Vertex of G2 by A4, Th30;

      thus s1 is_stable_at v1 implies s2 is_stable_at (f . v1)

      proof

        assume

         A6: for n be Nat holds (( Following (s1,n)) . v1) = (s1 . v1);

        let n be Nat;

        ( Following (s1,n)) = (( Following (s2,n)) * f) by A1, A2, A3, Th47;

        

        hence (( Following (s2,n)) . (f . v1)) = (( Following (s1,n)) . v1) by A5, FUNCT_1: 13

        .= (s1 . v1) by A6

        .= (s2 . (f . v1)) by A3, A5, FUNCT_1: 13;

      end;

      assume

       A7: for n be Nat holds (( Following (s2,n)) . (f . v1)) = (s2 . (f . v1));

      let n be Nat;

      ( Following (s1,n)) = (( Following (s2,n)) * f) by A1, A2, A3, Th47;

      

      hence (( Following (s1,n)) . v1) = (( Following (s2,n)) . v2) by A5, FUNCT_1: 13

      .= (s2 . v2) by A7

      .= (s1 . v1) by A3, A5, FUNCT_1: 13;

    end;

    theorem :: CIRCTRM1:50

    (C1,C2) are_similar_wrt (f,g) implies for s be State of C2 holds (s * f) is State of C1 by Th44;

    theorem :: CIRCTRM1:51

    

     Th51: (C1,C2) are_similar_wrt (f,g) implies for s1 be State of C1, s2 be State of C2 holds s1 = (s2 * f) iff s2 = (s1 * (f " ))

    proof

      assume that

       A1: (f,g) form_embedding_of (C1,C2) and

       A2: ((f " ),(g " )) form_embedding_of (C2,C1);

      

       A3: f is one-to-one by A1;

      let s1 be State of C1;

      let s2 be State of C2;

      (f,g) form_morphism_between (G1,G2) by A1;

      then

       A4: ( dom f) = the carrier of G1;

      

       A5: ( dom s1) = the carrier of G1 by CIRCUIT1: 3;

      

       A6: ((s1 * (f " )) * f) = (s1 * ((f " ) * f)) by RELAT_1: 36

      .= (s1 * ( id ( dom f))) by A3, FUNCT_1: 39

      .= s1 by A4, A5, RELAT_1: 52;

      ((f " ),(g " )) form_morphism_between (G2,G1) by A2;

      then

       A7: ( dom (f " )) = the carrier of G2;

      

       A8: ( dom s2) = the carrier of G2 by CIRCUIT1: 3;

      ((s2 * f) * (f " )) = (s2 * (f * (f " ))) by RELAT_1: 36

      .= (s2 * (((f " ) " ) * (f " ))) by A3, FUNCT_1: 43

      .= (s2 * ( id ( dom (f " )))) by A3, FUNCT_1: 39;

      hence thesis by A6, A7, A8, RELAT_1: 52;

    end;

    theorem :: CIRCTRM1:52

    

     Th52: (C1,C2) are_similar_wrt (f,g) implies (f .: ( InputVertices G1)) = ( InputVertices G2) & (f .: ( InnerVertices G1)) = ( InnerVertices G2)

    proof

      assume (C1,C2) are_similar_wrt (f,g);

      then (G1,G2) are_equivalent_wrt (f,g) by Th36;

      hence thesis by Th28;

    end;

    theorem :: CIRCTRM1:53

    

     Th53: (C1,C2) are_similar_wrt (f,g) implies f preserves_inputs_of (G1,G2) by Th52;

    theorem :: CIRCTRM1:54

    

     Th54: (C1,C2) are_similar_wrt (f,g) implies for s1 be State of C1, s2 be State of C2 st s1 = (s2 * f) holds ( Following s1) = (( Following s2) * f) by Th46, Th53;

    theorem :: CIRCTRM1:55

    

     Th55: (C1,C2) are_similar_wrt (f,g) implies for s1 be State of C1, s2 be State of C2 st s1 = (s2 * f) holds for n be Element of NAT holds ( Following (s1,n)) = (( Following (s2,n)) * f) by Th47, Th53;

    theorem :: CIRCTRM1:56

    (C1,C2) are_similar_wrt (f,g) implies for s1 be State of C1, s2 be State of C2 st s1 = (s2 * f) holds s1 is stable iff s2 is stable

    proof

      assume

       A1: (C1,C2) are_similar_wrt (f,g);

      then

       A2: (C2,C1) are_similar_wrt ((f " ),(g " )) by Th39;

      let s1 be State of C1, s2 be State of C2 such that

       A3: s1 = (s2 * f);

      

       A4: s2 = (s1 * (f " )) by A1, A3, Th51;

      thus s1 is stable implies s2 is stable by A2, A4, Th54;

      assume s2 = ( Following s2);

      hence s1 = ( Following s1) by A1, A3, Th54;

    end;

    theorem :: CIRCTRM1:57

    (C1,C2) are_similar_wrt (f,g) implies for s1 be State of C1, s2 be State of C2 st s1 = (s2 * f) holds for v1 be Vertex of G1 holds s1 is_stable_at v1 iff s2 is_stable_at (f . v1)

    proof

      assume

       A1: (C1,C2) are_similar_wrt (f,g);

      then

       A2: (C2,C1) are_similar_wrt ((f " ),(g " )) by Th39;

      let s1 be State of C1, s2 be State of C2 such that

       A3: s1 = (s2 * f);

      let v1 be Vertex of G1;

      

       A4: (G1,G2) are_equivalent_wrt (f,g) by A1, Th37;

      then

       A5: (f,g) form_morphism_between (G1,G2);

      

       A6: ((f " ),(g " )) form_morphism_between (G2,G1) by A4;

      

       A7: ( dom f) = the carrier of G1 by A5;

      

       A8: ( dom (f " )) = the carrier of G2 by A6;

      reconsider v2 = (f . v1) as Vertex of G2 by A5, Th30;

      f is one-to-one by A4;

      then

       A9: v1 = ((f " ) . v2) by A7, FUNCT_1: 34;

      thus s1 is_stable_at v1 implies s2 is_stable_at (f . v1)

      proof

        assume

         A10: for n be Nat holds (( Following (s1,n)) . v1) = (s1 . v1);

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        then ( Following (s1,n)) = (( Following (s2,n)) * f) by A1, A3, Th55;

        

        hence (( Following (s2,n)) . (f . v1)) = (( Following (s1,n)) . v1) by A7, FUNCT_1: 13

        .= (s1 . v1) by A10

        .= (s2 . (f . v1)) by A3, A7, FUNCT_1: 13;

      end;

      assume

       A11: for n be Nat holds (( Following (s2,n)) . (f . v1)) = (s2 . (f . v1));

      let n be Nat;

      

       A12: n in NAT by ORDINAL1:def 12;

      s2 = (s1 * (f " )) by A1, A3, Th51;

      then ( Following (s2,n)) = (( Following (s1,n)) * (f " )) by A2, A12, Th55;

      

      hence (( Following (s1,n)) . v1) = (( Following (s2,n)) . v2) by A8, A9, FUNCT_1: 13

      .= (s2 . v2) by A11

      .= (s1 . v1) by A3, A7, FUNCT_1: 13;

    end;

    begin

    definition

      let S be non empty non void ManySortedSign;

      let A be non-empty MSAlgebra over S;

      let V be non-empty ManySortedSet of the carrier of S;

      let X be non empty Subset of (S -Terms V);

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

      let C be non-empty Circuit of G;

      :: CIRCTRM1:def15

      pred C calculates X,A means ex f, g st (f,g) form_embedding_of ((X -Circuit A),C) & f preserves_inputs_of ((X -CircuitStr ),G);

      :: CIRCTRM1:def16

      pred X,A specifies C means (C,(X -Circuit A)) are_similar ;

    end

    definition

      let S be non empty non void ManySortedSign;

      let V be non-empty ManySortedSet of the carrier of S;

      let A be non-empty MSAlgebra over S;

      let X be non empty Subset of (S -Terms V);

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

      let C be non-empty Circuit of G;

      assume C calculates (X,A);

      then

      consider f, g such that

       A1: (f,g) form_embedding_of ((X -Circuit A),C) and

       A2: f preserves_inputs_of ((X -CircuitStr ),G);

      :: CIRCTRM1:def17

      mode SortMap of X,A,C -> one-to-one Function means

      : Def17: it preserves_inputs_of ((X -CircuitStr ),G) & ex g st (it ,g) form_embedding_of ((X -Circuit A),C);

      existence by A1, A2;

    end

    definition

      let S be non empty non void ManySortedSign;

      let V be non-empty ManySortedSet of the carrier of S;

      let A be non-empty MSAlgebra over S;

      let X be non empty Subset of (S -Terms V);

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

      let C be non-empty Circuit of G;

      let f be SortMap of X, A, C;

      consider g such that

       A2: (f,g) form_embedding_of ((X -Circuit A),C) by A1, Def17;

      :: CIRCTRM1:def18

      mode OperMap of X,A,C,f -> one-to-one Function means (f,it ) form_embedding_of ((X -Circuit A),C);

      existence by A2;

    end

    theorem :: CIRCTRM1:58

    

     Th58: for G be Circuit-like non void non empty ManySortedSign holds for C be non-empty Circuit of G st (X,A) specifies C holds C calculates (X,A)

    proof

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

      let C be non-empty Circuit of G;

      given f,g be Function such that

       A1: (C,(X -Circuit A)) are_similar_wrt (f,g);

      take (f " ), (g " );

      thus ((f " ),(g " )) form_embedding_of ((X -Circuit A),C) by A1;

      ((X -Circuit A),C) are_similar_wrt ((f " ),(g " )) by A1, Th39;

      hence thesis by Th53;

    end;

    theorem :: CIRCTRM1:59

    

     Th59: for G be Circuit-like non void non empty ManySortedSign holds for C be non-empty Circuit of G st C calculates (X,A) holds for f be SortMap of X, A, C holds for t be Term of S, V st t in ( Subtrees X) holds for s be State of C holds ( Following (s,(1 + ( height ( dom t))))) is_stable_at (f . t) & for s9 be State of (X -Circuit A) st s9 = (s * f) holds for h be CompatibleValuation of s9 holds (( Following (s,(1 + ( height ( dom t))))) . (f . t)) = (t @ (h,A))

    proof

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

      let C be non-empty Circuit of G such that

       A1: C calculates (X,A);

      let f be SortMap of X, A, C;

      consider g such that

       A2: (f,g) form_embedding_of ((X -Circuit A),C) by A1, Def17;

      

       A3: f preserves_inputs_of ((X -CircuitStr ),G) by A1, Def17;

      

       A4: (f,g) form_morphism_between ((X -CircuitStr ),G) by A2;

      let t be Term of S, V such that

       A5: t in ( Subtrees X);

      let s be State of C;

      reconsider s9 = (s * f) as State of (X -Circuit A) by A2, Th44;

      reconsider t9 = t as Vertex of (X -CircuitStr ) by A5;

      

       A6: ( Following (s9,(1 + ( height ( dom t))))) is_stable_at t9 by Th21;

      

       A7: ( Following (s9,(1 + ( height ( dom t))))) = (( Following (s,(1 + ( height ( dom t))))) * f) by A2, A3, Th47;

      hence ( Following (s,(1 + ( height ( dom t))))) is_stable_at (f . t) by A2, A3, A6, Th49;

      let s9 be State of (X -Circuit A) such that

       A8: s9 = (s * f);

      let h be CompatibleValuation of s9;

      

       A9: ( dom f) = the carrier of (X -CircuitStr ) by A4;

      (( Following (s9,(1 + ( height ( dom t))))) . t9) = (t @ (h,A)) by Th21;

      hence thesis by A7, A8, A9, FUNCT_1: 13;

    end;

    theorem :: CIRCTRM1:60

    

     Th60: for G be Circuit-like non void non empty ManySortedSign holds for C be non-empty Circuit of G st C calculates (X,A) holds for t be Term of S, V st t in ( Subtrees X) holds ex v be Vertex of G st for s be State of C holds ( Following (s,(1 + ( height ( dom t))))) is_stable_at v & ex f be SortMap of X, A, C st for s9 be State of (X -Circuit A) st s9 = (s * f) holds for h be CompatibleValuation of s9 holds (( Following (s,(1 + ( height ( dom t))))) . v) = (t @ (h,A))

    proof

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

      let C be non-empty Circuit of G;

      assume

       A1: C calculates (X,A);

      then

      consider f, g such that

       A2: (f,g) form_embedding_of ((X -Circuit A),C) and

       A3: f preserves_inputs_of ((X -CircuitStr ),G);

      reconsider f as SortMap of X, A, C by A1, A2, A3, Def17;

      let t be Term of S, V such that

       A4: t in ( Subtrees X);

      

       A5: (f,g) form_morphism_between ((X -CircuitStr ),G) by A2;

      reconsider t9 = t as Vertex of (X -CircuitStr ) by A4;

      reconsider v = (f . t9) as Vertex of G by A5, Th30;

      take v;

      let s be State of C;

      thus ( Following (s,(1 + ( height ( dom t))))) is_stable_at v by A1, Th59;

      take f;

      thus thesis by A1, Th59;

    end;

    theorem :: CIRCTRM1:61

    for G be Circuit-like non void non empty ManySortedSign holds for C be non-empty Circuit of G st (X,A) specifies C holds for f be SortMap of X, A, C holds for s be State of C, t be Term of S, V st t in ( Subtrees X) holds ( Following (s,(1 + ( height ( dom t))))) is_stable_at (f . t) & for s9 be State of (X -Circuit A) st s9 = (s * f) holds for h be CompatibleValuation of s9 holds (( Following (s,(1 + ( height ( dom t))))) . (f . t)) = (t @ (h,A))

    proof

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

      let C be non-empty Circuit of G;

      assume (X,A) specifies C;

      then C calculates (X,A) by Th58;

      hence thesis by Th59;

    end;

    theorem :: CIRCTRM1:62

    for G be Circuit-like non void non empty ManySortedSign holds for C be non-empty Circuit of G st (X,A) specifies C holds for t be Term of S, V st t in ( Subtrees X) holds ex v be Vertex of G st for s be State of C holds ( Following (s,(1 + ( height ( dom t))))) is_stable_at v & ex f be SortMap of X, A, C st for s9 be State of (X -Circuit A) st s9 = (s * f) holds for h be CompatibleValuation of s9 holds (( Following (s,(1 + ( height ( dom t))))) . v) = (t @ (h,A)) by Th58, Th60;