Copyright (c) 2001 Association of Mizar Users
environ
vocabulary AMI_1, MSUALG_1, ZF_REFLE, MSATERM, FUNCT_1, TREES_4, FREEALG,
RELAT_1, BOOLE, PBOOLE, TREES_9, CIRCCOMB, MSAFREE2, TREES_1, FINSEQ_1,
QC_LANG1, TREES_3, FINSET_1, TREES_2, PARTFUN1, FUNCT_4, MCART_1,
PRALG_1, TDGROUP, CARD_3, PRE_CIRC, FACIRC_1, FUNCT_6, PUA2MSS1,
ISOCAT_1, CQC_SIM1, CIRCUIT1, CIRCUIT2, CIRCTRM1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, NAT_1,
RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSET_1, PARTFUN1, MCART_1,
FUNCT_4, CARD_3, STRUCT_0, PRALG_1, PBOOLE, MSUALG_1, PRE_CIRC, MSAFREE2,
CIRCUIT1, CIRCUIT2, CIRCCOMB, FACIRC_1, TREES_1, TREES_2, TREES_3,
TREES_4, TREES_9, MSATERM, PUA2MSS1;
constructors TREES_9, MSATERM, FINSEQ_4, MSUALG_3, CIRCUIT1, CIRCUIT2,
FACIRC_1, PUA2MSS1, INSTALG1;
clusters ARYTM_3, SUBSET_1, STRUCT_0, PRELAMB, FUNCT_1, RELSET_1, FINSEQ_1,
MSUALG_1, MSUALG_2, TREES_2, TREES_3, XBOOLE_0, TREES_9, PRALG_1,
MSAFREE, MSATERM, PRE_CIRC, CIRCCOMB, INSTALG1, MEMBERED;
requirements NUMERALS, BOOLE, SUBSET;
definitions TARSKI, PARTFUN1, PRALG_1, PBOOLE, MSUALG_1, PRE_CIRC, MSAFREE2,
CIRCUIT2, CIRCCOMB, PUA2MSS1, FACIRC_1, XBOOLE_0;
theorems TARSKI, ZFMISC_1, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1,
PARTFUN1, FUNCT_4, FUNCT_6, MCART_1, PBOOLE, MSUALG_1, MSAFREE2,
PRE_CIRC, AMI_1, CARD_3, TREES_1, TREES_2, TREES_3, TREES_4, TREES_9,
MSAFREE, MSATERM, CIRCUIT1, CIRCUIT2, CIRCCOMB, FACIRC_1, PUA2MSS1,
INSTALG1, XBOOLE_0;
schemes NAT_1, FINSEQ_1, ZFREFLE1, MSUALG_1, MSATERM, PRALG_2, COMPTS_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 t' being Term of S,V, T being c-Term of A,V
st t' = $1 & T = t' holds the_sort_of T = the_sort_of t';
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 t = root-tree [v,s] & T = t;
then the_sort_of t = s & the_sort_of T = s by MSATERM:14,16;
hence thesis;
end;
A2: 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;
let p being ArgumentSeq of Sym(o,V); assume
for t' being Term of S,V st t' in rng p
for t being Term of S,V, T being c-Term of A,V
st t = t' & 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 A3: 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 A3,MSATERM:17;
end;
for t being Term of S,V holds P[t] from TermInd(A1,A2);
hence thesis;
end;
definition let D be non empty set;
let X be Subset of D;
redefine func id X -> Function of X, D;
correctness
proof
dom id X = X & rng id X = X & X c= D by RELAT_1:71;
hence thesis by FUNCT_2:4;
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;
func X-CircuitStr -> non empty strict ManySortedSign equals:
Def1:
ManySortedSign(#
Subtrees X, [:the OperSymbols of S,{the carrier of S}:]-Subtrees X,
[:the OperSymbols of S,{the carrier of S}:]-ImmediateSubtrees X,
id ([:the OperSymbols of S,{the carrier of S}:]-Subtrees X)
#);
correctness;
end;
definition
let S be non empty non void ManySortedSign;
let V be non-empty ManySortedSet of the carrier of S;
let X be non empty Subset of S-Terms V;
cluster X-CircuitStr -> unsplit;
coherence
proof
X-CircuitStr = ManySortedSign(#
Subtrees X, [:the OperSymbols of S,{the carrier of S}:]-Subtrees X,
[:the OperSymbols of S,{the carrier of S}:]-ImmediateSubtrees X,
id ([:the OperSymbols of S,{the carrier of S}:]-Subtrees X)
#) by Def1;
hence the ResultSort of X-CircuitStr = id the OperSymbols of X-CircuitStr;
end;
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 Th2:
X-CircuitStr is void iff
for t being Element of X holds t is root &
not t.{} in [:the OperSymbols of S, {the carrier of S}:]
proof set C = [:the OperSymbols of S,{the carrier of S}:];
A1: C-Subtrees X is empty iff for t holds t is root & not t.{} in C
by TREES_9:26;
X-CircuitStr = ManySortedSign(# Subtrees X, C-Subtrees X,
C-ImmediateSubtrees X, id(C-Subtrees X)#) by Def1;
hence thesis by A1,MSUALG_1:def 5;
end;
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 OperSymbols of S, {the carrier of S}:]
by MSATERM:def 6;
hence X-CircuitStr is non void by A1,Th2;
end;
assume X-CircuitStr is non void;
then consider t such that
A2: t is not root or t.{} in [:the OperSymbols of S, {the carrier of S}:]
by Th2;
t in X;
then t is CompoundTerm of S,V by A2,MSATERM:28,def 6;
hence thesis by MSATERM:def 7;
end;
definition
let S be non empty non void ManySortedSign;
let V be non-empty ManySortedSet of the carrier of S;
let X be SetWithCompoundTerm of S,V;
cluster 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 OperSymbols of X-CircuitStr holds
s is CompoundTerm of S,V)
proof set C = [:the OperSymbols of S, {the carrier of S}:];
A1: X-CircuitStr = ManySortedSign(# Subtrees X, C-Subtrees X,
C-ImmediateSubtrees X, id(C-Subtrees X)#) by Def1;
hereby let v be Vertex of X-CircuitStr;
consider t being Element of X, p being Node of t such that
A2: v = t|p by A1,TREES_9:20;
t in X;
hence v is Term of S,V by A2,MSATERM:29;
end;
let s be set; assume s in the OperSymbols of X-CircuitStr;
then consider t being Element of X, p being Node of t such that
A3: s = t|p & (not p in Leaves dom t or t.p in C) by A1,TREES_9:25;
t in X;
then reconsider s as Term of S,V by A3,MSATERM:29;
reconsider e = {} as Node of t|p by TREES_1:47;
dom (t|p) = (dom t qua Tree)|(p qua FinSequence of NAT) & p = p^e
by FINSEQ_1:47,TREES_2:def 11;
then t.p = s.e & (p in Leaves dom t iff s is root)
by A3,TREES_2:def 11,TREES_9:6;
hence thesis by A3,MSATERM:28,def 6;
end;
theorem Th5:
for t being Vertex of X-CircuitStr holds
t in the OperSymbols of X-CircuitStr iff t is CompoundTerm of S,V
proof let t being Vertex of X-CircuitStr;
thus t in the OperSymbols of X-CircuitStr implies t is CompoundTerm of S,V
by Th4;
set C = [:the OperSymbols of S, {the carrier of S}:];
A1: X-CircuitStr = ManySortedSign(# Subtrees X, C-Subtrees X,
C-ImmediateSubtrees X, id(C-Subtrees X)#) by Def1;
then consider tt being Element of X, p being Node of tt such that
A2: t = tt|p by TREES_9:20;
assume t is CompoundTerm of S,V;
then reconsider t' = t as CompoundTerm of S,V;
t'.{} in C & p^(<*>NAT) = p & {} in (dom tt)|p
by FINSEQ_1:47,MSATERM:def 6,TREES_1:47;
then tt.p in C by A2,TREES_2:def 11;
hence t in the OperSymbols of X-CircuitStr by A1,A2,TREES_9:25;
end;
theorem Th6:
for X being SetWithCompoundTerm of S,V, g being Gate of X-CircuitStr holds
(the ResultSort of X-CircuitStr).g = g & the_result_sort_of g = g
proof set C = [:the OperSymbols of S, {the carrier of S}:];
let X be SetWithCompoundTerm of S,V;
let g be Gate of X-CircuitStr;
X-CircuitStr = ManySortedSign(# Subtrees X, C-Subtrees X,
C-ImmediateSubtrees X, id(C-Subtrees X)#) by Def1;
hence (the ResultSort of X-CircuitStr).g = g by FUNCT_1:35;
hence the_result_sort_of g = g by MSUALG_1:def 7;
end;
definition
let S,V;
let X be SetWithCompoundTerm of S,V, g be Gate of X-CircuitStr;
cluster the_arity_of g -> DTree-yielding;
coherence
proof set C = [:the OperSymbols of S,{the carrier of S}:];
X-CircuitStr = ManySortedSign(# Subtrees X, C-Subtrees X,
C-ImmediateSubtrees X, id(C-Subtrees X)#) by Def1;
then the_arity_of g is FinSequence of Subtrees X;
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;
cluster -> finite Function-like Relation-like Vertex of X-CircuitStr;
coherence by Th4;
end;
definition
let S be non empty non void ManySortedSign;
let V be non-empty ManySortedSet of the carrier of S;
let X be non empty Subset of S-Terms V;
cluster -> DecoratedTree-like Vertex of X-CircuitStr;
coherence by Th4;
end;
definition
let S be non empty non void ManySortedSign;
let V be non-empty ManySortedSet of the carrier of S;
let X be SetWithCompoundTerm of S,V;
cluster -> finite Function-like Relation-like Gate of X-CircuitStr;
coherence by Th4;
end;
definition
let S be non empty non void ManySortedSign;
let V be non-empty ManySortedSet of the carrier of S;
let X be SetWithCompoundTerm of S,V;
cluster -> DecoratedTree-like Gate of X-CircuitStr;
coherence by Th4;
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 Th7:
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 OperSymbols of S, {the carrier of S}:];
A1: t1-CircuitStr = ManySortedSign(#Subtrees t1, C-Subtrees t1,
C-ImmediateSubtrees t1, id (C-Subtrees t1)#) &
t2-CircuitStr = ManySortedSign(#Subtrees t2, C-Subtrees t2,
C-ImmediateSubtrees t2, id (C-Subtrees t2)#)
by Def1;
A2: dom (C-ImmediateSubtrees t1) = C-Subtrees t1 &
dom id (C-Subtrees t1) = C-Subtrees t1 &
dom (C-ImmediateSubtrees t2) = C-Subtrees t2 &
dom id (C-Subtrees t2) = C-Subtrees t2 by FUNCT_2:def 1;
hereby let x be set; assume
x in (dom the Arity of t1-CircuitStr) /\ dom the Arity of t2-CircuitStr
;
then A3: x in dom the Arity of t1-CircuitStr &
x in dom the Arity of t2-CircuitStr by XBOOLE_0:def 3;
then reconsider u = x as Element of Subtrees t1 by A1,A2;
(C-ImmediateSubtrees t1).x in (Subtrees t1)* by A1,A2,A3,FUNCT_2:7;
then reconsider y1 = (the Arity of t1-CircuitStr).x as
FinSequence of Subtrees t1 by A1,FINSEQ_1:def 11;
(the Arity of t2-CircuitStr).x in (Subtrees t2)*
by A1,A2,A3,FUNCT_2:7;
then reconsider y2 = (the Arity of t2-CircuitStr).x as
FinSequence of Subtrees t2 by FINSEQ_1:def 11;
now
hereby let t be Element of t1; t in t1;
then t is Term of S,V;
hence t is finite;
end;
hereby let t be Element of t2; t in t2;
then t is Term of S,V;
hence t is finite;
end;
end;
then u = (u.{})-tree y1 & u = (u.{})-tree y2 by A1,A2,A3,TREES_9:def 13;
hence (the Arity of t1-CircuitStr).x = (the Arity of t2-CircuitStr).x
by TREES_4:15;
end;
let x be set; assume
x in (dom the ResultSort of t1-CircuitStr) /\
dom the ResultSort of t2-CircuitStr;
then A4: x in dom the ResultSort of t1-CircuitStr &
x in dom the ResultSort of t2-CircuitStr by XBOOLE_0:def 3;
hence (the ResultSort of t1-CircuitStr).x = x by A1,A2,FUNCT_1:35
.= (the ResultSort of t2-CircuitStr).x by A1,A2,A4,FUNCT_1:35;
end;
definition
let X,Y be constituted-DTrees set;
cluster X \/ Y -> constituted-DTrees;
coherence by TREES_3:9;
end;
theorem Th8:
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 set;
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:20;
t in X1 or t in X2 by XBOOLE_0:def 2;
then x in Subtrees X1 or x in Subtrees X2 by A1,TREES_9:20;
hence x in (Subtrees X1) \/ (Subtrees X2) by XBOOLE_0:def 2;
end;
let x be set; assume A2:x in (Subtrees X1) \/ (Subtrees X2);
per cases by A2,XBOOLE_0:def 2;
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:20;
t is Element of X1 \/ X2 by XBOOLE_0:def 2;
hence x in Subtrees (X1 \/ X2) by A3,TREES_9:20;
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:20;
t is Element of X1 \/ X2 by XBOOLE_0:def 2;
hence x in Subtrees (X1 \/ X2) by A4,TREES_9:20;
end;
theorem Th9:
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 set;
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 & (not n in Leaves dom t or t.n in C) by TREES_9:25;
t in X1 or t in X2 by XBOOLE_0:def 2;
then x in C-Subtrees X1 or x in C-Subtrees X2 by A1,TREES_9:25;
hence x in (C-Subtrees X1) \/ (C-Subtrees X2) by XBOOLE_0:def 2;
end;
let x be set; assume A2:x in (C-Subtrees X1) \/ (C-Subtrees X2);
per cases by A2,XBOOLE_0:def 2;
suppose x in C-Subtrees X1;
then consider t being Element of X1, n being Node of t such that
A3: x = t|n & (not n in Leaves dom t or t.n in C) by TREES_9:25;
t is Element of X1 \/ X2 by XBOOLE_0:def 2;
hence x in C-Subtrees (X1 \/ X2) by A3,TREES_9:25;
suppose x in C-Subtrees X2;
then consider t being Element of X2, n being Node of t such that
A4: x = t|n & (not n in Leaves dom t or t.n in C) by TREES_9:25;
t is Element of X1 \/ X2 by XBOOLE_0:def 2;
hence x in C-Subtrees (X1 \/ X2) by A4,TREES_9:25;
end;
theorem Th10:
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 2;
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 & dom f1 = C-Subtrees X1 & dom f2 = C-Subtrees X2
by FUNCT_2:def 1;
A5: C-Subtrees X = (C-Subtrees X1) \/ (C-Subtrees X2) by Th9;
now let x be set; assume
A6: x in dom f1 \/ dom f2;
then reconsider t = x as Element of Subtrees X by A4,A5;
f.x in (Subtrees X)* by A4,A5,A6,FUNCT_2:7;
then reconsider p = f.x as FinSequence of Subtrees X by FINSEQ_1:def 11;
hereby assume
A7: x in dom f2;
then f2.x in (Subtrees X2)* by A4,FUNCT_2:7;
then reconsider p2 = f2.x as FinSequence of Subtrees X2 by FINSEQ_1:def
11;
t = (t.{})-tree p & t = (t.{})-tree p2 by A2,A3,A4,A5,A6,A7,TREES_9:
def 13;
hence f.x = f2.x by TREES_4:15;
end;
assume not x in dom f2;
then A8: x in dom f1 by A6,XBOOLE_0:def 2;
then f1.x in (Subtrees X1)* by A4,FUNCT_2:7;
then reconsider p1 = f1.x as FinSequence of Subtrees X1 by FINSEQ_1:def 11
;
t = (t.{})-tree p & t = (t.{})-tree p1 by A1,A3,A4,A5,A6,A8,TREES_9:def
13;
hence f.x = f1.x by TREES_4:15;
end;
hence thesis by A4,A5,FUNCT_4:def 1;
end;
theorem Th11:
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 OperSymbols of S,{the carrier of S}:];
A1: X-CircuitStr = ManySortedSign(#
Subtrees X, C-Subtrees X, C-ImmediateSubtrees X, id (C-Subtrees X)#)
by Def1;
A2: X1-CircuitStr = ManySortedSign(#
Subtrees X1, C-Subtrees X1, C-ImmediateSubtrees X1, id (C-Subtrees X1)#)
by Def1;
A3: X2-CircuitStr = ManySortedSign(#
Subtrees X2, C-Subtrees X2, C-ImmediateSubtrees X2, id (C-Subtrees X2)#)
by Def1;
A4: Subtrees X = (Subtrees X1) \/ Subtrees X2 by Th8;
A5: C-Subtrees X = (C-Subtrees X1) \/ (C-Subtrees X2) by Th9;
now
hereby let t be Element of X1; t in X1;
then t is Term of S,V;
hence t is finite;
end;
hereby let t be Element of X2; t in X2;
then t is Term of S,V;
hence t is finite;
end;
end;
then A6: C-ImmediateSubtrees X = (C-ImmediateSubtrees X1)+*(C
-ImmediateSubtrees X2)
by Th10;
id (C-Subtrees X) = (id (C-Subtrees X1))+*id (C-Subtrees X2)
by A5,FUNCT_4:23;
hence thesis by A1,A2,A3,A4,A5,A6,CIRCCOMB:def 2;
end;
theorem Th12:
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;
set C = [:the OperSymbols of S, {the carrier of S}:];
the ResultSort of G = id the OperSymbols of G by CIRCCOMB:def 7;
then rng the ResultSort of G = the OperSymbols of G by RELAT_1:71;
then A1: InputVertices G = (the carrier of G) \ the OperSymbols of G
by MSAFREE2:def 2;
A2: X-CircuitStr = ManySortedSign(# Subtrees X, C-Subtrees X,
C-ImmediateSubtrees X, id(C-Subtrees X)#) by Def1;
let x be set;
hereby assume A3:x in InputVertices (X-CircuitStr);
then A4: x in the carrier of G & not x in the OperSymbols of G by A1,XBOOLE_0
:def 4;
thus x in Subtrees X by A2,A3;
reconsider t = x as Term of S,V by A3,Th4;
(ex s being SortSymbol of S, v being Element of V.s st t.{} = [v,s])
or t.{} in [:the OperSymbols 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
A5: t.{} = [v,s] by A4,Th5;
take s; reconsider v as Element of V.s; take v;
thus x = root-tree [v,s] by A5,MSATERM:5;
end;
assume
A6: x in Subtrees X;
given s being SortSymbol of S, v being Element of V.s such that
A7: x = root-tree [v,s];
assume not thesis;
then x in the OperSymbols of G by A1,A2,A6,XBOOLE_0:def 4;
then reconsider t = x as CompoundTerm of S,V by Th4;
t.{} = [v,s] by A7,TREES_4:3;
then [v,s] in [:the OperSymbols of S,{the carrier of S}:] by MSATERM:def 6
;
then s = the carrier of S by ZFMISC_1:129;
then s in s;
hence contradiction;
end;
theorem Th13:
for X being SetWithCompoundTerm of S,V, g being Gate of X-CircuitStr
holds g = (g.{})-tree the_arity_of g
proof set C = [:the OperSymbols of S, {the carrier of S}:];
let X be SetWithCompoundTerm of S,V;
let g be Gate of X-CircuitStr;
A1: X-CircuitStr = ManySortedSign(# Subtrees X, C-Subtrees X,
C-ImmediateSubtrees X, id(C-Subtrees X)#) by Def1;
then reconsider p = (C-ImmediateSubtrees X).g as Element of (Subtrees X)*
by FUNCT_2:7;
reconsider p as FinSequence of Subtrees X by FINSEQ_1:def 11;
A2: now let t be Element of X; t in X;
then t is Term of S,V;
hence t is finite;
end;
reconsider f = g as Term of S,V by Th4;
g = (f.{})-tree p by A1,A2,TREES_9:def 13;
hence thesis by A1,MSUALG_1:def 6;
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;
reconsider u = v as Term of S,V by Th4;
func the_sort_of (v, A) 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; assume
A1: not thesis;
then S1 = (the Sorts of A).the_sort_of u &
S2 = (the Sorts of A).the_sort_of u;
hence thesis by A1;
end;
existence
proof take (the Sorts of A).the_sort_of u;
thus 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 v be Vertex of X-CircuitStr;
let A be non-empty MSAlgebra over S;
reconsider u = v as Term of S,V by Th4;
cluster the_sort_of (v, A) -> non empty;
coherence
proof 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
X is SetWithCompoundTerm of S,V;
then reconsider X' = X as SetWithCompoundTerm of S,V;
let o be Gate of X-CircuitStr; reconsider o' = o as Gate of X'-CircuitStr;
let A be MSAlgebra over S;
func the_action_of (o, A) -> Function means:
Def3:
for X' being SetWithCompoundTerm of S,V st X' = X
for o' being Gate of X'-CircuitStr st o' = o holds
it = (the Charact of A).(o'.{})`1;
uniqueness
proof let f1, f2 be Function; assume
A1: not thesis;
then f1 = (the Charact of A).(o'.{})`1 &
f1 = (the Charact of A).(o'.{})`1;
hence thesis by A1;
end;
existence
proof
take (the Charact of A).(o'.{})`1; thus thesis;
end;
end;
scheme MSFuncEx {I() -> non empty set, A,B() -> non-empty ManySortedSet of I(),
P[set,set,set]}:
ex f being ManySortedFunction of A(),B() st
for i being Element of I(), a being Element of A().i holds P[i,a,f.i.a]
provided
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]
proof
defpred R[set,set] 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 set st i in I() ex y being set st R[i,y]
proof let i be set; assume i in I();
then reconsider i as Element of I();
defpred R[set,set] means P[i,$1,$2];
A3: for a being set st a in A().i ex b being set st b in B().i & R[a,b]
proof let a be set; assume a in A().i;
then ex b being Element of B().i 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 set st a in A().i holds R[a,g.a]
from NonUniqBoundFuncEx(A3);
take g;
g is Function of A().i, B().i by A4,FUNCT_2:4;
hence thesis by A5;
end;
consider f being Function such that
A6: dom f = I() and
A7: for i being set st i in I() holds R[i,f.i] from NonUniqFuncEx(A2);
reconsider f as ManySortedSet of I() by A6,PBOOLE:def 3;
f is ManySortedFunction of A(),B()
proof let i be set; 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 P[i,a,f.i.a];
end;
definition
let S be non empty non void ManySortedSign;
let V be non-empty ManySortedSet of the carrier of S;
let X be non empty Subset of S-Terms V;
let A be 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 set; 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 by PBOOLE:3;
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 LambdaDMS;
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;
cluster X-CircuitSorts A -> non-empty;
coherence
proof
let i be set; 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 Th14:
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;
set C = [:the OperSymbols of S, {the carrier of S}:];
t-CircuitStr = ManySortedSign(# Subtrees t, C-Subtrees t,
C-ImmediateSubtrees t, id(C-Subtrees t)#) by Def1;
then reconsider ag = the_arity_of g as FinSequence of Subtrees t;
A1: g = (f.{})-tree ag by Th13;
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 & a = ag by A1,A2,MSATERM:22,TREES_4:15;
then A4: dom the_arity_of o = Seg len a & dom the_arity_of g = Seg len a &
dom a = Seg len a by FINSEQ_1:def 3;
A5: rng the_arity_of g c= the carrier of t-CircuitStr &
rng the_arity_of o c= the carrier of S by FINSEQ_1:def 4;
dom (X-CircuitSorts A) = the carrier of X-CircuitStr &
dom the Sorts of A = the carrier of S by PBOOLE:def 3;
then A6: dom ((X-CircuitSorts A)*the_arity_of g) = Seg len a &
dom ((the Sorts of A)*the_arity_of o) = Seg len a by A4,A5,RELAT_1:46;
now let i be set; assume
A7: i in Seg len a;
then reconsider j = i as Nat;
ag.i in rng the_arity_of g by A4,A7,FUNCT_1:def 5;
then reconsider v = ag.j as Vertex of t-CircuitStr by A5;
(the_arity_of o).i in rng the_arity_of o by A4,A7,FUNCT_1:def 5;
then reconsider s = (the_arity_of o).j as SortSymbol of S by A5;
reconsider u = v as Term of S,V by A3,A4,A7,MSATERM:22;
A8: the_sort_of u = s by A3,A4,A7,MSATERM:23;
A9: ((t-CircuitSorts A)*the_arity_of g).i = (t-CircuitSorts A).v &
((the Sorts of A)*the_arity_of o).i = (the Sorts of A).s
by A6,A7,FUNCT_1:22;
hence ((t-CircuitSorts A)*the_arity_of g).i
= the_sort_of (v, A) by Def4
.= ((the Sorts of A)*the_arity_of o).i by A8,A9,Def2;
end;
hence thesis by A6,FUNCT_1:9;
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 OperSymbols 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 OperSymbols of X-CircuitStr
holds C1.o = the_action_of (o, A) and
A2: for o being Gate of X-CircuitStr st o in the OperSymbols of X-CircuitStr
holds C2.o = the_action_of (o, A);
now let x be set; assume
A3: x in the OperSymbols of X-CircuitStr;
then reconsider o = x as Gate of X-CircuitStr;
C1.o = the_action_of (o, A) & C2.o = the_action_of (o, A) by A1,A2,A3;
hence C1.x = C2.x;
end;
hence thesis by PBOOLE:3;
end;
existence
proof
defpred P[set,set] means ex g being Gate of X-CircuitStr st g = $1 &
$2 = the_action_of (g, A);
A4: now let x be set; assume x in the OperSymbols of X-CircuitStr;
then reconsider g = x as Gate of X-CircuitStr;
reconsider y = the_action_of (g, A) as set;
take y;
thus P[x,y];
end;
consider CHARACT being ManySortedSet of the OperSymbols of X-CircuitStr
such that
A5: for x being set st x in the OperSymbols of X-CircuitStr
holds P[x,CHARACT.x] from MSSEx(A4);
A6: dom CHARACT = the OperSymbols of X-CircuitStr by PBOOLE:def 3;
CHARACT is Function-yielding
proof let x be set; 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 OperSymbols 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; assume
A7: i in the OperSymbols of X-CircuitStr;
then X-CircuitStr is not void by MSUALG_1:def 5;
then reconsider X' = X as SetWithCompoundTerm of S,V by Th3;
reconsider g = i as Gate of X'-CircuitStr by A7;
A8: the_result_sort_of g = g by Th6;
then reconsider v = g as Vertex of X'-CircuitStr;
reconsider I = i as CompoundTerm of S,V by A7,Th4;
I.{} in [:the OperSymbols of S,{the carrier of S}:]
by MSATERM:def 6;
then consider o,y being set such that
A9: o in the OperSymbols of S & y in {the carrier of S} & I.{} = [o,y]
by ZFMISC_1:103;
reconsider o as OperSymbol of S by A9;
A10: o = (I.{})`1 by A9,MCART_1:7;
A11: y = the carrier of S & g.{} = [o,y] 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 A12: CHARACT.i = the_action_of (g, A)
.= (the Charact of A).o by A10,Def3;
A13: ((the Sorts of A)*the ResultSort of S).o
= (the Sorts of A).((the ResultSort of S).o) by FUNCT_2:21
.= (the Sorts of A).(the_result_sort_of o) by MSUALG_1:def 7
.= (the Sorts of A).(the_sort_of I) by A11,MSATERM:17;
A14: ((X-CircuitSorts A)*the ResultSort of X-CircuitStr).g
= (X-CircuitSorts A).((the ResultSort of X'-CircuitStr).g)
by FUNCT_2:21
.= (X-CircuitSorts A).(the_result_sort_of g) by MSUALG_1:def 7
.= the_sort_of (v, A) by A8,Def4
.= (the Sorts of A).the_sort_of I by Def2;
A15: ((X-CircuitSorts A)#*the Arity of X-CircuitStr).g
= (X-CircuitSorts A)#.((the Arity of X'-CircuitStr).g)
by FUNCT_2:21
.= (X-CircuitSorts A)#.(the_arity_of g) by MSUALG_1:def 6
.= product ((X'-CircuitSorts A)*the_arity_of g) by MSUALG_1:def 3
.= product ((the Sorts of A)*the_arity_of o) by A11,Th14;
((the Sorts of A)#*the Arity of S).o
= (the Sorts of A)#.((the Arity of S).o) by FUNCT_2:21
.= (the Sorts of A)#.the_arity_of o by MSUALG_1:def 6
.= product ((the Sorts of A)*the_arity_of o) by MSUALG_1:def 3;
hence thesis by A12,A13,A14,A15,MSUALG_1:def 2;
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 OperSymbols 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:
Def6:
MSAlgebra(#X-CircuitSorts A, X-CircuitCharact A#);
correctness
proof set C = MSAlgebra(#X-CircuitSorts A, X-CircuitCharact A#);
C is non-empty proof thus the Sorts of C is non-empty; end;
hence thesis;
end;
end;
theorem
for v being Vertex of X-CircuitStr
holds (the Sorts of X-Circuit A).v = the_sort_of (v, A)
proof let v be Vertex of X-CircuitStr;
X-Circuit A = MSAlgebra(#X-CircuitSorts A, X-CircuitCharact A#) by Def6;
hence thesis by Def4;
end;
theorem Th16:
for A being locally-finite non-empty MSAlgebra over S
for X being SetWithCompoundTerm of S,V
for g being OperSymbol of X-CircuitStr
holds Den(g, X-Circuit A) = the_action_of (g, A)
proof let A being locally-finite non-empty MSAlgebra over S;
let X being SetWithCompoundTerm of S,V;
let g being OperSymbol of X-CircuitStr;
X-Circuit A = MSAlgebra(#X-CircuitSorts A, X-CircuitCharact A#) by Def6;
hence Den(g, X-Circuit A) = (X-CircuitCharact A).g by MSUALG_1:def 11
.= the_action_of (g, A) by Def5;
end;
theorem Th17:
for A being locally-finite non-empty MSAlgebra over S
for X being SetWithCompoundTerm of S,V
for g being OperSymbol of X-CircuitStr, o being OperSymbol of S
st g.{} = [o, the carrier of S]
holds Den(g, X-Circuit A) = Den(o,A)
proof let A being locally-finite non-empty MSAlgebra over S;
let X being SetWithCompoundTerm of S,V;
let g being OperSymbol of X-CircuitStr, o being OperSymbol of S;
A1: Den(o, A) = (the Charact of A).o by MSUALG_1:def 11;
Den(g, X-Circuit A) = the_action_of (g, A) by Th16
.= (the Charact of A).(g.{})`1 by Def3;
hence thesis by A1,MCART_1:7;
end;
theorem Th18:
for A being locally-finite non-empty MSAlgebra over S,
X being non empty Subset of S-Terms V holds
X-Circuit A is locally-finite
proof let A be locally-finite non-empty MSAlgebra over S;
let t be non empty Subset of S-Terms V;
let i be set; 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 locally-finite by MSAFREE2:def 11;
t-Circuit A = MSAlgebra(#t-CircuitSorts A, t-CircuitCharact A#)
by Def6;
then (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,PRE_CIRC:def 3;
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 locally-finite non-empty MSAlgebra over S;
cluster X-Circuit A -> locally-finite;
coherence by Th18;
end;
theorem Th19:
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 Th7;
A1: X1-Circuit A = MSAlgebra(#X1-CircuitSorts A, X1-CircuitCharact A#) &
X2-Circuit A = MSAlgebra(#X2-CircuitSorts A, X2-CircuitCharact A#) by Def6;
thus the Sorts of X1-Circuit A tolerates the Sorts of X2-Circuit A
proof let x be set; assume
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 & x in dom the Sorts of
X2-Circuit A
by XBOOLE_0:def 3;
then A3: x in the carrier of X1-CircuitStr & x in the carrier of X2
-CircuitStr
by PBOOLE:def 3;
reconsider v1 = x as Vertex of X1-CircuitStr by A2,PBOOLE:def 3;
reconsider v2 = x as Vertex of X2-CircuitStr by A2,PBOOLE:def 3;
reconsider t = x as Term of S,V by A3,Th4;
thus (the Sorts of X1-Circuit A).x
= the_sort_of (v1, A) by A1,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 A1,Def4;
end;
let x be set; assume
x in (dom the Charact of X1-Circuit A) /\ dom the Charact of X2-Circuit A
;
then A4:x in dom the Charact of X1-Circuit A & x in dom the Charact of X2
-Circuit A
by XBOOLE_0:def 3;
then reconsider g1 = x as Gate of X1-CircuitStr by PBOOLE:def 3;
reconsider g2 = x as Gate of X2-CircuitStr by A4,PBOOLE:def 3;
thus (the Charact of X1-Circuit A).x
= the_action_of (g1, A) by A1,Def5
.= (the Charact of A).(g1.{})`1 by Def3
.= the_action_of (g2, A) by Def3
.= (the Charact of X2-Circuit A).x by A1,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 2;
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;
C1 tolerates C2 by Th19;
then A2: the Sorts of C1 tolerates the Sorts of C2 &
the Charact of C1 tolerates the Charact of C2 by CIRCCOMB:def 3;
then A3: the Sorts of C1+*C2 = (the Sorts of C1) +* (the Sorts of C2) &
the Charact of C1+*C2 = (the Charact of C1) +* (the Charact of C2)
by CIRCCOMB:def 4;
A4: X-CircuitStr = X1-CircuitStr+*(X2-CircuitStr) by Th11;
C1 tolerates C & C2 tolerates C by Th19;
then the Sorts of C1 tolerates the Sorts of C &
the Sorts of C2 tolerates the Sorts of C &
the Charact of C1 tolerates the Charact of C &
the Charact of C2 tolerates the Charact of C by CIRCCOMB:def 3;
then A5: the Sorts of C1+*C2 tolerates the Sorts of C &
the Charact of C1+*C2 tolerates the Charact of C by A2,A3,CIRCCOMB:5;
dom the Sorts of C1+*C2 = the carrier of X-CircuitStr &
dom the Charact of C1+*C2 = the OperSymbols of X-CircuitStr
by A4,PBOOLE:def 3;
then dom the Charact of C1+*C2 = dom the Charact of C &
dom the Sorts of C1+*C2 = dom the Sorts of C by PBOOLE:def 3;
then the Charact of C1+*C2 = the Charact of C &
the Sorts of C1+*C2 = the Sorts of C by A5,PARTFUN1:136;
hence thesis by Th11;
end;
begin :: <section3>Correctness of a Term Circuit</section3>
reserve S for non empty non void ManySortedSign,
A for non-empty locally-finite MSAlgebra over S,
V for Variables of A,
X for SetWithCompoundTerm of S,V;
definition
let S be non empty non void ManySortedSign;
let A be non-empty MSAlgebra over S;
let V be Variables of A;
let t be DecoratedTree such that A1: t is Term of S,V;
let f be ManySortedFunction of V, the Sorts of A;
func t@(f,A) means:
Def7:
ex t' being c-Term of A,V st t' = t & it = t'@f;
correctness
proof reconsider t' = t as c-Term of A,V by A1,MSATERM:27;
t'@f = t'@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 locally-finite MSAlgebra over S;
let s be State of X-Circuit A;
set C = [:the OperSymbols of S, {the carrier of S}:];
A1: X-CircuitStr = ManySortedSign(# Subtrees X, C-Subtrees X,
C-ImmediateSubtrees X, id(C-Subtrees X)#) by Def1;
A2: X-CircuitA = MSAlgebra(#X-CircuitSortsA,X-CircuitCharactA#) by Def6;
defpred P[set,set,set] means
root-tree [$2,$1] in Subtrees X implies $3 = s.root-tree [$2,$1];
A3: 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;
suppose root-tree [v,x] in Subtrees X;
then reconsider a = root-tree [v,x] as Vertex of X-CircuitStr by A1;
reconsider t = a as Term of S,V by MSATERM:4;
the_sort_of t = x &
the_sort_of (a, A) = (the Sorts of A).the_sort_of t &
(X-CircuitSorts A).a = the_sort_of (a, A) &
s.a in (the Sorts of X-Circuit A).a
by Def2,Def4,CIRCUIT1:5,MSATERM:14;
then reconsider b = s.a as Element of (the Sorts of A).x by A2;
take b;
thus thesis;
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(A3);
end;
end;
theorem
for s being State of X-Circuit A
for f being CompatibleValuation of s, n being Nat
holds f is CompatibleValuation of Following(s,n)
proof let s being State of X-Circuit A;
let f being CompatibleValuation of s, n being 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 Th12;
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 thesis by A1,Def8;
end;
definition
let x be set;
let S be non empty non void ManySortedSign;
let V be non-empty ManySortedSet of the carrier of S;
let p be FinSequence of S-Terms V;
cluster x-tree p -> finite;
coherence
proof
reconsider q = doms p as FinTree-yielding FinSequence;
dom (x-tree p) = tree q by TREES_4:10;
hence thesis by AMI_1:21;
end;
end;
theorem Th22:
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 OperSymbols of S,{the carrier of S}:]-Subtrees X,
[:the OperSymbols of S,{the carrier of S}:]-ImmediateSubtrees X,
id ([:the OperSymbols of S,{the carrier of S}:]-Subtrees X)#)
by Def1;
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;
A4: root-tree [v,s] in InputVertices (X-CircuitStr) by A3,Th12;
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] 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;
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:20;
<*>NAT in (dom tt)|n & n^{} = n by FINSEQ_1:47,TREES_1:47;
then tt.n = (tt|n).{} by TREES_2:def 11
.= [o,the carrier of S] by A9,TREES_4:def 4;
then tt.n in [:the OperSymbols of S,{the carrier of S}:]
by ZFMISC_1:129;
then reconsider g = [o,the carrier of S]-tree p as Gate of X-CircuitStr
by A1,A9,TREES_9:25;
A10: the_result_sort_of g = (the ResultSort of X-CircuitStr).g
by MSUALG_1:def 7
.= (id the OperSymbols of X-CircuitStr).g by CIRCCOMB:def 7
.= g by FUNCT_1:34;
A11: g.{} = [o,the carrier of S] by TREES_4:def 4;
g = (g.{})-tree the_arity_of g by Th13;
then A12: the_arity_of g = p by TREES_4:15;
A13: rng the_arity_of g c= Subtrees X by A1,FINSEQ_1:def 4;
A14: dom ([o,the carrier of S]-tree p) = tree doms p by TREES_4:10;
now let x being set; assume
A15: x in rng the_arity_of g;
then reconsider t = x as Element of Subtrees X by A13;
reconsider t as Term of S,V by A1,Th4;
A16: Following(q, 1+height dom t) is_stable_at t &
Following(q,1+height dom t).t = t@(f, A) by A7,A12,A15;
consider z being set such that
A17: z in dom p & t = p.z by A12,A15,FUNCT_1:def 5;
z in dom doms p & (doms p).z = dom t by A17,FUNCT_6:31;
then dom t in rng doms p by FUNCT_1:def 5;
then height dom t < height tree doms p by TREES_3:81;
then 1+height dom t <= height tree doms p by NAT_1:38;
then consider i being Nat such that
A18: height tree doms p = (1+height dom t)+i by NAT_1:28;
Following(q,height dom ([o,the carrier of S]-tree p))
= Following(Following(q,1+height dom t),i) by A14,A18,FACIRC_1:13;
hence Following(q,height dom ([o,the carrier of S]-tree p))
is_stable_at x by 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 A10,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;
A19: Sym(o,(the Sorts of A) \/ V) = [o, the carrier of S] &
Sym(o,V) = [o,the carrier of S] by MSAFREE:def 11;
A20: t = [o,the carrier of S]-tree p by MSAFREE:def 11;
deffunc f(set) = Following(q,height dom t).(p.$1);
consider vp being FinSequence such that
A21: len vp = len p and
A22: for i being Nat st i in Seg len p holds vp.i = f(i) from SeqLambda;
A23: dom vp = Seg len p & dom p = Seg len p by A21,FINSEQ_1:def 3;
A24: dom p = dom the_arity_of o by MSATERM:22;
now let i being Nat; assume
A25: i in dom p;
then reconsider t = p.i as Term of S,V by MSATERM:22;
reconsider t' = t as c-Term of A,V by MSATERM:27;
take t';
the_sort_of t = the_sort_of t' by Th1;
hence t' = p.i & the_sort_of t' = (the_arity_of o).i by A25,MSATERM:23;
end;
then reconsider p' = p as ArgumentSeq of o,A,V by A24,MSATERM:24;
now let i being Nat; assume
A26: i in dom p;
let t being c-Term of A,V; assume
A27: t = p.i;
then A28: t in rng p by A26,FUNCT_1:def 5;
then reconsider tt = t as Element of Subtrees X by A12,A13;
reconsider tt as Term of S,V by A1,Th4;
A29: Following(q, 1+height dom t) is_stable_at tt &
Following(q, 1+height dom t).tt = tt@(f, A) by A7,A28;
A30: vp.i = Following(q, height dom ([o,the carrier of S]-tree p)).t
by A20,A22,A23,A26,A27;
i in dom doms p & (doms p).i = dom t by A26,A27,FUNCT_6:31;
then dom t in rng doms p by FUNCT_1:def 5;
then height dom t < height tree doms p by TREES_3:81;
then 1+height dom t <= height tree doms p by NAT_1:38;
then consider j being Nat such that
A31: height tree doms p = (1+height dom t)+j by NAT_1:28;
Following(q,height dom ([o,the carrier of S]-tree p))
= Following(Following(q,1+height dom t),j) by A14,A31,FACIRC_1:13;
then Following(q,height dom ([o,the carrier of S]-tree p)).t
= Following(q,1+height dom t).t by A29,FACIRC_1:def 9;
hence vp.i = t@f by A29,A30,Def7;
end;
then A32: (Sym(o,(the Sorts of A) \/ V)-tree p' qua c-Term of A,V)@f = Den(
o,A).vp
by A21,MSATERM:43;
now
rng p c= the carrier of X-CircuitStr &
dom Following(q, height dom t) = the carrier of X-CircuitStr
by A12,CIRCUIT1:4,FINSEQ_1:def 4;
hence dom (Following(q, height dom t)*p) = dom p by RELAT_1:46;
let z be set; assume
A33: z in Seg len p; then reconsider i = z as Nat;
vp.i = Following(q, height dom t).(p.i) by A22,A33;
hence vp.z = (Following(q, height dom t)*p).z by A23,A33,FUNCT_1:23;
end;
then A34: vp = Following(q, height dom t)*the_arity_of g by A12,A23,FUNCT_1:9;
Den(g, X-Circuit A) = Den(o,A) by A11,Th17;
then Den(o,A).vp = (Following Following(q,height dom t)).t
by A10,A20,A34,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 A19,A32,FACIRC_1:12
.= ([o,the carrier of S]-tree p)@(f, A) by A19,Def7;
end;
thus for t being Term of S,V holds P[t] from TermInd(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 OperSymbols of S,{the carrier of S}:]-Subtrees X,
[:the OperSymbols of S,{the carrier of S}:]-ImmediateSubtrees X,
id ([:the OperSymbols of S,{the carrier of S}:]-Subtrees X)#)
by Def1;
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 Th12;
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:79
.= 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:20;
<*>NAT in (dom tt)|n & n^{} = n by FINSEQ_1:47,TREES_1:47;
then tt.n = (tt|n).{} by TREES_2:def 11
.= [o,the carrier of S] by A9,TREES_4:def 4;
then tt.n in [:the OperSymbols of S,{the carrier of S}:]
by ZFMISC_1:129;
then reconsider g = [o,the carrier of S]-tree p as Gate of X-CircuitStr
by A2,A9,TREES_9:25;
A10: the_result_sort_of g = (the ResultSort of X-CircuitStr).g
by MSUALG_1:def 7
.= (id the OperSymbols of X-CircuitStr).g by CIRCCOMB:def 7
.= g by FUNCT_1:34;
A11: g.{} = [o,the carrier of S] by TREES_4:def 4;
g = (g.{})-tree the_arity_of g by Th13;
then A12: the_arity_of g = p by TREES_4:15;
A13: rng the_arity_of g c= Subtrees X by A2,FINSEQ_1:def 4;
A14: 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 dom ([o,the carrier of S]-tree p) = elementary_tree 0
by TREES_1:80;
then [o,the carrier of S]-tree p = root-tree [o,the carrier of S]
by A11,TREES_4:5;
then p = {} by TREES_4:17;
then len p = 0 by FINSEQ_1:25;
then len the_arity_of o = 0 by MSATERM:22;
then the_arity_of o = {} & g is Term of S,V by Th4,FINSEQ_1:25;
hence contradiction by A1,A8,A11;
end;
then consider h being Nat such that
A15: height dom ([o,the carrier of S]-tree p) = h+1 by NAT_1:22;
now let x being set; assume
A16: x in rng the_arity_of g;
then reconsider t = x as Element of Subtrees X by A13;
reconsider t as Term of S,V by A2,Th4;
A17: Following(q, height dom t) is_stable_at t &
Following(q, height dom t).t = t@(f, A) by A7,A12,A16;
consider z being set such that
A18: z in dom p & t = p.z by A12,A16,FUNCT_1:def 5;
z in dom doms p & (doms p).z = dom t by A18,FUNCT_6:31;
then dom t in rng doms p by FUNCT_1:def 5;
then height dom t < height tree doms p by TREES_3:81;
then height dom t <= h by A14,A15,NAT_1:38;
then consider i being Nat such that
A19: h = (height dom t)+i by NAT_1:28;
Following(q,h) = Following(Following(q,height dom t),i)
by A19,FACIRC_1:13;
hence Following(q,h) is_stable_at x by A17,FACIRC_1:17;
end;
then Following Following(q,h) is_stable_at [o,the carrier of S]-tree p
by A10,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 A15,FACIRC_1:12;
reconsider t = Sym(o,V)-tree p as c-Term of A,V by MSATERM:27;
A20: Sym(o,(the Sorts of A) \/ V) = [o, the carrier of S] &
Sym(o,V) = [o,the carrier of S] by MSAFREE:def 11;
A21: t = [o,the carrier of S]-tree p by MSAFREE:def 11;
deffunc f(set) = Following(q,h).(p.$1);
consider vp being FinSequence such that
A22: len vp = len p and
A23: for i being Nat st i in Seg len p
holds vp.i = f(i) from SeqLambda;
A24: dom vp = Seg len p & dom p = Seg len p by A22,FINSEQ_1:def 3;
A25: dom p = dom the_arity_of o by MSATERM:22;
now let i being Nat; assume
A26: i in dom p;
then reconsider t = p.i as Term of S,V by MSATERM:22;
reconsider t' = t as c-Term of A,V by MSATERM:27;
take t';
the_sort_of t = the_sort_of t' by Th1;
hence t' = p.i & the_sort_of t' = (the_arity_of o).i by A26,MSATERM:23;
end;
then reconsider p' = p as ArgumentSeq of o,A,V by A25,MSATERM:24;
now let i being Nat; assume
A27: i in dom p;
let t being c-Term of A,V; assume
A28: t = p.i;
then A29: t in rng p by A27,FUNCT_1:def 5;
then reconsider tt = t as Element of Subtrees X by A12,A13;
reconsider tt as Term of S,V by A2,Th4;
A30: Following(q, height dom t) is_stable_at tt &
Following(q, height dom t).tt = tt@(f, A) by A7,A29;
A31: vp.i = Following(q,h).t by A23,A24,A27,A28;
i in dom doms p & (doms p).i = dom t by A27,A28,FUNCT_6:31;
then dom t in rng doms p by FUNCT_1:def 5;
then height dom t < height tree doms p by TREES_3:81;
then height dom t <= h by A14,A15,NAT_1:38;
then consider j being Nat such that
A32: h = (height dom t)+j by NAT_1:28;
Following(q,h) = Following(Following(q,height dom t),j)
by A32,FACIRC_1:13;
then Following(q,h).t = Following(q,height dom t).t by A30,FACIRC_1:
def 9;
hence vp.i = t@f by A30,A31,Def7;
end;
then A33: (Sym(o,(the Sorts of A) \/ V)-tree p' qua c-Term of A,V)@f = Den(
o,A).vp
by A22,MSATERM:43;
now
rng p c= the carrier of X-CircuitStr &
dom Following(q, h) = the carrier of X-CircuitStr
by A12,CIRCUIT1:4,FINSEQ_1:def 4;
hence dom (Following(q, h)*p) = dom p by RELAT_1:46;
let z be set; assume
A34: z in Seg len p; then reconsider i = z as Nat;
vp.i = Following(q, h).(p.i) by A23,A34;
hence vp.z = (Following(q, h)*p).z by A24,A34,FUNCT_1:23;
end;
then A35: vp = Following(q, h)*the_arity_of g by A12,A24,FUNCT_1:9;
Den(g, X-Circuit A) = Den(o,A) by A11,Th17;
then Den(o,A).vp = (Following Following(q,h)).t by A10,A21,A35,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 A15,A20,A33,FACIRC_1:12
.= ([o,the carrier of S]-tree p)@(f, A) by A20,Def7;
end;
thus for t being Term of S,V holds P[t] from TermInd(A3,A6);
end;
begin :: <section4>Circuit similarity</section4>
definition
let X be set;
cluster id X -> one-to-one;
coherence by FUNCT_1:52;
end;
definition
let f be one-to-one Function;
cluster f" -> one-to-one;
coherence by FUNCT_1:62;
let g be one-to-one Function;
cluster g*f -> one-to-one;
coherence by FUNCT_1:46;
end;
definition
let S1, S2 be non empty ManySortedSign;
let f,g be Function;
pred S1, S2 are_equivalent_wrt f, g means:
Def9:
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 Th24:
for S1, S2 being non empty ManySortedSign, f,g being Function
st S1, S2 are_equivalent_wrt f, g
holds the carrier of S2 = f.:the carrier of S1 &
the OperSymbols of S2 = g.:the OperSymbols of S1
proof let S1, S2 be non empty ManySortedSign, f,g be Function such that
A1: f is one-to-one & g is one-to-one and
A2: f, g form_morphism_between S1, S2 and
A3: f", g" form_morphism_between S2, S1;
thus the carrier of S2 = dom (f") by A3,PUA2MSS1:def 13
.= rng f by A1,FUNCT_1:55
.= f.:dom f by RELAT_1:146
.= f.:the carrier of S1 by A2,PUA2MSS1:def 13;
thus the OperSymbols of S2 = dom (g") by A3,PUA2MSS1:def 13
.= rng g by A1,FUNCT_1:55
.= g.:dom g by RELAT_1:146
.= g.:the OperSymbols of S1 by A2,PUA2MSS1:def 13;
end;
theorem Th25:
for S1, S2 being non empty ManySortedSign, f,g being Function
st S1, S2 are_equivalent_wrt f, g
holds rng f = the carrier of S2 & rng g = the OperSymbols of S2
proof let S1, S2 be non empty ManySortedSign, f,g be Function such that
A1: f is one-to-one & g is one-to-one and
f, g form_morphism_between S1, S2 and
A2: f", g" form_morphism_between S2, S1;
thus rng f = dom (f") by A1,FUNCT_1:55
.= the carrier of S2 by A2,PUA2MSS1:def 13;
thus rng g = dom (g") by A1,FUNCT_1:55
.= the OperSymbols of S2 by A2,PUA2MSS1:def 13;
end;
theorem Th26:
for S being non empty ManySortedSign holds
S, S are_equivalent_wrt id the carrier of S, id the OperSymbols of S
proof let S be non empty ManySortedSign;
set f = id the carrier of S, g = id the OperSymbols of S;
thus f is one-to-one;
f" = f & g" = g by FUNCT_1:67;
hence thesis by INSTALG1:9;
end;
theorem Th27:
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 & g is one-to-one and
A2: f, g form_morphism_between S1, S2 and
A3: f", g" form_morphism_between S2, S1;
thus f" is one-to-one & g" is one-to-one by A1,FUNCT_1:62;
f" " = f & g" " = g by A1,FUNCT_1:65;
hence thesis by A2,A3;
end;
theorem Th28:
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 & g1 is one-to-one and
A2: f1, g1 form_morphism_between S1, S2 and
A3: f1", g1" form_morphism_between S2, S1 and
A4: f2 is one-to-one & g2 is one-to-one and
A5: f2, g2 form_morphism_between S2, S3 and
A6: f2", g2" form_morphism_between S3, S2;
thus f2*f1 is one-to-one & g2*g1 is one-to-one by A1,A4,FUNCT_1:46;
(f2*f1)" = f1"*f2" & (g2*g1)" = g1"*g2" by A1,A4,FUNCT_1:66;
hence thesis by A2,A3,A5,A6,PUA2MSS1:30;
end;
theorem Th29:
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 & g is one-to-one by A1,Def9;
A3: f, g form_morphism_between S1, S2 by A1,Def9;
A4: rng g = the OperSymbols of S2 &
dom the ResultSort of S2 = the OperSymbols of S2 by A1,Th25,FUNCT_2:def 1;
A5: InputVertices S1 = (the carrier of S1) \ rng the ResultSort of S1
by MSAFREE2:def 2;
A6: InputVertices S2 = (the carrier of S2) \ rng the ResultSort of S2
by MSAFREE2:def 2;
A7: f.:rng the ResultSort of S1
= rng (f*the ResultSort of S1) by RELAT_1:160
.= rng ((the ResultSort of S2)*g) by A3,PUA2MSS1:def 13
.= rng the ResultSort of S2 by A4,RELAT_1:47;
thus f.:InputVertices S1
= f.:(the carrier of S1) \ f.:
rng the ResultSort of S1 by A2,A5,FUNCT_1:123
.= InputVertices S2 by A1,A6,A7,Th24;
thus f.:InnerVertices S1 = f.:rng the ResultSort of S1 by MSAFREE2:def 3
.= InnerVertices S2 by A7,MSAFREE2:def 3;
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 OperSymbols of S;
thus thesis by Th26;
end;
symmetry
proof let S1,S2 be non empty ManySortedSign;
given f, g being one-to-one Function such that
A1: S1, S2 are_equivalent_wrt f, g;
take f", g";
thus thesis by A1,Th27;
end;
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,Th28;
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 Th31:
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
A1: dom f = the carrier of S1 & dom g = the OperSymbols of S1 &
rng f c= the carrier of S2;
now let v be Vertex of S1; f.v in rng f by A1,FUNCT_1:def 5;
hence f.v in the carrier of S2 by A1;
end;
hence thesis;
end;
theorem Th32:
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
A1: dom f = the carrier of S1 & dom g = the OperSymbols of S1 &
rng f c= the carrier of S2 & rng g c= the OperSymbols of S2;
now let v be Gate of S1; g.v in rng g by A1,FUNCT_1:def 5;
hence g.v in the OperSymbols of S2 by A1;
end;
hence thesis;
end;
theorem Th33:
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 such that
A1: f, g form_morphism_between S1, S2;
A2: InnerVertices S1 = rng the ResultSort of S1 &
InnerVertices S2 = rng the ResultSort of S2 by MSAFREE2:def 3;
f*the ResultSort of S1 = (the ResultSort of S2)*g
by A1,PUA2MSS1:def 13;
then f.:InnerVertices S1 = rng ((the ResultSort of S2)*g) by A2,RELAT_1:160
;
hence thesis by A2,RELAT_1:45;
end;
theorem Th34:
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,Th32;
A4: dom g = the OperSymbols of S1 & dom f = the carrier of S1
by A1,PUA2MSS1:def 13;
A5: dom the ResultSort of S1 = the OperSymbols of S1 by FUNCT_2:def 1;
A6: f.:InnerVertices S1 c= InnerVertices S2 by A1,Th33;
A7: v2 in f.:InnerVertices S1 by A2,A3,A4,FUNCT_1:def 12;
the_result_sort_of g1 = (the ResultSort of S2).g1 by MSUALG_1:def 7
.= ((the ResultSort of S2)*g).action_at v1 by A4,FUNCT_1:23
.= (f*the ResultSort of S1).action_at v1 by A1,PUA2MSS1:def 13
.= f.((the ResultSort of S1).action_at v1) by A5,FUNCT_1:23
.= f.(the_result_sort_of action_at v1) by MSUALG_1:def 7
.= v2 by A2,A3,MSAFREE2:def 7;
hence thesis by A6,A7,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:
Def12:
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 Th35:
for S being non empty ManySortedSign
for C being non-empty MSAlgebra over S
holds id the carrier of S, id the OperSymbols of S form_embedding_of C, C
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;
dom the Sorts of C = the carrier of S &
dom the Charact of C = the OperSymbols of S by PBOOLE:def 3;
hence thesis by INSTALG1:9,RELAT_1:78;
end;
theorem Th36:
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;
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 such that
A1: f1 is one-to-one & g1 is one-to-one and
A2: f1, g1 form_morphism_between S1, S2 and
A3: the Sorts of C1 = (the Sorts of C2)*f1 and
A4: the Charact of C1 = (the Charact of C2)*g1 and
A5: f2 is one-to-one & g2 is one-to-one and
A6: f2, g2 form_morphism_between S2, S3 and
A7: the Sorts of C2 = (the Sorts of C3)*f2 and
A8: the Charact of C2 = (the Charact of C3)*g2;
thus f2*f1 is one-to-one & g2*g1 is one-to-one by A1,A5,FUNCT_1:46;
thus f2*f1, g2*g1 form_morphism_between S1, S3 by A2,A6,PUA2MSS1:30;
thus thesis by A3,A4,A7,A8,RELAT_1:55;
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 C1, C2 are_similar_wrt f, g means:
Def13:
f, g form_embedding_of C1, C2 & f", g" form_embedding_of C2, C1;
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
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
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 &
f" is one-to-one & g" is one-to-one &
f", g" form_morphism_between S2, S1;
hence thesis by Def9;
end;
theorem Th38:
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 Th37;
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;
end;
assume that
A2: f is one-to-one & g is one-to-one and
A3: f, g form_morphism_between S1, S2 and
A4: f", g" form_morphism_between S2, S1 and
A5: the Sorts of C1 = (the Sorts of C2)*f &
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,A5;
thus f" is one-to-one & g" is one-to-one by A2,FUNCT_1:62;
thus f", g" form_morphism_between S2, S1 by A4;
dom (f") = the carrier of S2 by A4,PUA2MSS1:def 13;
then rng f = the carrier of S2 by A2,FUNCT_1:55;
then f*(f") = id the carrier of S2 by A2,FUNCT_1:61
.= id dom the Sorts of C2 by PBOOLE:def 3;
hence the Sorts of C2 = (the Sorts of C2)*(f*f") by RELAT_1:78
.= (the Sorts of C1)*f" by A5,RELAT_1:55;
dom (g") = the OperSymbols of S2 by A4,PUA2MSS1:def 13;
then rng g = the OperSymbols of S2 by A2,FUNCT_1:55;
then g*(g") = id the OperSymbols of S2 by A2,FUNCT_1:61
.= id dom the Charact of C2 by PBOOLE:def 3;
hence the Charact of C2 = (the Charact of C2)*(g*g") by RELAT_1:78
.= (the Charact of C1)*g" by A5,RELAT_1:55;
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 OperSymbols 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 OperSymbols of S;
f" = f & g" = g by FUNCT_1:67;
hence
f, g form_embedding_of C, C & f", g" form_embedding_of C, C by Th35;
end;
theorem Th40:
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
A1: f, g form_embedding_of C1, C2 & f", g" form_embedding_of C2, C1;
then f is one-to-one & g is one-to-one by Def12;
then f" " = f & g" " = g by FUNCT_1:65;
hence f", g" form_embedding_of C2, C1 &
f" ", g" " form_embedding_of C1, C2 by A1;
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
A1: f1, g1 form_embedding_of C1, C2 & f1", g1" form_embedding_of C2, C1 &
f2, g2 form_embedding_of C2, C3 & f2", g2" form_embedding_of C3, C2;
hence f2*f1, g2*g1 form_embedding_of C1, C3 by Th36;
f1 is one-to-one & g1 is one-to-one &
f2 is one-to-one & g2 is one-to-one by A1,Def12;
then (f2*f1)" = f1"*f2" & (g2*g1)" = g1"*g2" by FUNCT_1:66;
hence thesis by A1,Th36;
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 Th42:
f, g form_embedding_of C1, C2 implies
dom f = the carrier of G1 & rng f c= the carrier of G2 &
dom g = the OperSymbols of G1 & rng g c= the OperSymbols of G2
proof assume
f is one-to-one & g is one-to-one &
dom f = the carrier of G1 & dom g = the OperSymbols of G1 &
rng f c= the carrier of G2 & rng g c= the OperSymbols of G2;
hence thesis;
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
holds Den(o2, C2) = Den(o1, C1)
proof assume that
f is one-to-one & 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;
A4: dom g = the OperSymbols of G1 by A1,PUA2MSS1:def 13;
thus Den(o2, C2) = (the Charact of C2).o2 by MSUALG_1:def 11
.= (the Charact of C1).o1 by A2,A3,A4,FUNCT_1:23
.= Den(o1, C1) by MSUALG_1:def 11;
end;
theorem Th44:
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 & 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;
A4: the_arity_of o1 = (the Arity of G1).o1 &
the_arity_of o2 = (the Arity of G2).o2 by MSUALG_1:def 6;
thus o2 depends_on_in s2 = s2*the_arity_of o2 by CIRCUIT1:def 3
.= s2*(f*the_arity_of o1) by A1,A2,A4,PUA2MSS1:def 13
.= s1*the_arity_of o1 by A3,RELAT_1:55
.= o1 depends_on_in s1 by CIRCUIT1:def 3;
end;
theorem Th45:
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 & 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 &
dom the Sorts of C1 = the carrier of S1 by PBOOLE:def 3;
A4: dom s = dom the Sorts of C2 &
for x being set st x in dom the Sorts of C2
holds s.x in (the Sorts of C2).x by CARD_3:18;
A5: rng f c= the carrier of S2 & dom f = the carrier of S1
by A1,PUA2MSS1:def 13;
then A6: dom (s*f) = the carrier of S1 by A3,A4,RELAT_1:46;
now let x be set; assume
A7: x in the carrier of S1;
then f.x in rng f & (s*f).x = s.(f.x) by A5,FUNCT_1:23,def 5;
then (s*f).x in (the Sorts of C2).(f.x) by A3,A5,CARD_3:18;
hence (s*f).x in (the Sorts of C1).x by A2,A5,A7,FUNCT_1:23;
end;
hence thesis by A3,A6,CARD_3:18;
end;
theorem Th46:
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 by Def12;
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 s2' = (Following s2)*f as State of C1 by A1,Th45;
A5: dom f = the carrier of G1 & rng f c= the carrier of G2
by A2,PUA2MSS1:def 13;
now let v be Vertex of G1;
A6: s2'.v = (Following s2).(f.v) by A5,FUNCT_1:23;
reconsider fv = f.v as Vertex of G2 by A2,Th31;
hereby assume v in InputVertices G1;
then s2 is_stable_at f.v & Following(s2, 1) = Following s2
by A4,FACIRC_1:14;
hence s2'.v = s2.(f.v) by A6,FACIRC_1:def 9 .= s1.v by A3,A5,FUNCT_1:23;
end;
A7: f.:InnerVertices G1 c= InnerVertices G2 by A2,Th33;
assume
A8: v in InnerVertices G1;
then A9: fv in f.:InnerVertices G1 by A5,FUNCT_1:def 12;
A10: action_at fv = g.action_at v by A2,A8,Th34;
thus s2'.v
= (Den(action_at fv, C2)).(action_at fv depends_on_in s2)
by A6,A7,A9,CIRCUIT2:def 5
.= (Den(action_at v, C1)).(action_at fv depends_on_in s2)
by A1,A10,Th43
.= (Den(action_at v,C1)).(action_at v depends_on_in s1)
by A1,A3,A10,Th44;
end;
hence thesis by CIRCUIT2:def 5;
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
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,Th42;
now let v be Vertex of G1; assume v in InputVertices G1;
then f.v in f.:InputVertices G1 by A4,FUNCT_1:def 12;
hence s2 is_stable_at f.v by A2,FACIRC_1:18;
end;
hence thesis by A1,A3,Th46;
end;
theorem Th48:
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,Th47;
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 Ind(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
proof assume
A1: f, g form_embedding_of C1, C2 & f preserves_inputs_of G1, G2;
let s2 be State of C2, s1 be State of C1 such that
A2: s1 = s2*f;
assume s2 = Following s2;
hence s1 = Following s1 by A1,A2,Th47;
end;
theorem Th50:
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
A1: f, g form_embedding_of C1, C2 & f preserves_inputs_of G1, G2;
let s2 be State of C2, s1 be State of C1 such that
A2: s1 = s2*f;
let v1 be Vertex of G1;
A3: f,g form_morphism_between G1,G2 by A1,Def12;
then A4: dom f = the carrier of G1 by PUA2MSS1:def 13;
reconsider v2 = f.v1 as Vertex of G2 by A3,Th31;
thus s1 is_stable_at v1 implies s2 is_stable_at f.v1
proof assume
A5: 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,Th48;
hence (Following(s2,n)).(f.v1)
= (Following(s1,n)).v1 by A4,FUNCT_1:23
.= s1.v1 by A5
.= s2.(f.v1) by A2,A4,FUNCT_1:23;
end;
assume
A6: 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,Th48;
hence (Following(s1,n)).v1
= (Following(s2,n)).v2 by A4,FUNCT_1:23
.= s2.v2 by A6
.= s1.v1 by A2,A4,FUNCT_1:23;
end;
theorem
C1, C2 are_similar_wrt f, g implies
for s being State of C2 holds s*f is State of C1
proof assume f, g form_embedding_of C1, C2;
hence thesis by Th45;
end;
theorem Th52:
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
A1: f, g form_embedding_of C1, C2 & f", g" form_embedding_of C2, C1;
then A2: f is one-to-one & f" is one-to-one by Def12;
let s1 be State of C1;
let s2 be State of C2;
f, g form_morphism_between G1, G2 by A1,Def12;
then A3: dom f = the carrier of G1 & dom s1 = the carrier of G1
by CIRCUIT1:4,PUA2MSS1:def 13;
A4: s1*f"*f = s1*(f"*f) by RELAT_1:55 .= s1*id dom f by A2,FUNCT_1:61
.= s1 by A3,RELAT_1:78;
f", g" form_morphism_between G2, G1 by A1,Def12;
then A5: dom (f") = the carrier of G2 & dom s2 = the carrier of G2
by CIRCUIT1:4,PUA2MSS1:def 13;
s2*f*(f") = s2*(f*(f")) by RELAT_1:55
.= s2*((f" ")*(f")) by A2,FUNCT_1:65
.= s2*id dom (f") by A2,FUNCT_1:61;
hence thesis by A4,A5,RELAT_1:78;
end;
theorem Th53:
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 Th37;
hence thesis by Th29;
end;
theorem Th54:
C1, C2 are_similar_wrt f, g implies f preserves_inputs_of G1, G2
proof assume C1, C2 are_similar_wrt f, g;
hence f.:InputVertices G1 c= InputVertices G2 by Th53;
end;
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
holds Following s1 = (Following s2)*f
proof assume C1, C2 are_similar_wrt f, g;
then f, g form_embedding_of C1, C2 & f preserves_inputs_of G1, G2
by Def13,Th54;
hence thesis by Th47;
end;
theorem Th56:
C1, C2 are_similar_wrt f, g implies
for s1 being State of C1, s2 being State of C2 st s1 = s2*f
for n being Nat holds Following(s1,n) = Following(s2,n)*f
proof assume C1, C2 are_similar_wrt f, g;
then f, g form_embedding_of C1, C2 & f preserves_inputs_of G1, G2
by Def13,Th54;
hence thesis by Th48;
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
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 Th40;
let s1 be State of C1, s2 be State of C2 such that
A3: s1 = s2*f;
A4: s2 = s1*f" by A1,A3,Th52;
thus s1 is stable implies s2 is stable
proof assume s1 = Following s1;
hence s2 = Following s2 by A2,A4,Th55;
end;
assume s2 = Following s2;
hence s1 = Following s1 by A1,A3,Th55;
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 Th40;
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,Th38;
then A5: f,g form_morphism_between G1,G2 & f",g" form_morphism_between G2,G1
by Def9;
then A6: dom f = the carrier of G1 & dom (f") = the carrier of G2
by PUA2MSS1:def 13;
reconsider v2 = f.v1 as Vertex of G2 by A5,Th31;
f is one-to-one by A4,Def9;
then A7: v1 = f".v2 by A6,FUNCT_1:56;
thus s1 is_stable_at v1 implies s2 is_stable_at f.v1
proof assume
A8: for n being Nat holds (Following(s1,n)).v1 = s1.v1;
let n be Nat;
Following(s1,n) = Following(s2,n)*f by A1,A3,Th56;
hence (Following(s2,n)).(f.v1)
= (Following(s1,n)).v1 by A6,FUNCT_1:23
.= s1.v1 by A8
.= s2.(f.v1) by A3,A6,FUNCT_1:23;
end;
assume
A9: for n being Nat holds (Following(s2,n)).(f.v1) = s2.(f.v1);
let n be Nat;
s2 = s1*f" by A1,A3,Th52;
then Following(s2,n) = Following(s1,n)*f" by A2,Th56;
hence (Following(s1,n)).v1
= (Following(s2,n)).v2 by A6,A7,FUNCT_1:23
.= s2.v2 by A9
.= s1.v1 by A3,A6,FUNCT_1:23;
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:
Def15:
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 by Def15;
A3: f is one-to-one by A1,Def12;
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,A3;
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;
A3: g is one-to-one by A2,Def12;
mode OperMap of X, A, C, f -> one-to-one Function means
f, it form_embedding_of X-Circuit A, C;
existence by A2,A3;
end;
theorem Th59:
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,Def13;
X-Circuit A, C are_similar_wrt f", g" by A1,Th40;
hence thesis by Th54;
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 f being SortMap of X, A, C
for t being Term of S,V st t in Subtrees X
for s being State of C
holds Following(s, 1+height dom t) is_stable_at f.t &
for s' being State of X-Circuit A st s' = s*f
for h being CompatibleValuation of s'
holds Following(s, 1+height dom t).(f.t) = t@(h, A)
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,Def12;
let t be Term of S,V such that
A5: t in Subtrees X;
let s be State of C;
reconsider s' = s*f as State of X-Circuit A by A2,Th45;
X-CircuitStr = ManySortedSign(#
Subtrees X, [:the OperSymbols of S,{the carrier of S}:]-Subtrees X,
[:the OperSymbols of S,{the carrier of S}:]-ImmediateSubtrees X,
id ([:the OperSymbols of S,{the carrier of S}:]-Subtrees X)
#) by Def1;
then reconsider t' = t as Vertex of X-CircuitStr by A5;
A6: Following(s', 1+height dom t) is_stable_at t' &
Following(s', 1+height dom t) = Following(s, 1+height dom t)*f
by A2,A3,A5,Th22,Th48;
hence Following(s, 1+height dom t) is_stable_at f.t by A2,A3,Th50;
let s' be State of X-Circuit A such that
A7: s' = s*f;
let h be CompatibleValuation of s';
dom f = the carrier of X-CircuitStr &
Following(s', 1+height dom t).t' = t@(h,A) by A4,A5,Th22,PUA2MSS1:def 13;
hence Following(s, 1+height dom t).(f.t) = t@(h, A)
by A6,A7,FUNCT_1:23;
end;
theorem Th61:
for G being Circuit-like non void (non empty ManySortedSign)
for C being non-empty Circuit of G
st C calculates X, A
for t being Term of S,V st t in Subtrees X
ex v being Vertex of G st
for s being State of C holds Following(s, 1+height dom t) is_stable_at v &
ex f being SortMap of X, A, C st
for s' being State of X-Circuit A st s' = s*f
for h being CompatibleValuation of s'
holds Following(s, 1+height dom t).v = t@(h, A)
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 by Def15;
f is one-to-one by A2,Def12;
then 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,Def12;
X-CircuitStr = ManySortedSign(#
Subtrees X, [:the OperSymbols of S,{the carrier of S}:]-Subtrees X,
[:the OperSymbols of S,{the carrier of S}:]-ImmediateSubtrees X,
id ([:the OperSymbols of S,{the carrier of S}:]-Subtrees X)
#) by Def1;
then reconsider t' = t as Vertex of X-CircuitStr by A4;
reconsider v = f.t' as Vertex of G by A5,Th31;
take v;
let s be State of C;
thus Following(s, 1+height dom t) is_stable_at v by A1,A4,Th60;
take f; thus thesis by A1,A4,Th60;
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 s' being State of X-Circuit A st s' = s*f
for h being CompatibleValuation of s'
holds Following(s, 1+height dom t).(f.t) = t@(h, A)
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 Th59;
hence thesis by Th60;
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 s' being State of X-Circuit A st s' = s*f
for h being CompatibleValuation of s'
holds Following(s, 1+height dom t).v = t@(h, A)
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 Th59;
hence thesis by Th61;
end;