:: Circuit Generated by Terms and Circuit Calculating Terms
:: by Grzegorz Bancerek
::
:: Received April 10, 2001
:: Copyright (c) 2001-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, STRUCT_0, MSUALG_1, RELAT_1, MSATERM, SUBSET_1,
FUNCT_1, TREES_4, MSAFREE, PBOOLE, TREES_9, ZFMISC_1, FUNCT_3, CIRCCOMB,
GLIB_000, TREES_1, FINSEQ_1, NUMBERS, ORDINAL4, MARGREL1, TREES_3,
FINSET_1, TREES_2, PARTFUN1, FUNCT_4, MSAFREE2, MCART_1, TARSKI,
FUNCOP_1, CARD_3, QC_LANG1, FSM_1, CIRCUIT2, FACIRC_1, FUNCT_6, TREES_A,
ARYTM_3, XXREAL_0, NAT_1, CARD_1, PUA2MSS1, REWRITE1, CQC_SIM1, CIRCUIT1,
CIRCTRM1, SETLIM_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS,
XCMPLX_0, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSET_1, PARTFUN1,
MCART_1, FINSEQ_2, FUNCT_4, CARD_3, FUNCOP_1, FUNCT_3, STRUCT_0, PBOOLE,
MSUALG_1, MSAFREE2, CIRCUIT1, CIRCUIT2, CIRCCOMB, FACIRC_1, TREES_1,
TREES_2, TREES_3, TREES_4, TREES_9, MSATERM, PUA2MSS1, XXREAL_0;
constructors TREES_9, MSUALG_3, MSATERM, CIRCUIT1, CIRCUIT2, FACIRC_1,
PUA2MSS1, INSTALG1, NAT_1, XREAL_0, RELSET_1, XTUPLE_0, NUMBERS;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCOP_1, XREAL_0, FINSEQ_1, CARD_3,
PBOOLE, TREES_2, TREES_3, TREES_9, STRUCT_0, MSUALG_1, MSUALG_2, MSAFREE,
MSATERM, CIRCCOMB, INSTALG1, ORDINAL1, FINSET_1, CARD_1, RELSET_1, NAT_1,
XTUPLE_0;
requirements NUMERALS, BOOLE, SUBSET;
definitions TARSKI, PARTFUN1, FUNCOP_1, PBOOLE, MSAFREE2, CIRCUIT2, CIRCCOMB,
PUA2MSS1, FINSET_1, FACIRC_1, XBOOLE_0;
equalities MSUALG_1, MSAFREE2;
expansions PBOOLE, CIRCUIT2, CIRCCOMB, PUA2MSS1, FACIRC_1;
theorems MSUALG_1, TARSKI, ZFMISC_1, NAT_1, RELAT_1, FUNCT_1, FUNCT_2,
FINSEQ_1, PARTFUN1, FUNCT_4, FUNCT_6, PBOOLE, MSAFREE2, CARD_3, TREES_1,
TREES_2, TREES_3, TREES_4, TREES_9, MSAFREE, MSATERM, CIRCUIT1, CIRCUIT2,
CIRCCOMB, FACIRC_1, PUA2MSS1, INSTALG1, XBOOLE_0, FINSET_1, ORDINAL1,
FINSEQ_2;
schemes NAT_1, FINSEQ_1, CLASSES1, PBOOLE, MSATERM, FUNCT_1;
begin :: <section1>Circuit structure generated by terms</section1>
theorem Th1:
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S for V being Variables of A
for t being Term of S,V, T being c-Term of A,V st T = t
holds the_sort_of T = the_sort_of t
proof
let S being non empty non void ManySortedSign;
let A being non-empty MSAlgebra over S;
let V being Variables of A;
defpred P[set] means for t9 being Term of S,V, 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, v being Element of V.s holds
P[root-tree [v,s]]
proof
let s being SortSymbol of S, v being Element of V.s;
let t be Term of S,V, T be c-Term of A,V;
assume that
A2: t = root-tree [v,s] and
A3: T = t;
the_sort_of t = s by A2,MSATERM:14;
hence thesis by A2,A3,MSATERM:16;
end;
A4: for o being OperSymbol of S, p being ArgumentSeq of Sym(o,V) st
for t9 being Term of S,V st t9 in rng p holds P[t9] holds
P[[o,the carrier of S]-tree p]
proof
let o being OperSymbol of S;
let p being ArgumentSeq of Sym(o,V);
assume for t9 being Term of S,V st t9 in rng p
for t being Term of S,V, T being c-Term of A,V
st t = t9 & T = t holds the_sort_of T = the_sort_of t;
let t being Term of S,V, T being c-Term of A,V;
assume t = [o,the carrier of S]-tree p;
then
A5: t.{} = [o,the carrier of S] by TREES_4:def 4;
then the_sort_of t = the_result_sort_of o by MSATERM:17;
hence thesis by A5,MSATERM:17;
end;
for t being Term of S,V holds P[t] from MSATERM:sch 1(A1,A4);
hence thesis;
end;
definition
let S be non empty non void ManySortedSign;
let V be non-empty ManySortedSet of the carrier of S;
let X be non empty Subset of S-Terms V;
func X-CircuitStr -> non empty strict ManySortedSign equals
ManySortedSign(#
Subtrees X, [:the carrier' of S,{the carrier of S}:]-Subtrees X,
[:the carrier' of S,{the carrier of S}:]-ImmediateSubtrees X,
incl([:the carrier' of S,{the carrier of S}:]-Subtrees X) #);
correctness;
end;
registration
let S be non empty non void ManySortedSign;
let V be non-empty ManySortedSet of the carrier of S;
let X be non empty Subset of S-Terms V;
cluster X-CircuitStr -> unsplit;
coherence;
end;
reserve S for non empty non void ManySortedSign,
V for non-empty ManySortedSet of the carrier of S,
A for non-empty MSAlgebra over S,
X for non empty Subset of S-Terms V,
t for Element of X;
theorem
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:
X is SetWithCompoundTerm of S,V iff X-CircuitStr is non void
proof
hereby
assume X is SetWithCompoundTerm of S,V;
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 X-CircuitStr is non void by A1,TREES_9:25;
end;
assume X-CircuitStr is non void;
then consider t such that
A2: t is not 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,def 6;
hence thesis by MSATERM:def 7;
end;
registration
let S be non empty non void ManySortedSign;
let V be non-empty ManySortedSet of the carrier of S;
let X be SetWithCompoundTerm of S,V;
cluster X-CircuitStr -> non void;
coherence by Th3;
end;
theorem Th4:
(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
set C = [:the carrier' of S, {the carrier of S}:];
hereby
let v be Vertex of X-CircuitStr;
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;
end;
let s be set;
assume s in the carrier' of X-CircuitStr;
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 C by TREES_9:24;
reconsider s as Term of S,V by A2;
reconsider e = {} as Node of t|p by TREES_1:22;
A4: dom (t|p) = (dom t qua Tree)|(p qua FinSequence of NAT) by TREES_2:def 10;
p = p^e by FINSEQ_1:34;
then
A5: t.p = s.e by A2,A4,TREES_2:def 10;
p in Leaves dom t iff s is root by A2,TREES_9:6;
hence thesis by A3,A5,MSATERM:28,def 6;
end;
theorem Th5:
for t being Vertex of X-CircuitStr holds
t in the carrier' of X-CircuitStr iff t is CompoundTerm of S,V
proof
let t being Vertex of X-CircuitStr;
thus t in the carrier' of X-CircuitStr implies t is CompoundTerm of S,V
by Th4;
set C = [:the carrier' of S, {the carrier of S}:];
consider tt 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;
then reconsider t9 = t as CompoundTerm of S,V;
A2: t9.{} in C by MSATERM:def 6;
A3: p^(<*>NAT) = p by FINSEQ_1:34;
{} in (dom tt)|p by TREES_1:22;
then tt.p in C by A1,A2,A3,TREES_2:def 10;
hence thesis by A1,TREES_9:24;
end;
registration
let S,V;
let X be SetWithCompoundTerm of S,V, g be Gate of X-CircuitStr;
cluster the_arity_of g -> DTree-yielding;
coherence;
end;
registration
let S be non empty non void ManySortedSign;
let V be non-empty ManySortedSet of the carrier of S;
let X be non empty Subset of S-Terms V;
cluster -> finite Function-like Relation-like for Vertex of X-CircuitStr;
coherence by Th4;
end;
registration
let S be non empty non void ManySortedSign;
let V be non-empty ManySortedSet of the carrier of S;
let X be non empty Subset of S-Terms V;
cluster -> DecoratedTree-like for Vertex of X-CircuitStr;
coherence;
end;
registration
let S be non empty non void ManySortedSign;
let V be non-empty ManySortedSet of the carrier of S;
let X be SetWithCompoundTerm of S,V;
cluster -> finite Function-like Relation-like for Gate of X-CircuitStr;
coherence by Th4;
end;
registration
let S be non empty non void ManySortedSign;
let V be non-empty ManySortedSet of the carrier of S;
let X be SetWithCompoundTerm of S,V;
cluster -> DecoratedTree-like for Gate of X-CircuitStr;
coherence;
end;
::theorem
:: for X being SetWithCompoundTerm of A,V, g being Gate of X-CircuitStr
:: for t being Term of A,V st t = g holds
:: the_arity_of g = subs t ? subs g
theorem Th6:
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 t1,t2 be non empty Subset of S-Terms V;
set C = [:the carrier' of S, {the carrier of S}:];
A1: dom (C-ImmediateSubtrees t1) = C-Subtrees t1 by FUNCT_2:def 1;
A2: dom (C-ImmediateSubtrees t2) = C-Subtrees t2 by FUNCT_2:def 1;
hereby
let x be object;
assume
A3: x in (dom the Arity of t1-CircuitStr) /\ dom the Arity of t2 -CircuitStr;
then
A4: x in dom the Arity of t1-CircuitStr by XBOOLE_0:def 4;
A5: x in dom the Arity of t2-CircuitStr by A3,XBOOLE_0:def 4;
reconsider u = x as Element of Subtrees t1 by A1,A4;
(C-ImmediateSubtrees t1).x in (Subtrees t1)* by A1,A4,FUNCT_2:5;
then reconsider y1 = (the Arity of t1-CircuitStr).x as
FinSequence of Subtrees t1 by FINSEQ_1:def 11;
(the Arity of t2-CircuitStr).x in (Subtrees t2)* by A2,A5,FUNCT_2:5;
then reconsider y2 = (the Arity of t2-CircuitStr).x as
FinSequence of Subtrees t2 by FINSEQ_1:def 11;
A6: (for t being Element of t1 holds t is finite)
& for t being Element of t2 holds t is finite;
then
A7: u = (u.{})-tree y1 by A1,A4,TREES_9:def 13;
u = (u.{})-tree y2 by A2,A5,A6,TREES_9:def 13;
hence (the Arity of t1-CircuitStr).x = (the Arity of t2-CircuitStr).x
by A7,TREES_4:15;
end;
let x be object;
assume
A8: x in (dom the ResultSort of t1-CircuitStr) /\
dom the ResultSort of t2-CircuitStr;
then
A9: x in dom the ResultSort of t1-CircuitStr by XBOOLE_0:def 4;
A10: x in dom the ResultSort of t2-CircuitStr by A8,XBOOLE_0:def 4;
thus (the ResultSort of t1-CircuitStr).x = x by A9,FUNCT_1:18
.= (the ResultSort of t2-CircuitStr).x by A10,FUNCT_1:18;
end;
registration
let X,Y be constituted-DTrees set;
cluster X \/ Y -> constituted-DTrees;
coherence by TREES_3:9;
end;
theorem Th7:
for X1,X2 being constituted-DTrees non empty set holds
Subtrees (X1 \/ X2) = (Subtrees X1) \/ (Subtrees X2)
proof
let X1,X2 be constituted-DTrees non empty set;
hereby
let x be object;
assume x in Subtrees (X1 \/ X2);
then consider t 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;
end;
let x be object;
assume
A2: x in (Subtrees X1) \/ (Subtrees X2);
per cases by A2,XBOOLE_0:def 3;
suppose x in Subtrees X1;
then consider t 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 thesis by A3,TREES_9:19;
end;
suppose x in Subtrees 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 thesis by A4,TREES_9:19;
end;
end;
theorem Th8:
for X1,X2 being constituted-DTrees non empty set, C be set holds
C-Subtrees (X1 \/ X2) = (C-Subtrees X1) \/ (C-Subtrees X2)
proof
let X1,X2 be constituted-DTrees non empty set, C be set;
hereby
let x be object;
assume x in C-Subtrees (X1 \/ X2);
then consider t 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;
end;
let x be object;
assume
A3: x in (C-Subtrees X1) \/ (C-Subtrees X2);
per cases by A3,XBOOLE_0:def 3;
suppose x in C-Subtrees X1;
then consider t 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 thesis by A4,A5,TREES_9:24;
end;
suppose x in C-Subtrees 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 thesis by A6,A7,TREES_9:24;
end;
end;
theorem Th9:
for X1,X2 being constituted-DTrees non empty set st
(for t being Element of X1 holds t is finite) &
(for t being Element of X2 holds t is finite) for C be set holds
C-ImmediateSubtrees (X1 \/ X2)
= (C-ImmediateSubtrees X1)+*(C-ImmediateSubtrees X2)
proof
let X1,X2 be constituted-DTrees non empty set such that
A1: for t being Element of X1 holds t is finite and
A2: for t being Element of X2 holds t is finite;
A3: now
let t be Element of X1 \/ X2;
t in X1 or t in X2 by XBOOLE_0:def 3;
hence t is finite by A1,A2;
end;
let C be set;
set X = X1 \/ X2;
set f = C-ImmediateSubtrees (X1 \/ X2);
set f1 = C-ImmediateSubtrees X1;
set f2 = C-ImmediateSubtrees X2;
A4: dom f = C-Subtrees X by FUNCT_2:def 1;
A5: dom f1 = C-Subtrees X1 by FUNCT_2:def 1;
A6: dom f2 = C-Subtrees X2 by FUNCT_2:def 1;
A7: C-Subtrees X = (C-Subtrees X1) \/ (C-Subtrees X2) by Th8;
now
let x be object;
assume
A8: x in dom f1 \/ dom f2;
then reconsider t = x as Element of Subtrees X by A5,A6,A7;
f.x in (Subtrees X)* by A5,A6,A7,A8,FUNCT_2:5;
then reconsider p = f.x as FinSequence of Subtrees X by FINSEQ_1:def 11;
hereby
assume
A9: x in dom f2;
then f2.x in (Subtrees X2)* by A6,FUNCT_2:5;
then reconsider p2 = f2.x as FinSequence of Subtrees X2 by
FINSEQ_1:def 11;
A10: t = (t.{})-tree p by A3,A5,A6,A7,A8,TREES_9:def 13;
t = (t.{})-tree p2 by A2,A6,A9,TREES_9:def 13;
hence f.x = f2.x by A10,TREES_4:15;
end;
assume not x in dom f2;
then
A11: x in dom f1 by A8,XBOOLE_0:def 3;
then f1.x in (Subtrees X1)* by A5,FUNCT_2:5;
then reconsider p1 = f1.x as FinSequence of Subtrees X1 by FINSEQ_1:def 11;
A12: t = (t.{})-tree p by A3,A5,A6,A7,A8,TREES_9:def 13;
t = (t.{})-tree p1 by A1,A5,A11,TREES_9:def 13;
hence f.x = f1.x by A12,TREES_4:15;
end;
hence thesis by A4,A5,A6,A7,FUNCT_4:def 1;
end;
theorem Th10:
for X1,X2 being non empty Subset of S-Terms V holds
(X1 \/ X2)-CircuitStr = (X1-CircuitStr)+*(X2-CircuitStr)
proof
let X1,X2 be non empty Subset of S-Terms V;
set X = X1 \/ X2;
set C = [:the carrier' of S,{the carrier of S}:];
A1: Subtrees X = (Subtrees X1) \/ Subtrees X2 by Th7;
A2: C-Subtrees X = (C-Subtrees X1) \/ (C-Subtrees X2) by Th8;
(for t being Element of X1 holds t is finite)
& for t being Element of X2 holds t is finite;
then
A3: C-ImmediateSubtrees X = (C-ImmediateSubtrees X1)+*(C
-ImmediateSubtrees X2) by Th9;
id (C-Subtrees X) = (id (C-Subtrees X1))+*id (C-Subtrees X2)
by A2,FUNCT_4:22;
hence thesis by A1,A2,A3,CIRCCOMB:def 2;
end;
theorem Th11:
for x being set holds x in InputVertices (X-CircuitStr) iff x in Subtrees X &
ex s being SortSymbol of S, v being Element of V.s st x = root-tree [v,s]
proof
set G = X-CircuitStr;
let x be set;
hereby
assume
A1: x in InputVertices (X-CircuitStr);
then
A2: not x in the carrier' of G by XBOOLE_0:def 5;
thus x in Subtrees X by A1;
reconsider t = x as Term of S,V by A1,Th4;
(ex s being SortSymbol of S, 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, 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
A3: t.{} = [v,s] by A1,A2,Th5;
take s;
reconsider v as Element of V.s;
take v;
thus x = root-tree [v,s] by A3,MSATERM:5;
end;
assume
A4: x in Subtrees X;
given s being SortSymbol of S, v being Element of V.s such that
A5: x = root-tree [v,s];
assume not thesis;
then x in the carrier' of G by A4,XBOOLE_0:def 5;
then reconsider t = x as CompoundTerm of S,V by Th4;
t.{} = [v,s] by A5,TREES_4:3;
then [v,s] in [:the carrier' of S,{the carrier of S}:] by MSATERM:def 6;
then s = the carrier of S by ZFMISC_1:106;
then s in s;
hence contradiction;
end;
theorem Th12:
for X being SetWithCompoundTerm of S,V, g being Gate of X-CircuitStr
holds g = (g.{})-tree the_arity_of g
proof
let X be SetWithCompoundTerm of S,V;
let g be Gate of X-CircuitStr;
for t being Element of X holds t is finite;
hence thesis by TREES_9:def 13;
end;
begin :: <section2>Circuit genereted by terms</section2>
definition
let S be non empty non void ManySortedSign;
let V be non-empty ManySortedSet of the carrier of S;
let X be non empty Subset of S-Terms V;
let v be Vertex of X-CircuitStr;
let A be MSAlgebra over S;
func the_sort_of (v, A) -> set means
: Def2:
for u being Term of S,V st u = v holds it = (the Sorts of A).the_sort_of u;
uniqueness
proof
let S1, S2 be set;
reconsider u = v as Term of S,V by Th4;
assume
A1: not thesis;
then S1 = (the Sorts of A).the_sort_of u;
hence thesis by A1;
end;
existence
proof
reconsider u = v as Term of S,V by Th4;
take (the Sorts of A).the_sort_of u;
thus thesis;
end;
end;
registration
let S be non empty non void ManySortedSign;
let V be non-empty ManySortedSet of the carrier of S;
let X be non empty Subset of S-Terms V;
let v be Vertex of X-CircuitStr;
let A be non-empty MSAlgebra over S;
cluster the_sort_of (v, A) -> non empty;
coherence
proof
reconsider u = v as Term of S,V by Th4;
the_sort_of (v, A) = (the Sorts of A).the_sort_of u by Def2;
hence thesis;
end;
end;
definition
let S be non empty non void ManySortedSign;
let V be non-empty ManySortedSet of the carrier of S;
let X be non empty Subset of S-Terms V;
assume
A1: X is SetWithCompoundTerm of S,V;
let o be Gate of X-CircuitStr;
let A be MSAlgebra over S;
func the_action_of (o, A) -> Function means
:
Def3: for X9 being SetWithCompoundTerm of S,V st X9 = X
for o9 being Gate of X9-CircuitStr st o9 = o holds
it = (the Charact of A).(o9.{})`1;
uniqueness
proof
let f1, f2 be Function;
reconsider X9 = X as SetWithCompoundTerm of S,V by A1;
reconsider o9 = o as Gate of X9-CircuitStr;
assume
A2: not thesis;
then f1 = (the Charact of A).(o9.{})`1;
hence thesis by A2;
end;
existence
proof
reconsider X9 = X as SetWithCompoundTerm of S,V by A1;
reconsider o9 = o as Gate of X9-CircuitStr;
take (the Charact of A).(o9.{})`1;
thus thesis;
end;
end;
scheme MSFuncEx {I() -> non empty set, A,B() -> non-empty ManySortedSet of I(),
P[object,object,object]}:
ex f being ManySortedFunction of A(),B() st
for i being Element of I(), a being Element of A().i holds P[i,a,f.i.a]
provided
A1: for i being Element of I(), a being Element of A().i
ex b being Element of B().i st P[i,a,b];
defpred R[object,object] means
ex g being Function of A().$1, B().$1 st $2 = g &
for a being set st a in A().$1 holds P[$1,a,g.a];
A2: for i being object st i in I() ex y being object st R[i,y]
proof
let i be object;
assume i in I();
then reconsider ii=i as Element of I();
defpred RR[object,object] means P[i,$1,$2];
A3: for a being object st a in A().i
ex b being object st b in B().i & RR[a,b]
proof
let a be object;
assume a in A().i;
then ex b being Element of B().ii st P[i,a,b] by A1;
hence thesis;
end;
consider g being Function such that
A4: dom g = A().i & rng g c= B().i and
A5: for a being object st a in A().i holds RR[a,g.a] from FUNCT_1:sch 6(A3);
take y = g;
reconsider g as Function of A().i, B().i by A4,FUNCT_2:2;
take g;
thus y = g &
for a being set st a in A().i holds P[i,a,g.a] by A5;
end;
consider f being Function such that
A6: dom f = I() and
A7: for i being object st i in I() holds R[i,f.i] from CLASSES1:sch 1(A2);
reconsider f as ManySortedSet of I() by A6,PARTFUN1:def 2,RELAT_1:def 18;
f is ManySortedFunction of A(),B()
proof
let i be object;
assume i in I();
then ex g being Function of A().i, B().i st f.i = g &
for a being set st a in A().i holds P[i,a,g.a] by A7;
hence thesis;
end;
then reconsider f as ManySortedFunction of A(),B();
take f;
let i being Element of I(), a being Element of A().i;
ex g being Function of A().i, B().i st f.i = g &
for a being set st a in A().i holds P[i,a,g.a] by A7;
hence thesis;
end;
definition
let S be non empty non void ManySortedSign;
let V be non-empty ManySortedSet of the carrier of S;
let X be non empty Subset of S-Terms V;
let A be MSAlgebra over S;
func X-CircuitSorts A -> ManySortedSet of the carrier of X-CircuitStr means
: Def4:
for v being Vertex of X-CircuitStr holds it.v = the_sort_of (v, A);
uniqueness
proof
let S1,S2 be ManySortedSet of the carrier of X-CircuitStr such that
A1: for v 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);
now
let x be object;
assume x in the carrier of X-CircuitStr;
then reconsider v = x as Vertex of X-CircuitStr;
thus S1.x = the_sort_of (v, A) by A1
.= S2.x by A2;
end;
hence thesis;
end;
existence
proof
deffunc f(Vertex of X-CircuitStr) = the_sort_of ($1,A);
thus ex f be ManySortedSet of the carrier of X-CircuitStr st
for d be Element of X-CircuitStr holds f.d = f(d) from PBOOLE:sch 5;
end;
end;
registration
let S be non empty non void ManySortedSign;
let V be non-empty ManySortedSet of the carrier of S;
let X be non empty Subset of S-Terms V;
let A be non-empty MSAlgebra over S;
cluster X-CircuitSorts A -> non-empty;
coherence
proof
let i be object;
assume i in the carrier of X-CircuitStr;
then reconsider i as Vertex of X-CircuitStr;
(X-CircuitSorts A).i = the_sort_of (i, A) by Def4;
hence thesis;
end;
end;
theorem Th13:
for X being SetWithCompoundTerm of S,V, g being Gate of X-CircuitStr
for o being OperSymbol of S st g.{} = [o,the carrier of S] holds
(X-CircuitSorts A)*the_arity_of g = (the Sorts of A)*the_arity_of o
proof
let t be SetWithCompoundTerm of S,V, g be Gate of t-CircuitStr;
set X = t;
reconsider f = g as CompoundTerm of S,V by Th4;
reconsider ag = the_arity_of g as FinSequence of Subtrees t;
A1: g = (f.{})-tree ag by Th12;
let o be OperSymbol of S;
assume g.{} = [o,the carrier of S];
then consider a 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 (X-CircuitSorts A) = the carrier of X-CircuitStr by PARTFUN1:def 2;
A10: dom the Sorts of A = the carrier of S by PARTFUN1:def 2;
A11: dom ((X-CircuitSorts A)*the_arity_of g) = Seg len a by A6,A7,A9,RELAT_1:27
;
A12: dom ((the Sorts of A)*the_arity_of o) = Seg len a by A5,A8,A10,RELAT_1:27;
now
let i be object;
assume
A13: i in Seg len a;
then reconsider j = i as Element of NAT;
ag.i in rng the_arity_of g by A6,A13,FUNCT_1:def 3;
then reconsider v = ag.j as Vertex of t-CircuitStr by A7;
(the_arity_of o).i in rng the_arity_of o by A5,A13,FUNCT_1:def 3;
then reconsider s = (the_arity_of o).j as SortSymbol of S by A8;
reconsider u = v as Term of S,V by A4,A6,A13,MSATERM:22;
A14: the_sort_of u = s by A4,A6,A13,MSATERM:23;
A15: ((t-CircuitSorts A)*the_arity_of g).i = (t-CircuitSorts A).v by A11,A13,
FUNCT_1:12;
A16: ((the Sorts of A)*the_arity_of o).i = (the Sorts of A).s by A12,A13,
FUNCT_1:12;
thus ((t-CircuitSorts A)*the_arity_of g).i = the_sort_of (v, A) by A15,Def4
.= ((the Sorts of A)*the_arity_of o).i by A14,A16,Def2;
end;
hence thesis by A11,A12,FUNCT_1:2;
end;
definition
let S be non empty non void ManySortedSign;
let V be non-empty ManySortedSet of the carrier of S;
let X be non empty Subset of S-Terms V;
let A be non-empty MSAlgebra over S;
func X-CircuitCharact A -> ManySortedFunction of
(X-CircuitSorts A)#*(the Arity of X-CircuitStr),
(X-CircuitSorts A)*(the ResultSort of X-CircuitStr) means
: Def5:
for g being Gate of X-CircuitStr st g in the carrier' of X-CircuitStr
holds it.g = the_action_of (g, A);
uniqueness
proof
let C1, C2 be ManySortedFunction of
(X-CircuitSorts A)#*(the Arity of X-CircuitStr),
(X-CircuitSorts A)*(the ResultSort of X-CircuitStr) such that
A1: for o 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);
now
let x be object;
assume
A3: x in the carrier' of X-CircuitStr;
then reconsider o = x as Gate of X-CircuitStr;
C1.o = the_action_of (o, A) by A1,A3;
hence C1.x = C2.x by A2,A3;
end;
hence thesis;
end;
existence
proof
defpred P[object,object] means
ex g being Gate of X-CircuitStr st g = $1 &
$2 = the_action_of (g, A);
A4: now
let x be object;
assume x in the carrier' of X-CircuitStr;
then reconsider g = x as Gate of X-CircuitStr;
reconsider y = the_action_of (g, A) as object;
take y;
thus P[x,y];
end;
consider CHARACT being ManySortedSet of the carrier' of X-CircuitStr
such that
A5: for x being object st x in the carrier' of X-CircuitStr
holds P[x,CHARACT.x] from PBOOLE:sch 3(A4);
A6: dom CHARACT = the carrier' of X-CircuitStr by PARTFUN1:def 2;
CHARACT is Function-yielding
proof
let x be object;
assume x in dom CHARACT;
then ex g being Gate of X-CircuitStr st g = x &
CHARACT.x = the_action_of (g, A) by A5,A6;
hence thesis;
end;
then reconsider CHARACT as
ManySortedFunction of the carrier' of X-CircuitStr;
CHARACT is ManySortedFunction of
(X-CircuitSorts A)#*the Arity of X-CircuitStr,
(X-CircuitSorts A)*the ResultSort of X-CircuitStr
proof
let i be object;
assume
A7: i in the carrier' of X-CircuitStr;
then X-CircuitStr is not void;
then reconsider X9 = X as SetWithCompoundTerm of S,V by Th3;
reconsider g = i as Gate of X9-CircuitStr by A7;
the_result_sort_of g = g;
then reconsider v = g as Vertex of X9-CircuitStr;
reconsider I = i as CompoundTerm of S,V by A7,Th4;
I.{} in [:the carrier' of S,{the carrier of S}:] by MSATERM:def 6;
then consider o,y being object such that
A8: o in the carrier' of S and
A9: y in {the carrier of S} and
A10: I.{} = [o,y] by ZFMISC_1:84;
reconsider o as OperSymbol of S by A8;
A11: o = (I.{})`1 by A10;
A12: y = the carrier of S by A9,TARSKI:def 1;
ex g being Gate of X-CircuitStr st
g = i & CHARACT.i = the_action_of (g, A) by A5,A7;
then
A13: CHARACT.i = the_action_of (g, A) .= (the Charact of A).o by A11,Def3;
A14: ((the Sorts of A)*the ResultSort of S).o
= (the Sorts of A).(the_result_sort_of o) by FUNCT_2:15
.= (the Sorts of A).(the_sort_of I) by A10,A12,MSATERM:17;
A15: ((X-CircuitSorts A)*the ResultSort of X-CircuitStr).g
= (X-CircuitSorts A).(the_result_sort_of g) by FUNCT_2:15
.= the_sort_of (v, A) by Def4
.= (the Sorts of A).the_sort_of I by Def2;
A16: ((X-CircuitSorts A)#*the Arity of X-CircuitStr).g
= (X-CircuitSorts A)#.(the_arity_of g) by FUNCT_2:15
.= product ((X9-CircuitSorts A)*the_arity_of g) by FINSEQ_2:def 5
.= product ((the Sorts of A)*the_arity_of o) by A10,A12,Th13;
((the Sorts of A)#*the Arity of S).o
= (the Sorts of A)#.the_arity_of o by FUNCT_2:15
.= product ((the Sorts of A)*the_arity_of o) by FINSEQ_2:def 5;
hence thesis by A13,A14,A15,A16,PBOOLE:def 15;
end;
then reconsider CHARACT as ManySortedFunction of
(X-CircuitSorts A)#*the Arity of X-CircuitStr,
(X-CircuitSorts A)*the ResultSort of X-CircuitStr;
take CHARACT;
let g being Gate of X-CircuitStr;
assume g in the carrier' of X-CircuitStr;
then ex h being Gate of X-CircuitStr st h = g &
CHARACT.g = the_action_of (h, A) by A5;
hence thesis;
end;
end;
definition
let S be non empty non void ManySortedSign;
let V be non-empty ManySortedSet of the carrier of S;
let X be non empty Subset of S-Terms V;
let A be non-empty MSAlgebra over S;
func X-Circuit A -> non-empty strict MSAlgebra over X-CircuitStr equals
MSAlgebra(#X-CircuitSorts A, X-CircuitCharact A#);
correctness by MSUALG_1:def 3;
end;
theorem
for v being Vertex of X-CircuitStr
holds (the Sorts of X-Circuit A).v = the_sort_of (v, A) by Def4;
theorem
for A being finite-yielding non-empty MSAlgebra over S
for X being SetWithCompoundTerm of S,V
for g being OperSymbol of X-CircuitStr
holds Den(g, X-Circuit A) = the_action_of (g, A) by Def5;
theorem Th16:
for A being finite-yielding non-empty MSAlgebra over S
for X being SetWithCompoundTerm of S,V
for g being OperSymbol of X-CircuitStr, o being OperSymbol of S
st g.{} = [o, the carrier of S] holds Den(g, X-Circuit A) = Den(o,A)
proof
let A being finite-yielding non-empty MSAlgebra over S;
let X being SetWithCompoundTerm of S,V;
let g being OperSymbol of X-CircuitStr, o being OperSymbol of S;
Den(g, X-Circuit A) = the_action_of (g, A) by Def5
.= (the Charact of A).(g.{})`1 by Def3;
hence thesis;
end;
theorem Th17:
for A being finite-yielding non-empty MSAlgebra over S,
X being non empty Subset of S-Terms V holds X-Circuit A is finite-yielding
proof
let A be finite-yielding non-empty MSAlgebra over S;
let t be non empty Subset of S-Terms V;
let i be object;
assume i in the carrier of t-CircuitStr;
then reconsider i as Vertex of t-CircuitStr;
reconsider u = i as Term of S,V by Th4;
A1: the Sorts of A is finite-yielding by MSAFREE2:def 11;
(the Sorts of t-Circuit A).i = the_sort_of (i, A) by Def4
.= (the Sorts of A).the_sort_of u by Def2;
hence thesis by A1;
end;
registration
let S be non empty non void ManySortedSign;
let V be non-empty ManySortedSet of the carrier of S;
let X be SetWithCompoundTerm of S,V;
let A be finite-yielding non-empty MSAlgebra over S;
cluster X-Circuit A -> finite-yielding;
coherence by Th17;
end;
theorem Th18:
for S being non empty non void ManySortedSign
for V being non-empty ManySortedSet of the carrier of S
for X1,X2 being SetWithCompoundTerm of S,V
for A being non-empty MSAlgebra over S holds
X1-Circuit A tolerates X2-Circuit A
proof
let S be non empty non void ManySortedSign;
let V be non-empty ManySortedSet of the carrier of S;
let X1,X2 be SetWithCompoundTerm of S,V;
let A be non-empty MSAlgebra over S;
thus the Arity of X1-CircuitStr tolerates the Arity of X2-CircuitStr &
the ResultSort of X1-CircuitStr tolerates the ResultSort of X2-CircuitStr
by Th6;
thus the Sorts of X1-Circuit A tolerates the Sorts of X2-Circuit A
proof
let x be object;
assume
A1: x in (dom the Sorts of X1-Circuit A) /\ dom the Sorts of X2-Circuit A;
then
A2: x in dom the Sorts of X1-Circuit A by XBOOLE_0:def 4;
A3: x in dom the Sorts of X2 -Circuit A by A1,XBOOLE_0:def 4;
A4: x in the carrier of X1-CircuitStr by A2,PARTFUN1:def 2;
reconsider v1 = x as Vertex of X1-CircuitStr by A2,PARTFUN1:def 2;
reconsider v2 = x as Vertex of X2-CircuitStr by A3,PARTFUN1:def 2;
reconsider t = x as Term of S,V by A4,Th4;
thus (the Sorts of X1-Circuit A).x = the_sort_of (v1, A) by Def4
.= (the Sorts of A).the_sort_of t by Def2
.= the_sort_of (v2, A) by Def2
.= (the Sorts of X2-Circuit A).x by Def4;
end;
let x be object;
assume
A5: x in (dom the Charact of X1-Circuit A) /\ dom the Charact of X2 -Circuit A;
then
A6: x in dom the Charact of X1-Circuit A by XBOOLE_0:def 4;
A7: x in dom the Charact of X2 -Circuit A by A5,XBOOLE_0:def 4;
reconsider g1 = x as Gate of X1-CircuitStr by A6,PARTFUN1:def 2;
reconsider g2 = x as Gate of X2-CircuitStr by A7,PARTFUN1:def 2;
thus (the Charact of X1-Circuit A).x = the_action_of (g1, A) by Def5
.= (the Charact of A).(g1.{})`1 by Def3
.= the_action_of (g2, A) by Def3
.= (the Charact of X2-Circuit A).x by Def5;
end;
theorem
for S being non empty non void ManySortedSign
for V being non-empty ManySortedSet of the carrier of S
for X1,X2 being SetWithCompoundTerm of S,V
for A being non-empty MSAlgebra over S holds
(X1 \/ X2)-Circuit A = (X1-Circuit A)+*(X2-Circuit A)
proof
let S be non empty non void ManySortedSign;
let V be non-empty ManySortedSet of the carrier of S;
let X1,X2 be SetWithCompoundTerm of S,V;
consider t1 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;
set C1 = X1-Circuit A, C2 = X2-Circuit A, C = X-Circuit A;
A2: C1 tolerates C2 by Th18;
then
A3: the Sorts of C1 tolerates the Sorts of C2;
A4: the Charact of C1 tolerates the Charact of C2 by A2;
A5: the Sorts of C1+*C2 = (the Sorts of C1) +* (the Sorts of C2) by A3,
CIRCCOMB:def 4;
A6: the Charact of C1+*C2 = (the Charact of C1) +* (the Charact of C2) by A3,
CIRCCOMB:def 4;
A7: X-CircuitStr = X1-CircuitStr+*(X2-CircuitStr) by Th10;
A8: C1 tolerates C by Th18;
A9: C2 tolerates C by Th18;
A10: the Sorts of C1 tolerates the Sorts of C by A8;
A11: the Sorts of C2 tolerates the Sorts of C by A9;
A12: the Charact of C1 tolerates the Charact of C by A8;
A13: the Charact of C2 tolerates the Charact of C by A9;
A14: dom the Sorts of C1+*C2 = the carrier of X-CircuitStr by A7,PARTFUN1:def 2
;
dom the Charact of C1+*C2 = the carrier' of X-CircuitStr by A7,PARTFUN1:def 2
;
then
A15: dom the Charact of C1+*C2 = dom the Charact of C by PARTFUN1:def 2;
A16: dom the Sorts of C1+*C2 = dom the Sorts of C by A14,PARTFUN1:def 2;
A17: the Charact of C1+*C2 = the Charact of C by A4,A6,A12,A13,A15,FUNCT_4:125
,PARTFUN1:55;
the Sorts of C1+*C2 = the Sorts of C by A3,A5,A10,A11,A16,FUNCT_4:125
,PARTFUN1:55;
hence thesis by A17;
end;
begin :: <section3>Correctness of a Term Circuit</section3>
reserve S for non empty non void ManySortedSign,
A for non-empty finite-yielding MSAlgebra over S,
V for Variables of A,
X for SetWithCompoundTerm of S,V;
definition
let S be non empty non void ManySortedSign;
let A be non-empty MSAlgebra over S;
let V be Variables of A;
let t be DecoratedTree such that
A1: t is Term of S,V;
let f be ManySortedFunction of V, the Sorts of A;
func t@(f,A) -> set means
: Def7:
ex t9 being c-Term of A,V st t9 = t & it = t9@f;
correctness
proof reconsider t9 = t as c-Term of A,V by A1,MSATERM:27;
t9@f = t9@f;
hence thesis;
end;
end;
definition
let S be non empty non void ManySortedSign;
let V be non-empty ManySortedSet of the carrier of S;
let X be SetWithCompoundTerm of S,V;
let A be non-empty finite-yielding MSAlgebra over S;
let s be State of X-Circuit A;
defpred P[set,set,set] means
root-tree [$2,$1] in Subtrees X implies $3 = s.root-tree [$2,$1];
A1: for x being Vertex of S, v being Element of V.x
ex a being Element of (the Sorts of A).x st P[x,v,a]
proof
let x being Vertex of S, v being Element of V.x;
per cases;
suppose not root-tree [v,x] in Subtrees X;
hence thesis;
end;
suppose root-tree [v,x] in Subtrees X;
then reconsider a = root-tree [v,x] as Vertex of X-CircuitStr;
reconsider t = a as Term of S,V by MSATERM:4;
A2: the_sort_of t = x by MSATERM:14;
A3: the_sort_of (a, A) = (the Sorts of A).the_sort_of t by Def2;
(X-CircuitSorts A).a = the_sort_of (a, A) by Def4;
then reconsider b = s.a as Element of (the Sorts of A).x by A2,A3,
CIRCUIT1:4;
take b;
thus thesis;
end;
end;
mode CompatibleValuation of s -> ManySortedFunction of V, the Sorts of A
means
: Def8:
for x being Vertex of S, v being Element of V.x
st root-tree [v,x] in Subtrees X holds it.x.v = s.root-tree [v,x];
existence
proof
thus ex f being ManySortedFunction of V,the Sorts of A st
for x being Element of S,
v being Element of V.x holds P[x,v,f.x.v] from MSFuncEx(A1);
end;
end;
theorem
for s being State of X-Circuit A
for f being CompatibleValuation of s, n being Element of NAT
holds f is CompatibleValuation of Following(s,n)
proof
let s being State of X-Circuit A;
let f being CompatibleValuation of s, n being Element of NAT;
let x being Vertex of S, v being Element of V.x;
assume
A1: root-tree [v,x] in Subtrees X;
then root-tree [v,x] in InputVertices (X-CircuitStr) by Th11;
then s is_stable_at root-tree [v,x] by FACIRC_1:18;
then Following(s,n).root-tree [v,x] = s.root-tree [v,x];
hence thesis by A1,Def8;
end;
registration
let x be object;
let S be non empty non void ManySortedSign;
let V be non-empty ManySortedSet of the carrier of S;
let p be FinSequence of S-Terms V;
cluster x-tree p -> finite;
coherence
proof
reconsider q = doms p as FinTree-yielding FinSequence;
dom (x-tree p) = tree q by TREES_4:10;
hence thesis by FINSET_1:10;
end;
end;
theorem Th21:
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 q be State of X-Circuit A;
let f be CompatibleValuation of q;
A1: X-CircuitStr = ManySortedSign(#Subtrees X,
[:the carrier' of S,{the carrier of S}:]-Subtrees X,
[:the carrier' of S,{the carrier of S}:]-ImmediateSubtrees X,
incl([:the carrier' of S,{the carrier of S}:]-Subtrees X)#);
defpred P[finite DecoratedTree] means $1 in Subtrees X implies
Following(q, 1+height dom $1) is_stable_at $1 &
Following(q, 1+height dom $1).$1 = $1@(f,A);
A2: for s being SortSymbol of S, v being Element of V.s holds
P [ root-tree [ v, s ] ]
proof
let s being SortSymbol of S, v being Element of V.s;
assume
A3: root-tree [v,s] in Subtrees X;
then
A4: root-tree [v,s] in InputVertices (X-CircuitStr) by Th11;
hence Following(q, 1+height dom root-tree [v,s])
is_stable_at root-tree [v,s] by FACIRC_1:18;
reconsider t = root-tree [v,s] as c-Term of A, V by MSATERM:8;
A5: t is Term of S, V by MSATERM:4;
q is_stable_at root-tree [v,s] by A4,FACIRC_1:18;
hence Following(q,1+height dom root-tree [v,s]).root-tree [v,s]
= q.root-tree [v,s]
.= f.s.v by A3,Def8
.= (v-term A)@f by MSATERM:42
.= t@f by MSATERM:def 4
.= (root-tree [v,s])@(f, A) by A5,Def7;
end;
A6: for o being OperSymbol of S, p being ArgumentSeq of Sym(o,V)
st for t being Term of S,V st t in rng p holds P[t] holds
P[[o,the carrier of S]-tree p]
proof
let o being OperSymbol of S, p being ArgumentSeq of Sym(o,V) such 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;
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;
A12: g.{} = [o,the carrier of S] by TREES_4:def 4;
g = (g.{})-tree the_arity_of g by Th12;
then
A13: the_arity_of g = p by TREES_4:15;
A14: rng the_arity_of g c= Subtrees X by FINSEQ_1:def 4;
A15: dom ([o,the carrier of S]-tree p) = tree doms p by TREES_4:10;
now
let x being set;
assume
A16: x in rng the_arity_of g;
then reconsider t = x as Element of Subtrees X by A14;
reconsider t as Term of S,V by A1,Th4;
consider z being object such that
A17: z in dom p and
A18: t = p.z by A13,A16,FUNCT_1:def 3;
A19: z in dom doms p by A17,A18,FUNCT_6:22;
(doms p).z = dom t by A17,A18,FUNCT_6:22;
then dom t in rng doms p by A19,FUNCT_1:def 3;
then height dom t < height tree doms p by TREES_3:78;
then 1+height dom t <= height tree doms p by NAT_1:13;
then consider i being Nat such that
A20: height tree doms p = (1+height dom t)+i by NAT_1:10;
reconsider i as Element of NAT by ORDINAL1:def 12;
Following(q,height dom ([o,the carrier of S]-tree p))
= Following(Following(q,1+height dom t),i) by A15,A20,FACIRC_1:13;
hence Following(q,height dom ([o,the carrier of S]-tree p))
is_stable_at x by A7,A13,A16,FACIRC_1:17;
end;
then Following Following(q,height dom ([o,the carrier of S]-tree p))
is_stable_at [o,the carrier of S]-tree p by A11,FACIRC_1:19;
hence Following(q,1+height dom ([o,the carrier of S]-tree p))
is_stable_at [o,the carrier of S]-tree p by FACIRC_1:12;
reconsider t = Sym(o,V)-tree p as c-Term of A,V by MSATERM:27;
A21: Sym(o,(the Sorts of A) (\/) V) = [o, the carrier of S] by MSAFREE:def 9;
A22: Sym(o,V) = [o,the carrier of S] by MSAFREE:def 9;
A23: t = [o,the carrier of S]-tree p by MSAFREE:def 9;
deffunc f(set) = Following(q,height dom t).(p.$1);
consider vp being FinSequence such that
A24: len vp = len p and
A25: for i being Nat st i in dom vp holds vp.i = f(i) from FINSEQ_1:sch 2;
A26: dom vp = Seg len p by A24,FINSEQ_1:def 3;
A27: dom p = Seg len p by FINSEQ_1:def 3;
A28: dom p = dom the_arity_of o by MSATERM:22;
now
let i be Nat;
assume
A29: i in dom p;
then reconsider t = p.i as Term of S,V by MSATERM:22;
reconsider t9 = t as c-Term of A,V by MSATERM:27;
take t9;
the_sort_of t = the_sort_of t9 by Th1;
hence t9 = p.i & the_sort_of t9 = (the_arity_of o).i by A29,MSATERM:23;
end;
then reconsider p9 = p as ArgumentSeq of o,A,V by A28,MSATERM:24;
now
let i be Nat;
assume
A30: i in dom p;
let t being c-Term of A,V;
assume
A31: t = p.i;
then
A32: t in rng p by A30,FUNCT_1:def 3;
then reconsider tt = t as Element of Subtrees X by A13,A14;
reconsider tt as Term of S,V by A1,Th4;
A33: Following(q, 1+height dom t) is_stable_at tt by A7,A32;
A34: Following(q, 1+height dom t).tt = tt@(f, A) by A7,A32;
A35: vp.i = Following(q, height dom ([o,the carrier of S]-tree p)).t
by A23,A25,A26,A27,A30,A31;
A36: i in dom doms p by A30,A31,FUNCT_6:22;
(doms p).i = dom t by A30,A31,FUNCT_6:22;
then dom t in rng doms p by A36,FUNCT_1:def 3;
then height dom t < height tree doms p by TREES_3:78;
then 1+height dom t <= height tree doms p by NAT_1:13;
then consider j being Nat such that
A37: height tree doms p = (1+height dom t)+j by NAT_1:10;
reconsider j as Element of NAT by ORDINAL1:def 12;
Following(q,height dom ([o,the carrier of S]-tree p))
= Following(Following(q,1+height dom t),j) by A15,A37,FACIRC_1:13;
then Following(q,height dom ([o,the carrier of S]-tree p)).t
= Following(q,1+height dom t).t by A33;
hence vp.i = t@f by A34,A35,Def7;
end;
then
A38: (
Sym(o,(the Sorts of A) (\/) V)-tree p9 qua c-Term of A,V)@f = Den( o,A).vp
by A24,MSATERM:43;
now
A39: rng p c= the carrier of X-CircuitStr by A13,FINSEQ_1:def 4;
dom Following(q, height dom t) = the carrier of X-CircuitStr by
CIRCUIT1:3;
hence dom (Following(q, height dom t)*p) = dom p by A39,RELAT_1:27;
let z be object;
assume
A40: z in Seg len p;
then reconsider i = z as Element of NAT;
vp.i = Following(q, height dom t).(p.i) by A25,A26,A40;
hence vp.z = (Following(q, height dom t)*p).z by A27,A40,FUNCT_1:13;
end;
then
A41: vp = Following(q, height dom t)*the_arity_of g by A13,A26,A27,FUNCT_1:2;
Den(g, X-Circuit A) = Den(o,A) by A12,Th16;
then Den(o,A).vp = (Following Following(q,height dom t)).t
by A11,A23,A41,FACIRC_1:10;
hence Following(q,1+height dom ([o,the carrier of S]-tree p)).
([o,the carrier of S]-tree p) = t@f by A21,A22,A38,FACIRC_1:12
.= ([o,the carrier of S]-tree p)@(f, A) by A22,Def7;
end;
thus for t being Term of S,V holds P[t] from MSATERM:sch 1(A2,A6);
end;
theorem
not (ex t being Term of S,V, o being OperSymbol of S st
t in Subtrees X & t.{} = [o,the carrier of S] & the_arity_of o = {}) implies
for s being State of X-Circuit A for f being CompatibleValuation of s
for t being Term of S,V st t in Subtrees X holds
Following(s, height dom t) is_stable_at t &
Following(s, height dom t).t = t@(f, A)
proof
assume
A1: not ex t being Term of S,V, o being OperSymbol of S st
t in Subtrees X & t.{} = [o,the carrier of S] & the_arity_of o = {};
let q be State of X-Circuit A;
let f be CompatibleValuation of q;
A2: X-CircuitStr = ManySortedSign(#Subtrees X,
[:the carrier' of S,{the carrier of S}:]-Subtrees X,
[:the carrier' of S,{the carrier of S}:]-ImmediateSubtrees X,
incl([:the carrier' of S,{the carrier of S}:]-Subtrees X)#);
defpred P[finite DecoratedTree] means $1 in Subtrees X implies
Following(q, height dom $1) is_stable_at $1 &
Following(q, height dom $1).$1 = $1@(f, A);
A3: for s being SortSymbol of S, v being Element of V.s holds
P[root-tree [v,s]]
proof
let s being SortSymbol of S, v being Element of V.s;
assume
A4: root-tree [v,s] in Subtrees X;
then root-tree [v,s] in InputVertices (X-CircuitStr) by Th11;
hence Following(q, height dom root-tree [v,s])
is_stable_at root-tree [v,s] by FACIRC_1:18;
reconsider t = root-tree [v,s] as c-Term of A, V by MSATERM:8;
A5: t is Term of S, V by MSATERM:4;
dom root-tree [v,s] = elementary_tree 0 by TREES_4:3;
hence Following(q,height dom root-tree [v,s]).root-tree [v,s]
= q.root-tree [v,s] by FACIRC_1:11,TREES_1:42
.= f.s.v by A4,Def8
.= (v-term A)@f by MSATERM:42
.= t@f by MSATERM:def 4
.= (root-tree [v,s])@(f, A) by A5,Def7;
end;
A6: for o being OperSymbol of S, p being ArgumentSeq of Sym(o,V)
st for t being Term of S,V st t in rng p holds P[t]
holds P[[o,the carrier of S]-tree p]
proof
let o being OperSymbol of S, p being ArgumentSeq of Sym(o,V) such 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;
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;
A12: g.{} = [o,the carrier of S] by TREES_4:def 4;
g = (g.{})-tree the_arity_of g by Th12;
then
A13: the_arity_of g = p by TREES_4:15;
A14: rng the_arity_of g c= Subtrees X by FINSEQ_1:def 4;
A15: dom ([o,the carrier of S]-tree p) = tree doms p by TREES_4:10;
now
assume height dom ([o,the carrier of S]-tree p) = 0;
then [o,the carrier of S]-tree p = root-tree [o,the carrier of S]
by A12,TREES_1:43,TREES_4:5;
then p = {} by TREES_4:17;
then len p = 0;
then len the_arity_of o = 0 by MSATERM:22;
then
A16: the_arity_of o = {};
g is Term of S,V by Th4;
hence contradiction by A1,A8,A12,A16;
end;
then consider h being Nat such that
A17: height dom ([o,the carrier of S]-tree p) = h+1 by NAT_1:6;
reconsider h as Element of NAT by ORDINAL1:def 12;
now
let x being set;
assume
A18: x in rng the_arity_of g;
then reconsider t = x as Element of Subtrees X by A14;
reconsider t as Term of S,V by A2,Th4;
consider z being object such that
A19: z in dom p and
A20: t = p.z by A13,A18,FUNCT_1:def 3;
A21: z in dom doms p by A19,A20,FUNCT_6:22;
(doms p).z = dom t by A19,A20,FUNCT_6:22;
then dom t in rng doms p by A21,FUNCT_1:def 3;
then height dom t < height tree doms p by TREES_3:78;
then height dom t <= h by A15,A17,NAT_1:13;
then consider i being Nat such that
A22: h = (height dom t)+i by NAT_1:10;
reconsider i as Element of NAT by ORDINAL1:def 12;
Following(q,h) = Following(Following(q,height dom t),i)
by A22,FACIRC_1:13;
hence Following(q,h) is_stable_at x by A7,A13,A18,FACIRC_1:17;
end;
then Following Following(q,h) is_stable_at [o,the carrier of S]-tree p
by A11,FACIRC_1:19;
hence Following(q,height dom ([o,the carrier of S]-tree p))
is_stable_at [o,the carrier of S]-tree p by A17,FACIRC_1:12;
reconsider t = Sym(o,V)-tree p as c-Term of A,V by MSATERM:27;
A23: Sym(o,(the Sorts of A) (\/) V) = [o, the carrier of S] by MSAFREE:def 9;
A24: Sym(o,V) = [o,the carrier of S] by MSAFREE:def 9;
A25: t = [o,the carrier of S]-tree p by MSAFREE:def 9;
deffunc f(set) = Following(q,h).(p.$1);
consider vp being FinSequence such that
A26: len vp = len p and
A27: for i being Nat st i in dom vp holds vp.i = f(i) from FINSEQ_1:sch 2;
A28: dom vp = Seg len p by A26,FINSEQ_1:def 3;
A29: dom p = Seg len p by FINSEQ_1:def 3;
A30: dom p = dom the_arity_of o by MSATERM:22;
now
let i be Nat;
assume
A31: i in dom p;
then reconsider t = p.i as Term of S,V by MSATERM:22;
reconsider t9 = t as c-Term of A,V by MSATERM:27;
take t9;
the_sort_of t = the_sort_of t9 by Th1;
hence t9 = p.i & the_sort_of t9 = (the_arity_of o).i by A31,MSATERM:23;
end;
then reconsider p9 = p as ArgumentSeq of o,A,V by A30,MSATERM:24;
now
let i be Nat;
assume
A32: i in dom p;
let t being c-Term of A,V;
assume
A33: t = p.i;
then
A34: t in rng p by A32,FUNCT_1:def 3;
then reconsider tt = t as Element of Subtrees X by A13,A14;
reconsider tt as Term of S,V by A2,Th4;
A35: Following(q, height dom t) is_stable_at tt by A7,A34;
A36: Following(q, height dom t).tt = tt@(f, A) by A7,A34;
A37: vp.i = Following(q,h).t by A27,A28,A29,A32,A33;
A38: i in dom doms p by A32,A33,FUNCT_6:22;
(doms p).i = dom t by A32,A33,FUNCT_6:22;
then dom t in rng doms p by A38,FUNCT_1:def 3;
then height dom t < height tree doms p by TREES_3:78;
then height dom t <= h by A15,A17,NAT_1:13;
then consider j being Nat such that
A39: h = (height dom t)+j by NAT_1:10;
reconsider j as Element of NAT by ORDINAL1:def 12;
Following(q,h) = Following(Following(q,height dom t),j)
by A39,FACIRC_1:13;
then Following(q,h).t = Following(q,height dom t).t by A35;
hence vp.i = t@f by A36,A37,Def7;
end;
then
A40: (
Sym(o,(the Sorts of A) (\/) V)-tree p9 qua c-Term of A,V)@f = Den( o,A).vp
by A26,MSATERM:43;
now
A41: rng p c= the carrier of X-CircuitStr by A13,FINSEQ_1:def 4;
dom Following(q, h) = the carrier of X-CircuitStr by CIRCUIT1:3;
hence dom (Following(q, h)*p) = dom p by A41,RELAT_1:27;
let z be object;
assume
A42: z in Seg len p;
then reconsider i = z as Element of NAT;
vp.i = Following(q, h).(p.i) by A27,A28,A42;
hence vp.z = (Following(q, h)*p).z by A29,A42,FUNCT_1:13;
end;
then
A43: vp = Following(q, h)*the_arity_of g by A13,A28,A29,FUNCT_1:2;
Den(g, X-Circuit A) = Den(o,A) by A12,Th16;
then Den(o,A).vp = (Following Following(q,h)).t by A11,A25,A43,FACIRC_1:10;
hence Following(q,height dom ([o,the carrier of S]-tree p)).
([o,the carrier of S]-tree p) = t@f by A17,A23,A24,A40,FACIRC_1:12
.= ([o,the carrier of S]-tree p)@(f, A) by A24,Def7;
end;
thus for t being Term of S,V holds P[t] from MSATERM:sch 1(A3,A6);
end;
begin :: <section4>Circuit similarity</section4>
definition
let S1, S2 be non empty ManySortedSign;
let f,g be Function;
pred S1, S2 are_equivalent_wrt f, g means
f is one-to-one & g is one-to-one &
f, g form_morphism_between S1, S2 & f", g" form_morphism_between S2, S1;
end;
theorem Th23:
for S1, S2 being non empty ManySortedSign, f,g being Function
st S1, S2 are_equivalent_wrt f, g
holds the carrier of S2 = f.:the carrier of S1 &
the carrier' of S2 = g.:the carrier' of S1
proof
let S1, S2 be non empty ManySortedSign, f,g be Function such that
A1: f is one-to-one and
A2: g is one-to-one and
A3: f, g form_morphism_between S1, S2 and
A4: f", g" form_morphism_between S2, S1;
thus the carrier of S2 = dom (f") by A4
.= rng f by A1,FUNCT_1:33
.= f.:dom f by RELAT_1:113
.= f.:the carrier of S1 by A3;
thus the carrier' of S2 = dom (g") by A4
.= rng g by A2,FUNCT_1:33
.= g.:dom g by RELAT_1:113
.= g.:the carrier' of S1 by A3;
end;
theorem Th24:
for S1, S2 being non empty ManySortedSign, f,g being Function
st S1, S2 are_equivalent_wrt f, g
holds rng f = the carrier of S2 & rng g = the carrier' of S2
proof
let S1, S2 be non empty ManySortedSign, f,g be Function such that
A1: f is one-to-one and
A2: g is one-to-one and
f, g form_morphism_between S1, S2 and
A3: f", g" form_morphism_between S2, S1;
thus rng f = dom (f") by A1,FUNCT_1:33
.= the carrier of S2 by A3;
thus rng g = dom (g") by A2,FUNCT_1:33
.= the carrier' of S2 by A3;
end;
theorem Th25:
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;
set f = id the carrier of S, g = id the carrier' of S;
thus f is one-to-one;
A1: f" = f by FUNCT_1:45;
g" = g by FUNCT_1:45;
hence thesis by A1,INSTALG1:8;
end;
theorem Th26:
for S1, S2 being non empty ManySortedSign, f,g being Function
st S1, S2 are_equivalent_wrt f, g holds S2, S1 are_equivalent_wrt f", g"
proof
let S1, S2 be non empty ManySortedSign, f,g be Function such that
A1: f is one-to-one and
A2: g is one-to-one and
A3: f, g form_morphism_between S1, S2 and
A4: f", g" form_morphism_between S2, S1;
thus f" is one-to-one & g" is one-to-one by A1,A2;
f" " = f by A1,FUNCT_1:43;
hence thesis by A2,A3,A4,FUNCT_1:43;
end;
theorem Th27:
for S1, S2, S3 being non empty ManySortedSign, f1,g1, f2,g2 being Function
st S1, S2 are_equivalent_wrt f1, g1 & S2, S3 are_equivalent_wrt f2, g2
holds S1, S3 are_equivalent_wrt f2*f1, g2*g1
proof
let S1, S2, S3 be non empty ManySortedSign;
let f1,g1, f2,g2 be Function such that
A1: f1 is one-to-one and
A2: g1 is one-to-one and
A3: f1, g1 form_morphism_between S1, S2 and
A4: f1", g1" form_morphism_between S2, S1 and
A5: f2 is one-to-one and
A6: g2 is one-to-one and
A7: f2, g2 form_morphism_between S2, S3 and
A8: f2", g2" form_morphism_between S3, S2;
thus f2*f1 is one-to-one & g2*g1 is one-to-one by A1,A2,A5,A6;
A9: (f2*f1)" = f1"*f2" by A1,A5,FUNCT_1:44;
(g2*g1)" = g1"*g2" by A2,A6,FUNCT_1:44;
hence thesis by A3,A4,A7,A8,A9,PUA2MSS1:29;
end;
theorem Th28:
for S1, S2 being non empty ManySortedSign, f,g being Function
st S1, S2 are_equivalent_wrt f, g holds
f.:InputVertices S1 = InputVertices S2 &
f.:InnerVertices S1 = InnerVertices S2
proof
let S1, S2 be non empty ManySortedSign, f,g be Function such that
A1: S1, S2 are_equivalent_wrt f, g;
A2: f is one-to-one by A1;
A3: f, g form_morphism_between S1, S2 by A1;
A4: rng g = the carrier' of S2 by A1,Th24;
A5: dom the ResultSort of S2 = the carrier' of S2 by FUNCT_2:def 1;
A6: f.:rng the ResultSort of S1 = rng (f*the ResultSort of S1) by RELAT_1:127
.= rng ((the ResultSort of S2)*g) by A3
.= rng the ResultSort of S2 by A4,A5,RELAT_1:28;
thus f.:InputVertices S1 = f.:(the carrier of S1) \ f.:
rng the ResultSort of S1 by A2,FUNCT_1:64
.= InputVertices S2 by A1,A6,Th23;
thus thesis by A6;
end;
definition
let S1, S2 be non empty ManySortedSign;
pred S1, S2 are_equivalent means
ex f,g being one-to-one Function st S1, S2 are_equivalent_wrt f, g;
reflexivity
proof
let S be non empty ManySortedSign;
take id the carrier of S, id the carrier' of S;
thus thesis by Th25;
end;
symmetry
by Th26;
end;
theorem
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;
given f1,g1 be one-to-one Function such that
A1: S1, S2 are_equivalent_wrt f1, g1;
given f2,g2 be one-to-one Function such that
A2: S2, S3 are_equivalent_wrt f2, g2;
take f2*f1, g2*g1;
thus thesis by A1,A2,Th27;
end;
definition
let S1, S2 be non empty ManySortedSign;
let f be Function;
pred f preserves_inputs_of S1, S2 means
f.:InputVertices S1 c= InputVertices S2;
end;
theorem Th30:
for S1, S2 being non empty ManySortedSign
for f, g being Function st f, g form_morphism_between S1, S2
for v being Vertex of S1 holds f.v is Vertex of S2
proof
let S1, S2 be non empty ManySortedSign;
let f, g be Function;
assume that
A1: dom f = the carrier of S1 and dom g = the carrier' of S1 and
A2: rng f c= the carrier of S2;
now
let v be Vertex of S1;
f.v in rng f by A1,FUNCT_1:def 3;
hence f.v in the carrier of S2 by A2;
end;
hence thesis;
end;
theorem Th31:
for S1, S2 being non empty non void ManySortedSign
for f, g being Function st f, g form_morphism_between S1, S2
for v being Gate of S1 holds g.v is Gate of S2
proof
let S1, S2 be non empty non void ManySortedSign;
let f, g be Function;
assume that
dom f = the carrier of S1 and
A1: dom g = the carrier' of S1 and rng f c= the carrier of S2 and
A2: rng g c= the carrier' of S2;
now
let v be Gate of S1;
g.v in rng g by A1,FUNCT_1:def 3;
hence g.v in the carrier' of S2 by A2;
end;
hence thesis;
end;
theorem Th32:
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;
let f, g be Function;
assume f, g form_morphism_between S1, S2;
then f*the ResultSort of S1 = (the ResultSort of S2)*g;
then f.:InnerVertices S1 = rng ((the ResultSort of S2)*g) by RELAT_1:127;
hence thesis by RELAT_1:26;
end;
theorem Th33:
for S1, S2 being Circuit-like non void non empty ManySortedSign
for f, g being Function st f, g form_morphism_between S1, S2
for v1 being Vertex of S1 st v1 in InnerVertices S1
for v2 being Vertex of S2 st v2 = f.v1 holds action_at v2 = g.action_at v1
proof
let S1, S2 be Circuit-like non void non empty ManySortedSign;
let f,g be Function such that
A1: f, g form_morphism_between S1, S2;
let v1 be Vertex of S1 such that
A2: v1 in InnerVertices S1;
let v2 be Vertex of S2 such that
A3: v2 = f.v1;
reconsider g1 = g.action_at v1 as Gate of S2 by A1,Th31;
A4: dom g = the carrier' of S1 by A1;
A5: dom f = the carrier of S1 by A1;
A6: dom the ResultSort of S1 = the carrier' of S1 by FUNCT_2:def 1;
A7: f.:InnerVertices S1 c= InnerVertices S2 by A1,Th32;
A8: v2 in f.:InnerVertices S1 by A2,A3,A5,FUNCT_1:def 6;
the_result_sort_of g1 =
((the ResultSort of S2)*g).action_at v1 by A4,FUNCT_1:13
.= (f*the ResultSort of S1).action_at v1 by A1
.= f.(the_result_sort_of action_at v1) by A6,FUNCT_1:13
.= v2 by A2,A3,MSAFREE2:def 7;
hence thesis by A7,A8,MSAFREE2:def 7;
end;
definition
let S1, S2 be non empty ManySortedSign;
let f,g be Function;
let C1 be non-empty MSAlgebra over S1;
let C2 be non-empty MSAlgebra over S2;
pred f, g form_embedding_of C1, C2 means
f is one-to-one & g is one-to-one & f, g form_morphism_between S1, S2 &
the Sorts of C1 = (the Sorts of C2)*f &
the Charact of C1 = (the Charact of C2)*g;
end;
theorem Th34:
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;
let C be non-empty MSAlgebra over S;
thus id the carrier of S is one-to-one;
A1: dom the Sorts of C = the carrier of S by PARTFUN1:def 2;
dom the Charact of C = the carrier' of S by PARTFUN1:def 2;
hence thesis by A1,INSTALG1:8,RELAT_1:52;
end;
theorem Th35:
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
by PUA2MSS1:29,RELAT_1:36;
definition
let S1, S2 be non empty ManySortedSign;
let f,g be Function;
let C1 be non-empty MSAlgebra over S1;
let C2 be non-empty MSAlgebra over S2;
pred C1, C2 are_similar_wrt f, g means
f, g form_embedding_of C1, C2 & f", g" form_embedding_of C2, C1;
end;
theorem Th36:
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;
let f,g be Function;
let C1 be non-empty MSAlgebra over S1;
let C2 be non-empty MSAlgebra over S2;
assume that
A1: f is one-to-one and
A2: g is one-to-one and
A3: f, g form_morphism_between S1, S2 and the Sorts of C1 = (the Sorts of C2)*f
and the Charact of C1 = (the Charact of C2)*g
and f" is one-to-one
and g" is one-to-one and
A4: f", g" form_morphism_between S2, S1;
thus thesis by A1,A2,A3,A4;
end;
theorem Th37:
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;
let f,g be Function;
let C1 be non-empty MSAlgebra over S1;
let C2 be non-empty MSAlgebra over S2;
hereby
assume
A1: C1, C2 are_similar_wrt f, g;
hence S1, S2 are_equivalent_wrt f, g by Th36;
f, g form_embedding_of C1, C2 by A1;
hence the Sorts of C1 = (the Sorts of C2)*f &
the Charact of C1 = (the Charact of C2)*g;
end;
assume that
A2: f is one-to-one and
A3: g is one-to-one and
A4: f, g form_morphism_between S1, S2 and
A5: f", g" form_morphism_between S2, S1 and
A6: the Sorts of C1 = (the Sorts of C2)*f and
A7: the Charact of C1 = (the Charact of C2)*g;
thus
f is one-to-one & g is one-to-one & f, g form_morphism_between S1, S2 &
the Sorts of C1 = (the Sorts of C2)*f &
the Charact of C1 = (the Charact of C2)*g by A2,A3,A4,A6,A7;
thus f" is one-to-one & g" is one-to-one by A2,A3;
thus f", g" form_morphism_between S2, S1 by A5;
dom (f") = the carrier of S2 by A5;
then rng f = the carrier of S2 by A2,FUNCT_1:33;
then f*(f") = id the carrier of S2 by A2,FUNCT_1:39
.= id dom the Sorts of C2 by PARTFUN1:def 2;
hence the Sorts of C2 = (the Sorts of C2)*(f*f") by RELAT_1:52
.= (the Sorts of C1)*f" by A6,RELAT_1:36;
dom (g") = the carrier' of S2 by A5;
then rng g = the carrier' of S2 by A3,FUNCT_1:33;
then g*(g") = id the carrier' of S2 by A3,FUNCT_1:39
.= id dom the Charact of C2 by PARTFUN1:def 2;
hence the Charact of C2 = (the Charact of C2)*(g*g") by RELAT_1:52
.= (the Charact of C1)*g" by A7,RELAT_1:36;
end;
theorem
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;
let C be non-empty MSAlgebra over S;
set f = id the carrier of S, g = id the carrier' of S;
A1: f" = f by FUNCT_1:45;
g" = g by FUNCT_1:45;
hence f, g form_embedding_of C, C & f", g" form_embedding_of C, C by A1,Th34;
end;
theorem Th39:
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;
let f,g be Function;
let C1 be non-empty MSAlgebra over S1;
let C2 be non-empty MSAlgebra over S2;
assume that
A1: f, g form_embedding_of C1, C2 and
A2: f", g" form_embedding_of C2, C1;
A3: f is one-to-one by A1;
f" " = f by A3,FUNCT_1:43;
hence f", g" form_embedding_of C2, C1 &
f" ", g" " form_embedding_of C1, C2 by A1,A2,FUNCT_1:43;
end;
theorem
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;
let f1,g1, f2,g2 be Function;
let C1 be non-empty MSAlgebra over S1;
let C2 be non-empty MSAlgebra over S2;
let C3 be non-empty MSAlgebra over S3;
assume that
A1: f1, g1 form_embedding_of C1, C2 and
A2: f1", g1" form_embedding_of C2, C1 and
A3: f2, g2 form_embedding_of C2, C3 and
A4: f2", g2" form_embedding_of C3, C2;
thus f2*f1, g2*g1 form_embedding_of C1, C3 by A1,A3,Th35;
A5: f1 is one-to-one by A1;
A6: g1 is one-to-one by A1;
A7: f2 is one-to-one by A3;
A8: g2 is one-to-one by A3;
A9: (f2*f1)" = f1"*f2" by A5,A7,FUNCT_1:44;
(g2*g1)" = g1"*g2" by A6,A8,FUNCT_1:44;
hence thesis by A2,A4,A9,Th35;
end;
definition
let S1, S2 be non empty ManySortedSign;
let C1 be non-empty MSAlgebra over S1;
let C2 be non-empty MSAlgebra over S2;
pred C1, C2 are_similar means
ex f, g being Function st C1, C2 are_similar_wrt f, g;
end;
reserve G1, G2 for Circuit-like non void non empty ManySortedSign,
f, g for Function,
C1 for non-empty Circuit of G1,
C2 for non-empty Circuit of G2;
theorem Th41:
f, g form_embedding_of C1, C2 implies
dom f = the carrier of G1 & rng f c= the carrier of G2 &
dom g = the carrier' of G1 & rng g c= the carrier' of G2
proof
assume that f is one-to-one and g is one-to-one and
A1: dom f = the carrier of G1 and
A2: dom g = the carrier' of G1 and
A3: rng f c= the carrier of G2 and
A4: rng g c= the carrier' of G2;
thus thesis by A1,A2,A3,A4;
end;
theorem Th42:
f, g form_embedding_of C1, C2 implies
for o1 being Gate of G1, o2 being Gate of G2 st o2 = g.o1
holds Den(o2, C2) = Den(o1, C1)
proof
assume that f is one-to-one and g is one-to-one and
A1: f, g form_morphism_between G1, G2 and
the Sorts of C1 = (the Sorts of C2)*f and
A2: the Charact of C1 = (the Charact of C2)*g;
let o1 be Gate of G1, o2 be Gate of G2 such that
A3: o2 = g.o1;
dom g = the carrier' of G1 by A1;
hence thesis by A2,A3,FUNCT_1:13;
end;
theorem Th43:
f, g form_embedding_of C1, C2 implies
for o1 being Gate of G1, o2 being Gate of G2 st o2 = g.o1
for s1 being State of C1, s2 being State of C2 st s1 = s2*f
holds o2 depends_on_in s2 = o1 depends_on_in s1
proof
assume that f is one-to-one and g is one-to-one and
A1: f, g form_morphism_between G1, G2 and
the Sorts of C1 = (the Sorts of C2)*f and
the Charact of C1 = (the Charact of C2)*g;
let o1 be Gate of G1, o2 be Gate of G2 such that
A2: o2 = g.o1;
let s1 be State of C1, s2 be State of C2 such that
A3: s1 = s2*f;
thus o2 depends_on_in s2 = s2*the_arity_of o2 by CIRCUIT1:def 3
.= s2*(f*the_arity_of o1) by A1,A2
.= s1*the_arity_of o1 by A3,RELAT_1:36
.= o1 depends_on_in s1 by CIRCUIT1:def 3;
end;
theorem Th44:
f, g form_embedding_of C1, C2 implies
for s being State of C2 holds s*f is State of C1
proof
set S1 = G1, S2 = G2;
assume that f is one-to-one and g is one-to-one and
A1: f, g form_morphism_between S1, S2 and
A2: the Sorts of C1 = (the Sorts of C2)*f and
the Charact of C1 = (the Charact of C2)*g;
let s be State of C2;
A3: dom the Sorts of C2 = the carrier of S2 by PARTFUN1:def 2;
A4: dom the Sorts of C1 = the carrier of S1 by PARTFUN1:def 2;
A5: dom s = dom the Sorts of C2 by CARD_3:9;
A6: rng f c= the carrier of S2 by A1;
A7: dom f = the carrier of S1 by A1;
then
A8: dom (s*f) = the carrier of S1 by A3,A5,A6,RELAT_1:27;
now
let x be object;
assume
A9: x in the carrier of S1;
then
A10: f.x in rng f by A7,FUNCT_1:def 3;
(s*f).x = s.(f.x) by A7,A9,FUNCT_1:13;
then (s*f).x in (the Sorts of C2).(f.x) by A3,A6,A10,CARD_3:9;
hence (s*f).x in (the Sorts of C1).x by A2,A7,A9,FUNCT_1:13;
end;
hence thesis by A4,A8,CARD_3:9;
end;
theorem Th45:
f, g form_embedding_of C1, C2 implies
for s2 being State of C2, s1 being State of C1 st s1 = s2*f &
for v being Vertex of G1 st v in InputVertices G1 holds s2 is_stable_at f.v
holds Following s1 = (Following s2)*f
proof
assume
A1: f, g form_embedding_of C1, C2;
then
A2: f, g form_morphism_between G1, G2;
let s2 be State of C2, s1 be State of C1 such that
A3: s1 = s2*f and
A4: for v being Vertex of G1 st v in InputVertices G1
holds s2 is_stable_at f.v;
reconsider s29 = (Following s2)*f as State of C1 by A1,Th44;
A5: dom f = the carrier of G1 by A2;
now
let v be Vertex of G1;
A6: s29.v = (Following s2).(f.v) by A5,FUNCT_1:13;
reconsider fv = f.v as Vertex of G2 by A2,Th30;
hereby
assume v in InputVertices G1;
then
A7: s2 is_stable_at f.v by A4;
Following(s2, 1) = Following s2 by FACIRC_1:14;
hence s29.v = s2.(f.v) by A6,A7
.= s1.v by A3,A5,FUNCT_1:13;
end;
A8: f.:InnerVertices G1 c= InnerVertices G2 by A2,Th32;
assume
A9: v in InnerVertices G1;
then
A10: fv in f.:InnerVertices G1 by A5,FUNCT_1:def 6;
A11: action_at fv = g.action_at v by A2,A9,Th33;
thus s29.v = (Den(action_at fv, C2)).(action_at fv depends_on_in s2)
by A6,A8,A10,CIRCUIT2:def 5
.= (Den(action_at v, C1)).(action_at fv depends_on_in s2) by A1,A11,Th42
.= (Den(action_at v,C1)).(action_at v depends_on_in s1)
by A1,A3,A11,Th43;
end;
hence thesis by CIRCUIT2:def 5;
end;
theorem Th46:
f, g form_embedding_of C1, C2 & f preserves_inputs_of G1, G2 implies
for s2 being State of C2, s1 being State of C1 st s1 = s2*f
holds Following s1 = (Following s2)*f
proof
assume that
A1: f, g form_embedding_of C1, C2 and
A2: f.:InputVertices G1 c= InputVertices G2;
let s2 be State of C2, s1 be State of C1 such that
A3: s1 = s2*f;
A4: dom f = the carrier of G1 by A1,Th41;
now
let v be Vertex of G1;
assume v in InputVertices G1;
then f.v in f.:InputVertices G1 by A4,FUNCT_1:def 6;
hence s2 is_stable_at f.v by A2,FACIRC_1:18;
end;
hence thesis by A1,A3,Th45;
end;
theorem Th47:
f, g form_embedding_of C1, C2 & f preserves_inputs_of G1, G2 implies
for s2 being State of C2, s1 being State of C1 st s1 = s2*f
for n being Nat holds Following(s1,n) = Following(s2,n)*f
proof
assume that
A1: f, g form_embedding_of C1, C2 and
A2: f preserves_inputs_of G1, G2;
let s2 be State of C2, s1 be State of C1 such that
A3: s1 = s2*f;
defpred P[Nat] means Following(s1,$1) = Following(s2,$1)*f;
Following(s1,0) = s1 by FACIRC_1:11;
then
A4: P[ 0 ] by A3,FACIRC_1:11;
A5: now
let n be Nat;
assume P[n];
then Following Following(s1,n) = (Following Following(s2,n))*f
by A1,A2,Th46;
then Following(s1,n+1) = (Following Following(s2,n))*f by FACIRC_1:12
.= Following(s2,n+1)*f by FACIRC_1:12;
hence P[n+1];
end;
thus for n be Nat holds P[n] from NAT_1:sch 2(A4,A5);
end;
theorem
f, g form_embedding_of C1, C2 & f preserves_inputs_of G1, G2 implies
for s2 being State of C2, s1 being State of C1 st s1 = s2*f
holds s2 is stable implies s1 is stable
by Th46;
theorem Th49:
f, g form_embedding_of C1, C2 & f preserves_inputs_of G1, G2 implies
for s2 being State of C2, s1 being State of C1 st s1 = s2*f
for v1 being Vertex of G1 holds s1 is_stable_at v1 iff s2 is_stable_at f.v1
proof
assume that
A1: f, g form_embedding_of C1, C2 and
A2: f preserves_inputs_of G1, G2;
let s2 be State of C2, s1 be State of C1 such that
A3: s1 = s2*f;
let v1 be Vertex of G1;
A4: f,g form_morphism_between G1,G2 by A1;
then
A5: dom f = the carrier of G1;
reconsider v2 = f.v1 as Vertex of G2 by A4,Th30;
thus s1 is_stable_at v1 implies s2 is_stable_at f.v1
proof
assume
A6: for n being Nat holds (Following(s1,n)).v1 = s1.v1;
let n be Nat;
Following(s1,n) = Following(s2,n)*f by A1,A2,A3,Th47;
hence (Following(s2,n)).(f.v1) = (Following(s1,n)).v1 by A5,FUNCT_1:13
.= s1.v1 by A6
.= s2.(f.v1) by A3,A5,FUNCT_1:13;
end;
assume
A7: for n being Nat holds (Following(s2,n)).(f.v1) = s2.(f.v1);
let n be Nat;
Following(s1,n) = Following(s2,n)*f by A1,A2,A3,Th47;
hence (Following(s1,n)).v1 = (Following(s2,n)).v2 by A5,FUNCT_1:13
.= s2.v2 by A7
.= s1.v1 by A3,A5,FUNCT_1:13;
end;
theorem
C1, C2 are_similar_wrt f, g implies
for s being State of C2 holds s*f is State of C1
by Th44;
theorem Th51:
C1, C2 are_similar_wrt f, g implies
for s1 being State of C1, s2 being State of C2
holds s1 = s2*f iff s2 = s1*f"
proof
assume that
A1: f, g form_embedding_of C1, C2 and
A2: f", g" form_embedding_of C2, C1;
A3: f is one-to-one by A1;
let s1 be State of C1;
let s2 be State of C2;
f, g form_morphism_between G1, G2 by A1;
then
A4: dom f = the carrier of G1;
A5: dom s1 = the carrier of G1 by CIRCUIT1:3;
A6: s1*f"*f = s1*(f"*f) by RELAT_1:36
.= s1*id dom f by A3,FUNCT_1:39
.= s1 by A4,A5,RELAT_1:52;
f", g" form_morphism_between G2, G1 by A2;
then
A7: dom (f") = the carrier of G2;
A8: dom s2 = the carrier of G2 by CIRCUIT1:3;
s2*f*(f") = s2*(f*(f")) by RELAT_1:36
.= s2*((f" ")*(f")) by A3,FUNCT_1:43
.= s2*id dom (f") by A3,FUNCT_1:39;
hence thesis by A6,A7,A8,RELAT_1:52;
end;
theorem Th52:
C1, C2 are_similar_wrt f, g implies f.:InputVertices G1 = InputVertices G2 &
f.:InnerVertices G1 = InnerVertices G2
proof
assume C1, C2 are_similar_wrt f, g;
then G1, G2 are_equivalent_wrt f, g by Th36;
hence thesis by Th28;
end;
theorem Th53:
C1, C2 are_similar_wrt f, g implies f preserves_inputs_of G1, G2
by Th52;
theorem Th54:
C1, C2 are_similar_wrt f, g implies
for s1 being State of C1, s2 being State of C2 st s1 = s2*f
holds Following s1 = (Following s2)*f
by Th46,Th53;
theorem Th55:
C1, C2 are_similar_wrt f, g implies
for s1 being State of C1, s2 being State of C2 st s1 = s2*f
for n being Element of NAT holds Following(s1,n) = Following(s2,n)*f
by Th47,Th53;
theorem
C1, C2 are_similar_wrt f, g implies
for s1 being State of C1, s2 being State of C2 st s1 = s2*f
holds s1 is stable iff s2 is stable
proof
assume
A1: C1, C2 are_similar_wrt f, g;
then
A2: C2, C1 are_similar_wrt f", g" by Th39;
let s1 be State of C1, s2 be State of C2 such that
A3: s1 = s2*f;
A4: s2 = s1*f" by A1,A3,Th51;
thus s1 is stable implies s2 is stable
by A2,A4,Th54;
assume s2 = Following s2;
hence s1 = Following s1 by A1,A3,Th54;
end;
theorem
C1, C2 are_similar_wrt f, g implies
for s1 being State of C1, s2 being State of C2 st s1 = s2*f
for v1 being Vertex of G1 holds s1 is_stable_at v1 iff s2 is_stable_at f.v1
proof
assume
A1: C1, C2 are_similar_wrt f, g;
then
A2: C2, C1 are_similar_wrt f", g" by Th39;
let s1 be State of C1, s2 be State of C2 such that
A3: s1 = s2*f;
let v1 be Vertex of G1;
A4: G1, G2 are_equivalent_wrt f, g by A1,Th37;
then
A5: f,g form_morphism_between G1,G2;
A6: f",g" form_morphism_between G2,G1 by A4;
A7: dom f = the carrier of G1 by A5;
A8: dom (f") = the carrier of G2 by A6;
reconsider v2 = f.v1 as Vertex of G2 by A5,Th30;
f is one-to-one by A4;
then
A9: v1 = f".v2 by A7,FUNCT_1:34;
thus s1 is_stable_at v1 implies s2 is_stable_at f.v1
proof
assume
A10: for n being Nat holds (Following(s1,n)).v1 = s1.v1;
let n be Nat;
n in NAT by ORDINAL1:def 12;
then Following(s1,n) = Following(s2,n)*f by A1,A3,Th55;
hence (Following(s2,n)).(f.v1) = (Following(s1,n)).v1 by A7,FUNCT_1:13
.= s1.v1 by A10
.= s2.(f.v1) by A3,A7,FUNCT_1:13;
end;
assume
A11: for n being Nat holds (Following(s2,n)).(f.v1) = s2.(f.v1);
let n be Nat;
A12: n in NAT by ORDINAL1:def 12;
s2 = s1*f" by A1,A3,Th51;
then Following(s2,n) = Following(s1,n)*f" by A2,A12,Th55;
hence (Following(s1,n)).v1 = (Following(s2,n)).v2 by A8,A9,FUNCT_1:13
.= s2.v2 by A11
.= s1.v1 by A3,A7,FUNCT_1:13;
end;
begin :: <section5>Term specification</section5>
definition
let S be non empty non void ManySortedSign;
let A be non-empty MSAlgebra over S;
let V be non-empty ManySortedSet of the carrier of S;
let X be non empty Subset of S-Terms V;
let G be Circuit-like non void non empty ManySortedSign;
let C be non-empty Circuit of G;
pred C calculates X, A means
ex f, g st f, g form_embedding_of X-Circuit A, C &
f preserves_inputs_of X-CircuitStr, G;
pred X, A specifies C means
C, X-Circuit A are_similar;
end;
definition
let S be non empty non void ManySortedSign;
let V be non-empty ManySortedSet of the carrier of S;
let A be non-empty MSAlgebra over S;
let X be non empty Subset of S-Terms V;
let G be Circuit-like non void non empty ManySortedSign;
let C be non-empty Circuit of G;
assume C calculates X, A;
then consider f, g such that
A1: f, g form_embedding_of X-Circuit A, C and
A2: f preserves_inputs_of X-CircuitStr, G;
mode SortMap of X, A, C -> one-to-one Function means
:
Def17: it preserves_inputs_of X-CircuitStr, G &
ex g st it, g form_embedding_of X-Circuit A, C;
existence by A1,A2;
end;
definition
let S be non empty non void ManySortedSign;
let V be non-empty ManySortedSet of the carrier of S;
let A be non-empty MSAlgebra over S;
let X be non empty Subset of S-Terms V;
let G be Circuit-like non void non empty ManySortedSign;
let C be non-empty Circuit of G such that
A1: C calculates X, A;
let f be SortMap of X, A, C;
consider g such that
A2: f, g form_embedding_of X-Circuit A, C by A1,Def17;
mode OperMap of X, A, C, f -> one-to-one Function means
f, it form_embedding_of X-Circuit A, C;
existence by A2;
end;
theorem Th58:
for G being Circuit-like non void non empty ManySortedSign
for C being non-empty Circuit of G st X, A specifies C
holds C calculates X, A
proof
let G be Circuit-like non void non empty ManySortedSign;
let C be non-empty Circuit of G;
given f, g being Function such that
A1: C, X-Circuit A are_similar_wrt f, g;
take f", g";
thus f", g" form_embedding_of X-Circuit A, C by A1;
X-Circuit A, C are_similar_wrt f", g" by A1,Th39;
hence thesis by Th53;
end;
theorem Th59:
for G being Circuit-like non void non empty ManySortedSign
for C being non-empty Circuit of G st C calculates X, A
for f being SortMap of X, A, C for t being Term of S,V st t in Subtrees X
for s being State of C holds Following(s, 1+height dom t) is_stable_at f.t &
for s9 being State of X-Circuit A st s9 = s*f
for h being CompatibleValuation of s9
holds Following(s, 1+height dom t).(f.t) = t@(h, A)
proof
let G be Circuit-like non void non empty ManySortedSign;
let C be non-empty Circuit of G such that
A1: C calculates X, A;
let f be SortMap of X, A, C;
consider g such that
A2: f, g form_embedding_of X-Circuit A, C by A1,Def17;
A3: f preserves_inputs_of X-CircuitStr, G by A1,Def17;
A4: f, g form_morphism_between X-CircuitStr, G by A2;
let t be Term of S,V such that
A5: t in Subtrees X;
let s be State of C;
reconsider s9 = s*f as State of X-Circuit A by A2,Th44;
reconsider t9 = t as Vertex of X-CircuitStr by A5;
A6: Following(s9, 1+height dom t) is_stable_at t9 by Th21;
A7: Following(s9, 1+height dom t) = Following(s, 1+height dom t)*f by A2,A3
,Th47;
hence Following(s, 1+height dom t) is_stable_at f.t by A2,A3,A6,Th49;
let s9 be State of X-Circuit A such that
A8: s9 = s*f;
let h be CompatibleValuation of s9;
A9: dom f = the carrier of X-CircuitStr by A4;
Following(s9, 1+height dom t).t9 = t@(h,A) by Th21;
hence thesis by A7,A8,A9,FUNCT_1:13;
end;
theorem Th60:
for G being Circuit-like non void non empty ManySortedSign
for C being non-empty Circuit of G st C calculates X, A
for t being Term of S,V st t in Subtrees X ex v being Vertex of G st
for s being State of C holds Following(s, 1+height dom t) is_stable_at v &
ex f being SortMap of X, A, C st
for s9 being State of X-Circuit A st s9 = s*f
for h being CompatibleValuation of s9
holds Following(s, 1+height dom t).v = t@(h, A)
proof
let G be Circuit-like non void non empty ManySortedSign;
let C be non-empty Circuit of G;
assume
A1: C calculates X, A;
then consider f, g such that
A2: f, g form_embedding_of X-Circuit A, C and
A3: f preserves_inputs_of X-CircuitStr, G;
reconsider f as SortMap of X, A, C by A1,A2,A3,Def17;
let t be Term of S,V such that
A4: t in Subtrees X;
A5: f, g form_morphism_between X-CircuitStr, G by A2;
reconsider t9 = t as Vertex of X-CircuitStr by A4;
reconsider v = f.t9 as Vertex of G by A5,Th30;
take v;
let s be State of C;
thus Following(s, 1+height dom t) is_stable_at v by A1,Th59;
take f;
thus thesis by A1,Th59;
end;
theorem
for G being Circuit-like non void non empty ManySortedSign
for C being non-empty Circuit of G st X, A specifies C
for f being SortMap of X, A, C
for s being State of C, t being Term of S,V st t in Subtrees X
holds Following(s, 1+height dom t) is_stable_at f.t &
for s9 being State of X-Circuit A st s9 = s*f
for h being CompatibleValuation of s9
holds Following(s, 1+height dom t).(f.t) = t@(h, A)
proof
let G be Circuit-like non void non empty ManySortedSign;
let C be non-empty Circuit of G;
assume X, A specifies C;
then C calculates X, A by Th58;
hence thesis by Th59;
end;
theorem
for G being Circuit-like non void non empty ManySortedSign
for C being non-empty Circuit of G st X, A specifies C
for t being Term of S,V st t in Subtrees X ex v being Vertex of G st
for s being State of C holds Following(s, 1+height dom t) is_stable_at v &
ex f being SortMap of X, A, C st
for s9 being State of X-Circuit A st s9 = s*f
for h being CompatibleValuation of s9
holds Following(s, 1+height dom t).v = t@(h, A) by Th58,Th60;