:: CIRCTRM1 semantic presentation begin theorem Th1: :: 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 for T being 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 ; ::_thesis: for A being non-empty MSAlgebra over S for V being Variables of A for t being Term of S,V for T being c-Term of A,V st T = t holds the_sort_of T = the_sort_of t let A be non-empty MSAlgebra over S; ::_thesis: for V being Variables of A for t being Term of S,V for T being c-Term of A,V st T = t holds the_sort_of T = the_sort_of t let V be Variables of A; ::_thesis: for t being Term of S,V for T being c-Term of A,V st T = t holds the_sort_of T = the_sort_of t defpred S1[ set ] means for t9 being Term of S,V for T being c-Term of A,V st t9 = \$1 & T = t9 holds the_sort_of T = the_sort_of t9; A1: for s being SortSymbol of S for v being Element of V . s holds S1[ root-tree [v,s]] proof let s be SortSymbol of S; ::_thesis: for v being Element of V . s holds S1[ root-tree [v,s]] let v be Element of V . s; ::_thesis: S1[ root-tree [v,s]] let t be Term of S,V; ::_thesis: for T being c-Term of A,V st t = root-tree [v,s] & T = t holds the_sort_of T = the_sort_of t let T be c-Term of A,V; ::_thesis: ( t = root-tree [v,s] & T = t implies the_sort_of T = the_sort_of t ) assume that A2: t = root-tree [v,s] and A3: T = t ; ::_thesis: the_sort_of T = the_sort_of t the_sort_of t = s by A2, MSATERM:14; hence the_sort_of T = the_sort_of t by A2, A3, MSATERM:16; ::_thesis: verum end; A4: for o being OperSymbol of S for p being ArgumentSeq of Sym (o,V) st ( for t9 being Term of S,V st t9 in rng p holds S1[t9] ) holds S1[[o, the carrier of S] -tree p] proof let o be OperSymbol of S; ::_thesis: for p being ArgumentSeq of Sym (o,V) st ( for t9 being Term of S,V st t9 in rng p holds S1[t9] ) holds S1[[o, the carrier of S] -tree p] let p be ArgumentSeq of Sym (o,V); ::_thesis: ( ( for t9 being Term of S,V st t9 in rng p holds S1[t9] ) implies S1[[o, the carrier of S] -tree p] ) assume for t9 being Term of S,V st t9 in rng p holds for t being Term of S,V for T being c-Term of A,V st t = t9 & T = t holds the_sort_of T = the_sort_of t ; ::_thesis: S1[[o, the carrier of S] -tree p] let t be Term of S,V; ::_thesis: for T being c-Term of A,V st t = [o, the carrier of S] -tree p & T = t holds the_sort_of T = the_sort_of t let T be c-Term of A,V; ::_thesis: ( t = [o, the carrier of S] -tree p & T = t implies the_sort_of T = the_sort_of t ) assume t = [o, the carrier of S] -tree p ; ::_thesis: ( not T = t or the_sort_of T = the_sort_of t ) 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 ( not T = t or the_sort_of T = the_sort_of t ) by A5, MSATERM:17; ::_thesis: verum end; for t being Term of S,V holds S1[t] from MSATERM:sch_1(A1, A4); hence for t being Term of S,V for T being c-Term of A,V st T = t holds the_sort_of T = the_sort_of t ; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let V be V2() ManySortedSet of the carrier of S; let X be non empty Subset of (S -Terms V); funcX -CircuitStr -> non empty strict ManySortedSign equals :: CIRCTRM1:def 1 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 coherence 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)) #) is non empty strict ManySortedSign ; ; end; :: deftheorem defines -CircuitStr CIRCTRM1:def_1_:_ for S being non empty non void ManySortedSign for V being V2() ManySortedSet of the carrier of S for X being non empty Subset of (S -Terms V) holds 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)) #); registration let S be non empty non void ManySortedSign ; let V be V2() ManySortedSet of the carrier of S; let X be non empty Subset of (S -Terms V); clusterX -CircuitStr -> non empty strict unsplit ; coherence X -CircuitStr is unsplit proof thus the ResultSort of (X -CircuitStr) = id the carrier' of (X -CircuitStr) ; :: according to CIRCCOMB:def_7 ::_thesis: verum end; end; theorem :: CIRCTRM1:2 for S being non empty non void ManySortedSign for V being V2() ManySortedSet of the carrier of S for X being non empty Subset of (S -Terms V) holds ( X -CircuitStr is void iff for t being Element of X holds ( t is root & not t . {} in [: the carrier' of S,{ the carrier of S}:] ) ) by TREES_9:25; theorem Th3: :: CIRCTRM1:3 for S being non empty non void ManySortedSign for V being V2() ManySortedSet of the carrier of S for X being non empty Subset of (S -Terms V) holds ( X is SetWithCompoundTerm of S,V iff not X -CircuitStr is void ) proof let S be non empty non void ManySortedSign ; ::_thesis: for V being V2() ManySortedSet of the carrier of S for X being non empty Subset of (S -Terms V) holds ( X is SetWithCompoundTerm of S,V iff not X -CircuitStr is void ) let V be V2() ManySortedSet of the carrier of S; ::_thesis: for X being non empty Subset of (S -Terms V) holds ( X is SetWithCompoundTerm of S,V iff not X -CircuitStr is void ) let X be non empty Subset of (S -Terms V); ::_thesis: ( X is SetWithCompoundTerm of S,V iff not X -CircuitStr is void ) hereby ::_thesis: ( not X -CircuitStr is void implies X is SetWithCompoundTerm of S,V ) assume X is SetWithCompoundTerm of S,V ; ::_thesis: not X -CircuitStr is void then consider t being 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 not X -CircuitStr is void by A1, TREES_9:25; ::_thesis: verum end; assume not X -CircuitStr is void ; ::_thesis: X is SetWithCompoundTerm of S,V then consider t being Element of X 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 X is SetWithCompoundTerm of S,V by MSATERM:def_7; ::_thesis: verum end; registration let S be non empty non void ManySortedSign ; let V be V2() ManySortedSet of the carrier of S; let X be SetWithCompoundTerm of S,V; clusterX -CircuitStr -> non empty non void strict ; coherence not X -CircuitStr is void by Th3; end; theorem Th4: :: CIRCTRM1:4 for S being non empty non void ManySortedSign for V being V2() ManySortedSet of the carrier of S for X being non empty Subset of (S -Terms V) holds ( ( for v being Vertex of (X -CircuitStr) holds v is Term of S,V ) & ( for s being set st s in the carrier' of (X -CircuitStr) holds s is CompoundTerm of S,V ) ) proof let S be non empty non void ManySortedSign ; ::_thesis: for V being V2() ManySortedSet of the carrier of S for X being non empty Subset of (S -Terms V) holds ( ( for v being Vertex of (X -CircuitStr) holds v is Term of S,V ) & ( for s being set st s in the carrier' of (X -CircuitStr) holds s is CompoundTerm of S,V ) ) let V be V2() ManySortedSet of the carrier of S; ::_thesis: for X being non empty Subset of (S -Terms V) holds ( ( for v being Vertex of (X -CircuitStr) holds v is Term of S,V ) & ( for s being set st s in the carrier' of (X -CircuitStr) holds s is CompoundTerm of S,V ) ) let X be non empty Subset of (S -Terms V); ::_thesis: ( ( for v being Vertex of (X -CircuitStr) holds v is Term of S,V ) & ( for s being set st s in the carrier' of (X -CircuitStr) holds s is CompoundTerm of S,V ) ) set C = [: the carrier' of S,{ the carrier of S}:]; hereby ::_thesis: for s being set st s in the carrier' of (X -CircuitStr) holds s is CompoundTerm of S,V let v be Vertex of (X -CircuitStr); ::_thesis: v is Term of S,V consider t being Element of X, p being Node of t such that A1: v = t | p by TREES_9:19; thus v is Term of S,V by A1; ::_thesis: verum end; let s be set ; ::_thesis: ( s in the carrier' of (X -CircuitStr) implies s is CompoundTerm of S,V ) assume s in the carrier' of (X -CircuitStr) ; ::_thesis: s is CompoundTerm of S,V then consider t being Element of X, p being Node of t such that A2: s = t | p and A3: ( not p in Leaves (dom t) or t . p in [: the carrier' of S,{ the carrier of S}:] ) by TREES_9:24; reconsider s = 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) | p 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 s is CompoundTerm of S,V by A3, A5, MSATERM:28, MSATERM:def_6; ::_thesis: verum end; theorem Th5: :: CIRCTRM1:5 for S being non empty non void ManySortedSign for V being V2() ManySortedSet of the carrier of S for X being non empty Subset of (S -Terms V) for t being Vertex of (X -CircuitStr) holds ( t in the carrier' of (X -CircuitStr) iff t is CompoundTerm of S,V ) proof let S be non empty non void ManySortedSign ; ::_thesis: for V being V2() ManySortedSet of the carrier of S for X being non empty Subset of (S -Terms V) for t being Vertex of (X -CircuitStr) holds ( t in the carrier' of (X -CircuitStr) iff t is CompoundTerm of S,V ) let V be V2() ManySortedSet of the carrier of S; ::_thesis: for X being non empty Subset of (S -Terms V) for t being Vertex of (X -CircuitStr) holds ( t in the carrier' of (X -CircuitStr) iff t is CompoundTerm of S,V ) let X be non empty Subset of (S -Terms V); ::_thesis: for t being Vertex of (X -CircuitStr) holds ( t in the carrier' of (X -CircuitStr) iff t is CompoundTerm of S,V ) let t be Vertex of (X -CircuitStr); ::_thesis: ( t in the carrier' of (X -CircuitStr) iff t is CompoundTerm of S,V ) thus ( t in the carrier' of (X -CircuitStr) implies t is CompoundTerm of S,V ) by Th4; ::_thesis: ( t is CompoundTerm of S,V implies t in the carrier' of (X -CircuitStr) ) set C = [: the carrier' of S,{ the carrier of S}:]; consider tt being Element of X, p being Node of tt such that A1: t = tt | p by TREES_9:19; assume t is CompoundTerm of S,V ; ::_thesis: t in the carrier' of (X -CircuitStr) then reconsider t9 = t as CompoundTerm of S,V ; A2: t9 . {} in [: the carrier' of S,{ the carrier of S}:] by MSATERM:def_6; A3: p ^ (<*> NAT) = p by FINSEQ_1:34; {} in (dom tt) | p by TREES_1:22; then tt . p in [: the carrier' of S,{ the carrier of S}:] by A1, A2, A3, TREES_2:def_10; hence t in the carrier' of (X -CircuitStr) by A1, TREES_9:24; ::_thesis: verum end; registration let S be non empty non void ManySortedSign ; let V be V2() ManySortedSet of the carrier of S; let X be SetWithCompoundTerm of S,V; let g be Gate of (X -CircuitStr); cluster the_arity_of g -> DTree-yielding ; coherence the_arity_of g is DTree-yielding ; end; registration let S be non empty non void ManySortedSign ; let V be V2() ManySortedSet of the carrier of S; let X be non empty Subset of (S -Terms V); cluster -> Relation-like Function-like finite for Element of the carrier of (X -CircuitStr); coherence for b1 being Vertex of (X -CircuitStr) holds ( b1 is finite & b1 is Function-like & b1 is Relation-like ) by Th4; end; registration let S be non empty non void ManySortedSign ; let V be V2() ManySortedSet of the carrier of S; let X be non empty Subset of (S -Terms V); cluster -> DecoratedTree-like for Element of the carrier of (X -CircuitStr); coherence for b1 being Vertex of (X -CircuitStr) holds b1 is DecoratedTree-like ; end; registration let S be non empty non void ManySortedSign ; let V be V2() ManySortedSet of the carrier of S; let X be SetWithCompoundTerm of S,V; cluster -> Relation-like Function-like finite for Element of the carrier' of (X -CircuitStr); coherence for b1 being Gate of (X -CircuitStr) holds ( b1 is finite & b1 is Function-like & b1 is Relation-like ) by Th4; end; registration let S be non empty non void ManySortedSign ; let V be V2() ManySortedSet of the carrier of S; let X be SetWithCompoundTerm of S,V; cluster -> DecoratedTree-like for Element of the carrier' of (X -CircuitStr); coherence for b1 being Gate of (X -CircuitStr) holds b1 is DecoratedTree-like ; end; theorem Th6: :: CIRCTRM1:6 for S being non empty non void ManySortedSign for V being V2() ManySortedSet of the carrier of S 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) ) proof let S be non empty non void ManySortedSign ; ::_thesis: for V being V2() ManySortedSet of the carrier of S 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) ) let V be V2() ManySortedSet of the carrier of S; ::_thesis: 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) ) let t1, t2 be non empty Subset of (S -Terms V); ::_thesis: ( the Arity of (t1 -CircuitStr) tolerates the Arity of (t2 -CircuitStr) & the ResultSort of (t1 -CircuitStr) tolerates the ResultSort of (t2 -CircuitStr) ) set C = [: the carrier' of S,{ the carrier of S}:]; A1: dom ([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees t1) = [: the carrier' of S,{ the carrier of S}:] -Subtrees t1 by FUNCT_2:def_1; A2: dom (id ([: the carrier' of S,{ the carrier of S}:] -Subtrees t1)) = [: the carrier' of S,{ the carrier of S}:] -Subtrees t1 ; A3: dom ([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees t2) = [: the carrier' of S,{ the carrier of S}:] -Subtrees t2 by FUNCT_2:def_1; A4: dom (id ([: the carrier' of S,{ the carrier of S}:] -Subtrees t2)) = [: the carrier' of S,{ the carrier of S}:] -Subtrees t2 ; hereby :: according to PARTFUN1:def_4 ::_thesis: the ResultSort of (t1 -CircuitStr) tolerates the ResultSort of (t2 -CircuitStr) let x be set ; ::_thesis: ( x in (dom the Arity of (t1 -CircuitStr)) /\ (dom the Arity of (t2 -CircuitStr)) implies the Arity of (t1 -CircuitStr) . x = the Arity of (t2 -CircuitStr) . x ) assume A5: x in (dom the Arity of (t1 -CircuitStr)) /\ (dom the Arity of (t2 -CircuitStr)) ; ::_thesis: the Arity of (t1 -CircuitStr) . x = the Arity of (t2 -CircuitStr) . x then A6: x in dom the Arity of (t1 -CircuitStr) by XBOOLE_0:def_4; A7: x in dom the Arity of (t2 -CircuitStr) by A5, XBOOLE_0:def_4; reconsider u = x as Element of Subtrees t1 by A1, A6; ([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees t1) . x in (Subtrees t1) * by A1, A6, 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 A3, A7, FUNCT_2:5; then reconsider y2 = the Arity of (t2 -CircuitStr) . x as FinSequence of Subtrees t2 by FINSEQ_1:def_11; A8: ( ( for t being Element of t1 holds t is finite ) & ( for t being Element of t2 holds t is finite ) ) ; then A9: u = (u . {}) -tree y1 by A1, A6, TREES_9:def_13; u = (u . {}) -tree y2 by A3, A7, A8, TREES_9:def_13; hence the Arity of (t1 -CircuitStr) . x = the Arity of (t2 -CircuitStr) . x by A9, TREES_4:15; ::_thesis: verum end; let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( not x in (proj1 the ResultSort of (t1 -CircuitStr)) /\ (proj1 the ResultSort of (t2 -CircuitStr)) or the ResultSort of (t1 -CircuitStr) . x = the ResultSort of (t2 -CircuitStr) . x ) assume A10: x in (dom the ResultSort of (t1 -CircuitStr)) /\ (dom the ResultSort of (t2 -CircuitStr)) ; ::_thesis: the ResultSort of (t1 -CircuitStr) . x = the ResultSort of (t2 -CircuitStr) . x then A11: x in dom the ResultSort of (t1 -CircuitStr) by XBOOLE_0:def_4; A12: x in dom the ResultSort of (t2 -CircuitStr) by A10, XBOOLE_0:def_4; thus the ResultSort of (t1 -CircuitStr) . x = x by A2, A11, FUNCT_1:18 .= the ResultSort of (t2 -CircuitStr) . x by A4, A12, FUNCT_1:18 ; ::_thesis: verum end; registration let X, Y be constituted-DTrees set ; clusterX \/ Y -> constituted-DTrees ; coherence X \/ Y is constituted-DTrees by TREES_3:9; end; theorem Th7: :: CIRCTRM1:7 for X1, X2 being non empty constituted-DTrees set holds Subtrees (X1 \/ X2) = (Subtrees X1) \/ (Subtrees X2) proof let X1, X2 be non empty constituted-DTrees set ; ::_thesis: Subtrees (X1 \/ X2) = (Subtrees X1) \/ (Subtrees X2) hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: (Subtrees X1) \/ (Subtrees X2) c= Subtrees (X1 \/ X2) let x be set ; ::_thesis: ( x in Subtrees (X1 \/ X2) implies x in (Subtrees X1) \/ (Subtrees X2) ) assume x in Subtrees (X1 \/ X2) ; ::_thesis: x in (Subtrees X1) \/ (Subtrees X2) then consider t being Element of X1 \/ X2, n being 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; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Subtrees X1) \/ (Subtrees X2) or x in Subtrees (X1 \/ X2) ) assume A2: x in (Subtrees X1) \/ (Subtrees X2) ; ::_thesis: x in Subtrees (X1 \/ X2) percases ( x in Subtrees X1 or x in Subtrees X2 ) by A2, XBOOLE_0:def_3; suppose x in Subtrees X1 ; ::_thesis: x in Subtrees (X1 \/ X2) then consider t being Element of X1, n being 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 x in Subtrees (X1 \/ X2) by A3, TREES_9:19; ::_thesis: verum end; suppose x in Subtrees X2 ; ::_thesis: x in Subtrees (X1 \/ X2) then consider t being Element of X2, n being 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 x in Subtrees (X1 \/ X2) by A4, TREES_9:19; ::_thesis: verum end; end; end; theorem Th8: :: CIRCTRM1:8 for X1, X2 being non empty constituted-DTrees set for C being set holds C -Subtrees (X1 \/ X2) = (C -Subtrees X1) \/ (C -Subtrees X2) proof let X1, X2 be non empty constituted-DTrees set ; ::_thesis: for C being set holds C -Subtrees (X1 \/ X2) = (C -Subtrees X1) \/ (C -Subtrees X2) let C be set ; ::_thesis: C -Subtrees (X1 \/ X2) = (C -Subtrees X1) \/ (C -Subtrees X2) hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: (C -Subtrees X1) \/ (C -Subtrees X2) c= C -Subtrees (X1 \/ X2) let x be set ; ::_thesis: ( x in C -Subtrees (X1 \/ X2) implies x in (C -Subtrees X1) \/ (C -Subtrees X2) ) assume x in C -Subtrees (X1 \/ X2) ; ::_thesis: x in (C -Subtrees X1) \/ (C -Subtrees X2) then consider t being Element of X1 \/ X2, n being 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; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (C -Subtrees X1) \/ (C -Subtrees X2) or x in C -Subtrees (X1 \/ X2) ) assume A3: x in (C -Subtrees X1) \/ (C -Subtrees X2) ; ::_thesis: x in C -Subtrees (X1 \/ X2) percases ( x in C -Subtrees X1 or x in C -Subtrees X2 ) by A3, XBOOLE_0:def_3; suppose x in C -Subtrees X1 ; ::_thesis: x in C -Subtrees (X1 \/ X2) then consider t being Element of X1, n being 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 x in C -Subtrees (X1 \/ X2) by A4, A5, TREES_9:24; ::_thesis: verum end; suppose x in C -Subtrees X2 ; ::_thesis: x in C -Subtrees (X1 \/ X2) then consider t being Element of X2, n being 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 x in C -Subtrees (X1 \/ X2) by A6, A7, TREES_9:24; ::_thesis: verum end; end; end; theorem Th9: :: CIRCTRM1:9 for X1, X2 being non empty constituted-DTrees set st ( for t being Element of X1 holds t is finite ) & ( for t being Element of X2 holds t is finite ) holds for C being set holds C -ImmediateSubtrees (X1 \/ X2) = (C -ImmediateSubtrees X1) +* (C -ImmediateSubtrees X2) proof let X1, X2 be non empty constituted-DTrees set ; ::_thesis: ( ( for t being Element of X1 holds t is finite ) & ( for t being Element of X2 holds t is finite ) implies for C being set holds C -ImmediateSubtrees (X1 \/ X2) = (C -ImmediateSubtrees X1) +* (C -ImmediateSubtrees X2) ) assume that A1: for t being Element of X1 holds t is finite and A2: for t being Element of X2 holds t is finite ; ::_thesis: for C being set holds C -ImmediateSubtrees (X1 \/ X2) = (C -ImmediateSubtrees X1) +* (C -ImmediateSubtrees X2) A3: now__::_thesis:_for_t_being_Element_of_X1_\/_X2_holds_t_is_finite let t be Element of X1 \/ X2; ::_thesis: t is finite ( t in X1 or t in X2 ) by XBOOLE_0:def_3; hence t is finite by A1, A2; ::_thesis: verum end; let C be set ; ::_thesis: C -ImmediateSubtrees (X1 \/ X2) = (C -ImmediateSubtrees X1) +* (C -ImmediateSubtrees X2) set X = X1 \/ X2; set f = C -ImmediateSubtrees (X1 \/ X2); set f1 = C -ImmediateSubtrees X1; set f2 = C -ImmediateSubtrees X2; A4: dom (C -ImmediateSubtrees (X1 \/ X2)) = C -Subtrees (X1 \/ X2) by FUNCT_2:def_1; A5: dom (C -ImmediateSubtrees X1) = C -Subtrees X1 by FUNCT_2:def_1; A6: dom (C -ImmediateSubtrees X2) = C -Subtrees X2 by FUNCT_2:def_1; A7: C -Subtrees (X1 \/ X2) = (C -Subtrees X1) \/ (C -Subtrees X2) by Th8; now__::_thesis:_for_x_being_set_st_x_in_(dom_(C_-ImmediateSubtrees_X1))_\/_(dom_(C_-ImmediateSubtrees_X2))_holds_ (_(_x_in_dom_(C_-ImmediateSubtrees_X2)_implies_(C_-ImmediateSubtrees_(X1_\/_X2))_._x_=_(C_-ImmediateSubtrees_X2)_._x_)_&_(_not_x_in_dom_(C_-ImmediateSubtrees_X2)_implies_(C_-ImmediateSubtrees_(X1_\/_X2))_._x_=_(C_-ImmediateSubtrees_X1)_._x_)_) let x be set ; ::_thesis: ( x in (dom (C -ImmediateSubtrees X1)) \/ (dom (C -ImmediateSubtrees X2)) implies ( ( x in dom (C -ImmediateSubtrees X2) implies (C -ImmediateSubtrees (X1 \/ X2)) . x = (C -ImmediateSubtrees X2) . x ) & ( not x in dom (C -ImmediateSubtrees X2) implies (C -ImmediateSubtrees (X1 \/ X2)) . x = (C -ImmediateSubtrees X1) . x ) ) ) assume A8: x in (dom (C -ImmediateSubtrees X1)) \/ (dom (C -ImmediateSubtrees X2)) ; ::_thesis: ( ( x in dom (C -ImmediateSubtrees X2) implies (C -ImmediateSubtrees (X1 \/ X2)) . x = (C -ImmediateSubtrees X2) . x ) & ( not x in dom (C -ImmediateSubtrees X2) implies (C -ImmediateSubtrees (X1 \/ X2)) . x = (C -ImmediateSubtrees X1) . x ) ) then reconsider t = x as Element of Subtrees (X1 \/ X2) by A5, A6, A7; (C -ImmediateSubtrees (X1 \/ X2)) . x in (Subtrees (X1 \/ X2)) * by A5, A6, A7, A8, FUNCT_2:5; then reconsider p = (C -ImmediateSubtrees (X1 \/ X2)) . x as FinSequence of Subtrees (X1 \/ X2) by FINSEQ_1:def_11; hereby ::_thesis: ( not x in dom (C -ImmediateSubtrees X2) implies (C -ImmediateSubtrees (X1 \/ X2)) . x = (C -ImmediateSubtrees X1) . x ) assume A9: x in dom (C -ImmediateSubtrees X2) ; ::_thesis: (C -ImmediateSubtrees (X1 \/ X2)) . x = (C -ImmediateSubtrees X2) . x then (C -ImmediateSubtrees X2) . x in (Subtrees X2) * by A6, FUNCT_2:5; then reconsider p2 = (C -ImmediateSubtrees X2) . 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 (C -ImmediateSubtrees (X1 \/ X2)) . x = (C -ImmediateSubtrees X2) . x by A10, TREES_4:15; ::_thesis: verum end; assume not x in dom (C -ImmediateSubtrees X2) ; ::_thesis: (C -ImmediateSubtrees (X1 \/ X2)) . x = (C -ImmediateSubtrees X1) . x then A11: x in dom (C -ImmediateSubtrees X1) by A8, XBOOLE_0:def_3; then (C -ImmediateSubtrees X1) . x in (Subtrees X1) * by A5, FUNCT_2:5; then reconsider p1 = (C -ImmediateSubtrees X1) . 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 (C -ImmediateSubtrees (X1 \/ X2)) . x = (C -ImmediateSubtrees X1) . x by A12, TREES_4:15; ::_thesis: verum end; hence C -ImmediateSubtrees (X1 \/ X2) = (C -ImmediateSubtrees X1) +* (C -ImmediateSubtrees X2) by A4, A5, A6, A7, FUNCT_4:def_1; ::_thesis: verum end; theorem Th10: :: CIRCTRM1:10 for S being non empty non void ManySortedSign for V being V2() ManySortedSet of the carrier of S for X1, X2 being non empty Subset of (S -Terms V) holds (X1 \/ X2) -CircuitStr = (X1 -CircuitStr) +* (X2 -CircuitStr) proof let S be non empty non void ManySortedSign ; ::_thesis: for V being V2() ManySortedSet of the carrier of S for X1, X2 being non empty Subset of (S -Terms V) holds (X1 \/ X2) -CircuitStr = (X1 -CircuitStr) +* (X2 -CircuitStr) let V be V2() ManySortedSet of the carrier of S; ::_thesis: for X1, X2 being non empty Subset of (S -Terms V) holds (X1 \/ X2) -CircuitStr = (X1 -CircuitStr) +* (X2 -CircuitStr) let X1, X2 be non empty Subset of (S -Terms V); ::_thesis: (X1 \/ X2) -CircuitStr = (X1 -CircuitStr) +* (X2 -CircuitStr) set X = X1 \/ X2; set C = [: the carrier' of S,{ the carrier of S}:]; A1: Subtrees (X1 \/ X2) = (Subtrees X1) \/ (Subtrees X2) by Th7; A2: [: the carrier' of S,{ the carrier of S}:] -Subtrees (X1 \/ X2) = ([: the carrier' of S,{ the carrier of S}:] -Subtrees X1) \/ ([: the carrier' of S,{ the carrier of S}:] -Subtrees X2) by Th8; ( ( for t being Element of X1 holds t is finite ) & ( for t being Element of X2 holds t is finite ) ) ; then A3: [: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees (X1 \/ X2) = ([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees X1) +* ([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees X2) by Th9; id ([: the carrier' of S,{ the carrier of S}:] -Subtrees (X1 \/ X2)) = (id ([: the carrier' of S,{ the carrier of S}:] -Subtrees X1)) +* (id ([: the carrier' of S,{ the carrier of S}:] -Subtrees X2)) by A2, FUNCT_4:22; hence (X1 \/ X2) -CircuitStr = (X1 -CircuitStr) +* (X2 -CircuitStr) by A1, A2, A3, CIRCCOMB:def_2; ::_thesis: verum end; theorem Th11: :: CIRCTRM1:11 for S being non empty non void ManySortedSign for V being V2() ManySortedSet of the carrier of S for X being non empty Subset of (S -Terms V) for x being set holds ( x in InputVertices (X -CircuitStr) iff ( x in Subtrees X & ex s being SortSymbol of S ex v being Element of V . s st x = root-tree [v,s] ) ) proof let S be non empty non void ManySortedSign ; ::_thesis: for V being V2() ManySortedSet of the carrier of S for X being non empty Subset of (S -Terms V) for x being set holds ( x in InputVertices (X -CircuitStr) iff ( x in Subtrees X & ex s being SortSymbol of S ex v being Element of V . s st x = root-tree [v,s] ) ) let V be V2() ManySortedSet of the carrier of S; ::_thesis: for X being non empty Subset of (S -Terms V) for x being set holds ( x in InputVertices (X -CircuitStr) iff ( x in Subtrees X & ex s being SortSymbol of S ex v being Element of V . s st x = root-tree [v,s] ) ) let X be non empty Subset of (S -Terms V); ::_thesis: for x being set holds ( x in InputVertices (X -CircuitStr) iff ( x in Subtrees X & ex s being SortSymbol of S ex v being Element of V . s st x = root-tree [v,s] ) ) set G = X -CircuitStr ; A1: rng the ResultSort of (X -CircuitStr) = the carrier' of (X -CircuitStr) by RELAT_1:45; let x be set ; ::_thesis: ( x in InputVertices (X -CircuitStr) iff ( x in Subtrees X & ex s being SortSymbol of S ex v being Element of V . s st x = root-tree [v,s] ) ) hereby ::_thesis: ( x in Subtrees X & ex s being SortSymbol of S ex v being Element of V . s st x = root-tree [v,s] implies x in InputVertices (X -CircuitStr) ) assume A2: x in InputVertices (X -CircuitStr) ; ::_thesis: ( x in Subtrees X & ex s being SortSymbol of S ex v being Element of V . s st x = root-tree [v,s] ) then A3: not x in the carrier' of (X -CircuitStr) by A1, XBOOLE_0:def_5; thus x in Subtrees X by A2; ::_thesis: ex s being SortSymbol of S ex v being Element of V . s st x = root-tree [v,s] reconsider t = x as Term of S,V by A2, Th4; ( ex s being SortSymbol of S ex v being 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 being SortSymbol of S ex v being Element of V . s st t . {} = [v,s] or t is CompoundTerm of S,V ) by MSATERM:def_6; then consider s being SortSymbol of S, v being Element of V . s such that A4: t . {} = [v,s] by A2, A3, Th5; take s = s; ::_thesis: ex v being Element of V . s st x = root-tree [v,s] reconsider v = v as Element of V . s ; take v = v; ::_thesis: x = root-tree [v,s] thus x = root-tree [v,s] by A4, MSATERM:5; ::_thesis: verum end; assume A5: x in Subtrees X ; ::_thesis: ( for s being SortSymbol of S for v being Element of V . s holds not x = root-tree [v,s] or x in InputVertices (X -CircuitStr) ) given s being SortSymbol of S, v being Element of V . s such that A6: x = root-tree [v,s] ; ::_thesis: x in InputVertices (X -CircuitStr) assume not x in InputVertices (X -CircuitStr) ; ::_thesis: contradiction then x in the carrier' of (X -CircuitStr) by A1, A5, XBOOLE_0:def_5; then reconsider t = x as CompoundTerm of S,V by Th4; t . {} = [v,s] by A6, 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 ; ::_thesis: verum end; theorem Th12: :: CIRCTRM1:12 for S being non empty non void ManySortedSign for V being V2() ManySortedSet of the carrier of S for X being SetWithCompoundTerm of S,V for g being Gate of (X -CircuitStr) holds g = (g . {}) -tree (the_arity_of g) proof let S be non empty non void ManySortedSign ; ::_thesis: for V being V2() ManySortedSet of the carrier of S for X being SetWithCompoundTerm of S,V for g being Gate of (X -CircuitStr) holds g = (g . {}) -tree (the_arity_of g) let V be V2() ManySortedSet of the carrier of S; ::_thesis: for X being SetWithCompoundTerm of S,V for g being Gate of (X -CircuitStr) holds g = (g . {}) -tree (the_arity_of g) let X be SetWithCompoundTerm of S,V; ::_thesis: for g being Gate of (X -CircuitStr) holds g = (g . {}) -tree (the_arity_of g) let g be Gate of (X -CircuitStr); ::_thesis: g = (g . {}) -tree (the_arity_of g) for t being Element of X holds t is finite ; hence g = (g . {}) -tree (the_arity_of g) by TREES_9:def_13; ::_thesis: verum end; begin definition let S be non empty non void ManySortedSign ; let V be V2() 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) -> set means :Def2: :: CIRCTRM1:def 2 for u being Term of S,V st u = v holds it = the Sorts of A . (the_sort_of u); uniqueness for b1, b2 being set st ( for u being Term of S,V st u = v holds b1 = the Sorts of A . (the_sort_of u) ) & ( for u being Term of S,V st u = v holds b2 = the Sorts of A . (the_sort_of u) ) holds b1 = b2 proof let S1, S2 be set ; ::_thesis: ( ( for u being Term of S,V st u = v holds S1 = the Sorts of A . (the_sort_of u) ) & ( for u being Term of S,V st u = v holds S2 = the Sorts of A . (the_sort_of u) ) implies S1 = S2 ) reconsider u = v as Term of S,V by Th4; assume A1: ( ( for u being Term of S,V st u = v holds S1 = the Sorts of A . (the_sort_of u) ) & ( for u being Term of S,V st u = v holds S2 = the Sorts of A . (the_sort_of u) ) & not S1 = S2 ) ; ::_thesis: contradiction then S1 = the Sorts of A . (the_sort_of u) ; hence contradiction by A1; ::_thesis: verum end; existence ex b1 being set st for u being Term of S,V st u = v holds b1 = the Sorts of A . (the_sort_of u) proof reconsider u = v as Term of S,V by Th4; take the Sorts of A . (the_sort_of u) ; ::_thesis: for u being Term of S,V st u = v holds the Sorts of A . (the_sort_of u) = the Sorts of A . (the_sort_of u) thus for u being Term of S,V st u = v holds the Sorts of A . (the_sort_of u) = the Sorts of A . (the_sort_of u) ; ::_thesis: verum end; end; :: deftheorem Def2 defines the_sort_of CIRCTRM1:def_2_:_ for S being non empty non void ManySortedSign for V being V2() ManySortedSet of the carrier of S for X being non empty Subset of (S -Terms V) for v being Vertex of (X -CircuitStr) for A being MSAlgebra over S for b6 being set holds ( b6 = the_sort_of (v,A) iff for u being Term of S,V st u = v holds b6 = the Sorts of A . (the_sort_of u) ); registration let S be non empty non void ManySortedSign ; let V be V2() 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 not the_sort_of (v,A) is empty 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 not the_sort_of (v,A) is empty ; ::_thesis: verum end; end; definition let S be non empty non void ManySortedSign ; let V be V2() 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; func the_action_of (o,A) -> Function means :Def3: :: CIRCTRM1:def 3 for X9 being SetWithCompoundTerm of S,V st X9 = X holds for o9 being Gate of (X9 -CircuitStr) st o9 = o holds it = the Charact of A . ((o9 . {}) `1); uniqueness for b1, b2 being Function st ( for X9 being SetWithCompoundTerm of S,V st X9 = X holds for o9 being Gate of (X9 -CircuitStr) st o9 = o holds b1 = the Charact of A . ((o9 . {}) `1) ) & ( for X9 being SetWithCompoundTerm of S,V st X9 = X holds for o9 being Gate of (X9 -CircuitStr) st o9 = o holds b2 = the Charact of A . ((o9 . {}) `1) ) holds b1 = b2 proof let f1, f2 be Function; ::_thesis: ( ( for X9 being SetWithCompoundTerm of S,V st X9 = X holds for o9 being Gate of (X9 -CircuitStr) st o9 = o holds f1 = the Charact of A . ((o9 . {}) `1) ) & ( for X9 being SetWithCompoundTerm of S,V st X9 = X holds for o9 being Gate of (X9 -CircuitStr) st o9 = o holds f2 = the Charact of A . ((o9 . {}) `1) ) implies f1 = f2 ) reconsider X9 = X as SetWithCompoundTerm of S,V by A1; reconsider o9 = o as Gate of (X9 -CircuitStr) ; assume A2: ( ( for X9 being SetWithCompoundTerm of S,V st X9 = X holds for o9 being Gate of (X9 -CircuitStr) st o9 = o holds f1 = the Charact of A . ((o9 . {}) `1) ) & ( for X9 being SetWithCompoundTerm of S,V st X9 = X holds for o9 being Gate of (X9 -CircuitStr) st o9 = o holds f2 = the Charact of A . ((o9 . {}) `1) ) & not f1 = f2 ) ; ::_thesis: contradiction then f1 = the Charact of A . ((o9 . {}) `1) ; hence contradiction by A2; ::_thesis: verum end; existence ex b1 being Function st for X9 being SetWithCompoundTerm of S,V st X9 = X holds for o9 being Gate of (X9 -CircuitStr) st o9 = o holds b1 = the Charact of A . ((o9 . {}) `1) 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) ; ::_thesis: for X9 being SetWithCompoundTerm of S,V st X9 = X holds for o9 being Gate of (X9 -CircuitStr) st o9 = o holds the Charact of A . ((o9 . {}) `1) = the Charact of A . ((o9 . {}) `1) thus for X9 being SetWithCompoundTerm of S,V st X9 = X holds for o9 being Gate of (X9 -CircuitStr) st o9 = o holds the Charact of A . ((o9 . {}) `1) = the Charact of A . ((o9 . {}) `1) ; ::_thesis: verum end; end; :: deftheorem Def3 defines the_action_of CIRCTRM1:def_3_:_ for S being non empty non void ManySortedSign for V being V2() ManySortedSet of the carrier of S for X being non empty Subset of (S -Terms V) st X is SetWithCompoundTerm of S,V holds for o being Gate of (X -CircuitStr) for A being MSAlgebra over S for b6 being Function holds ( b6 = the_action_of (o,A) iff for X9 being SetWithCompoundTerm of S,V st X9 = X holds for o9 being Gate of (X9 -CircuitStr) st o9 = o holds b6 = the Charact of A . ((o9 . {}) `1) ); scheme :: CIRCTRM1:sch 1 MSFuncEx{ F1() -> non empty set , F2() -> V2() ManySortedSet of F1(), F3() -> V2() ManySortedSet of F1(), P1[ set , set , set ] } : ex f being ManySortedFunction of F2(),F3() st for i being Element of F1() for a being Element of F2() . i holds P1[i,a,(f . i) . a] provided A1: for i being Element of F1() for a being Element of F2() . i ex b being Element of F3() . i st P1[i,a,b] proof defpred S1[ set , set ] means ex g being Function of (F2() . \$1),(F3() . \$1) st ( \$2 = g & ( for a being set st a in F2() . \$1 holds P1[\$1,a,g . a] ) ); A2: for i being set st i in F1() holds ex y being set st S1[i,y] proof let i be set ; ::_thesis: ( i in F1() implies ex y being set st S1[i,y] ) assume i in F1() ; ::_thesis: ex y being set st S1[i,y] then reconsider i = i as Element of F1() ; defpred S2[ set , set ] means P1[i,\$1,\$2]; A3: for a being set st a in F2() . i holds ex b being set st ( b in F3() . i & S2[a,b] ) proof let a be set ; ::_thesis: ( a in F2() . i implies ex b being set st ( b in F3() . i & S2[a,b] ) ) assume a in F2() . i ; ::_thesis: ex b being set st ( b in F3() . i & S2[a,b] ) then ex b being Element of F3() . i st P1[i,a,b] by A1; hence ex b being set st ( b in F3() . i & S2[a,b] ) ; ::_thesis: verum end; consider g being Function such that A4: ( dom g = F2() . i & rng g c= F3() . i ) and A5: for a being set st a in F2() . i holds S2[a,g . a] from FUNCT_1:sch_5(A3); take g ; ::_thesis: S1[i,g] g is Function of (F2() . i),(F3() . i) by A4, FUNCT_2:2; hence S1[i,g] by A5; ::_thesis: verum end; consider f being Function such that A6: dom f = F1() and A7: for i being set st i in F1() holds S1[i,f . i] from CLASSES1:sch_1(A2); reconsider f = f as ManySortedSet of F1() by A6, PARTFUN1:def_2, RELAT_1:def_18; f is ManySortedFunction of F2(),F3() proof let i be set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in F1() or f . i is Element of bool [:(F2() . i),(F3() . i):] ) assume i in F1() ; ::_thesis: f . i is Element of bool [:(F2() . i),(F3() . i):] then ex g being Function of (F2() . i),(F3() . i) st ( f . i = g & ( for a being set st a in F2() . i holds P1[i,a,g . a] ) ) by A7; hence f . i is Element of bool [:(F2() . i),(F3() . i):] ; ::_thesis: verum end; then reconsider f = f as ManySortedFunction of F2(),F3() ; take f ; ::_thesis: for i being Element of F1() for a being Element of F2() . i holds P1[i,a,(f . i) . a] let i be Element of F1(); ::_thesis: for a being Element of F2() . i holds P1[i,a,(f . i) . a] let a be Element of F2() . i; ::_thesis: P1[i,a,(f . i) . a] ex g being Function of (F2() . i),(F3() . i) st ( f . i = g & ( for a being set st a in F2() . i holds P1[i,a,g . a] ) ) by A7; hence P1[i,a,(f . i) . a] ; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let V be V2() ManySortedSet of the carrier of S; let X be non empty Subset of (S -Terms V); let A be MSAlgebra over S; funcX -CircuitSorts A -> ManySortedSet of the carrier of (X -CircuitStr) means :Def4: :: CIRCTRM1:def 4 for v being Vertex of (X -CircuitStr) holds it . v = the_sort_of (v,A); uniqueness for b1, b2 being ManySortedSet of the carrier of (X -CircuitStr) st ( for v being Vertex of (X -CircuitStr) holds b1 . v = the_sort_of (v,A) ) & ( for v being Vertex of (X -CircuitStr) holds b2 . v = the_sort_of (v,A) ) holds b1 = b2 proof let S1, S2 be ManySortedSet of the carrier of (X -CircuitStr); ::_thesis: ( ( for v being Vertex of (X -CircuitStr) holds S1 . v = the_sort_of (v,A) ) & ( for v being Vertex of (X -CircuitStr) holds S2 . v = the_sort_of (v,A) ) implies S1 = S2 ) assume that A1: for v being Vertex of (X -CircuitStr) holds S1 . v = the_sort_of (v,A) and A2: for v being Vertex of (X -CircuitStr) holds S2 . v = the_sort_of (v,A) ; ::_thesis: S1 = S2 now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(X_-CircuitStr)_holds_ S1_._x_=_S2_._x let x be set ; ::_thesis: ( x in the carrier of (X -CircuitStr) implies S1 . x = S2 . x ) assume x in the carrier of (X -CircuitStr) ; ::_thesis: S1 . x = S2 . x then reconsider v = x as Vertex of (X -CircuitStr) ; thus S1 . x = the_sort_of (v,A) by A1 .= S2 . x by A2 ; ::_thesis: verum end; hence S1 = S2 by PBOOLE:3; ::_thesis: verum end; existence ex b1 being ManySortedSet of the carrier of (X -CircuitStr) st for v being Vertex of (X -CircuitStr) holds b1 . v = the_sort_of (v,A) proof deffunc H1( Vertex of (X -CircuitStr)) -> set = the_sort_of (\$1,A); thus ex f being ManySortedSet of the carrier of (X -CircuitStr) st for d being Element of (X -CircuitStr) holds f . d = H1(d) from PBOOLE:sch_5(); ::_thesis: verum end; end; :: deftheorem Def4 defines -CircuitSorts CIRCTRM1:def_4_:_ for S being non empty non void ManySortedSign for V being V2() ManySortedSet of the carrier of S for X being non empty Subset of (S -Terms V) for A being MSAlgebra over S for b5 being ManySortedSet of the carrier of (X -CircuitStr) holds ( b5 = X -CircuitSorts A iff for v being Vertex of (X -CircuitStr) holds b5 . v = the_sort_of (v,A) ); registration let S be non empty non void ManySortedSign ; let V be V2() ManySortedSet of the carrier of S; let X be non empty Subset of (S -Terms V); let A be non-empty MSAlgebra over S; clusterX -CircuitSorts A -> V2() ; coherence X -CircuitSorts A is non-empty proof let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in the carrier of (X -CircuitStr) or not (X -CircuitSorts A) . i is empty ) assume i in the carrier of (X -CircuitStr) ; ::_thesis: not (X -CircuitSorts A) . i is empty then reconsider i = i as Vertex of (X -CircuitStr) ; (X -CircuitSorts A) . i = the_sort_of (i,A) by Def4; hence not (X -CircuitSorts A) . i is empty ; ::_thesis: verum end; end; theorem Th13: :: CIRCTRM1:13 for S being non empty non void ManySortedSign for V being V2() ManySortedSet of the carrier of S for A being non-empty MSAlgebra over S for X being SetWithCompoundTerm of S,V for 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) proof let S be non empty non void ManySortedSign ; ::_thesis: for V being V2() ManySortedSet of the carrier of S for A being non-empty MSAlgebra over S for X being SetWithCompoundTerm of S,V for 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) let V be V2() ManySortedSet of the carrier of S; ::_thesis: for A being non-empty MSAlgebra over S for X being SetWithCompoundTerm of S,V for 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) let A be non-empty MSAlgebra over S; ::_thesis: for X being SetWithCompoundTerm of S,V for 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) let t be SetWithCompoundTerm of S,V; ::_thesis: for g being Gate of (t -CircuitStr) for o being OperSymbol of S st g . {} = [o, the carrier of S] holds (t -CircuitSorts A) * (the_arity_of g) = the Sorts of A * (the_arity_of o) let g be Gate of (t -CircuitStr); ::_thesis: for o being OperSymbol of S st g . {} = [o, the carrier of S] holds (t -CircuitSorts A) * (the_arity_of g) = the Sorts of A * (the_arity_of o) 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; ::_thesis: ( g . {} = [o, the carrier of S] implies (t -CircuitSorts A) * (the_arity_of g) = the Sorts of A * (the_arity_of o) ) assume g . {} = [o, the carrier of S] ; ::_thesis: (t -CircuitSorts A) * (the_arity_of g) = the Sorts of A * (the_arity_of o) then consider a being 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 (t -CircuitSorts A) = the carrier of (t -CircuitStr) by PARTFUN1:def_2; A10: dom the Sorts of A = the carrier of S by PARTFUN1:def_2; A11: dom ((t -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__::_thesis:_for_i_being_set_st_i_in_Seg_(len_a)_holds_ ((t_-CircuitSorts_A)_*_(the_arity_of_g))_._i_=_(_the_Sorts_of_A_*_(the_arity_of_o))_._i let i be set ; ::_thesis: ( i in Seg (len a) implies ((t -CircuitSorts A) * (the_arity_of g)) . i = ( the Sorts of A * (the_arity_of o)) . i ) assume A13: i in Seg (len a) ; ::_thesis: ((t -CircuitSorts A) * (the_arity_of g)) . i = ( the Sorts of A * (the_arity_of o)) . i 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 ; ::_thesis: verum end; hence (t -CircuitSorts A) * (the_arity_of g) = the Sorts of A * (the_arity_of o) by A11, A12, FUNCT_1:2; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let V be V2() ManySortedSet of the carrier of S; let X be non empty Subset of (S -Terms V); let A be non-empty MSAlgebra over S; funcX -CircuitCharact A -> ManySortedFunction of ((X -CircuitSorts A) #) * the Arity of (X -CircuitStr),(X -CircuitSorts A) * the ResultSort of (X -CircuitStr) means :Def5: :: CIRCTRM1:def 5 for g being Gate of (X -CircuitStr) st g in the carrier' of (X -CircuitStr) holds it . g = the_action_of (g,A); uniqueness for b1, b2 being ManySortedFunction of ((X -CircuitSorts A) #) * the Arity of (X -CircuitStr),(X -CircuitSorts A) * the ResultSort of (X -CircuitStr) st ( for g being Gate of (X -CircuitStr) st g in the carrier' of (X -CircuitStr) holds b1 . g = the_action_of (g,A) ) & ( for g being Gate of (X -CircuitStr) st g in the carrier' of (X -CircuitStr) holds b2 . g = the_action_of (g,A) ) holds b1 = b2 proof let C1, C2 be ManySortedFunction of ((X -CircuitSorts A) #) * the Arity of (X -CircuitStr),(X -CircuitSorts A) * the ResultSort of (X -CircuitStr); ::_thesis: ( ( for g being Gate of (X -CircuitStr) st g in the carrier' of (X -CircuitStr) holds C1 . g = the_action_of (g,A) ) & ( for g being Gate of (X -CircuitStr) st g in the carrier' of (X -CircuitStr) holds C2 . g = the_action_of (g,A) ) implies C1 = C2 ) assume that A1: for o being Gate of (X -CircuitStr) st o in the carrier' of (X -CircuitStr) holds C1 . o = the_action_of (o,A) and A2: for o being Gate of (X -CircuitStr) st o in the carrier' of (X -CircuitStr) holds C2 . o = the_action_of (o,A) ; ::_thesis: C1 = C2 now__::_thesis:_for_x_being_set_st_x_in_the_carrier'_of_(X_-CircuitStr)_holds_ C1_._x_=_C2_._x let x be set ; ::_thesis: ( x in the carrier' of (X -CircuitStr) implies C1 . x = C2 . x ) assume A3: x in the carrier' of (X -CircuitStr) ; ::_thesis: C1 . x = C2 . x 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; ::_thesis: verum end; hence C1 = C2 by PBOOLE:3; ::_thesis: verum end; existence ex b1 being ManySortedFunction of ((X -CircuitSorts A) #) * the Arity of (X -CircuitStr),(X -CircuitSorts A) * the ResultSort of (X -CircuitStr) st for g being Gate of (X -CircuitStr) st g in the carrier' of (X -CircuitStr) holds b1 . g = the_action_of (g,A) proof defpred S1[ set , set ] means ex g being Gate of (X -CircuitStr) st ( g = \$1 & \$2 = the_action_of (g,A) ); A4: now__::_thesis:_for_x_being_set_st_x_in_the_carrier'_of_(X_-CircuitStr)_holds_ ex_y_being_set_st_S1[x,y] let x be set ; ::_thesis: ( x in the carrier' of (X -CircuitStr) implies ex y being set st S1[x,y] ) assume x in the carrier' of (X -CircuitStr) ; ::_thesis: ex y being set st S1[x,y] then reconsider g = x as Gate of (X -CircuitStr) ; reconsider y = the_action_of (g,A) as set ; take y = y; ::_thesis: S1[x,y] thus S1[x,y] ; ::_thesis: verum end; consider CHARACT being ManySortedSet of the carrier' of (X -CircuitStr) such that A5: for x being set st x in the carrier' of (X -CircuitStr) holds S1[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 set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not x in proj1 CHARACT or CHARACT . x is set ) assume x in dom CHARACT ; ::_thesis: CHARACT . x is set then ex g being Gate of (X -CircuitStr) st ( g = x & CHARACT . x = the_action_of (g,A) ) by A5, A6; hence CHARACT . x is set ; ::_thesis: verum end; then reconsider CHARACT = 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 set ; :: according to PBOOLE:def_15 ::_thesis: ( not i in the carrier' of (X -CircuitStr) or CHARACT . i is Element of bool [:((((X -CircuitSorts A) #) * the Arity of (X -CircuitStr)) . i),(((X -CircuitSorts A) * the ResultSort of (X -CircuitStr)) . i):] ) assume A7: i in the carrier' of (X -CircuitStr) ; ::_thesis: CHARACT . i is Element of bool [:((((X -CircuitSorts A) #) * the Arity of (X -CircuitStr)) . i),(((X -CircuitSorts A) * the ResultSort of (X -CircuitStr)) . i):] 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; A8: the_result_sort_of g = g by FUNCT_1:18; 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 being set such that A9: o in the carrier' of S and A10: y in { the carrier of S} and A11: I . {} = [o,y] by ZFMISC_1:84; reconsider o = o as OperSymbol of S by A9; A12: o = (I . {}) `1 by A11, MCART_1:7; A13: y = the carrier of S by A10, TARSKI:def_1; ex g being Gate of (X -CircuitStr) st ( g = i & CHARACT . i = the_action_of (g,A) ) by A5, A7; then A14: CHARACT . i = the_action_of (g,A) .= the Charact of A . o by A12, Def3 ; A15: ( 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 A11, A13, MSATERM:17 ; A16: ((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 A8, Def4 .= the Sorts of A . (the_sort_of I) by Def2 ; A17: (((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 A11, A13, 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 CHARACT . i is Element of bool [:((((X -CircuitSorts A) #) * the Arity of (X -CircuitStr)) . i),(((X -CircuitSorts A) * the ResultSort of (X -CircuitStr)) . i):] by A14, A15, A16, A17, PBOOLE:def_15; ::_thesis: verum end; then reconsider CHARACT = CHARACT as ManySortedFunction of ((X -CircuitSorts A) #) * the Arity of (X -CircuitStr),(X -CircuitSorts A) * the ResultSort of (X -CircuitStr) ; take CHARACT ; ::_thesis: for g being Gate of (X -CircuitStr) st g in the carrier' of (X -CircuitStr) holds CHARACT . g = the_action_of (g,A) let g be Gate of (X -CircuitStr); ::_thesis: ( g in the carrier' of (X -CircuitStr) implies CHARACT . g = the_action_of (g,A) ) assume g in the carrier' of (X -CircuitStr) ; ::_thesis: CHARACT . g = the_action_of (g,A) then ex h being Gate of (X -CircuitStr) st ( h = g & CHARACT . g = the_action_of (h,A) ) by A5; hence CHARACT . g = the_action_of (g,A) ; ::_thesis: verum end; end; :: deftheorem Def5 defines -CircuitCharact CIRCTRM1:def_5_:_ for S being non empty non void ManySortedSign for V being V2() ManySortedSet of the carrier of S for X being non empty Subset of (S -Terms V) for A being non-empty MSAlgebra over S for b5 being ManySortedFunction of ((X -CircuitSorts A) #) * the Arity of (X -CircuitStr),(X -CircuitSorts A) * the ResultSort of (X -CircuitStr) holds ( b5 = X -CircuitCharact A iff for g being Gate of (X -CircuitStr) st g in the carrier' of (X -CircuitStr) holds b5 . g = the_action_of (g,A) ); definition let S be non empty non void ManySortedSign ; let V be V2() ManySortedSet of the carrier of S; let X be non empty Subset of (S -Terms V); let A be non-empty MSAlgebra over S; funcX -Circuit A -> strict non-empty MSAlgebra over X -CircuitStr equals :: CIRCTRM1:def 6 MSAlgebra(# (X -CircuitSorts A),(X -CircuitCharact A) #); correctness coherence MSAlgebra(# (X -CircuitSorts A),(X -CircuitCharact A) #) is strict non-empty MSAlgebra over X -CircuitStr ; by MSUALG_1:def_3; end; :: deftheorem defines -Circuit CIRCTRM1:def_6_:_ for S being non empty non void ManySortedSign for V being V2() ManySortedSet of the carrier of S for X being non empty Subset of (S -Terms V) for A being non-empty MSAlgebra over S holds X -Circuit A = MSAlgebra(# (X -CircuitSorts A),(X -CircuitCharact A) #); theorem :: CIRCTRM1:14 for S being non empty non void ManySortedSign for V being V2() ManySortedSet of the carrier of S for A being non-empty MSAlgebra over S for X being non empty Subset of (S -Terms V) for v being Vertex of (X -CircuitStr) holds the Sorts of (X -Circuit A) . v = the_sort_of (v,A) by Def4; theorem :: CIRCTRM1:15 for S being non empty non void ManySortedSign for V being V2() ManySortedSet of the carrier of S for A being non-empty finite-yielding 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) by Def5; theorem Th16: :: CIRCTRM1:16 for S being non empty non void ManySortedSign for V being V2() ManySortedSet of the carrier of S for A being non-empty finite-yielding MSAlgebra over S for X being SetWithCompoundTerm of S,V for g being OperSymbol of (X -CircuitStr) for o being OperSymbol of S st g . {} = [o, the carrier of S] holds Den (g,(X -Circuit A)) = Den (o,A) proof let S be non empty non void ManySortedSign ; ::_thesis: for V being V2() ManySortedSet of the carrier of S for A being non-empty finite-yielding MSAlgebra over S for X being SetWithCompoundTerm of S,V for g being OperSymbol of (X -CircuitStr) for o being OperSymbol of S st g . {} = [o, the carrier of S] holds Den (g,(X -Circuit A)) = Den (o,A) let V be V2() ManySortedSet of the carrier of S; ::_thesis: for A being non-empty finite-yielding MSAlgebra over S for X being SetWithCompoundTerm of S,V for g being OperSymbol of (X -CircuitStr) for o being OperSymbol of S st g . {} = [o, the carrier of S] holds Den (g,(X -Circuit A)) = Den (o,A) let A be non-empty finite-yielding MSAlgebra over S; ::_thesis: for X being SetWithCompoundTerm of S,V for g being OperSymbol of (X -CircuitStr) for o being OperSymbol of S st g . {} = [o, the carrier of S] holds Den (g,(X -Circuit A)) = Den (o,A) let X be SetWithCompoundTerm of S,V; ::_thesis: for g being OperSymbol of (X -CircuitStr) for o being OperSymbol of S st g . {} = [o, the carrier of S] holds Den (g,(X -Circuit A)) = Den (o,A) let g be OperSymbol of (X -CircuitStr); ::_thesis: for o being OperSymbol of S st g . {} = [o, the carrier of S] holds Den (g,(X -Circuit A)) = Den (o,A) let o be OperSymbol of S; ::_thesis: ( g . {} = [o, the carrier of S] implies Den (g,(X -Circuit A)) = Den (o,A) ) Den (g,(X -Circuit A)) = the_action_of (g,A) by Def5 .= the Charact of A . ((g . {}) `1) by Def3 ; hence ( g . {} = [o, the carrier of S] implies Den (g,(X -Circuit A)) = Den (o,A) ) by MCART_1:7; ::_thesis: verum end; theorem Th17: :: CIRCTRM1:17 for S being non empty non void ManySortedSign for V being V2() ManySortedSet of the carrier of S for A being non-empty finite-yielding MSAlgebra over S for X being non empty Subset of (S -Terms V) holds X -Circuit A is finite-yielding proof let S be non empty non void ManySortedSign ; ::_thesis: for V being V2() ManySortedSet of the carrier of S for A being non-empty finite-yielding MSAlgebra over S for X being non empty Subset of (S -Terms V) holds X -Circuit A is finite-yielding let V be V2() ManySortedSet of the carrier of S; ::_thesis: for A being non-empty finite-yielding MSAlgebra over S for X being non empty Subset of (S -Terms V) holds X -Circuit A is finite-yielding let A be non-empty finite-yielding MSAlgebra over S; ::_thesis: for X being non empty Subset of (S -Terms V) holds X -Circuit A is finite-yielding let t be non empty Subset of (S -Terms V); ::_thesis: t -Circuit A is finite-yielding let i be set ; :: according to MSAFREE2:def_11,FINSET_1:def_5 ::_thesis: ( not i in the carrier of (t -CircuitStr) or the Sorts of (t -Circuit A) . i is finite ) assume i in the carrier of (t -CircuitStr) ; ::_thesis: the Sorts of (t -Circuit A) . i is finite then reconsider i = i as Vertex of (t -CircuitStr) ; reconsider u = i as Term of S,V by Th4; A1: the Sorts of A is V29() 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 the Sorts of (t -Circuit A) . i is finite by A1; ::_thesis: verum end; registration let S be non empty non void ManySortedSign ; let V be V2() ManySortedSet of the carrier of S; let X be SetWithCompoundTerm of S,V; let A be non-empty finite-yielding MSAlgebra over S; clusterX -Circuit A -> strict non-empty finite-yielding ; coherence X -Circuit A is finite-yielding by Th17; end; theorem Th18: :: CIRCTRM1:18 for S being non empty non void ManySortedSign for V being V2() 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 proof let S be non empty non void ManySortedSign ; ::_thesis: for V being V2() 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 let V be V2() ManySortedSet of the carrier of S; ::_thesis: for X1, X2 being SetWithCompoundTerm of S,V for A being non-empty MSAlgebra over S holds X1 -Circuit A tolerates X2 -Circuit A let X1, X2 be SetWithCompoundTerm of S,V; ::_thesis: for A being non-empty MSAlgebra over S holds X1 -Circuit A tolerates X2 -Circuit A let A be non-empty MSAlgebra over S; ::_thesis: X1 -Circuit A tolerates X2 -Circuit A 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; :: according to CIRCCOMB:def_1,CIRCCOMB:def_3 ::_thesis: ( the Sorts of (X1 -Circuit A) tolerates the Sorts of (X2 -Circuit A) & the Charact of (X1 -Circuit A) tolerates the Charact of (X2 -Circuit A) ) thus the Sorts of (X1 -Circuit A) tolerates the Sorts of (X2 -Circuit A) ::_thesis: the Charact of (X1 -Circuit A) tolerates the Charact of (X2 -Circuit A) proof let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( not x in (proj1 the Sorts of (X1 -Circuit A)) /\ (proj1 the Sorts of (X2 -Circuit A)) or the Sorts of (X1 -Circuit A) . x = the Sorts of (X2 -Circuit A) . x ) assume A1: x in (dom the Sorts of (X1 -Circuit A)) /\ (dom the Sorts of (X2 -Circuit A)) ; ::_thesis: the Sorts of (X1 -Circuit A) . x = the Sorts of (X2 -Circuit A) . x 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 ; ::_thesis: verum end; let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( not x in (proj1 the Charact of (X1 -Circuit A)) /\ (proj1 the Charact of (X2 -Circuit A)) or the Charact of (X1 -Circuit A) . x = the Charact of (X2 -Circuit A) . x ) assume A5: x in (dom the Charact of (X1 -Circuit A)) /\ (dom the Charact of (X2 -Circuit A)) ; ::_thesis: the Charact of (X1 -Circuit A) . x = the Charact of (X2 -Circuit A) . x 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 ; ::_thesis: verum end; theorem :: CIRCTRM1:19 for S being non empty non void ManySortedSign for V being V2() 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) proof let S be non empty non void ManySortedSign ; ::_thesis: for V being V2() 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) let V be V2() ManySortedSet of the carrier of S; ::_thesis: 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) let X1, X2 be SetWithCompoundTerm of S,V; ::_thesis: for A being non-empty MSAlgebra over S holds (X1 \/ X2) -Circuit A = (X1 -Circuit A) +* (X2 -Circuit A) consider t1 being 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; ::_thesis: (X1 \/ X2) -Circuit A = (X1 -Circuit A) +* (X2 -Circuit A) set C1 = X1 -Circuit A; set C2 = X2 -Circuit A; set C = X -Circuit A; A2: X1 -Circuit A tolerates X2 -Circuit A by Th18; then A3: the Sorts of (X1 -Circuit A) tolerates the Sorts of (X2 -Circuit A) by CIRCCOMB:def_3; A4: the Charact of (X1 -Circuit A) tolerates the Charact of (X2 -Circuit A) by A2, CIRCCOMB:def_3; A5: the Sorts of ((X1 -Circuit A) +* (X2 -Circuit A)) = the Sorts of (X1 -Circuit A) +* the Sorts of (X2 -Circuit A) by A3, CIRCCOMB:def_4; A6: the Charact of ((X1 -Circuit A) +* (X2 -Circuit A)) = the Charact of (X1 -Circuit A) +* the Charact of (X2 -Circuit A) by A3, CIRCCOMB:def_4; A7: X -CircuitStr = (X1 -CircuitStr) +* (X2 -CircuitStr) by Th10; A8: X1 -Circuit A tolerates X -Circuit A by Th18; A9: X2 -Circuit A tolerates X -Circuit A by Th18; A10: the Sorts of (X1 -Circuit A) tolerates the Sorts of (X -Circuit A) by A8, CIRCCOMB:def_3; A11: the Sorts of (X2 -Circuit A) tolerates the Sorts of (X -Circuit A) by A9, CIRCCOMB:def_3; A12: the Charact of (X1 -Circuit A) tolerates the Charact of (X -Circuit A) by A8, CIRCCOMB:def_3; A13: the Charact of (X2 -Circuit A) tolerates the Charact of (X -Circuit A) by A9, CIRCCOMB:def_3; A14: dom the Sorts of ((X1 -Circuit A) +* (X2 -Circuit A)) = the carrier of (X -CircuitStr) by A7, PARTFUN1:def_2; dom the Charact of ((X1 -Circuit A) +* (X2 -Circuit A)) = the carrier' of (X -CircuitStr) by A7, PARTFUN1:def_2; then A15: dom the Charact of ((X1 -Circuit A) +* (X2 -Circuit A)) = dom the Charact of (X -Circuit A) by PARTFUN1:def_2; A16: dom the Sorts of ((X1 -Circuit A) +* (X2 -Circuit A)) = dom the Sorts of (X -Circuit A) by A14, PARTFUN1:def_2; A17: the Charact of ((X1 -Circuit A) +* (X2 -Circuit A)) = the Charact of (X -Circuit A) by A4, A6, A12, A13, A15, FUNCT_4:125, PARTFUN1:55; the Sorts of ((X1 -Circuit A) +* (X2 -Circuit A)) = the Sorts of (X -Circuit A) by A3, A5, A10, A11, A16, FUNCT_4:125, PARTFUN1:55; hence (X1 \/ X2) -Circuit A = (X1 -Circuit A) +* (X2 -Circuit A) by A17; ::_thesis: verum end; begin 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; assume A1: t is Term of S,V ; let f be ManySortedFunction of V, the Sorts of A; funct @ (f,A) -> set means :Def7: :: CIRCTRM1:def 7 ex t9 being c-Term of A,V st ( t9 = t & it = t9 @ f ); correctness existence ex b1 being set ex t9 being c-Term of A,V st ( t9 = t & b1 = t9 @ f ); uniqueness for b1, b2 being set st ex t9 being c-Term of A,V st ( t9 = t & b1 = t9 @ f ) & ex t9 being c-Term of A,V st ( t9 = t & b2 = t9 @ f ) holds b1 = b2; proof reconsider t9 = t as c-Term of A,V by A1, MSATERM:27; t9 @ f = t9 @ f ; hence ( ex b1 being set ex t9 being c-Term of A,V st ( t9 = t & b1 = t9 @ f ) & ( for b1, b2 being set st ex t9 being c-Term of A,V st ( t9 = t & b1 = t9 @ f ) & ex t9 being c-Term of A,V st ( t9 = t & b2 = t9 @ f ) holds b1 = b2 ) ) ; ::_thesis: verum end; end; :: deftheorem Def7 defines @ CIRCTRM1:def_7_:_ 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 DecoratedTree st t is Term of S,V holds for f being ManySortedFunction of V, the Sorts of A for b6 being set holds ( b6 = t @ (f,A) iff ex t9 being c-Term of A,V st ( t9 = t & b6 = t9 @ f ) ); definition let S be non empty non void ManySortedSign ; let V be V2() 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 S1[ set , set , set ] means ( root-tree [\$2,\$1] in Subtrees X implies \$3 = s . (root-tree [\$2,\$1]) ); A1: for x being Vertex of S for v being Element of V . x ex a being Element of the Sorts of A . x st S1[x,v,a] proof let x be Vertex of S; ::_thesis: for v being Element of V . x ex a being Element of the Sorts of A . x st S1[x,v,a] let v be Element of V . x; ::_thesis: ex a being Element of the Sorts of A . x st S1[x,v,a] percases ( not root-tree [v,x] in Subtrees X or root-tree [v,x] in Subtrees X ) ; suppose not root-tree [v,x] in Subtrees X ; ::_thesis: ex a being Element of the Sorts of A . x st S1[x,v,a] hence ex a being Element of the Sorts of A . x st S1[x,v,a] ; ::_thesis: verum end; suppose root-tree [v,x] in Subtrees X ; ::_thesis: ex a being Element of the Sorts of A . x st S1[x,v,a] 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 ; ::_thesis: S1[x,v,b] thus S1[x,v,b] ; ::_thesis: verum end; end; end; mode CompatibleValuation of s -> ManySortedFunction of V, the Sorts of A means :Def8: :: CIRCTRM1:def 8 for x being Vertex of S for v being Element of V . x st root-tree [v,x] in Subtrees X holds (it . x) . v = s . (root-tree [v,x]); existence ex b1 being ManySortedFunction of V, the Sorts of A st for x being Vertex of S for v being Element of V . x st root-tree [v,x] in Subtrees X holds (b1 . x) . v = s . (root-tree [v,x]) proof thus ex f being ManySortedFunction of V, the Sorts of A st for x being Element of S for v being Element of V . x holds S1[x,v,(f . x) . v] from CIRCTRM1:sch_1(A1); ::_thesis: verum end; end; :: deftheorem Def8 defines CompatibleValuation CIRCTRM1:def_8_:_ for S being non empty non void ManySortedSign for V being V2() ManySortedSet of the carrier of S for X being SetWithCompoundTerm of S,V for A being non-empty finite-yielding MSAlgebra over S for s being State of (X -Circuit A) for b6 being ManySortedFunction of V, the Sorts of A holds ( b6 is CompatibleValuation of s iff for x being Vertex of S for v being Element of V . x st root-tree [v,x] in Subtrees X holds (b6 . x) . v = s . (root-tree [v,x]) ); theorem :: CIRCTRM1:20 for S being non empty non void ManySortedSign for A being non-empty finite-yielding MSAlgebra over S for V being Variables of A for X being SetWithCompoundTerm of S,V for s being State of (X -Circuit A) for f being CompatibleValuation of s for n being Element of NAT holds f is CompatibleValuation of Following (s,n) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty finite-yielding MSAlgebra over S for V being Variables of A for X being SetWithCompoundTerm of S,V for s being State of (X -Circuit A) for f being CompatibleValuation of s for n being Element of NAT holds f is CompatibleValuation of Following (s,n) let A be non-empty finite-yielding MSAlgebra over S; ::_thesis: for V being Variables of A for X being SetWithCompoundTerm of S,V for s being State of (X -Circuit A) for f being CompatibleValuation of s for n being Element of NAT holds f is CompatibleValuation of Following (s,n) let V be Variables of A; ::_thesis: for X being SetWithCompoundTerm of S,V for s being State of (X -Circuit A) for f being CompatibleValuation of s for n being Element of NAT holds f is CompatibleValuation of Following (s,n) let X be SetWithCompoundTerm of S,V; ::_thesis: for s being State of (X -Circuit A) for f being CompatibleValuation of s for n being Element of NAT holds f is CompatibleValuation of Following (s,n) let s be State of (X -Circuit A); ::_thesis: for f being CompatibleValuation of s for n being Element of NAT holds f is CompatibleValuation of Following (s,n) let f be CompatibleValuation of s; ::_thesis: for n being Element of NAT holds f is CompatibleValuation of Following (s,n) let n be Element of NAT ; ::_thesis: f is CompatibleValuation of Following (s,n) let x be Vertex of S; :: according to CIRCTRM1:def_8 ::_thesis: for v being Element of V . x st root-tree [v,x] in Subtrees X holds (f . x) . v = (Following (s,n)) . (root-tree [v,x]) let v be Element of V . x; ::_thesis: ( root-tree [v,x] in Subtrees X implies (f . x) . v = (Following (s,n)) . (root-tree [v,x]) ) assume A1: root-tree [v,x] in Subtrees X ; ::_thesis: (f . x) . v = (Following (s,n)) . (root-tree [v,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]) by FACIRC_1:def_9; hence (f . x) . v = (Following (s,n)) . (root-tree [v,x]) by A1, Def8; ::_thesis: verum end; registration let x be set ; let S be non empty non void ManySortedSign ; let V be V2() ManySortedSet of the carrier of S; let p be FinSequence of S -Terms V; clusterx -tree p -> finite ; coherence x -tree p is finite proof reconsider q = doms p as FinTree-yielding FinSequence ; dom (x -tree p) = tree q by TREES_4:10; hence x -tree p is finite by FINSET_1:10; ::_thesis: verum end; end; theorem Th21: :: CIRCTRM1:21 for S being non empty non void ManySortedSign for A being non-empty finite-yielding MSAlgebra over S for V being Variables of A for X being SetWithCompoundTerm of S,V 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) ) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty finite-yielding MSAlgebra over S for V being Variables of A for X being SetWithCompoundTerm of S,V 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) ) let A be non-empty finite-yielding MSAlgebra over S; ::_thesis: for V being Variables of A for X being SetWithCompoundTerm of S,V 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) ) let V be Variables of A; ::_thesis: for X being SetWithCompoundTerm of S,V 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) ) let X be SetWithCompoundTerm of S,V; ::_thesis: 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) ) let q be State of (X -Circuit A); ::_thesis: for f being CompatibleValuation of q for t being Term of S,V st 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) ) let f be CompatibleValuation of q; ::_thesis: for t being Term of S,V st 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) ) 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 S1[ 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 being SortSymbol of S for v being Element of V . s holds S1[ root-tree [v,s]] proof let s be SortSymbol of S; ::_thesis: for v being Element of V . s holds S1[ root-tree [v,s]] let v be Element of V . s; ::_thesis: S1[ root-tree [v,s]] assume A3: root-tree [v,s] in Subtrees X ; ::_thesis: ( Following (q,(1 + (height (dom (root-tree [v,s]))))) is_stable_at root-tree [v,s] & (Following (q,(1 + (height (dom (root-tree [v,s])))))) . (root-tree [v,s]) = (root-tree [v,s]) @ (f,A) ) 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; ::_thesis: (Following (q,(1 + (height (dom (root-tree [v,s])))))) . (root-tree [v,s]) = (root-tree [v,s]) @ (f,A) 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]) by FACIRC_1:def_9 .= (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 ; ::_thesis: verum end; A6: for o being OperSymbol of S for p being ArgumentSeq of Sym (o,V) st ( for t being Term of S,V st t in rng p holds S1[t] ) holds S1[[o, the carrier of S] -tree p] proof let o be OperSymbol of S; ::_thesis: for p being ArgumentSeq of Sym (o,V) st ( for t being Term of S,V st t in rng p holds S1[t] ) holds S1[[o, the carrier of S] -tree p] let p be ArgumentSeq of Sym (o,V); ::_thesis: ( ( for t being Term of S,V st t in rng p holds S1[t] ) implies S1[[o, the carrier of S] -tree p] ) assume that A7: for t being 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 ; ::_thesis: ( Following (q,(1 + (height (dom ([o, the carrier of S] -tree p))))) is_stable_at [o, the carrier of S] -tree p & (Following (q,(1 + (height (dom ([o, the carrier of S] -tree p)))))) . ([o, the carrier of S] -tree p) = ([o, the carrier of S] -tree p) @ (f,A) ) consider tt being Element of X, n being 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 by FUNCT_1:17; 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__::_thesis:_for_x_being_set_st_x_in_rng_(the_arity_of_g)_holds_ Following_(q,(height_(dom_([o,_the_carrier_of_S]_-tree_p))))_is_stable_at_x let x be set ; ::_thesis: ( x in rng (the_arity_of g) implies Following (q,(height (dom ([o, the carrier of S] -tree p)))) is_stable_at x ) assume A16: x in rng (the_arity_of g) ; ::_thesis: Following (q,(height (dom ([o, the carrier of S] -tree p)))) is_stable_at x then reconsider t = x as Element of Subtrees X by A14; reconsider t = t as Term of S,V by A1, Th4; consider z being set 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 being Nat such that A20: height (tree (doms p)) = (1 + (height (dom t))) + i by NAT_1:10; reconsider i = 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; ::_thesis: verum 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; ::_thesis: (Following (q,(1 + (height (dom ([o, the carrier of S] -tree p)))))) . ([o, the carrier of S] -tree p) = ([o, the carrier of S] -tree p) @ (f,A) 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 H1( set ) -> set = (Following (q,(height (dom t)))) . (p . \$1); consider vp being FinSequence such that A24: len vp = len p and A25: for i being Nat st i in dom vp holds vp . i = H1(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__::_thesis:_for_i_being_Nat_st_i_in_dom_p_holds_ ex_t9_being_c-Term_of_A,V_st_ (_t9_=_p_._i_&_the_sort_of_t9_=_(the_arity_of_o)_._i_) let i be Nat; ::_thesis: ( i in dom p implies ex t9 being c-Term of A,V st ( t9 = p . i & the_sort_of t9 = (the_arity_of o) . i ) ) assume A29: i in dom p ; ::_thesis: ex t9 being c-Term of A,V st ( t9 = p . i & the_sort_of t9 = (the_arity_of o) . i ) 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 = t9; ::_thesis: ( t9 = p . i & the_sort_of t9 = (the_arity_of o) . i ) 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; ::_thesis: verum end; then reconsider p9 = p as ArgumentSeq of o,A,V by A28, MSATERM:24; now__::_thesis:_for_i_being_Nat_st_i_in_dom_p_holds_ for_t_being_c-Term_of_A,V_st_t_=_p_._i_holds_ vp_._i_=_t_@_f let i be Nat; ::_thesis: ( i in dom p implies for t being c-Term of A,V st t = p . i holds vp . i = t @ f ) assume A30: i in dom p ; ::_thesis: for t being c-Term of A,V st t = p . i holds vp . i = t @ f let t be c-Term of A,V; ::_thesis: ( t = p . i implies vp . i = t @ f ) assume A31: t = p . i ; ::_thesis: vp . i = t @ f 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 = 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 being Nat such that A37: height (tree (doms p)) = (1 + (height (dom t))) + j by NAT_1:10; reconsider j = 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, FACIRC_1:def_9; hence vp . i = t @ f by A34, A35, Def7; ::_thesis: verum end; then A38: ((Sym (o,( the Sorts of A \/ V))) -tree p9) @ f = (Den (o,A)) . vp by A24, MSATERM:43; now__::_thesis:_(_dom_((Following_(q,(height_(dom_t))))_*_p)_=_dom_p_&_(_for_z_being_set_st_z_in_Seg_(len_p)_holds_ vp_._z_=_((Following_(q,(height_(dom_t))))_*_p)_._z_)_) 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; ::_thesis: for z being set st z in Seg (len p) holds vp . z = ((Following (q,(height (dom t)))) * p) . z let z be set ; ::_thesis: ( z in Seg (len p) implies vp . z = ((Following (q,(height (dom t)))) * p) . z ) assume A40: z in Seg (len p) ; ::_thesis: vp . z = ((Following (q,(height (dom t)))) * p) . z 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; ::_thesis: verum 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 ; ::_thesis: verum end; thus for t being Term of S,V holds S1[t] from MSATERM:sch_1(A2, A6); ::_thesis: verum end; theorem :: CIRCTRM1:22 for S being non empty non void ManySortedSign for A being non-empty finite-yielding MSAlgebra over S for V being Variables of A for X being SetWithCompoundTerm of S,V st ( for t being Term of S,V for o being OperSymbol of S holds ( not t in Subtrees X or not t . {} = [o, the carrier of S] or not the_arity_of o = {} ) ) holds 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) ) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty finite-yielding MSAlgebra over S for V being Variables of A for X being SetWithCompoundTerm of S,V st ( for t being Term of S,V for o being OperSymbol of S holds ( not t in Subtrees X or not t . {} = [o, the carrier of S] or not the_arity_of o = {} ) ) holds 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) ) let A be non-empty finite-yielding MSAlgebra over S; ::_thesis: for V being Variables of A for X being SetWithCompoundTerm of S,V st ( for t being Term of S,V for o being OperSymbol of S holds ( not t in Subtrees X or not t . {} = [o, the carrier of S] or not the_arity_of o = {} ) ) holds 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) ) let V be Variables of A; ::_thesis: for X being SetWithCompoundTerm of S,V st ( for t being Term of S,V for o being OperSymbol of S holds ( not t in Subtrees X or not t . {} = [o, the carrier of S] or not the_arity_of o = {} ) ) holds 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) ) let X be SetWithCompoundTerm of S,V; ::_thesis: ( ( for t being Term of S,V for o being OperSymbol of S holds ( not t in Subtrees X or not t . {} = [o, the carrier of S] or not 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) ) ) assume A1: for t being Term of S,V for o being OperSymbol of S holds ( not t in Subtrees X or not t . {} = [o, the carrier of S] or not the_arity_of o = {} ) ; ::_thesis: 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) ) let q be State of (X -Circuit A); ::_thesis: for f being CompatibleValuation of q for t being Term of S,V st t in Subtrees X holds ( Following (q,(height (dom t))) is_stable_at t & (Following (q,(height (dom t)))) . t = t @ (f,A) ) let f be CompatibleValuation of q; ::_thesis: for t being Term of S,V st t in Subtrees X holds ( Following (q,(height (dom t))) is_stable_at t & (Following (q,(height (dom t)))) . t = t @ (f,A) ) 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 S1[ 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 being SortSymbol of S for v being Element of V . s holds S1[ root-tree [v,s]] proof let s be SortSymbol of S; ::_thesis: for v being Element of V . s holds S1[ root-tree [v,s]] let v be Element of V . s; ::_thesis: S1[ root-tree [v,s]] assume A4: root-tree [v,s] in Subtrees X ; ::_thesis: ( Following (q,(height (dom (root-tree [v,s])))) is_stable_at root-tree [v,s] & (Following (q,(height (dom (root-tree [v,s]))))) . (root-tree [v,s]) = (root-tree [v,s]) @ (f,A) ) 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; ::_thesis: (Following (q,(height (dom (root-tree [v,s]))))) . (root-tree [v,s]) = (root-tree [v,s]) @ (f,A) 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 ; ::_thesis: verum end; A6: for o being OperSymbol of S for p being ArgumentSeq of Sym (o,V) st ( for t being Term of S,V st t in rng p holds S1[t] ) holds S1[[o, the carrier of S] -tree p] proof let o be OperSymbol of S; ::_thesis: for p being ArgumentSeq of Sym (o,V) st ( for t being Term of S,V st t in rng p holds S1[t] ) holds S1[[o, the carrier of S] -tree p] let p be ArgumentSeq of Sym (o,V); ::_thesis: ( ( for t being Term of S,V st t in rng p holds S1[t] ) implies S1[[o, the carrier of S] -tree p] ) assume that A7: for t being 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 ; ::_thesis: ( Following (q,(height (dom ([o, the carrier of S] -tree p)))) is_stable_at [o, the carrier of S] -tree p & (Following (q,(height (dom ([o, the carrier of S] -tree p))))) . ([o, the carrier of S] -tree p) = ([o, the carrier of S] -tree p) @ (f,A) ) consider tt being Element of X, n being 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 by FUNCT_1:17; 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__::_thesis:_not_height_(dom_([o,_the_carrier_of_S]_-tree_p))_=_0 assume height (dom ([o, the carrier of S] -tree p)) = 0 ; ::_thesis: contradiction 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; ::_thesis: verum end; then consider h being Nat such that A17: height (dom ([o, the carrier of S] -tree p)) = h + 1 by NAT_1:6; reconsider h = h as Element of NAT by ORDINAL1:def_12; now__::_thesis:_for_x_being_set_st_x_in_rng_(the_arity_of_g)_holds_ Following_(q,h)_is_stable_at_x let x be set ; ::_thesis: ( x in rng (the_arity_of g) implies Following (q,h) is_stable_at x ) assume A18: x in rng (the_arity_of g) ; ::_thesis: Following (q,h) is_stable_at x then reconsider t = x as Element of Subtrees X by A14; reconsider t = t as Term of S,V by A2, Th4; consider z being set 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 being Nat such that A22: h = (height (dom t)) + i by NAT_1:10; reconsider i = 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; ::_thesis: verum 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; ::_thesis: (Following (q,(height (dom ([o, the carrier of S] -tree p))))) . ([o, the carrier of S] -tree p) = ([o, the carrier of S] -tree p) @ (f,A) 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 H1( set ) -> set = (Following (q,h)) . (p . \$1); consider vp being FinSequence such that A26: len vp = len p and A27: for i being Nat st i in dom vp holds vp . i = H1(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__::_thesis:_for_i_being_Nat_st_i_in_dom_p_holds_ ex_t9_being_c-Term_of_A,V_st_ (_t9_=_p_._i_&_the_sort_of_t9_=_(the_arity_of_o)_._i_) let i be Nat; ::_thesis: ( i in dom p implies ex t9 being c-Term of A,V st ( t9 = p . i & the_sort_of t9 = (the_arity_of o) . i ) ) assume A31: i in dom p ; ::_thesis: ex t9 being c-Term of A,V st ( t9 = p . i & the_sort_of t9 = (the_arity_of o) . i ) 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 = t9; ::_thesis: ( t9 = p . i & the_sort_of t9 = (the_arity_of o) . i ) 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; ::_thesis: verum end; then reconsider p9 = p as ArgumentSeq of o,A,V by A30, MSATERM:24; now__::_thesis:_for_i_being_Nat_st_i_in_dom_p_holds_ for_t_being_c-Term_of_A,V_st_t_=_p_._i_holds_ vp_._i_=_t_@_f let i be Nat; ::_thesis: ( i in dom p implies for t being c-Term of A,V st t = p . i holds vp . i = t @ f ) assume A32: i in dom p ; ::_thesis: for t being c-Term of A,V st t = p . i holds vp . i = t @ f let t be c-Term of A,V; ::_thesis: ( t = p . i implies vp . i = t @ f ) assume A33: t = p . i ; ::_thesis: vp . i = t @ f 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 = 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 being Nat such that A39: h = (height (dom t)) + j by NAT_1:10; reconsider j = 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, FACIRC_1:def_9; hence vp . i = t @ f by A36, A37, Def7; ::_thesis: verum end; then A40: ((Sym (o,( the Sorts of A \/ V))) -tree p9) @ f = (Den (o,A)) . vp by A26, MSATERM:43; now__::_thesis:_(_dom_((Following_(q,h))_*_p)_=_dom_p_&_(_for_z_being_set_st_z_in_Seg_(len_p)_holds_ vp_._z_=_((Following_(q,h))_*_p)_._z_)_) 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; ::_thesis: for z being set st z in Seg (len p) holds vp . z = ((Following (q,h)) * p) . z let z be set ; ::_thesis: ( z in Seg (len p) implies vp . z = ((Following (q,h)) * p) . z ) assume A42: z in Seg (len p) ; ::_thesis: vp . z = ((Following (q,h)) * p) . z 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; ::_thesis: verum 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 ; ::_thesis: verum end; thus for t being Term of S,V holds S1[t] from MSATERM:sch_1(A3, A6); ::_thesis: verum end; begin definition let S1, S2 be non empty ManySortedSign ; let f, g be Function; predS1,S2 are_equivalent_wrt f,g means :Def9: :: 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; :: deftheorem Def9 defines are_equivalent_wrt CIRCTRM1:def_9_:_ for S1, S2 being non empty ManySortedSign for f, g being Function holds ( S1,S2 are_equivalent_wrt f,g iff ( f is one-to-one & g is one-to-one & f,g form_morphism_between S1,S2 & f " ,g " form_morphism_between S2,S1 ) ); theorem Th23: :: CIRCTRM1:23 for S1, S2 being non empty ManySortedSign for f, g being 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 ; ::_thesis: for f, g being 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 ) let f, g be Function; ::_thesis: ( S1,S2 are_equivalent_wrt f,g implies ( the carrier of S2 = f .: the carrier of S1 & the carrier' of S2 = g .: the carrier' of S1 ) ) 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 A4: f " ,g " form_morphism_between S2,S1 ; :: according to CIRCTRM1:def_9 ::_thesis: ( the carrier of S2 = f .: the carrier of S1 & the carrier' of S2 = g .: the carrier' of S1 ) thus the carrier of S2 = dom (f ") by A4, PUA2MSS1:def_12 .= rng f by A1, FUNCT_1:33 .= f .: (dom f) by RELAT_1:113 .= f .: the carrier of S1 by A3, PUA2MSS1:def_12 ; ::_thesis: the carrier' of S2 = g .: the carrier' of S1 thus the carrier' of S2 = dom (g ") by A4, PUA2MSS1:def_12 .= rng g by A2, FUNCT_1:33 .= g .: (dom g) by RELAT_1:113 .= g .: the carrier' of S1 by A3, PUA2MSS1:def_12 ; ::_thesis: verum end; theorem Th24: :: CIRCTRM1:24 for S1, S2 being non empty ManySortedSign for f, g being 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 ; ::_thesis: for f, g being Function st S1,S2 are_equivalent_wrt f,g holds ( rng f = the carrier of S2 & rng g = the carrier' of S2 ) let f, g be Function; ::_thesis: ( S1,S2 are_equivalent_wrt f,g implies ( rng f = the carrier of S2 & rng g = the carrier' of S2 ) ) assume 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 ; :: according to CIRCTRM1:def_9 ::_thesis: ( rng f = the carrier of S2 & rng g = the carrier' of S2 ) thus rng f = dom (f ") by A1, FUNCT_1:33 .= the carrier of S2 by A3, PUA2MSS1:def_12 ; ::_thesis: rng g = the carrier' of S2 thus rng g = dom (g ") by A2, FUNCT_1:33 .= the carrier' of S2 by A3, PUA2MSS1:def_12 ; ::_thesis: verum end; theorem Th25: :: CIRCTRM1:25 for S being 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 ; ::_thesis: S,S are_equivalent_wrt id the carrier of S, id the carrier' of S set f = id the carrier of S; set g = id the carrier' of S; thus id the carrier of S is one-to-one ; :: according to CIRCTRM1:def_9 ::_thesis: ( id the carrier' of S is one-to-one & id the carrier of S, id the carrier' of S form_morphism_between S,S & (id the carrier of S) " ,(id the carrier' of S) " form_morphism_between S,S ) A1: (id the carrier of S) " = id the carrier of S by FUNCT_1:45; (id the carrier' of S) " = id the carrier' of S by FUNCT_1:45; hence ( id the carrier' of S is one-to-one & id the carrier of S, id the carrier' of S form_morphism_between S,S & (id the carrier of S) " ,(id the carrier' of S) " form_morphism_between S,S ) by A1, INSTALG1:8; ::_thesis: verum end; theorem Th26: :: CIRCTRM1:26 for S1, S2 being non empty ManySortedSign for f, g being 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 ; ::_thesis: for f, g being Function st S1,S2 are_equivalent_wrt f,g holds S2,S1 are_equivalent_wrt f " ,g " let f, g be Function; ::_thesis: ( S1,S2 are_equivalent_wrt f,g implies S2,S1 are_equivalent_wrt f " ,g " ) 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 A4: f " ,g " form_morphism_between S2,S1 ; :: according to CIRCTRM1:def_9 ::_thesis: S2,S1 are_equivalent_wrt f " ,g " thus ( f " is one-to-one & g " is one-to-one ) by A1, A2; :: according to CIRCTRM1:def_9 ::_thesis: ( f " ,g " form_morphism_between S2,S1 & (f ") " ,(g ") " form_morphism_between S1,S2 ) (f ") " = f by A1, FUNCT_1:43; hence ( f " ,g " form_morphism_between S2,S1 & (f ") " ,(g ") " form_morphism_between S1,S2 ) by A2, A3, A4, FUNCT_1:43; ::_thesis: verum end; theorem Th27: :: CIRCTRM1:27 for S1, S2, S3 being non empty ManySortedSign for 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 proof let S1, S2, S3 be non empty ManySortedSign ; ::_thesis: for 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 let f1, g1, f2, g2 be Function; ::_thesis: ( S1,S2 are_equivalent_wrt f1,g1 & S2,S3 are_equivalent_wrt f2,g2 implies S1,S3 are_equivalent_wrt f2 * f1,g2 * g1 ) assume 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 ; :: according to CIRCTRM1:def_9 ::_thesis: S1,S3 are_equivalent_wrt f2 * f1,g2 * g1 thus ( f2 * f1 is one-to-one & g2 * g1 is one-to-one ) by A1, A2, A5, A6; :: according to CIRCTRM1:def_9 ::_thesis: ( f2 * f1,g2 * g1 form_morphism_between S1,S3 & (f2 * f1) " ,(g2 * g1) " form_morphism_between S3,S1 ) A9: (f2 * f1) " = (f1 ") * (f2 ") by A1, A5, FUNCT_1:44; (g2 * g1) " = (g1 ") * (g2 ") by A2, A6, FUNCT_1:44; hence ( f2 * f1,g2 * g1 form_morphism_between S1,S3 & (f2 * f1) " ,(g2 * g1) " form_morphism_between S3,S1 ) by A3, A4, A7, A8, A9, PUA2MSS1:29; ::_thesis: verum end; theorem Th28: :: CIRCTRM1:28 for S1, S2 being non empty ManySortedSign for f, g being 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 ; ::_thesis: for f, g being Function st S1,S2 are_equivalent_wrt f,g holds ( f .: (InputVertices S1) = InputVertices S2 & f .: (InnerVertices S1) = InnerVertices S2 ) let f, g be Function; ::_thesis: ( S1,S2 are_equivalent_wrt f,g implies ( f .: (InputVertices S1) = InputVertices S2 & f .: (InnerVertices S1) = InnerVertices S2 ) ) assume A1: S1,S2 are_equivalent_wrt f,g ; ::_thesis: ( f .: (InputVertices S1) = InputVertices S2 & f .: (InnerVertices S1) = InnerVertices S2 ) A2: f is one-to-one by A1, Def9; A3: f,g form_morphism_between S1,S2 by A1, Def9; 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, PUA2MSS1:def_12 .= 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 ; ::_thesis: f .: (InnerVertices S1) = InnerVertices S2 thus f .: (InnerVertices S1) = InnerVertices S2 by A6; ::_thesis: verum end; definition let S1, S2 be non empty ManySortedSign ; predS1,S2 are_equivalent means :: CIRCTRM1:def 10 ex f, g being one-to-one Function st S1,S2 are_equivalent_wrt f,g; reflexivity for S1 being non empty ManySortedSign ex f, g being one-to-one Function st S1,S1 are_equivalent_wrt f,g proof let S be non empty ManySortedSign ; ::_thesis: ex f, g being one-to-one Function st S,S are_equivalent_wrt f,g take id the carrier of S ; ::_thesis: ex g being one-to-one Function st S,S are_equivalent_wrt id the carrier of S,g take id the carrier' of S ; ::_thesis: S,S are_equivalent_wrt id the carrier of S, id the carrier' of S thus S,S are_equivalent_wrt id the carrier of S, id the carrier' of S by Th25; ::_thesis: verum end; symmetry for S1, S2 being non empty ManySortedSign st ex f, g being one-to-one Function st S1,S2 are_equivalent_wrt f,g holds ex f, g being one-to-one Function st S2,S1 are_equivalent_wrt f,g proof let S1, S2 be non empty ManySortedSign ; ::_thesis: ( ex f, g being one-to-one Function st S1,S2 are_equivalent_wrt f,g implies ex f, g being one-to-one Function st S2,S1 are_equivalent_wrt f,g ) given f, g being one-to-one Function such that A1: S1,S2 are_equivalent_wrt f,g ; ::_thesis: ex f, g being one-to-one Function st S2,S1 are_equivalent_wrt f,g take f " ; ::_thesis: ex g being one-to-one Function st S2,S1 are_equivalent_wrt f " ,g take g " ; ::_thesis: S2,S1 are_equivalent_wrt f " ,g " thus S2,S1 are_equivalent_wrt f " ,g " by A1, Th26; ::_thesis: verum end; end; :: deftheorem defines are_equivalent CIRCTRM1:def_10_:_ for S1, S2 being non empty ManySortedSign holds ( S1,S2 are_equivalent iff ex f, g being one-to-one Function st S1,S2 are_equivalent_wrt f,g ); theorem :: CIRCTRM1:29 for S1, S2, S3 being 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 ; ::_thesis: ( S1,S2 are_equivalent & S2,S3 are_equivalent implies S1,S3 are_equivalent ) given f1, g1 being one-to-one Function such that A1: S1,S2 are_equivalent_wrt f1,g1 ; :: according to CIRCTRM1:def_10 ::_thesis: ( not S2,S3 are_equivalent or S1,S3 are_equivalent ) given f2, g2 being one-to-one Function such that A2: S2,S3 are_equivalent_wrt f2,g2 ; :: according to CIRCTRM1:def_10 ::_thesis: S1,S3 are_equivalent take f2 * f1 ; :: according to CIRCTRM1:def_10 ::_thesis: ex g being one-to-one Function st S1,S3 are_equivalent_wrt f2 * f1,g take g2 * g1 ; ::_thesis: S1,S3 are_equivalent_wrt f2 * f1,g2 * g1 thus S1,S3 are_equivalent_wrt f2 * f1,g2 * g1 by A1, A2, Th27; ::_thesis: verum end; definition let S1, S2 be non empty ManySortedSign ; let f be Function; predf preserves_inputs_of S1,S2 means :: CIRCTRM1:def 11 f .: (InputVertices S1) c= InputVertices S2; end; :: deftheorem defines preserves_inputs_of CIRCTRM1:def_11_:_ for S1, S2 being non empty ManySortedSign for f being Function holds ( f preserves_inputs_of S1,S2 iff f .: (InputVertices S1) c= InputVertices S2 ); theorem Th30: :: CIRCTRM1:30 for S1, S2 being non empty ManySortedSign for f, g being Function st f,g form_morphism_between S1,S2 holds for v being Vertex of S1 holds f . v is Vertex of S2 proof let S1, S2 be non empty ManySortedSign ; ::_thesis: for f, g being Function st f,g form_morphism_between S1,S2 holds for v being Vertex of S1 holds f . v is Vertex of S2 let f, g be Function; ::_thesis: ( f,g form_morphism_between S1,S2 implies for v being Vertex of S1 holds f . v is Vertex of S2 ) 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 ; :: according to PUA2MSS1:def_12 ::_thesis: ( not proj2 g c= the carrier' of S2 or not the ResultSort of S1 * f = g * the ResultSort of S2 or ex b1 being set ex b2 being set st ( b1 in the carrier' of S1 & b2 = the Arity of S1 . b1 & not b2 * f = the Arity of S2 . (g . b1) ) or for v being Vertex of S1 holds f . v is Vertex of S2 ) now__::_thesis:_for_v_being_Vertex_of_S1_holds_f_._v_in_the_carrier_of_S2 let v be Vertex of S1; ::_thesis: f . v in the carrier of S2 f . v in rng f by A1, FUNCT_1:def_3; hence f . v in the carrier of S2 by A2; ::_thesis: verum end; hence ( not proj2 g c= the carrier' of S2 or not the ResultSort of S1 * f = g * the ResultSort of S2 or ex b1 being set ex b2 being set st ( b1 in the carrier' of S1 & b2 = the Arity of S1 . b1 & not b2 * f = the Arity of S2 . (g . b1) ) or for v being Vertex of S1 holds f . v is Vertex of S2 ) ; ::_thesis: verum end; theorem Th31: :: CIRCTRM1:31 for S1, S2 being non empty non void ManySortedSign for f, g being Function st f,g form_morphism_between S1,S2 holds for v being Gate of S1 holds g . v is Gate of S2 proof let S1, S2 be non empty non void ManySortedSign ; ::_thesis: for f, g being Function st f,g form_morphism_between S1,S2 holds for v being Gate of S1 holds g . v is Gate of S2 let f, g be Function; ::_thesis: ( f,g form_morphism_between S1,S2 implies for v being Gate of S1 holds g . v is Gate of S2 ) 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 ; :: according to PUA2MSS1:def_12 ::_thesis: ( not the ResultSort of S1 * f = g * the ResultSort of S2 or ex b1 being set ex b2 being set st ( b1 in the carrier' of S1 & b2 = the Arity of S1 . b1 & not b2 * f = the Arity of S2 . (g . b1) ) or for v being Gate of S1 holds g . v is Gate of S2 ) now__::_thesis:_for_v_being_Gate_of_S1_holds_g_._v_in_the_carrier'_of_S2 let v be Gate of S1; ::_thesis: g . v in the carrier' of S2 g . v in rng g by A1, FUNCT_1:def_3; hence g . v in the carrier' of S2 by A2; ::_thesis: verum end; hence ( not the ResultSort of S1 * f = g * the ResultSort of S2 or ex b1 being set ex b2 being set st ( b1 in the carrier' of S1 & b2 = the Arity of S1 . b1 & not b2 * f = the Arity of S2 . (g . b1) ) or for v being Gate of S1 holds g . v is Gate of S2 ) ; ::_thesis: verum end; theorem Th32: :: CIRCTRM1:32 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 proof let S1, S2 be non empty ManySortedSign ; ::_thesis: for f, g being Function st f,g form_morphism_between S1,S2 holds f .: (InnerVertices S1) c= InnerVertices S2 let f, g be Function; ::_thesis: ( f,g form_morphism_between S1,S2 implies f .: (InnerVertices S1) c= InnerVertices S2 ) assume f,g form_morphism_between S1,S2 ; ::_thesis: f .: (InnerVertices S1) c= InnerVertices S2 then f * the ResultSort of S1 = the ResultSort of S2 * g by PUA2MSS1:def_12; then f .: (InnerVertices S1) = rng ( the ResultSort of S2 * g) by RELAT_1:127; hence f .: (InnerVertices S1) c= InnerVertices S2 by RELAT_1:26; ::_thesis: verum end; theorem Th33: :: CIRCTRM1:33 for S1, S2 being non empty non void Circuit-like ManySortedSign for f, g being Function st f,g form_morphism_between S1,S2 holds for v1 being Vertex of S1 st v1 in InnerVertices S1 holds for v2 being Vertex of S2 st v2 = f . v1 holds action_at v2 = g . (action_at v1) proof let S1, S2 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function st f,g form_morphism_between S1,S2 holds for v1 being Vertex of S1 st v1 in InnerVertices S1 holds for v2 being Vertex of S2 st v2 = f . v1 holds action_at v2 = g . (action_at v1) let f, g be Function; ::_thesis: ( f,g form_morphism_between S1,S2 implies for v1 being Vertex of S1 st v1 in InnerVertices S1 holds for v2 being Vertex of S2 st v2 = f . v1 holds action_at v2 = g . (action_at v1) ) assume A1: f,g form_morphism_between S1,S2 ; ::_thesis: for v1 being Vertex of S1 st v1 in InnerVertices S1 holds for v2 being Vertex of S2 st v2 = f . v1 holds action_at v2 = g . (action_at v1) let v1 be Vertex of S1; ::_thesis: ( v1 in InnerVertices S1 implies for v2 being Vertex of S2 st v2 = f . v1 holds action_at v2 = g . (action_at v1) ) assume A2: v1 in InnerVertices S1 ; ::_thesis: for v2 being Vertex of S2 st v2 = f . v1 holds action_at v2 = g . (action_at v1) let v2 be Vertex of S2; ::_thesis: ( v2 = f . v1 implies action_at v2 = g . (action_at v1) ) assume A3: v2 = f . v1 ; ::_thesis: action_at v2 = g . (action_at v1) reconsider g1 = g . (action_at v1) as Gate of S2 by A1, Th31; A4: dom g = the carrier' of S1 by A1, PUA2MSS1:def_12; A5: dom f = the carrier of S1 by A1, PUA2MSS1:def_12; 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, PUA2MSS1:def_12 .= f . (the_result_sort_of (action_at v1)) by A6, FUNCT_1:13 .= v2 by A2, A3, MSAFREE2:def_7 ; hence action_at v2 = g . (action_at v1) by A7, A8, MSAFREE2:def_7; ::_thesis: verum 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; predf,g form_embedding_of C1,C2 means :Def12: :: 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; :: deftheorem Def12 defines form_embedding_of CIRCTRM1:def_12_:_ 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 ( f,g form_embedding_of C1,C2 iff ( 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 ) ); theorem Th34: :: CIRCTRM1:34 for S being non empty ManySortedSign for C being 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 ; ::_thesis: for C being non-empty MSAlgebra over S holds id the carrier of S, id the carrier' of S form_embedding_of C,C let C be non-empty MSAlgebra over S; ::_thesis: id the carrier of S, id the carrier' of S form_embedding_of C,C thus id the carrier of S is one-to-one ; :: according to CIRCTRM1:def_12 ::_thesis: ( id the carrier' of S is one-to-one & id the carrier of S, id the carrier' of S form_morphism_between S,S & the Sorts of C = the Sorts of C * (id the carrier of S) & the Charact of C = the Charact of C * (id the carrier' of S) ) 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 ( id the carrier' of S is one-to-one & id the carrier of S, id the carrier' of S form_morphism_between S,S & the Sorts of C = the Sorts of C * (id the carrier of S) & the Charact of C = the Charact of C * (id the carrier' of S) ) by A1, INSTALG1:8, RELAT_1:52; ::_thesis: verum end; theorem Th35: :: CIRCTRM1:35 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 proof let S1, S2, S3 be non empty ManySortedSign ; ::_thesis: 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 let f1, g1, f2, g2 be Function; ::_thesis: 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 let C1 be non-empty MSAlgebra over S1; ::_thesis: 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 let C2 be non-empty MSAlgebra over S2; ::_thesis: 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 let C3 be non-empty MSAlgebra over S3; ::_thesis: ( f1,g1 form_embedding_of C1,C2 & f2,g2 form_embedding_of C2,C3 implies f2 * f1,g2 * g1 form_embedding_of C1,C3 ) assume 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: the Sorts of C1 = the Sorts of C2 * f1 and A5: the Charact of C1 = the Charact of C2 * g1 and A6: f2 is one-to-one and A7: g2 is one-to-one and A8: f2,g2 form_morphism_between S2,S3 and A9: the Sorts of C2 = the Sorts of C3 * f2 and A10: the Charact of C2 = the Charact of C3 * g2 ; :: according to CIRCTRM1:def_12 ::_thesis: f2 * f1,g2 * g1 form_embedding_of C1,C3 thus ( f2 * f1 is one-to-one & g2 * g1 is one-to-one ) by A1, A2, A6, A7; :: according to CIRCTRM1:def_12 ::_thesis: ( f2 * f1,g2 * g1 form_morphism_between S1,S3 & the Sorts of C1 = the Sorts of C3 * (f2 * f1) & the Charact of C1 = the Charact of C3 * (g2 * g1) ) thus f2 * f1,g2 * g1 form_morphism_between S1,S3 by A3, A8, PUA2MSS1:29; ::_thesis: ( the Sorts of C1 = the Sorts of C3 * (f2 * f1) & the Charact of C1 = the Charact of C3 * (g2 * g1) ) thus ( the Sorts of C1 = the Sorts of C3 * (f2 * f1) & the Charact of C1 = the Charact of C3 * (g2 * g1) ) by A4, A5, A9, A10, RELAT_1:36; ::_thesis: verum 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; predC1,C2 are_similar_wrt f,g means :Def13: :: CIRCTRM1:def 13 ( f,g form_embedding_of C1,C2 & f " ,g " form_embedding_of C2,C1 ); end; :: deftheorem Def13 defines are_similar_wrt CIRCTRM1:def_13_:_ 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 ( f,g form_embedding_of C1,C2 & f " ,g " form_embedding_of C2,C1 ) ); theorem Th36: :: CIRCTRM1:36 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 proof let S1, S2 be non empty ManySortedSign ; ::_thesis: 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 let f, g be Function; ::_thesis: 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 let C1 be non-empty MSAlgebra over S1; ::_thesis: for C2 being non-empty MSAlgebra over S2 st C1,C2 are_similar_wrt f,g holds S1,S2 are_equivalent_wrt f,g let C2 be non-empty MSAlgebra over S2; ::_thesis: ( C1,C2 are_similar_wrt f,g implies S1,S2 are_equivalent_wrt f,g ) 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 ; :: according to CIRCTRM1:def_12,CIRCTRM1:def_13 ::_thesis: ( not the Sorts of C2 = the Sorts of C1 * (f ") or not the Charact of C2 = the Charact of C1 * (g ") or S1,S2 are_equivalent_wrt f,g ) thus ( not the Sorts of C2 = the Sorts of C1 * (f ") or not the Charact of C2 = the Charact of C1 * (g ") or S1,S2 are_equivalent_wrt f,g ) by A1, A2, A3, A4, Def9; ::_thesis: verum end; theorem Th37: :: 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 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 ; ::_thesis: 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 ) ) let f, g be Function; ::_thesis: 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 ) ) let C1 be non-empty MSAlgebra over S1; ::_thesis: 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 ) ) let C2 be non-empty MSAlgebra over S2; ::_thesis: ( 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 ) ) hereby ::_thesis: ( 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 implies C1,C2 are_similar_wrt f,g ) assume A1: C1,C2 are_similar_wrt f,g ; ::_thesis: ( 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 ) hence S1,S2 are_equivalent_wrt f,g by Th36; ::_thesis: ( the Sorts of C1 = the Sorts of C2 * f & the Charact of C1 = the Charact of C2 * g ) f,g form_embedding_of C1,C2 by A1, Def13; hence ( the Sorts of C1 = the Sorts of C2 * f & the Charact of C1 = the Charact of C2 * g ) by Def12; ::_thesis: verum 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 ; :: according to CIRCTRM1:def_9 ::_thesis: C1,C2 are_similar_wrt f,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; :: according to CIRCTRM1:def_12,CIRCTRM1:def_13 ::_thesis: f " ,g " form_embedding_of C2,C1 thus ( f " is one-to-one & g " is one-to-one ) by A2, A3; :: according to CIRCTRM1:def_12 ::_thesis: ( f " ,g " form_morphism_between S2,S1 & the Sorts of C2 = the Sorts of C1 * (f ") & the Charact of C2 = the Charact of C1 * (g ") ) thus f " ,g " form_morphism_between S2,S1 by A5; ::_thesis: ( the Sorts of C2 = the Sorts of C1 * (f ") & the Charact of C2 = the Charact of C1 * (g ") ) dom (f ") = the carrier of S2 by A5, PUA2MSS1:def_12; 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 ; ::_thesis: the Charact of C2 = the Charact of C1 * (g ") dom (g ") = the carrier' of S2 by A5, PUA2MSS1:def_12; 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 ; ::_thesis: verum end; theorem :: CIRCTRM1:38 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 carrier' of S proof let S be non empty ManySortedSign ; ::_thesis: for C being non-empty MSAlgebra over S holds C,C are_similar_wrt id the carrier of S, id the carrier' of S let C be non-empty MSAlgebra over S; ::_thesis: C,C are_similar_wrt id the carrier of S, id the carrier' of S set f = id the carrier of S; set g = id the carrier' of S; A1: (id the carrier of S) " = id the carrier of S by FUNCT_1:45; (id the carrier' of S) " = id the carrier' of S by FUNCT_1:45; hence ( id the carrier of S, id the carrier' of S form_embedding_of C,C & (id the carrier of S) " ,(id the carrier' of S) " form_embedding_of C,C ) by A1, Th34; :: according to CIRCTRM1:def_13 ::_thesis: verum end; theorem Th39: :: CIRCTRM1:39 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 " proof let S1, S2 be non empty ManySortedSign ; ::_thesis: 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 " let f, g be Function; ::_thesis: 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 " let C1 be non-empty MSAlgebra over S1; ::_thesis: for C2 being non-empty MSAlgebra over S2 st C1,C2 are_similar_wrt f,g holds C2,C1 are_similar_wrt f " ,g " let C2 be non-empty MSAlgebra over S2; ::_thesis: ( C1,C2 are_similar_wrt f,g implies C2,C1 are_similar_wrt f " ,g " ) assume that A1: f,g form_embedding_of C1,C2 and A2: f " ,g " form_embedding_of C2,C1 ; :: according to CIRCTRM1:def_13 ::_thesis: C2,C1 are_similar_wrt f " ,g " A3: f is one-to-one by A1, Def12; A4: g is one-to-one by A1, Def12; (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, A4, FUNCT_1:43; :: according to CIRCTRM1:def_13 ::_thesis: verum end; theorem :: CIRCTRM1:40 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 proof let S1, S2, S3 be non empty ManySortedSign ; ::_thesis: 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 let f1, g1, f2, g2 be Function; ::_thesis: 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 let C1 be non-empty MSAlgebra over S1; ::_thesis: 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 let C2 be non-empty MSAlgebra over S2; ::_thesis: 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 let C3 be non-empty MSAlgebra over S3; ::_thesis: ( C1,C2 are_similar_wrt f1,g1 & C2,C3 are_similar_wrt f2,g2 implies C1,C3 are_similar_wrt f2 * f1,g2 * g1 ) 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 ; :: according to CIRCTRM1:def_13 ::_thesis: C1,C3 are_similar_wrt f2 * f1,g2 * g1 thus f2 * f1,g2 * g1 form_embedding_of C1,C3 by A1, A3, Th35; :: according to CIRCTRM1:def_13 ::_thesis: (f2 * f1) " ,(g2 * g1) " form_embedding_of C3,C1 A5: f1 is one-to-one by A1, Def12; A6: g1 is one-to-one by A1, Def12; A7: f2 is one-to-one by A3, Def12; A8: g2 is one-to-one by A3, Def12; A9: (f2 * f1) " = (f1 ") * (f2 ") by A5, A7, FUNCT_1:44; (g2 * g1) " = (g1 ") * (g2 ") by A6, A8, FUNCT_1:44; hence (f2 * f1) " ,(g2 * g1) " form_embedding_of C3,C1 by A2, A4, A9, Th35; ::_thesis: verum 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; predC1,C2 are_similar means :: CIRCTRM1:def 14 ex f, g being Function st C1,C2 are_similar_wrt f,g; end; :: deftheorem defines are_similar CIRCTRM1:def_14_:_ for S1, S2 being non empty ManySortedSign for C1 being non-empty MSAlgebra over S1 for C2 being non-empty MSAlgebra over S2 holds ( C1,C2 are_similar iff ex f, g being Function st C1,C2 are_similar_wrt f,g ); theorem Th41: :: CIRCTRM1:41 for G1, G2 being non empty non void Circuit-like ManySortedSign for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds ( 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 let G1, G2 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds ( 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 ) let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds ( 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 ) let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds ( 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 ) let C2 be non-empty Circuit of G2; ::_thesis: ( 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 ) ) 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 ; :: according to PUA2MSS1:def_12,CIRCTRM1:def_12 ::_thesis: ( not the ResultSort of G1 * f = g * the ResultSort of G2 or ex b1 being set ex b2 being set st ( b1 in the carrier' of G1 & b2 = the Arity of G1 . b1 & not b2 * f = the Arity of G2 . (g . b1) ) or not the Sorts of C1 = the Sorts of C2 * f or not the Charact of C1 = the Charact of C2 * g or ( 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 ) ) thus ( not the ResultSort of G1 * f = g * the ResultSort of G2 or ex b1 being set ex b2 being set st ( b1 in the carrier' of G1 & b2 = the Arity of G1 . b1 & not b2 * f = the Arity of G2 . (g . b1) ) or not the Sorts of C1 = the Sorts of C2 * f or not the Charact of C1 = the Charact of C2 * g or ( 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 ) ) by A1, A2, A3, A4; ::_thesis: verum end; theorem Th42: :: CIRCTRM1:42 for G1, G2 being non empty non void Circuit-like ManySortedSign for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds for o1 being Gate of G1 for o2 being Gate of G2 st o2 = g . o1 holds Den (o2,C2) = Den (o1,C1) proof let G1, G2 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds for o1 being Gate of G1 for o2 being Gate of G2 st o2 = g . o1 holds Den (o2,C2) = Den (o1,C1) let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds for o1 being Gate of G1 for o2 being Gate of G2 st o2 = g . o1 holds Den (o2,C2) = Den (o1,C1) let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds for o1 being Gate of G1 for o2 being Gate of G2 st o2 = g . o1 holds Den (o2,C2) = Den (o1,C1) let C2 be non-empty Circuit of G2; ::_thesis: ( f,g form_embedding_of C1,C2 implies for o1 being Gate of G1 for o2 being Gate of G2 st o2 = g . o1 holds Den (o2,C2) = Den (o1,C1) ) 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 ; :: according to CIRCTRM1:def_12 ::_thesis: for o1 being Gate of G1 for o2 being Gate of G2 st o2 = g . o1 holds Den (o2,C2) = Den (o1,C1) let o1 be Gate of G1; ::_thesis: for o2 being Gate of G2 st o2 = g . o1 holds Den (o2,C2) = Den (o1,C1) let o2 be Gate of G2; ::_thesis: ( o2 = g . o1 implies Den (o2,C2) = Den (o1,C1) ) assume A3: o2 = g . o1 ; ::_thesis: Den (o2,C2) = Den (o1,C1) dom g = the carrier' of G1 by A1, PUA2MSS1:def_12; hence Den (o2,C2) = Den (o1,C1) by A2, A3, FUNCT_1:13; ::_thesis: verum end; theorem Th43: :: CIRCTRM1:43 for G1, G2 being non empty non void Circuit-like ManySortedSign for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds for o1 being Gate of G1 for o2 being Gate of G2 st o2 = g . o1 holds for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds o2 depends_on_in s2 = o1 depends_on_in s1 proof let G1, G2 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds for o1 being Gate of G1 for o2 being Gate of G2 st o2 = g . o1 holds for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds o2 depends_on_in s2 = o1 depends_on_in s1 let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds for o1 being Gate of G1 for o2 being Gate of G2 st o2 = g . o1 holds for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds o2 depends_on_in s2 = o1 depends_on_in s1 let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds for o1 being Gate of G1 for o2 being Gate of G2 st o2 = g . o1 holds for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds o2 depends_on_in s2 = o1 depends_on_in s1 let C2 be non-empty Circuit of G2; ::_thesis: ( f,g form_embedding_of C1,C2 implies for o1 being Gate of G1 for o2 being Gate of G2 st o2 = g . o1 holds for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds o2 depends_on_in s2 = o1 depends_on_in s1 ) 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 ; :: according to CIRCTRM1:def_12 ::_thesis: for o1 being Gate of G1 for o2 being Gate of G2 st o2 = g . o1 holds for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds o2 depends_on_in s2 = o1 depends_on_in s1 let o1 be Gate of G1; ::_thesis: for o2 being Gate of G2 st o2 = g . o1 holds for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds o2 depends_on_in s2 = o1 depends_on_in s1 let o2 be Gate of G2; ::_thesis: ( o2 = g . o1 implies for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds o2 depends_on_in s2 = o1 depends_on_in s1 ) assume A2: o2 = g . o1 ; ::_thesis: for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds o2 depends_on_in s2 = o1 depends_on_in s1 let s1 be State of C1; ::_thesis: for s2 being State of C2 st s1 = s2 * f holds o2 depends_on_in s2 = o1 depends_on_in s1 let s2 be State of C2; ::_thesis: ( s1 = s2 * f implies o2 depends_on_in s2 = o1 depends_on_in s1 ) assume A3: s1 = s2 * f ; ::_thesis: o2 depends_on_in s2 = o1 depends_on_in s1 thus o2 depends_on_in s2 = s2 * (the_arity_of o2) by CIRCUIT1:def_3 .= s2 * (f * (the_arity_of o1)) by A1, A2, PUA2MSS1:def_12 .= s1 * (the_arity_of o1) by A3, RELAT_1:36 .= o1 depends_on_in s1 by CIRCUIT1:def_3 ; ::_thesis: verum end; theorem Th44: :: CIRCTRM1:44 for G1, G2 being non empty non void Circuit-like ManySortedSign for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds for s being State of C2 holds s * f is State of C1 proof let G1, G2 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds for s being State of C2 holds s * f is State of C1 let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds for s being State of C2 holds s * f is State of C1 let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds for s being State of C2 holds s * f is State of C1 let C2 be non-empty Circuit of G2; ::_thesis: ( f,g form_embedding_of C1,C2 implies for s being State of C2 holds s * f is State of C1 ) set S1 = G1; set S2 = G2; assume that f is one-to-one and g is one-to-one and A1: f,g form_morphism_between G1,G2 and A2: the Sorts of C1 = the Sorts of C2 * f and the Charact of C1 = the Charact of C2 * g ; :: according to CIRCTRM1:def_12 ::_thesis: for s being State of C2 holds s * f is State of C1 let s be State of C2; ::_thesis: s * f is State of C1 A3: dom the Sorts of C2 = the carrier of G2 by PARTFUN1:def_2; A4: dom the Sorts of C1 = the carrier of G1 by PARTFUN1:def_2; A5: dom s = dom the Sorts of C2 by CARD_3:9; A6: rng f c= the carrier of G2 by A1, PUA2MSS1:def_12; A7: dom f = the carrier of G1 by A1, PUA2MSS1:def_12; then A8: dom (s * f) = the carrier of G1 by A3, A5, A6, RELAT_1:27; now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_G1_holds_ (s_*_f)_._x_in_the_Sorts_of_C1_._x let x be set ; ::_thesis: ( x in the carrier of G1 implies (s * f) . x in the Sorts of C1 . x ) assume A9: x in the carrier of G1 ; ::_thesis: (s * f) . x in the Sorts of C1 . x 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; ::_thesis: verum end; hence s * f is State of C1 by A4, A8, CARD_3:9; ::_thesis: verum end; theorem Th45: :: CIRCTRM1:45 for G2, G1 being non empty non void Circuit-like ManySortedSign for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds for s2 being State of C2 for 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 proof let G2, G1 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds for s2 being State of C2 for 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 let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds for s2 being State of C2 for 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 let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 holds for s2 being State of C2 for 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 let C2 be non-empty Circuit of G2; ::_thesis: ( f,g form_embedding_of C1,C2 implies for s2 being State of C2 for 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 ) assume A1: f,g form_embedding_of C1,C2 ; ::_thesis: for s2 being State of C2 for 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 then A2: f,g form_morphism_between G1,G2 by Def12; let s2 be State of C2; ::_thesis: for 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 let s1 be State of C1; ::_thesis: ( s1 = s2 * f & ( for v being Vertex of G1 st v in InputVertices G1 holds s2 is_stable_at f . v ) implies Following s1 = (Following s2) * f ) assume that A3: s1 = s2 * f and A4: for v being Vertex of G1 st v in InputVertices G1 holds s2 is_stable_at f . v ; ::_thesis: Following s1 = (Following s2) * f reconsider s29 = (Following s2) * f as State of C1 by A1, Th44; A5: dom f = the carrier of G1 by A2, PUA2MSS1:def_12; now__::_thesis:_for_v_being_Vertex_of_G1_holds_ (_(_v_in_InputVertices_G1_implies_s29_._v_=_s1_._v_)_&_(_v_in_InnerVertices_G1_implies_s29_._v_=_(Den_((action_at_v),C1))_._((action_at_v)_depends_on_in_s1)_)_) let v be Vertex of G1; ::_thesis: ( ( v in InputVertices G1 implies s29 . v = s1 . v ) & ( v in InnerVertices G1 implies s29 . v = (Den ((action_at v),C1)) . ((action_at v) depends_on_in s1) ) ) A6: s29 . v = (Following s2) . (f . v) by A5, FUNCT_1:13; reconsider fv = f . v as Vertex of G2 by A2, Th30; hereby ::_thesis: ( v in InnerVertices G1 implies s29 . v = (Den ((action_at v),C1)) . ((action_at v) depends_on_in s1) ) assume v in InputVertices G1 ; ::_thesis: s29 . v = s1 . v 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, FACIRC_1:def_9 .= s1 . v by A3, A5, FUNCT_1:13 ; ::_thesis: verum end; A8: f .: (InnerVertices G1) c= InnerVertices G2 by A2, Th32; assume A9: v in InnerVertices G1 ; ::_thesis: s29 . v = (Den ((action_at v),C1)) . ((action_at v) depends_on_in s1) 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 ; ::_thesis: verum end; hence Following s1 = (Following s2) * f by CIRCUIT2:def_5; ::_thesis: verum end; theorem Th46: :: CIRCTRM1:46 for G1, G2 being non empty non void Circuit-like ManySortedSign for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds for s2 being State of C2 for s1 being State of C1 st s1 = s2 * f holds Following s1 = (Following s2) * f proof let G1, G2 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds for s2 being State of C2 for s1 being State of C1 st s1 = s2 * f holds Following s1 = (Following s2) * f let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds for s2 being State of C2 for s1 being State of C1 st s1 = s2 * f holds Following s1 = (Following s2) * f let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds for s2 being State of C2 for s1 being State of C1 st s1 = s2 * f holds Following s1 = (Following s2) * f let C2 be non-empty Circuit of G2; ::_thesis: ( f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 implies for s2 being State of C2 for s1 being State of C1 st s1 = s2 * f holds Following s1 = (Following s2) * f ) assume that A1: f,g form_embedding_of C1,C2 and A2: f .: (InputVertices G1) c= InputVertices G2 ; :: according to CIRCTRM1:def_11 ::_thesis: for s2 being State of C2 for s1 being State of C1 st s1 = s2 * f holds Following s1 = (Following s2) * f let s2 be State of C2; ::_thesis: for s1 being State of C1 st s1 = s2 * f holds Following s1 = (Following s2) * f let s1 be State of C1; ::_thesis: ( s1 = s2 * f implies Following s1 = (Following s2) * f ) assume A3: s1 = s2 * f ; ::_thesis: Following s1 = (Following s2) * f A4: dom f = the carrier of G1 by A1, Th41; now__::_thesis:_for_v_being_Vertex_of_G1_st_v_in_InputVertices_G1_holds_ s2_is_stable_at_f_._v let v be Vertex of G1; ::_thesis: ( v in InputVertices G1 implies s2 is_stable_at f . v ) assume v in InputVertices G1 ; ::_thesis: s2 is_stable_at f . v 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; ::_thesis: verum end; hence Following s1 = (Following s2) * f by A1, A3, Th45; ::_thesis: verum end; theorem Th47: :: CIRCTRM1:47 for G1, G2 being non empty non void Circuit-like ManySortedSign for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds for s2 being State of C2 for s1 being State of C1 st s1 = s2 * f holds for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f proof let G1, G2 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds for s2 being State of C2 for s1 being State of C1 st s1 = s2 * f holds for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds for s2 being State of C2 for s1 being State of C1 st s1 = s2 * f holds for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds for s2 being State of C2 for s1 being State of C1 st s1 = s2 * f holds for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f let C2 be non-empty Circuit of G2; ::_thesis: ( f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 implies for s2 being State of C2 for s1 being State of C1 st s1 = s2 * f holds for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f ) assume that A1: f,g form_embedding_of C1,C2 and A2: f preserves_inputs_of G1,G2 ; ::_thesis: for s2 being State of C2 for s1 being State of C1 st s1 = s2 * f holds for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f let s2 be State of C2; ::_thesis: for s1 being State of C1 st s1 = s2 * f holds for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f let s1 be State of C1; ::_thesis: ( s1 = s2 * f implies for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f ) assume A3: s1 = s2 * f ; ::_thesis: for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f defpred S1[ Element of NAT ] means Following (s1,\$1) = (Following (s2,\$1)) * f; Following (s1,0) = s1 by FACIRC_1:11; then A4: S1[ 0 ] by A3, FACIRC_1:11; A5: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_ S1[n_+_1] let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume S1[n] ; ::_thesis: S1[n + 1] 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 S1[n + 1] ; ::_thesis: verum end; thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A5); ::_thesis: verum end; theorem :: CIRCTRM1:48 for G1, G2 being non empty non void Circuit-like ManySortedSign for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds for s2 being State of C2 for s1 being State of C1 st s1 = s2 * f & s2 is stable holds s1 is stable proof let G1, G2 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds for s2 being State of C2 for s1 being State of C1 st s1 = s2 * f & s2 is stable holds s1 is stable let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds for s2 being State of C2 for s1 being State of C1 st s1 = s2 * f & s2 is stable holds s1 is stable let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds for s2 being State of C2 for s1 being State of C1 st s1 = s2 * f & s2 is stable holds s1 is stable let C2 be non-empty Circuit of G2; ::_thesis: ( f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 implies for s2 being State of C2 for s1 being State of C1 st s1 = s2 * f & s2 is stable holds s1 is stable ) assume that A1: f,g form_embedding_of C1,C2 and A2: f preserves_inputs_of G1,G2 ; ::_thesis: for s2 being State of C2 for s1 being State of C1 st s1 = s2 * f & s2 is stable holds s1 is stable let s2 be State of C2; ::_thesis: for s1 being State of C1 st s1 = s2 * f & s2 is stable holds s1 is stable let s1 be State of C1; ::_thesis: ( s1 = s2 * f & s2 is stable implies s1 is stable ) assume A3: s1 = s2 * f ; ::_thesis: ( not s2 is stable or s1 is stable ) assume s2 = Following s2 ; :: according to CIRCUIT2:def_6 ::_thesis: s1 is stable hence s1 = Following s1 by A1, A2, A3, Th46; :: according to CIRCUIT2:def_6 ::_thesis: verum end; theorem Th49: :: CIRCTRM1:49 for G1, G2 being non empty non void Circuit-like ManySortedSign for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds for s2 being State of C2 for s1 being State of C1 st s1 = s2 * f holds for v1 being Vertex of G1 holds ( s1 is_stable_at v1 iff s2 is_stable_at f . v1 ) proof let G1, G2 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds for s2 being State of C2 for s1 being State of C1 st s1 = s2 * f holds for v1 being Vertex of G1 holds ( s1 is_stable_at v1 iff s2 is_stable_at f . v1 ) let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds for s2 being State of C2 for s1 being State of C1 st s1 = s2 * f holds for v1 being Vertex of G1 holds ( s1 is_stable_at v1 iff s2 is_stable_at f . v1 ) let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds for s2 being State of C2 for s1 being State of C1 st s1 = s2 * f holds for v1 being Vertex of G1 holds ( s1 is_stable_at v1 iff s2 is_stable_at f . v1 ) let C2 be non-empty Circuit of G2; ::_thesis: ( f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 implies for s2 being State of C2 for s1 being State of C1 st s1 = s2 * f holds for v1 being Vertex of G1 holds ( s1 is_stable_at v1 iff s2 is_stable_at f . v1 ) ) assume that A1: f,g form_embedding_of C1,C2 and A2: f preserves_inputs_of G1,G2 ; ::_thesis: for s2 being State of C2 for s1 being State of C1 st s1 = s2 * f holds for v1 being Vertex of G1 holds ( s1 is_stable_at v1 iff s2 is_stable_at f . v1 ) let s2 be State of C2; ::_thesis: for s1 being State of C1 st s1 = s2 * f holds for v1 being Vertex of G1 holds ( s1 is_stable_at v1 iff s2 is_stable_at f . v1 ) let s1 be State of C1; ::_thesis: ( s1 = s2 * f implies for v1 being Vertex of G1 holds ( s1 is_stable_at v1 iff s2 is_stable_at f . v1 ) ) assume A3: s1 = s2 * f ; ::_thesis: for v1 being Vertex of G1 holds ( s1 is_stable_at v1 iff s2 is_stable_at f . v1 ) let v1 be Vertex of G1; ::_thesis: ( s1 is_stable_at v1 iff s2 is_stable_at f . v1 ) A4: f,g form_morphism_between G1,G2 by A1, Def12; then A5: dom f = the carrier of G1 by PUA2MSS1:def_12; reconsider v2 = f . v1 as Vertex of G2 by A4, Th30; thus ( s1 is_stable_at v1 implies s2 is_stable_at f . v1 ) ::_thesis: ( s2 is_stable_at f . v1 implies s1 is_stable_at v1 ) proof assume A6: for n being Nat holds (Following (s1,n)) . v1 = s1 . v1 ; :: according to FACIRC_1:def_9 ::_thesis: s2 is_stable_at f . v1 let n be Nat; :: according to FACIRC_1:def_9 ::_thesis: (Following (s2,n)) . (f . v1) = s2 . (f . v1) n in NAT by ORDINAL1:def_12; then 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 ; ::_thesis: verum end; assume A7: for n being Nat holds (Following (s2,n)) . (f . v1) = s2 . (f . v1) ; :: according to FACIRC_1:def_9 ::_thesis: s1 is_stable_at v1 let n be Nat; :: according to FACIRC_1:def_9 ::_thesis: (Following (s1,n)) . v1 = s1 . v1 n in NAT by ORDINAL1:def_12; then 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 ; ::_thesis: verum end; theorem :: CIRCTRM1:50 for G1, G2 being non empty non void Circuit-like ManySortedSign for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds for s being State of C2 holds s * f is State of C1 proof let G1, G2 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds for s being State of C2 holds s * f is State of C1 let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds for s being State of C2 holds s * f is State of C1 let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds for s being State of C2 holds s * f is State of C1 let C2 be non-empty Circuit of G2; ::_thesis: ( C1,C2 are_similar_wrt f,g implies for s being State of C2 holds s * f is State of C1 ) assume f,g form_embedding_of C1,C2 ; :: according to CIRCTRM1:def_13 ::_thesis: ( not f " ,g " form_embedding_of C2,C1 or for s being State of C2 holds s * f is State of C1 ) hence ( not f " ,g " form_embedding_of C2,C1 or for s being State of C2 holds s * f is State of C1 ) by Th44; ::_thesis: verum end; theorem Th51: :: CIRCTRM1:51 for G1, G2 being non empty non void Circuit-like ManySortedSign for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds for s1 being State of C1 for s2 being State of C2 holds ( s1 = s2 * f iff s2 = s1 * (f ") ) proof let G1, G2 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds for s1 being State of C1 for s2 being State of C2 holds ( s1 = s2 * f iff s2 = s1 * (f ") ) let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds for s1 being State of C1 for s2 being State of C2 holds ( s1 = s2 * f iff s2 = s1 * (f ") ) let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds for s1 being State of C1 for s2 being State of C2 holds ( s1 = s2 * f iff s2 = s1 * (f ") ) let C2 be non-empty Circuit of G2; ::_thesis: ( C1,C2 are_similar_wrt f,g implies for s1 being State of C1 for s2 being State of C2 holds ( s1 = s2 * f iff s2 = s1 * (f ") ) ) assume that A1: f,g form_embedding_of C1,C2 and A2: f " ,g " form_embedding_of C2,C1 ; :: according to CIRCTRM1:def_13 ::_thesis: for s1 being State of C1 for s2 being State of C2 holds ( s1 = s2 * f iff s2 = s1 * (f ") ) A3: f is one-to-one by A1, Def12; let s1 be State of C1; ::_thesis: for s2 being State of C2 holds ( s1 = s2 * f iff s2 = s1 * (f ") ) let s2 be State of C2; ::_thesis: ( s1 = s2 * f iff s2 = s1 * (f ") ) f,g form_morphism_between G1,G2 by A1, Def12; then A4: dom f = the carrier of G1 by PUA2MSS1:def_12; 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, Def12; then A7: dom (f ") = the carrier of G2 by PUA2MSS1:def_12; 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 ( s1 = s2 * f iff s2 = s1 * (f ") ) by A6, A7, A8, RELAT_1:52; ::_thesis: verum end; theorem Th52: :: CIRCTRM1:52 for G1, G2 being non empty non void Circuit-like ManySortedSign for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds ( f .: (InputVertices G1) = InputVertices G2 & f .: (InnerVertices G1) = InnerVertices G2 ) proof let G1, G2 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds ( f .: (InputVertices G1) = InputVertices G2 & f .: (InnerVertices G1) = InnerVertices G2 ) let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds ( f .: (InputVertices G1) = InputVertices G2 & f .: (InnerVertices G1) = InnerVertices G2 ) let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds ( f .: (InputVertices G1) = InputVertices G2 & f .: (InnerVertices G1) = InnerVertices G2 ) let C2 be non-empty Circuit of G2; ::_thesis: ( C1,C2 are_similar_wrt f,g implies ( f .: (InputVertices G1) = InputVertices G2 & f .: (InnerVertices G1) = InnerVertices G2 ) ) assume C1,C2 are_similar_wrt f,g ; ::_thesis: ( f .: (InputVertices G1) = InputVertices G2 & f .: (InnerVertices G1) = InnerVertices G2 ) then G1,G2 are_equivalent_wrt f,g by Th36; hence ( f .: (InputVertices G1) = InputVertices G2 & f .: (InnerVertices G1) = InnerVertices G2 ) by Th28; ::_thesis: verum end; theorem Th53: :: CIRCTRM1:53 for G1, G2 being non empty non void Circuit-like ManySortedSign for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds f preserves_inputs_of G1,G2 proof let G1, G2 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds f preserves_inputs_of G1,G2 let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds f preserves_inputs_of G1,G2 let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds f preserves_inputs_of G1,G2 let C2 be non-empty Circuit of G2; ::_thesis: ( C1,C2 are_similar_wrt f,g implies f preserves_inputs_of G1,G2 ) assume C1,C2 are_similar_wrt f,g ; ::_thesis: f preserves_inputs_of G1,G2 hence f .: (InputVertices G1) c= InputVertices G2 by Th52; :: according to CIRCTRM1:def_11 ::_thesis: verum end; theorem Th54: :: CIRCTRM1:54 for G1, G2 being non empty non void Circuit-like ManySortedSign for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds Following s1 = (Following s2) * f proof let G1, G2 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds Following s1 = (Following s2) * f let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds Following s1 = (Following s2) * f let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds Following s1 = (Following s2) * f let C2 be non-empty Circuit of G2; ::_thesis: ( C1,C2 are_similar_wrt f,g implies for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds Following s1 = (Following s2) * f ) assume A1: C1,C2 are_similar_wrt f,g ; ::_thesis: for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds Following s1 = (Following s2) * f then f,g form_embedding_of C1,C2 by Def13; hence for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds Following s1 = (Following s2) * f by A1, Th46, Th53; ::_thesis: verum end; theorem Th55: :: CIRCTRM1:55 for G1, G2 being non empty non void Circuit-like ManySortedSign for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f proof let G1, G2 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f let C2 be non-empty Circuit of G2; ::_thesis: ( C1,C2 are_similar_wrt f,g implies for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f ) assume A1: C1,C2 are_similar_wrt f,g ; ::_thesis: for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f then f,g form_embedding_of C1,C2 by Def13; hence for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds for n being Element of NAT holds Following (s1,n) = (Following (s2,n)) * f by A1, Th47, Th53; ::_thesis: verum end; theorem :: CIRCTRM1:56 for G1, G2 being non empty non void Circuit-like ManySortedSign for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds ( s1 is stable iff s2 is stable ) proof let G1, G2 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds ( s1 is stable iff s2 is stable ) let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds ( s1 is stable iff s2 is stable ) let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds ( s1 is stable iff s2 is stable ) let C2 be non-empty Circuit of G2; ::_thesis: ( C1,C2 are_similar_wrt f,g implies for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds ( s1 is stable iff s2 is stable ) ) assume A1: C1,C2 are_similar_wrt f,g ; ::_thesis: for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds ( s1 is stable iff s2 is stable ) then A2: C2,C1 are_similar_wrt f " ,g " by Th39; let s1 be State of C1; ::_thesis: for s2 being State of C2 st s1 = s2 * f holds ( s1 is stable iff s2 is stable ) let s2 be State of C2; ::_thesis: ( s1 = s2 * f implies ( s1 is stable iff s2 is stable ) ) assume A3: s1 = s2 * f ; ::_thesis: ( s1 is stable iff s2 is stable ) A4: s2 = s1 * (f ") by A1, A3, Th51; thus ( s1 is stable implies s2 is stable ) ::_thesis: ( s2 is stable implies s1 is stable ) proof assume s1 = Following s1 ; :: according to CIRCUIT2:def_6 ::_thesis: s2 is stable hence s2 = Following s2 by A2, A4, Th54; :: according to CIRCUIT2:def_6 ::_thesis: verum end; assume s2 = Following s2 ; :: according to CIRCUIT2:def_6 ::_thesis: s1 is stable hence s1 = Following s1 by A1, A3, Th54; :: according to CIRCUIT2:def_6 ::_thesis: verum end; theorem :: CIRCTRM1:57 for G2, G1 being non empty non void Circuit-like ManySortedSign for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds for v1 being Vertex of G1 holds ( s1 is_stable_at v1 iff s2 is_stable_at f . v1 ) proof let G2, G1 be non empty non void Circuit-like ManySortedSign ; ::_thesis: for f, g being Function for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds for v1 being Vertex of G1 holds ( s1 is_stable_at v1 iff s2 is_stable_at f . v1 ) let f, g be Function; ::_thesis: for C1 being non-empty Circuit of G1 for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds for v1 being Vertex of G1 holds ( s1 is_stable_at v1 iff s2 is_stable_at f . v1 ) let C1 be non-empty Circuit of G1; ::_thesis: for C2 being non-empty Circuit of G2 st C1,C2 are_similar_wrt f,g holds for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds for v1 being Vertex of G1 holds ( s1 is_stable_at v1 iff s2 is_stable_at f . v1 ) let C2 be non-empty Circuit of G2; ::_thesis: ( C1,C2 are_similar_wrt f,g implies for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds for v1 being Vertex of G1 holds ( s1 is_stable_at v1 iff s2 is_stable_at f . v1 ) ) assume A1: C1,C2 are_similar_wrt f,g ; ::_thesis: for s1 being State of C1 for s2 being State of C2 st s1 = s2 * f holds for v1 being Vertex of G1 holds ( s1 is_stable_at v1 iff s2 is_stable_at f . v1 ) then A2: C2,C1 are_similar_wrt f " ,g " by Th39; let s1 be State of C1; ::_thesis: for s2 being State of C2 st s1 = s2 * f holds for v1 being Vertex of G1 holds ( s1 is_stable_at v1 iff s2 is_stable_at f . v1 ) let s2 be State of C2; ::_thesis: ( s1 = s2 * f implies for v1 being Vertex of G1 holds ( s1 is_stable_at v1 iff s2 is_stable_at f . v1 ) ) assume A3: s1 = s2 * f ; ::_thesis: for v1 being Vertex of G1 holds ( s1 is_stable_at v1 iff s2 is_stable_at f . v1 ) let v1 be Vertex of G1; ::_thesis: ( s1 is_stable_at v1 iff s2 is_stable_at f . v1 ) A4: G1,G2 are_equivalent_wrt f,g by A1, Th37; then A5: f,g form_morphism_between G1,G2 by Def9; A6: f " ,g " form_morphism_between G2,G1 by A4, Def9; A7: dom f = the carrier of G1 by A5, PUA2MSS1:def_12; A8: dom (f ") = the carrier of G2 by A6, PUA2MSS1:def_12; reconsider v2 = f . v1 as Vertex of G2 by A5, Th30; f is one-to-one by A4, Def9; then A9: v1 = (f ") . v2 by A7, FUNCT_1:34; thus ( s1 is_stable_at v1 implies s2 is_stable_at f . v1 ) ::_thesis: ( s2 is_stable_at f . v1 implies s1 is_stable_at v1 ) proof assume A10: for n being Nat holds (Following (s1,n)) . v1 = s1 . v1 ; :: according to FACIRC_1:def_9 ::_thesis: s2 is_stable_at f . v1 let n be Nat; :: according to FACIRC_1:def_9 ::_thesis: (Following (s2,n)) . (f . v1) = s2 . (f . v1) 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 ; ::_thesis: verum end; assume A11: for n being Nat holds (Following (s2,n)) . (f . v1) = s2 . (f . v1) ; :: according to FACIRC_1:def_9 ::_thesis: s1 is_stable_at v1 let n be Nat; :: according to FACIRC_1:def_9 ::_thesis: (Following (s1,n)) . v1 = s1 . v1 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 ; ::_thesis: verum end; begin definition let S be non empty non void ManySortedSign ; let A be non-empty MSAlgebra over S; let V be V2() ManySortedSet of the carrier of S; let X be non empty Subset of (S -Terms V); let G be non empty non void Circuit-like ManySortedSign ; let C be non-empty Circuit of G; predC calculates X,A means :Def15: :: CIRCTRM1:def 15 ex f, g being Function st ( f,g form_embedding_of X -Circuit A,C & f preserves_inputs_of X -CircuitStr ,G ); predX,A specifies C means :: CIRCTRM1:def 16 C,X -Circuit A are_similar ; end; :: deftheorem Def15 defines calculates CIRCTRM1:def_15_:_ for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for V being V2() ManySortedSet of the carrier of S for X being non empty Subset of (S -Terms V) for G being non empty non void Circuit-like ManySortedSign for C being non-empty Circuit of G holds ( C calculates X,A iff ex f, g being Function st ( f,g form_embedding_of X -Circuit A,C & f preserves_inputs_of X -CircuitStr ,G ) ); :: deftheorem defines specifies CIRCTRM1:def_16_:_ for S being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for V being V2() ManySortedSet of the carrier of S for X being non empty Subset of (S -Terms V) for G being non empty non void Circuit-like ManySortedSign for C being non-empty Circuit of G holds ( X,A specifies C iff C,X -Circuit A are_similar ); definition let S be non empty non void ManySortedSign ; let V be V2() 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 non empty non void Circuit-like ManySortedSign ; let C be non-empty Circuit of G; assume C calculates X,A ; then consider f, g being Function such that A1: f,g form_embedding_of X -Circuit A,C and A2: f preserves_inputs_of X -CircuitStr ,G by Def15; A3: f is one-to-one by A1, Def12; mode SortMap of X,A,C -> one-to-one Function means :Def17: :: CIRCTRM1:def 17 ( it preserves_inputs_of X -CircuitStr ,G & ex g being Function st it,g form_embedding_of X -Circuit A,C ); existence ex b1 being one-to-one Function st ( b1 preserves_inputs_of X -CircuitStr ,G & ex g being Function st b1,g form_embedding_of X -Circuit A,C ) by A1, A2, A3; end; :: deftheorem Def17 defines SortMap CIRCTRM1:def_17_:_ for S being non empty non void ManySortedSign for V being V2() ManySortedSet of the carrier of S for A being non-empty MSAlgebra over S for X being non empty Subset of (S -Terms V) for G being non empty non void Circuit-like ManySortedSign for C being non-empty Circuit of G st C calculates X,A holds for b7 being one-to-one Function holds ( b7 is SortMap of X,A,C iff ( b7 preserves_inputs_of X -CircuitStr ,G & ex g being Function st b7,g form_embedding_of X -Circuit A,C ) ); definition let S be non empty non void ManySortedSign ; let V be V2() 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 non empty non void Circuit-like ManySortedSign ; let C be non-empty Circuit of G; assume B1: C calculates X,A ; let f be SortMap of X,A,C; consider g being Function such that A1: f,g form_embedding_of X -Circuit A,C by B1, Def17; A2: g is one-to-one by A1, Def12; mode OperMap of X,A,C,f -> one-to-one Function means :: CIRCTRM1:def 18 f,it form_embedding_of X -Circuit A,C; existence ex b1 being one-to-one Function st f,b1 form_embedding_of X -Circuit A,C by A1, A2; end; :: deftheorem defines OperMap CIRCTRM1:def_18_:_ for S being non empty non void ManySortedSign for V being V2() ManySortedSet of the carrier of S for A being non-empty MSAlgebra over S for X being non empty Subset of (S -Terms V) for G being non empty non void Circuit-like ManySortedSign for C being non-empty Circuit of G st C calculates X,A holds for f being SortMap of X,A,C for b8 being one-to-one Function holds ( b8 is OperMap of X,A,C,f iff f,b8 form_embedding_of X -Circuit A,C ); theorem Th58: :: CIRCTRM1:58 for S being non empty non void ManySortedSign for A being non-empty finite-yielding MSAlgebra over S for V being Variables of A for X being SetWithCompoundTerm of S,V for G being non empty non void Circuit-like ManySortedSign for C being non-empty Circuit of G st X,A specifies C holds C calculates X,A proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty finite-yielding MSAlgebra over S for V being Variables of A for X being SetWithCompoundTerm of S,V for G being non empty non void Circuit-like ManySortedSign for C being non-empty Circuit of G st X,A specifies C holds C calculates X,A let A be non-empty finite-yielding MSAlgebra over S; ::_thesis: for V being Variables of A for X being SetWithCompoundTerm of S,V for G being non empty non void Circuit-like ManySortedSign for C being non-empty Circuit of G st X,A specifies C holds C calculates X,A let V be Variables of A; ::_thesis: for X being SetWithCompoundTerm of S,V for G being non empty non void Circuit-like ManySortedSign for C being non-empty Circuit of G st X,A specifies C holds C calculates X,A let X be SetWithCompoundTerm of S,V; ::_thesis: for G being non empty non void Circuit-like ManySortedSign for C being non-empty Circuit of G st X,A specifies C holds C calculates X,A let G be non empty non void Circuit-like ManySortedSign ; ::_thesis: for C being non-empty Circuit of G st X,A specifies C holds C calculates X,A let C be non-empty Circuit of G; ::_thesis: ( X,A specifies C implies C calculates X,A ) given f, g being Function such that A1: C,X -Circuit A are_similar_wrt f,g ; :: according to CIRCTRM1:def_14,CIRCTRM1:def_16 ::_thesis: C calculates X,A take f " ; :: according to CIRCTRM1:def_15 ::_thesis: ex g being Function st ( f " ,g form_embedding_of X -Circuit A,C & f " preserves_inputs_of X -CircuitStr ,G ) take g " ; ::_thesis: ( f " ,g " form_embedding_of X -Circuit A,C & f " preserves_inputs_of X -CircuitStr ,G ) thus f " ,g " form_embedding_of X -Circuit A,C by A1, Def13; ::_thesis: f " preserves_inputs_of X -CircuitStr ,G X -Circuit A,C are_similar_wrt f " ,g " by A1, Th39; hence f " preserves_inputs_of X -CircuitStr ,G by Th53; ::_thesis: verum end; theorem Th59: :: CIRCTRM1:59 for S being non empty non void ManySortedSign for A being non-empty finite-yielding MSAlgebra over S for V being Variables of A for X being SetWithCompoundTerm of S,V for G being non empty non void Circuit-like ManySortedSign for C being non-empty Circuit of G st C calculates X,A holds for f being SortMap of X,A,C for t being Term of S,V st t in Subtrees X holds for s being State of C holds ( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) ) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty finite-yielding MSAlgebra over S for V being Variables of A for X being SetWithCompoundTerm of S,V for G being non empty non void Circuit-like ManySortedSign for C being non-empty Circuit of G st C calculates X,A holds for f being SortMap of X,A,C for t being Term of S,V st t in Subtrees X holds for s being State of C holds ( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) ) let A be non-empty finite-yielding MSAlgebra over S; ::_thesis: for V being Variables of A for X being SetWithCompoundTerm of S,V for G being non empty non void Circuit-like ManySortedSign for C being non-empty Circuit of G st C calculates X,A holds for f being SortMap of X,A,C for t being Term of S,V st t in Subtrees X holds for s being State of C holds ( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) ) let V be Variables of A; ::_thesis: for X being SetWithCompoundTerm of S,V for G being non empty non void Circuit-like ManySortedSign for C being non-empty Circuit of G st C calculates X,A holds for f being SortMap of X,A,C for t being Term of S,V st t in Subtrees X holds for s being State of C holds ( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) ) let X be SetWithCompoundTerm of S,V; ::_thesis: for G being non empty non void Circuit-like ManySortedSign for C being non-empty Circuit of G st C calculates X,A holds for f being SortMap of X,A,C for t being Term of S,V st t in Subtrees X holds for s being State of C holds ( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) ) let G be non empty non void Circuit-like ManySortedSign ; ::_thesis: for C being non-empty Circuit of G st C calculates X,A holds for f being SortMap of X,A,C for t being Term of S,V st t in Subtrees X holds for s being State of C holds ( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) ) let C be non-empty Circuit of G; ::_thesis: ( C calculates X,A implies for f being SortMap of X,A,C for t being Term of S,V st t in Subtrees X holds for s being State of C holds ( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) ) ) assume A1: C calculates X,A ; ::_thesis: for f being SortMap of X,A,C for t being Term of S,V st t in Subtrees X holds for s being State of C holds ( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) ) let f be SortMap of X,A,C; ::_thesis: for t being Term of S,V st t in Subtrees X holds for s being State of C holds ( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) ) consider g being Function 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, Def12; let t be Term of S,V; ::_thesis: ( t in Subtrees X implies for s being State of C holds ( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) ) ) assume A5: t in Subtrees X ; ::_thesis: for s being State of C holds ( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) ) let s be State of C; ::_thesis: ( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) ) 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; ::_thesis: for s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) let s9 be State of (X -Circuit A); ::_thesis: ( s9 = s * f implies for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) assume A8: s9 = s * f ; ::_thesis: for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) let h be CompatibleValuation of s9; ::_thesis: (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) A9: dom f = the carrier of (X -CircuitStr) by A4, PUA2MSS1:def_12; (Following (s9,(1 + (height (dom t))))) . t9 = t @ (h,A) by Th21; hence (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) by A7, A8, A9, FUNCT_1:13; ::_thesis: verum end; theorem Th60: :: CIRCTRM1:60 for S being non empty non void ManySortedSign for A being non-empty finite-yielding MSAlgebra over S for V being Variables of A for X being SetWithCompoundTerm of S,V for G being non empty non void Circuit-like ManySortedSign for C being non-empty Circuit of G st C calculates X,A holds for t being Term of S,V st t in Subtrees X holds 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 s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) ) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty finite-yielding MSAlgebra over S for V being Variables of A for X being SetWithCompoundTerm of S,V for G being non empty non void Circuit-like ManySortedSign for C being non-empty Circuit of G st C calculates X,A holds for t being Term of S,V st t in Subtrees X holds 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 s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) ) let A be non-empty finite-yielding MSAlgebra over S; ::_thesis: for V being Variables of A for X being SetWithCompoundTerm of S,V for G being non empty non void Circuit-like ManySortedSign for C being non-empty Circuit of G st C calculates X,A holds for t being Term of S,V st t in Subtrees X holds 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 s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) ) let V be Variables of A; ::_thesis: for X being SetWithCompoundTerm of S,V for G being non empty non void Circuit-like ManySortedSign for C being non-empty Circuit of G st C calculates X,A holds for t being Term of S,V st t in Subtrees X holds 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 s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) ) let X be SetWithCompoundTerm of S,V; ::_thesis: for G being non empty non void Circuit-like ManySortedSign for C being non-empty Circuit of G st C calculates X,A holds for t being Term of S,V st t in Subtrees X holds 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 s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) ) let G be non empty non void Circuit-like ManySortedSign ; ::_thesis: for C being non-empty Circuit of G st C calculates X,A holds for t being Term of S,V st t in Subtrees X holds 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 s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) ) let C be non-empty Circuit of G; ::_thesis: ( C calculates X,A implies for t being Term of S,V st t in Subtrees X holds 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 s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) ) ) assume A1: C calculates X,A ; ::_thesis: for t being Term of S,V st t in Subtrees X holds 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 s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) ) then consider f, g being Function such that A2: f,g form_embedding_of X -Circuit A,C and A3: f preserves_inputs_of X -CircuitStr ,G by Def15; f is one-to-one by A2, Def12; then reconsider f = f as SortMap of X,A,C by A1, A2, A3, Def17; let t be Term of S,V; ::_thesis: ( t in Subtrees X implies 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 s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) ) ) assume A4: t in Subtrees X ; ::_thesis: 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 s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) ) A5: f,g form_morphism_between X -CircuitStr ,G by A2, Def12; reconsider t9 = t as Vertex of (X -CircuitStr) by A4; reconsider v = f . t9 as Vertex of G by A5, Th30; take v ; ::_thesis: 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 s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) ) let s be State of C; ::_thesis: ( Following (s,(1 + (height (dom t)))) is_stable_at v & ex f being SortMap of X,A,C st for s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) ) thus Following (s,(1 + (height (dom t)))) is_stable_at v by A1, Th59; ::_thesis: ex f being SortMap of X,A,C st for s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) take f ; ::_thesis: for s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) thus for s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) by A1, Th59; ::_thesis: verum end; theorem :: CIRCTRM1:61 for S being non empty non void ManySortedSign for A being non-empty finite-yielding MSAlgebra over S for V being Variables of A for X being SetWithCompoundTerm of S,V for G being non empty non void Circuit-like ManySortedSign for C being non-empty Circuit of G st X,A specifies C holds for f being SortMap of X,A,C for s being State of C for t being Term of S,V st t in Subtrees X holds ( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) ) proof let S be non empty non void ManySortedSign ; ::_thesis: for A being non-empty finite-yielding MSAlgebra over S for V being Variables of A for X being SetWithCompoundTerm of S,V for G being non empty non void Circuit-like ManySortedSign for C being non-empty Circuit of G st X,A specifies C holds for f being SortMap of X,A,C for s being State of C for t being Term of S,V st t in Subtrees X holds ( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) ) let A be non-empty finite-yielding MSAlgebra over S; ::_thesis: for V being Variables of A for X being SetWithCompoundTerm of S,V for G being non empty non void Circuit-like ManySortedSign for C being non-empty Circuit of G st X,A specifies C holds for f being SortMap of X,A,C for s being State of C for t being Term of S,V st t in Subtrees X holds ( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) ) let V be Variables of A; ::_thesis: for X being SetWithCompoundTerm of S,V for G being non empty non void Circuit-like ManySortedSign for C being non-empty Circuit of G st X,A specifies C holds for f being SortMap of X,A,C for s being State of C for t being Term of S,V st t in Subtrees X holds ( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) ) let X be SetWithCompoundTerm of S,V; ::_thesis: for G being non empty non void Circuit-like ManySortedSign for C being non-empty Circuit of G st X,A specifies C holds for f being SortMap of X,A,C for s being State of C for t being Term of S,V st t in Subtrees X holds ( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) ) let G be non empty non void Circuit-like ManySortedSign ; ::_thesis: for C being non-empty Circuit of G st X,A specifies C holds for f being SortMap of X,A,C for s being State of C for t being Term of S,V st t in Subtrees X holds ( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) ) let C be non-empty Circuit of G; ::_thesis: ( X,A specifies C implies for f being SortMap of X,A,C for s being State of C for t being Term of S,V st t in Subtrees X holds ( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) ) ) assume X,A specifies C ; ::_thesis: for f being SortMap of X,A,C for s being State of C for t being Term of S,V st t in Subtrees X holds ( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) ) then C calculates X,A by Th58; hence for f being SortMap of X,A,C for s being State of C for t being Term of S,V st t in Subtrees X holds ( Following (s,(1 + (height (dom t)))) is_stable_at f . t & ( for s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . (f . t) = t @ (h,A) ) ) by Th59; ::_thesis: verum end; theorem :: CIRCTRM1:62 for S being non empty non void ManySortedSign for A being non-empty finite-yielding MSAlgebra over S for V being Variables of A for X being SetWithCompoundTerm of S,V for G being non empty non void Circuit-like ManySortedSign for C being non-empty Circuit of G st X,A specifies C holds for t being Term of S,V st t in Subtrees X holds 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 s9 being State of (X -Circuit A) st s9 = s * f holds for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) ) by Th58, Th60;