The abstract of the Mizar article:

Circuit Generated by Terms and Circuit Calculating Terms

by

Grzegorz Bancerek

Received April 10, 2001

MML identifier: CIRCTRM1

[ Mizar article, MML identifier index ]

environ

 vocabulary AMI_1, MSUALG_1, ZF_REFLE, MSATERM, FUNCT_1, TREES_4, FREEALG,
      RELAT_1, BOOLE, PBOOLE, TREES_9, CIRCCOMB, MSAFREE2, TREES_1, FINSEQ_1,
      QC_LANG1, TREES_3, FINSET_1, TREES_2, PARTFUN1, FUNCT_4, MCART_1,
      PRALG_1, TDGROUP, CARD_3, PRE_CIRC, FACIRC_1, FUNCT_6, PUA2MSS1,
      ISOCAT_1, CQC_SIM1, CIRCUIT1, CIRCUIT2, CIRCTRM1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, NAT_1,
      RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSET_1, PARTFUN1, MCART_1,
      FUNCT_4, CARD_3, STRUCT_0, PRALG_1, PBOOLE, MSUALG_1, PRE_CIRC, MSAFREE2,
      CIRCUIT1, CIRCUIT2, CIRCCOMB, FACIRC_1, TREES_1, TREES_2, TREES_3,
      TREES_4, TREES_9, MSATERM, PUA2MSS1;
 constructors TREES_9, MSATERM, FINSEQ_4, MSUALG_3, CIRCUIT1, CIRCUIT2,
      FACIRC_1, PUA2MSS1, INSTALG1;
 clusters ARYTM_3, SUBSET_1, STRUCT_0, PRELAMB, FUNCT_1, RELSET_1, FINSEQ_1,
      MSUALG_1, MSUALG_2, TREES_2, TREES_3, XBOOLE_0, TREES_9, PRALG_1,
      MSAFREE, MSATERM, PRE_CIRC, CIRCCOMB, INSTALG1, MEMBERED;
 requirements NUMERALS, BOOLE, SUBSET;


begin :: <section1>Circuit structure generated by terms</section1>

theorem :: CIRCTRM1:1
 for S being non empty non void ManySortedSign
 for A being non-empty MSAlgebra over S
 for V being Variables of A
 for t being Term of S,V, T being c-Term of A,V st T = t
  holds the_sort_of T = the_sort_of t;

definition let D be non empty set;
 let X be Subset of D;
 redefine func id X -> Function of X, D;
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;
 func X-CircuitStr -> non empty strict ManySortedSign equals
:: CIRCTRM1:def 1

  ManySortedSign(#
        Subtrees X, [:the OperSymbols of S,{the carrier of S}:]-Subtrees X,
        [:the OperSymbols of S,{the carrier of S}:]-ImmediateSubtrees X,
        id ([:the OperSymbols of S,{the carrier of S}:]-Subtrees X)
       #);
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;
 cluster X-CircuitStr -> unsplit;
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 being Element of X holds t is root &
        not t.{} in [:the OperSymbols of S, {the carrier of S}:];

theorem :: CIRCTRM1:3
 X is SetWithCompoundTerm of S,V iff X-CircuitStr is non void;

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;
 cluster X-CircuitStr -> non void;
end;

theorem :: CIRCTRM1:4
 (for v being Vertex of X-CircuitStr holds v is Term of S,V) &
 (for s being set st s in the OperSymbols of X-CircuitStr holds
      s is CompoundTerm of S,V);

theorem :: CIRCTRM1:5
 for t being Vertex of X-CircuitStr holds
  t in the OperSymbols of X-CircuitStr iff t is CompoundTerm of S,V;

theorem :: CIRCTRM1:6
 for X being SetWithCompoundTerm of S,V, g being Gate of X-CircuitStr holds
   (the ResultSort of X-CircuitStr).g = g & the_result_sort_of g = g;

definition
 let S,V;
 let X be SetWithCompoundTerm of S,V, g be Gate of X-CircuitStr;
 cluster the_arity_of g -> DTree-yielding;
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;
 cluster -> finite Function-like Relation-like Vertex of X-CircuitStr;
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;
 cluster -> DecoratedTree-like Vertex of X-CircuitStr;
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;
 cluster -> finite Function-like Relation-like Gate of X-CircuitStr;
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;
 cluster -> DecoratedTree-like Gate of X-CircuitStr;
end;

::theorem
:: for X being SetWithCompoundTerm of A,V, g being Gate of X-CircuitStr
::  for t being Term of A,V st t = g holds
::   the_arity_of g = subs t ? subs g

theorem :: CIRCTRM1:7
 for X1,X2 being 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;

definition
 let X,Y be constituted-DTrees set;
 cluster X \/ Y -> constituted-DTrees;
end;

theorem :: CIRCTRM1:8
 for X1,X2 being constituted-DTrees non empty set holds
   Subtrees (X1 \/ X2) = (Subtrees X1) \/ (Subtrees X2);

theorem :: CIRCTRM1:9
 for X1,X2 being constituted-DTrees non empty set, C be set holds
   C-Subtrees (X1 \/ X2) = (C-Subtrees X1) \/ (C-Subtrees X2);

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

theorem :: CIRCTRM1:11
 for X1,X2 being non empty Subset of S-Terms V holds
  (X1 \/ X2)-CircuitStr = (X1-CircuitStr)+*(X2-CircuitStr);

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

theorem :: CIRCTRM1:13
 for X being SetWithCompoundTerm of S,V, g being Gate of X-CircuitStr
  holds g = (g.{})-tree the_arity_of g;

begin  :: <section2>Circuit genereted by terms</section2>

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;
 func the_sort_of (v, A) means
:: CIRCTRM1:def 2

  for u being Term of S,V st u = v holds it = (the Sorts of A).the_sort_of u;
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 v be Vertex of X-CircuitStr;
 let A be non-empty MSAlgebra over S;
 cluster the_sort_of (v, A) -> non empty;
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
       X is SetWithCompoundTerm of S,V;
 let o be Gate of X-CircuitStr;

 let A be MSAlgebra over S;
 func the_action_of (o, A) -> Function means
:: CIRCTRM1:def 3

  for X' being SetWithCompoundTerm of S,V st X' = X
   for o' being Gate of X'-CircuitStr st o' = o holds
    it = (the Charact of A).(o'.{})`1;
end;

scheme MSFuncEx {I() -> non empty set, A,B() -> non-empty ManySortedSet of I(),
          P[set,set,set]}:
 ex f being ManySortedFunction of A(),B() st
  for i being Element of I(), a being Element of A().i holds P[i,a,f.i.a]
 provided
  for i being Element of I(), a being Element of A().i
     ex b being Element of B().i st P[i,a,b];

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;
 func X-CircuitSorts A ->
   ManySortedSet of the carrier of X-CircuitStr means
:: CIRCTRM1:def 4

  for v being Vertex of X-CircuitStr holds it.v = the_sort_of (v, A);
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;
 cluster X-CircuitSorts A -> non-empty;
end;

theorem :: CIRCTRM1:14
 for X being SetWithCompoundTerm of S,V,
     g being Gate of X-CircuitStr
  for o being 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;

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;
 func X-CircuitCharact A -> ManySortedFunction of
   (X-CircuitSorts A)#*(the Arity of X-CircuitStr),
   (X-CircuitSorts A)*(the ResultSort of X-CircuitStr)
 means
:: CIRCTRM1:def 5

  for g being Gate of X-CircuitStr st g in the OperSymbols of X-CircuitStr
   holds it.g = the_action_of (g, A);
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;
 func X-Circuit A -> non-empty strict MSAlgebra over X-CircuitStr equals
:: CIRCTRM1:def 6

   MSAlgebra(#X-CircuitSorts A, X-CircuitCharact A#);
end;

theorem :: CIRCTRM1:15
   for v being Vertex of X-CircuitStr
  holds (the Sorts of X-Circuit A).v = the_sort_of (v, A);

theorem :: CIRCTRM1:16
 for A being locally-finite non-empty MSAlgebra over S
 for X being SetWithCompoundTerm of S,V
 for g being OperSymbol of X-CircuitStr
  holds Den(g, X-Circuit A) = the_action_of (g, A);

theorem :: CIRCTRM1:17
 for A being locally-finite non-empty MSAlgebra over S
 for X being SetWithCompoundTerm of S,V
 for g being OperSymbol of X-CircuitStr, o being OperSymbol of S
  st g.{} = [o, the carrier of S]
  holds Den(g, X-Circuit A) = Den(o,A);

theorem :: CIRCTRM1:18
 for A being locally-finite non-empty MSAlgebra over S,
     X being non empty Subset of S-Terms V holds
 X-Circuit A is locally-finite;

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 locally-finite non-empty MSAlgebra over S;
 cluster X-Circuit A -> locally-finite;
end;

theorem :: CIRCTRM1:19
 for S being non empty non void ManySortedSign
 for V being non-empty ManySortedSet of the carrier of S
 for X1,X2 being SetWithCompoundTerm of S,V
 for A being non-empty MSAlgebra over S holds
  X1-Circuit A tolerates X2-Circuit A;

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

begin :: <section3>Correctness of a Term Circuit</section3>

reserve S for non empty non void ManySortedSign,
 A for non-empty locally-finite 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 such that  t is Term of S,V;
 let f be ManySortedFunction of V, the Sorts of A;
 func t@(f,A) means
:: CIRCTRM1:def 7

  ex t' being c-Term of A,V st t' = t & it = t'@f;
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 locally-finite MSAlgebra over S;
 let s be State of X-Circuit A;
 mode CompatibleValuation of s -> ManySortedFunction of V, the Sorts of A
 means
:: CIRCTRM1:def 8

  for x being Vertex of S, v being Element of V.x
   st root-tree [v,x] in Subtrees X
   holds it.x.v = s.root-tree [v,x];
end;

theorem :: CIRCTRM1:21
   for s being State of X-Circuit A
 for f being CompatibleValuation of s, n being Nat
  holds f is CompatibleValuation of Following(s,n);

definition
 let x be set;
 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;
end;

theorem :: CIRCTRM1:22
 for s being State of X-Circuit A
 for f being CompatibleValuation of s
 for t being 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);

theorem :: CIRCTRM1:23
   not (ex t being Term of S,V, o being OperSymbol of S st
       t in Subtrees X & t.{} = [o,the carrier of S] & the_arity_of o = {})
 implies
  for s being State of X-Circuit A
  for f being CompatibleValuation of s
  for t being 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);

begin :: <section4>Circuit similarity</section4>

definition
 let X be set;
 cluster id X -> one-to-one;
end;

definition
 let f be one-to-one Function;
 cluster f" -> one-to-one;
 let g be one-to-one Function;
 cluster g*f -> one-to-one;
end;

definition
 let S1, S2 be non empty ManySortedSign;
 let f,g be Function;
 pred S1, S2 are_equivalent_wrt f, g means
:: CIRCTRM1:def 9

   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:24
 for S1, S2 being non empty ManySortedSign, f,g being Function
  st S1, S2 are_equivalent_wrt f, g
  holds the carrier of S2 = f.:the carrier of S1 &
        the OperSymbols of S2 = g.:the OperSymbols of S1;

theorem :: CIRCTRM1:25
 for S1, S2 being non empty ManySortedSign, f,g being Function
  st S1, S2 are_equivalent_wrt f, g
  holds rng f = the carrier of S2 & rng g = the OperSymbols of S2;

theorem :: CIRCTRM1:26
 for S being non empty ManySortedSign holds
  S, S are_equivalent_wrt id the carrier of S, id the OperSymbols of S;

theorem :: CIRCTRM1:27
 for S1, S2 being non empty ManySortedSign, f,g being Function
  st S1, S2 are_equivalent_wrt f, g
  holds S2, S1 are_equivalent_wrt f", g";

theorem :: CIRCTRM1:28
 for S1, S2, S3 being non empty ManySortedSign, f1,g1, f2,g2 being 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;

theorem :: CIRCTRM1:29
 for S1, S2 being non empty ManySortedSign, f,g being Function
  st S1, S2 are_equivalent_wrt f, g
  holds
   f.:InputVertices S1 = InputVertices S2 &
   f.:InnerVertices S1 = InnerVertices S2;

definition
 let S1, S2 be non empty ManySortedSign;
 pred S1, S2 are_equivalent means
:: CIRCTRM1:def 10
    ex f,g being one-to-one Function st S1, S2 are_equivalent_wrt f, g;
 reflexivity;
 symmetry;
end;

theorem :: CIRCTRM1:30
   for S1, S2, S3 being non empty ManySortedSign
  st S1, S2 are_equivalent & S2, S3 are_equivalent
  holds S1, S3 are_equivalent;

definition
 let S1, S2 be non empty ManySortedSign;
 let f be Function;
 pred f preserves_inputs_of S1, S2 means
:: CIRCTRM1:def 11
   f.:InputVertices S1 c= InputVertices S2;
end;

theorem :: CIRCTRM1:31
 for S1, S2 being non empty ManySortedSign
 for f, g being Function st f, g form_morphism_between S1, S2
 for v being Vertex of S1 holds f.v is Vertex of S2;

theorem :: CIRCTRM1:32
 for S1, S2 being non empty non void ManySortedSign
 for f, g being Function st f, g form_morphism_between S1, S2
 for v being Gate of S1 holds g.v is Gate of S2;

theorem :: CIRCTRM1:33
 for S1, S2 being non empty ManySortedSign
 for f, g being Function st f, g form_morphism_between S1, S2
  holds f.:InnerVertices S1 c= InnerVertices S2;

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

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;
 pred f, g form_embedding_of C1, C2 means
:: CIRCTRM1:def 12

  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:35
 for S being non empty ManySortedSign
 for C being non-empty MSAlgebra over S
  holds id the carrier of S, id the OperSymbols of S form_embedding_of C, C;

theorem :: CIRCTRM1:36
 for S1,S2,S3 being non empty ManySortedSign
 for f1,g1, f2,g2 being Function
 for C1 being non-empty MSAlgebra over S1
 for C2 being non-empty MSAlgebra over S2
 for C3 being 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;

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;
 pred C1, C2 are_similar_wrt f, g means
:: CIRCTRM1:def 13

  f, g form_embedding_of C1, C2 & f", g" form_embedding_of C2, C1;
end;

theorem :: CIRCTRM1:37
 for S1, S2 being non empty ManySortedSign
 for f, g being Function
 for C1 being non-empty MSAlgebra over S1
 for C2 being non-empty MSAlgebra over S2
  st C1, C2 are_similar_wrt f, g
  holds S1, S2 are_equivalent_wrt f, g;

theorem :: CIRCTRM1:38
 for S1, S2 being non empty ManySortedSign
 for f, g being Function
 for C1 being non-empty MSAlgebra over S1
 for C2 being 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;

theorem :: CIRCTRM1:39
   for S being non empty ManySortedSign
 for C being non-empty MSAlgebra over S
  holds C, C are_similar_wrt id the carrier of S, id the OperSymbols of S;

theorem :: CIRCTRM1:40
 for S1, S2 being non empty ManySortedSign
 for f, g being Function
 for C1 being non-empty MSAlgebra over S1
 for C2 being non-empty MSAlgebra over S2
  st C1, C2 are_similar_wrt f, g
  holds C2, C1 are_similar_wrt f", g";

theorem :: CIRCTRM1:41
   for S1, S2, S3 being non empty ManySortedSign
 for f1, g1, f2, g2 being Function
 for C1 being non-empty MSAlgebra over S1
 for C2 being non-empty MSAlgebra over S2
 for C3 being 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;


definition
 let S1, S2 be non empty ManySortedSign;
 let C1 be non-empty MSAlgebra over S1;
 let C2 be non-empty MSAlgebra over S2;
 pred C1, C2 are_similar means
:: CIRCTRM1:def 14
    ex f, g being 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:42
 f, g form_embedding_of C1, C2 implies
  dom f = the carrier of G1 & rng f c= the carrier of G2 &
  dom g = the OperSymbols of G1 & rng g c= the OperSymbols of G2;

theorem :: CIRCTRM1:43
 f, g form_embedding_of C1, C2 implies
  for o1 being Gate of G1, o2 being Gate of G2 st o2 = g.o1
   holds Den(o2, C2) = Den(o1, C1);

theorem :: CIRCTRM1:44
 f, g form_embedding_of C1, C2 implies
  for o1 being Gate of G1, o2 being Gate of G2 st o2 = g.o1
  for s1 being State of C1, s2 being State of C2 st s1 = s2*f
   holds o2 depends_on_in s2 = o1 depends_on_in s1;

theorem :: CIRCTRM1:45
 f, g form_embedding_of C1, C2 implies
  for s being State of C2 holds s*f is State of C1;

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

theorem :: CIRCTRM1:47
 f, g form_embedding_of C1, C2 & f preserves_inputs_of G1, G2 implies
  for s2 being State of C2, s1 being State of C1 st s1 = s2*f
   holds Following s1 = (Following s2)*f;

theorem :: CIRCTRM1:48
 f, g form_embedding_of C1, C2 & f preserves_inputs_of G1, G2 implies
  for s2 being State of C2, s1 being State of C1 st s1 = s2*f
  for n being Nat
   holds Following(s1,n) = Following(s2,n)*f;

theorem :: CIRCTRM1:49
   f, g form_embedding_of C1, C2 & f preserves_inputs_of G1, G2 implies
  for s2 being State of C2, s1 being State of C1 st s1 = s2*f
   holds s2 is stable implies s1 is stable;

theorem :: CIRCTRM1:50
 f, g form_embedding_of C1, C2 & f preserves_inputs_of G1, G2 implies
  for s2 being State of C2, s1 being State of C1 st s1 = s2*f
  for v1 being Vertex of G1
   holds s1 is_stable_at v1 iff s2 is_stable_at f.v1;

theorem :: CIRCTRM1:51
   C1, C2 are_similar_wrt f, g implies
  for s being State of C2 holds s*f is State of C1;

theorem :: CIRCTRM1:52
 C1, C2 are_similar_wrt f, g implies
  for s1 being State of C1, s2 being State of C2
   holds s1 = s2*f iff s2 = s1*f";

theorem :: CIRCTRM1:53
 C1, C2 are_similar_wrt f, g implies
   f.:InputVertices G1 = InputVertices G2 &
   f.:InnerVertices G1 = InnerVertices G2;

theorem :: CIRCTRM1:54
 C1, C2 are_similar_wrt f, g implies f preserves_inputs_of G1, G2;

theorem :: CIRCTRM1:55
 C1, C2 are_similar_wrt f, g implies
  for s1 being State of C1, s2 being State of C2 st s1 = s2*f
   holds Following s1 = (Following s2)*f;

theorem :: CIRCTRM1:56
 C1, C2 are_similar_wrt f, g implies
  for s1 being State of C1, s2 being State of C2 st s1 = s2*f
  for n being Nat holds Following(s1,n) = Following(s2,n)*f;

theorem :: CIRCTRM1:57
   C1, C2 are_similar_wrt f, g implies
  for s1 being State of C1, s2 being State of C2 st s1 = s2*f
   holds s1 is stable iff s2 is stable;


theorem :: CIRCTRM1:58
   C1, C2 are_similar_wrt f, g implies
  for s1 being State of C1, s2 being State of C2 st s1 = s2*f
  for v1 being Vertex of G1
   holds s1 is_stable_at v1 iff s2 is_stable_at f.v1;


begin :: <section5>Term specification</section5>

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;
 pred C calculates X, A means
:: CIRCTRM1:def 15

  ex f, g st f, g form_embedding_of X-Circuit A, C &
             f preserves_inputs_of X-CircuitStr, G;

 pred X, A specifies C means
:: CIRCTRM1:def 16
     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;
 mode SortMap of X, A, C -> one-to-one Function means
:: CIRCTRM1:def 17

  it preserves_inputs_of X-CircuitStr, G &
  ex g st it, g form_embedding_of X-Circuit A, C;
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 such that
   C calculates X, A;
 let f be SortMap of X, A, C;
 mode OperMap of X, A, C, f -> one-to-one Function means
:: CIRCTRM1:def 18
    f, it form_embedding_of X-Circuit A, C;
end;

theorem :: CIRCTRM1:59
 for G being Circuit-like non void (non empty ManySortedSign)
 for C being non-empty Circuit of G
  st X, A specifies C
  holds C calculates X, A;

theorem :: CIRCTRM1:60
 for G being Circuit-like non void (non empty ManySortedSign)
 for C being non-empty Circuit of G
                       st C calculates X, A
 for f being SortMap of X, A, C
 for t being Term of S,V st t in Subtrees X
 for s being State of C
  holds Following(s, 1+height dom t) is_stable_at f.t &
 for s' being State of X-Circuit A st s' = s*f
 for h being CompatibleValuation of s'
  holds Following(s, 1+height dom t).(f.t) = t@(h, A);

theorem :: CIRCTRM1:61
 for G being Circuit-like non void (non empty ManySortedSign)
 for C being non-empty Circuit of G
                       st C calculates X, A
 for t being Term of S,V st t in Subtrees X
 ex v being Vertex of G st
   for s being State of C holds Following(s, 1+height dom t) is_stable_at v &
 ex f being SortMap of X, A, C st
   for s' being State of X-Circuit A st s' = s*f
   for h being CompatibleValuation of s'
    holds Following(s, 1+height dom t).v = t@(h, A);

theorem :: CIRCTRM1:62
   for G being Circuit-like non void (non empty ManySortedSign)
 for C being non-empty Circuit of G
                       st X, A specifies C
 for f being SortMap of X, A, C
 for s being State of C, t being Term of S,V st t in Subtrees X
  holds Following(s, 1+height dom t) is_stable_at f.t &
 for s' being State of X-Circuit A st s' = s*f
 for h being CompatibleValuation of s'
  holds Following(s, 1+height dom t).(f.t) = t@(h, A);

theorem :: CIRCTRM1:63
   for G being Circuit-like non void (non empty ManySortedSign)
 for C being non-empty Circuit of G
                       st X, A specifies C
 for t being Term of S,V st t in Subtrees X
 ex v being Vertex of G st
   for s being State of C holds Following(s, 1+height dom t) is_stable_at v &
 ex f being SortMap of X, A, C st
   for s' being State of X-Circuit A st s' = s*f
   for h being CompatibleValuation of s'
    holds Following(s, 1+height dom t).v = t@(h, A);