:: Circuit Generated by Terms and Circuit Calculating Terms
:: by Grzegorz Bancerek
::
:: Received April 10, 2001
:: Copyright (c) 2001 Association of Mizar Users
theorem Th1: :: CIRCTRM1:1
definition
let S be non
empty non
void ManySortedSign ;
let V be
V5 ManySortedSet of the
carrier of
S;
let X be non
empty Subset of
(S -Terms V);
func X -CircuitStr -> non
empty strict ManySortedSign equals :: CIRCTRM1:def 1
ManySortedSign(#
(Subtrees X),
([:the carrier' of S,{the carrier of S}:] -Subtrees X),
([:the carrier' of S,{the carrier of S}:] -ImmediateSubtrees X),
(incl ([:the carrier' of S,{the carrier of S}:] -Subtrees X)) #);
correctness
coherence
ManySortedSign(# (Subtrees X),([:the carrier' of S,{the carrier of S}:] -Subtrees X),([:the carrier' of S,{the carrier of S}:] -ImmediateSubtrees X),(incl ([:the carrier' of S,{the carrier of S}:] -Subtrees X)) #) is non empty strict ManySortedSign ;
;
end;
:: deftheorem defines -CircuitStr CIRCTRM1:def 1 :
theorem Th2: :: CIRCTRM1:2
theorem Th3: :: CIRCTRM1:3
theorem Th4: :: CIRCTRM1:4
theorem Th5: :: CIRCTRM1:5
theorem :: CIRCTRM1:6
canceled;
theorem Th7: :: CIRCTRM1:7
theorem Th8: :: CIRCTRM1:8
theorem Th9: :: CIRCTRM1:9
theorem Th10: :: CIRCTRM1:10
theorem Th11: :: CIRCTRM1:11
theorem Th12: :: CIRCTRM1:12
theorem Th13: :: CIRCTRM1:13
:: deftheorem Def2 defines the_sort_of CIRCTRM1:def 2 :
:: deftheorem Def3 defines the_action_of CIRCTRM1:def 3 :
:: deftheorem Def4 defines -CircuitSorts CIRCTRM1:def 4 :
theorem Th14: :: CIRCTRM1:14
:: deftheorem Def5 defines -CircuitCharact CIRCTRM1:def 5 :
:: deftheorem defines -Circuit CIRCTRM1:def 6 :
theorem :: CIRCTRM1:15
theorem :: CIRCTRM1:16
theorem Th17: :: CIRCTRM1:17
theorem Th18: :: CIRCTRM1:18
theorem Th19: :: CIRCTRM1:19
theorem :: CIRCTRM1:20
:: deftheorem Def7 defines @ CIRCTRM1:def 7 :
definition
let S be non
empty non
void ManySortedSign ;
let V be
V5 ManySortedSet of the
carrier of
S;
let X be
SetWithCompoundTerm of
S,
V;
let A be
non-empty locally-finite MSAlgebra of
S;
let s be
State of
(X -Circuit A);
defpred S1[
set ,
set ,
set ]
means (
root-tree [$2,$1] in Subtrees X implies $3
= s . (root-tree [$2,$1]) );
A1:
for
x being
Vertex of
S for
v being
Element of
V . x ex
a being
Element of the
Sorts of
A . x st
S1[
x,
v,
a]
mode CompatibleValuation of
s -> ManySortedFunction of
V,the
Sorts of
A means :
Def8:
:: CIRCTRM1:def 8
for
x being
Vertex of
S for
v being
Element of
V . x st
root-tree [v,x] in Subtrees X holds
(it . x) . v = s . (root-tree [v,x]);
existence
ex b1 being ManySortedFunction of V,the Sorts of A st
for x being Vertex of S
for v being Element of V . x st root-tree [v,x] in Subtrees X holds
(b1 . x) . v = s . (root-tree [v,x])
end;
:: deftheorem Def8 defines CompatibleValuation CIRCTRM1:def 8 :
theorem :: CIRCTRM1:21
theorem Th22: :: CIRCTRM1:22
theorem :: CIRCTRM1:23
:: deftheorem Def9 defines are_equivalent_wrt CIRCTRM1:def 9 :
theorem Th24: :: CIRCTRM1:24
theorem Th25: :: CIRCTRM1:25
theorem Th26: :: CIRCTRM1:26
theorem Th27: :: CIRCTRM1:27
theorem Th28: :: CIRCTRM1:28
for
S1,
S2,
S3 being non
empty ManySortedSign for
f1,
g1,
f2,
g2 being
Function st
S1,
S2 are_equivalent_wrt f1,
g1 &
S2,
S3 are_equivalent_wrt f2,
g2 holds
S1,
S3 are_equivalent_wrt f2 * f1,
g2 * g1
theorem Th29: :: CIRCTRM1:29
definition
let S1,
S2 be non
empty ManySortedSign ;
pred S1,
S2 are_equivalent means :: CIRCTRM1:def 10
ex
f,
g being
one-to-one Function st
S1,
S2 are_equivalent_wrt f,
g;
reflexivity
for S1 being non empty ManySortedSign ex f, g being one-to-one Function st S1,S1 are_equivalent_wrt f,g
symmetry
for S1, S2 being non empty ManySortedSign st ex f, g being one-to-one Function st S1,S2 are_equivalent_wrt f,g holds
ex f, g being one-to-one Function st S2,S1 are_equivalent_wrt f,g
end;
:: deftheorem defines are_equivalent CIRCTRM1:def 10 :
theorem :: CIRCTRM1:30
:: deftheorem defines preserves_inputs_of CIRCTRM1:def 11 :
theorem Th31: :: CIRCTRM1:31
theorem Th32: :: CIRCTRM1:32
theorem Th33: :: CIRCTRM1:33
theorem Th34: :: CIRCTRM1:34
:: deftheorem Def12 defines form_embedding_of CIRCTRM1:def 12 :
theorem Th35: :: CIRCTRM1:35
theorem Th36: :: CIRCTRM1:36
for
S1,
S2,
S3 being non
empty ManySortedSign for
f1,
g1,
f2,
g2 being
Function for
C1 being
non-empty MSAlgebra of
S1 for
C2 being
non-empty MSAlgebra of
S2 for
C3 being
non-empty MSAlgebra of
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
:: deftheorem Def13 defines are_similar_wrt CIRCTRM1:def 13 :
theorem Th37: :: CIRCTRM1:37
theorem Th38: :: CIRCTRM1:38
theorem :: CIRCTRM1:39
theorem Th40: :: CIRCTRM1:40
theorem :: CIRCTRM1:41
for
S1,
S2,
S3 being non
empty ManySortedSign for
f1,
g1,
f2,
g2 being
Function for
C1 being
non-empty MSAlgebra of
S1 for
C2 being
non-empty MSAlgebra of
S2 for
C3 being
non-empty MSAlgebra of
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
:: deftheorem defines are_similar CIRCTRM1:def 14 :
theorem Th42: :: CIRCTRM1:42
theorem Th43: :: CIRCTRM1:43
theorem Th44: :: CIRCTRM1:44
theorem Th45: :: CIRCTRM1:45
theorem Th46: :: CIRCTRM1:46
theorem Th47: :: CIRCTRM1:47
theorem Th48: :: CIRCTRM1:48
theorem :: CIRCTRM1:49
theorem Th50: :: CIRCTRM1:50
theorem :: CIRCTRM1:51
theorem Th52: :: CIRCTRM1:52
theorem Th53: :: CIRCTRM1:53
theorem Th54: :: CIRCTRM1:54
theorem Th55: :: CIRCTRM1:55
theorem Th56: :: CIRCTRM1:56
theorem :: CIRCTRM1:57
theorem :: CIRCTRM1:58
:: deftheorem Def15 defines calculates CIRCTRM1:def 15 :
:: deftheorem defines specifies CIRCTRM1:def 16 :
definition
let S be non
empty non
void ManySortedSign ;
let V be
V5 ManySortedSet of the
carrier of
S;
let A be
non-empty MSAlgebra of
S;
let X be non
empty Subset of
(S -Terms V);
let G be non
empty non
void Circuit-like ManySortedSign ;
let C be
non-empty Circuit of
G;
assume
C calculates X,
A
;
then consider f,
g being
Function such that A1:
f,
g form_embedding_of X -Circuit A,
C
and A2:
f preserves_inputs_of X -CircuitStr ,
G
by Def15;
A3:
f is
one-to-one
by A1, Def12;
mode SortMap of
X,
A,
C -> one-to-one Function means :
Def17:
:: CIRCTRM1:def 17
(
it preserves_inputs_of X -CircuitStr ,
G & ex
g being
Function st
it,
g form_embedding_of X -Circuit A,
C );
existence
ex b1 being one-to-one Function st
( b1 preserves_inputs_of X -CircuitStr ,G & ex g being Function st b1,g form_embedding_of X -Circuit A,C )
by A1, A2, A3;
end;
:: deftheorem Def17 defines SortMap CIRCTRM1:def 17 :
definition
let S be non
empty non
void ManySortedSign ;
let V be
V5 ManySortedSet of the
carrier of
S;
let A be
non-empty MSAlgebra of
S;
let X be non
empty Subset of
(S -Terms V);
let G be non
empty non
void Circuit-like ManySortedSign ;
let C be
non-empty Circuit of
G;
assume A1:
C calculates X,
A
;
let f be
SortMap of
X,
A,
C;
consider g being
Function 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 :: CIRCTRM1:def 18
f,
it form_embedding_of X -Circuit A,
C;
existence
ex b1 being one-to-one Function st f,b1 form_embedding_of X -Circuit A,C
by A2, A3;
end;
:: deftheorem defines OperMap CIRCTRM1:def 18 :
theorem Th59: :: CIRCTRM1:59
theorem Th60: :: CIRCTRM1:60
theorem Th61: :: CIRCTRM1:61
theorem :: CIRCTRM1:62
theorem :: CIRCTRM1:63