:: FACIRC_1 semantic presentation

definition

let c₁ be set ;
attr a₁ is pair means :Def1: :: FACIRC_1:def 1
ex b₁, b₂ being set st a₁ = [b₁,b₂];

end;

:: deftheorem Def1 defines pair FACIRC_1:def 1 :

registration

cluster pair -> non empty set ;
coherence

proof end;

end;

registration

let c₁, c₂ be set ;
cluster [a₁,a₂] -> pair ;
coherence

proof end;

end;

registration

cluster non empty pair set ;
existence

proof end;

cluster non pair set ;
existence

proof end;

end;

registration

cluster -> non pair Element of NAT ;
coherence

proof end;

end;

definition

let c₁ be set ;
attr a₁ is with_pair means :Def2: :: FACIRC_1:def 2
ex b₁ being pair set st b₁ in a₁;

end;

:: deftheorem Def2 defines with_pair FACIRC_1:def 2 :

notation

let c₁ be set ;
antonym without_pairs c₁ for with_pair c₁;

end;

registration

cluster empty -> without_pairs set ;
coherence

proof end;

let c₁ be non pair set ;
cluster {a₁} -> without_pairs ;
coherence

proof end;

let c₂ be non pair set ;
cluster {a₁,a₂} -> without_pairs ;
coherence

proof end;

let c₃ be non pair set ;
cluster {a₁,a₂,a₃} -> without_pairs ;
coherence

proof end;

end;

registration

cluster non empty without_pairs set ;
existence

proof end;

end;

registration

let c₁, c₂ be without_pairs set ;
cluster a₁ \/ a₂ -> without_pairs ;
coherence

proof end;

end;

registration

let c₁ be without_pairs set ;
let c₂ be set ;
cluster a₁ \ a₂ -> without_pairs ;
coherence

proof end;

cluster a₁ /\ a₂ -> without_pairs ;
coherence

proof end;

cluster a₂ /\ a₁ -> without_pairs ;
coherence ;

end;

registration

let c₁ be pair set ;
cluster {a₁} -> Relation-like ;
coherence

proof end;

let c₂ be pair set ;
cluster {a₁,a₂} -> Relation-like ;
coherence

proof end;

let c₃ be pair set ;
cluster {a₁,a₂,a₃} -> Relation-like ;
coherence

proof end;

end;

registration

cluster Relation-like without_pairs -> empty without_pairs set ;
coherence

proof end;

end;

definition

let c₁ be Function;
attr a₁ is nonpair-yielding means :: FACIRC_1:def 3
for b₁ being set st b₁ in dom a₁ holds
not a₁ . b₁ is pair;

end;

:: deftheorem Def3 defines nonpair-yielding FACIRC_1:def 3 :

registration

let c₁ be non pair set ;
cluster <*a₁*> -> nonpair-yielding ;
coherence

proof end;

let c₂ be non pair set ;
cluster <*a₁,a₂*> -> nonpair-yielding ;
coherence

proof end;

let c₃ be non pair set ;
cluster <*a₁,a₂,a₃*> -> nonpair-yielding ;
coherence

proof end;

end;

theorem Th1: :: FACIRC_1:1

for b₁ being Function st b₁ is nonpair-yielding holds
not rng b₁ is with_pair

proof end;

registration

let c₁ be Nat;
cluster one-to-one nonpair-yielding FinSeqLen of a₁;
existence

proof end;

end;

registration

cluster one-to-one nonpair-yielding set ;
existence

proof end;

end;

registration

let c₁ be nonpair-yielding Function;
cluster rng a₁ -> without_pairs ;
coherence by Th1;

end;

theorem Th2: :: FACIRC_1:2

for b₁, b₂ being non empty ManySortedSign st b₁ tolerates b₂ & InnerVertices b₁ is Relation & InnerVertices b₂ is Relation holds
InnerVertices (b₁ +* b₂) is Relation

proof end;

theorem Th3: :: FACIRC_1:3

for b₁, b₂ being non empty unsplit gate`1=arity ManySortedSign st InnerVertices b₁ is Relation & InnerVertices b₂ is Relation holds
InnerVertices (b₁ +* b₂) is Relation

proof end;

theorem Th4: :: FACIRC_1:4

for b₁, b₂ being non empty ManySortedSign st b₁ tolerates b₂ & InnerVertices b₂ misses InputVertices b₁ holds
( InputVertices b₁ c= InputVertices (b₁ +* b₂) & InputVertices (b₁ +* b₂) = (InputVertices b₁) \/ ((InputVertices b₂) \ (InnerVertices b₁)) )

proof end;

theorem Th5: :: FACIRC_1:5

for b₁, b₂ being set st not b₁ is with_pair & b₂ is Relation holds
b₁ misses b₂

proof end;

theorem Th6: :: FACIRC_1:6

for b₁, b₂ being non empty unsplit gate`1=arity ManySortedSign st not InputVertices b₁ is with_pair & InnerVertices b₂ is Relation holds
( InputVertices b₁ c= InputVertices (b₁ +* b₂) & InputVertices (b₁ +* b₂) = (InputVertices b₁) \/ ((InputVertices b₂) \ (InnerVertices b₁)) )

proof end;

theorem Th7: :: FACIRC_1:7

for b₁, b₂ being non empty unsplit gate`1=arity ManySortedSign st not InputVertices b₁ is with_pair & InnerVertices b₁ is Relation & not InputVertices b₂ is with_pair & InnerVertices b₂ is Relation holds
InputVertices (b₁ +* b₂) = (InputVertices b₁) \/ (InputVertices b₂)

proof end;

theorem Th8: :: FACIRC_1:8

for b₁, b₂ being non empty ManySortedSign st b₁ tolerates b₂ & not InputVertices b₁ is with_pair & not InputVertices b₂ is with_pair holds
not InputVertices (b₁ +* b₂) is with_pair

proof end;

theorem Th9: :: FACIRC_1:9

for b₁, b₂ being non empty unsplit gate`1=arity ManySortedSign st not InputVertices b₁ is with_pair & not InputVertices b₂ is with_pair holds
not InputVertices (b₁ +* b₂) is with_pair

proof end;

scheme :: FACIRC_1:sch 1
s1{ F₁( set , set ) -> Element of BOOLEAN } :

ex b₁ being Function of 2 -tuples_on BOOLEAN , BOOLEAN st
for b₂, b₃ being Element of BOOLEAN holds b₁ . <*b₂,b₃*> = F₁(b₂,b₃)

proof end;

scheme :: FACIRC_1:sch 2
s2{ F₁( set , set ) -> Element of BOOLEAN } :

for b₁, b₂ being Function of 2 -tuples_on BOOLEAN , BOOLEAN st ( for b₃, b₄ being Element of BOOLEAN holds b₁ . <*b₃,b₄*> = F₁(b₃,b₄) ) & ( for b₃, b₄ being Element of BOOLEAN holds b₂ . <*b₃,b₄*> = F₁(b₃,b₄) ) holds
b₁ = b₂

proof end;

scheme :: FACIRC_1:sch 3
s3{ F₁( set , set ) -> Element of BOOLEAN } :

( ex b₁ being Function of 2 -tuples_on BOOLEAN , BOOLEAN st
for b₂, b₃ being Element of BOOLEAN holds b₁ . <*b₂,b₃*> = F₁(b₂,b₃) & ( for b₁, b₂ being Function of 2 -tuples_on BOOLEAN , BOOLEAN st ( for b₃, b₄ being Element of BOOLEAN holds b₁ . <*b₃,b₄*> = F₁(b₃,b₄) ) & ( for b₃, b₄ being Element of BOOLEAN holds b₂ . <*b₃,b₄*> = F₁(b₃,b₄) ) holds
b₁ = b₂ ) )

proof end;

scheme :: FACIRC_1:sch 4
s4{ F₁( set , set , set ) -> Element of BOOLEAN } :

ex b₁ being Function of 3 -tuples_on BOOLEAN , BOOLEAN st
for b₂, b₃, b₄ being Element of BOOLEAN holds b₁ . <*b₂,b₃,b₄*> = F₁(b₂,b₃,b₄)

proof end;

scheme :: FACIRC_1:sch 5
s5{ F₁( set , set , set ) -> Element of BOOLEAN } :

for b₁, b₂ being Function of 3 -tuples_on BOOLEAN , BOOLEAN st ( for b₃, b₄, b₅ being Element of BOOLEAN holds b₁ . <*b₃,b₄,b₅*> = F₁(b₃,b₄,b₅) ) & ( for b₃, b₄, b₅ being Element of BOOLEAN holds b₂ . <*b₃,b₄,b₅*> = F₁(b₃,b₄,b₅) ) holds
b₁ = b₂

proof end;

scheme :: FACIRC_1:sch 6
s6{ F₁( set , set , set ) -> Element of BOOLEAN } :

( ex b₁ being Function of 3 -tuples_on BOOLEAN , BOOLEAN st
for b₂, b₃, b₄ being Element of BOOLEAN holds b₁ . <*b₂,b₃,b₄*> = F₁(b₂,b₃,b₄) & ( for b₁, b₂ being Function of 3 -tuples_on BOOLEAN , BOOLEAN st ( for b₃, b₄, b₅ being Element of BOOLEAN holds b₁ . <*b₃,b₄,b₅*> = F₁(b₃,b₄,b₅) ) & ( for b₃, b₄, b₅ being Element of BOOLEAN holds b₂ . <*b₃,b₄,b₅*> = F₁(b₃,b₄,b₅) ) holds
b₁ = b₂ ) )

proof end;

definition

func 'xor' -> Function of 2 -tuples_on BOOLEAN , BOOLEAN means :Def4: :: FACIRC_1:def 4
for b₁, b₂ being Element of BOOLEAN holds a₁ . <*b₁,b₂*> = b₁ 'xor' b₂;
correctness

proof end;

func 'or' -> Function of 2 -tuples_on BOOLEAN , BOOLEAN means :Def5: :: FACIRC_1:def 5
for b₁, b₂ being Element of BOOLEAN holds a₁ . <*b₁,b₂*> = b₁ 'or' b₂;
correctness

proof end;

func '&' -> Function of 2 -tuples_on BOOLEAN , BOOLEAN means :Def6: :: FACIRC_1:def 6
for b₁, b₂ being Element of BOOLEAN holds a₁ . <*b₁,b₂*> = b₁ '&' b₂;
correctness

proof end;

end;

:: deftheorem Def4 defines 'xor' FACIRC_1:def 4 :

:: deftheorem Def5 defines 'or' FACIRC_1:def 5 :

:: deftheorem Def6 defines '&' FACIRC_1:def 6 :

definition

func or3 -> Function of 3 -tuples_on BOOLEAN , BOOLEAN means :Def7: :: FACIRC_1:def 7
for b₁, b₂, b₃ being Element of BOOLEAN holds a₁ . <*b₁,b₂,b₃*> = (b₁ 'or' b₂) 'or' b₃;
correctness

proof end;

end;

:: deftheorem Def7 defines or3 FACIRC_1:def 7 :

definition

let c₁ be set ;
redefine func <* as <*c₁*> -> FinSeqLen of 1;
coherence

proof end;

let c₂ be set ;
redefine func <* as <*c₁,c₂*> -> FinSeqLen of 2;
coherence

proof end;

let c₃ be set ;
redefine func <* as <*c₁,c₂,c₃*> -> FinSeqLen of 3;
coherence

proof end;

end;

definition

let c₁, c₂ be Nat;
let c₃ be FinSeqLen of c₁;
let c₄ be FinSeqLen of c₂;
redefine func ^ as c₃ ^ c₄ -> FinSeqLen of a₁ + a₂;
coherence

proof end;

end;

E16: now

let c₁ be non empty non void ManySortedSign ;
let c₂ be Gate of c₁;
not the OperSymbols of c₁ is empty by MSUALG_1:def 5;
hence c₂ in the OperSymbols of c₁ ;

end;

theorem Th10: :: FACIRC_1:10

for b₁ being non empty non void Circuit-like ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being State of b₂
for b₄ being Gate of b₁ holds (Following b₃) . (the_result_sort_of b₄) = (Den b₄,b₂) . (b₃ * (the_arity_of b₄))

proof end;

definition

let c₁ be non empty non void Circuit-like ManySortedSign ;
let c₂ be non-empty Circuit of c₁;
let c₃ be State of c₂;
let c₄ be Nat;
func Following c₃,c₄ -> State of a₂ means :Def8: :: FACIRC_1:def 8
ex b₁ being Function of NAT , product the Sorts of a₂ st
( a₅ = b₁ . a₄ & b₁ . 0 = a₃ & ( for b₂ being Nat holds b₁ . (b₂ + 1) = Following (b₁ . b₂) ) );
correctness

proof end;

end;

:: deftheorem Def8 defines Following FACIRC_1:def 8 :

theorem Th11: :: FACIRC_1:11

for b₁ being non empty non void Circuit-like ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being State of b₂ holds Following b₃,0 = b₃

proof end;

theorem Th12: :: FACIRC_1:12

for b₁ being non empty non void Circuit-like ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being State of b₂
for b₄ being Nat holds Following b₃,(b₄ + 1) = Following (Following b₃,b₄)

proof end;

theorem Th13: :: FACIRC_1:13

for b₁ being non empty non void Circuit-like ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being State of b₂
for b₄, b₅ being Nat holds Following b₃,(b₄ + b₅) = Following (Following b₃,b₄),b₅

proof end;

theorem Th14: :: FACIRC_1:14

for b₁ being non empty non void Circuit-like ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being State of b₂ holds Following b₃,1 = Following b₃

proof end;

theorem Th15: :: FACIRC_1:15

for b₁ being non empty non void Circuit-like ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being State of b₂ holds Following b₃,2 = Following (Following b₃)

proof end;

theorem Th16: :: FACIRC_1:16

proof end;

definition

let c₁ be non empty non void Circuit-like ManySortedSign ;
let c₂ be non-empty Circuit of c₁;
let c₃ be State of c₂;
let c₄ be set ;
pred c₃ is_stable_at c₄ means :Def9: :: FACIRC_1:def 9
for b₁ being Nat holds (Following a₃,b₁) . a₄ = a₃ . a₄;

end;

:: deftheorem Def9 defines is_stable_at FACIRC_1:def 9 :

theorem Th17: :: FACIRC_1:17

for b₁ being non empty non void Circuit-like ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being State of b₂
for b₄ being set st b₃ is_stable_at b₄ holds
for b₅ being Nat holds Following b₃,b₅ is_stable_at b₄

proof end;

theorem Th18: :: FACIRC_1:18

for b₁ being non empty non void Circuit-like ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being State of b₂
for b₄ being set st b₄ in InputVertices b₁ holds
b₃ is_stable_at b₄

proof end;

theorem Th19: :: FACIRC_1:19

for b₁ being non empty non void Circuit-like ManySortedSign
for b₂ being non-empty Circuit of b₁
for b₃ being State of b₂
for b₄ being Gate of b₁ st ( for b₅ being set st b₅ in rng (the_arity_of b₄) holds
b₃ is_stable_at b₅ ) holds
Following b₃ is_stable_at the_result_sort_of b₄

proof end;

theorem Th20: :: FACIRC_1:20

for b₁, b₂ being non empty ManySortedSign
for b₃ being Vertex of b₁ holds
( b₃ in the carrier of (b₁ +* b₂) & b₃ in the carrier of (b₂ +* b₁) )

proof end;

theorem Th21: :: FACIRC_1:21

for b₁, b₂ being non empty unsplit gate`1=arity ManySortedSign
for b₃ being set st b₃ in InnerVertices b₁ holds
( b₃ in InnerVertices (b₁ +* b₂) & b₃ in InnerVertices (b₂ +* b₁) )

proof end;

theorem Th22: :: FACIRC_1:22

for b₁, b₂ being non empty ManySortedSign
for b₃ being set st b₃ in InnerVertices b₂ holds
b₃ in InnerVertices (b₁ +* b₂)

proof end;

theorem Th23: :: FACIRC_1:23

for b₁, b₂ being non empty unsplit gate`1=arity ManySortedSign holds b₁ +* b₂ = b₂ +* b₁

proof end;

theorem Th24: :: FACIRC_1:24

for b₁, b₂ being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign
for b₃ being gate`2=den Boolean Circuit of b₁
for b₄ being gate`2=den Boolean Circuit of b₂ holds b₃ +* b₄ = b₄ +* b₃

proof end;

theorem Th25: :: FACIRC_1:25

for b₁, b₂, b₃ being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign
for b₄ being Boolean Circuit of b₁
for b₅ being Boolean Circuit of b₂
for b₆ being Boolean Circuit of b₃ holds (b₄ +* b₅) +* b₆ = b₄ +* (b₅ +* b₆)

proof end;

theorem Th26: :: FACIRC_1:26

for b₁, b₂ being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign
for b₃ being non-empty gate`2=den Boolean Circuit of b₁
for b₄ being non-empty gate`2=den Boolean Circuit of b₂
for b₅ being State of (b₃ +* b₄) holds
( b₅ | the carrier of b₁ is State of b₃ & b₅ | the carrier of b₂ is State of b₄ )

proof end;

theorem Th27: :: FACIRC_1:27

for b₁, b₂ being non empty unsplit gate`1=arity ManySortedSign holds InnerVertices (b₁ +* b₂) = (InnerVertices b₁) \/ (InnerVertices b₂)

proof end;

theorem Th28: :: FACIRC_1:28

for b₁, b₂ being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st InnerVertices b₂ misses InputVertices b₁ holds
for b₃ being gate`2=den Boolean Circuit of b₁
for b₄ being gate`2=den Boolean Circuit of b₂
for b₅ being State of (b₃ +* b₄)
for b₆ being State of b₃ st b₆ = b₅ | the carrier of b₁ holds
(Following b₅) | the carrier of b₁ = Following b₆

proof end;

theorem Th29: :: FACIRC_1:29

for b₁, b₂ being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st InnerVertices b₁ misses InputVertices b₂ holds
for b₃ being gate`2=den Boolean Circuit of b₁
for b₄ being gate`2=den Boolean Circuit of b₂
for b₅ being State of (b₃ +* b₄)
for b₆ being State of b₄ st b₆ = b₅ | the carrier of b₂ holds
(Following b₅) | the carrier of b₂ = Following b₆

proof end;

theorem Th30: :: FACIRC_1:30

for b₁, b₂ being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st InnerVertices b₂ misses InputVertices b₁ holds
for b₃ being gate`2=den Boolean Circuit of b₁
for b₄ being gate`2=den Boolean Circuit of b₂
for b₅ being State of (b₃ +* b₄)
for b₆ being State of b₃ st b₆ = b₅ | the carrier of b₁ holds
for b₇ being Nat holds (Following b₅,b₇) | the carrier of b₁ = Following b₆,b₇

proof end;

theorem Th31: :: FACIRC_1:31

for b₁, b₂ being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st InnerVertices b₁ misses InputVertices b₂ holds
for b₃ being gate`2=den Boolean Circuit of b₁
for b₄ being gate`2=den Boolean Circuit of b₂
for b₅ being State of (b₃ +* b₄)
for b₆ being State of b₄ st b₆ = b₅ | the carrier of b₂ holds
for b₇ being Nat holds (Following b₅,b₇) | the carrier of b₂ = Following b₆,b₇

proof end;

theorem Th32: :: FACIRC_1:32

for b₁, b₂ being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st InnerVertices b₂ misses InputVertices b₁ holds
for b₃ being gate`2=den Boolean Circuit of b₁
for b₄ being gate`2=den Boolean Circuit of b₂
for b₅ being State of (b₃ +* b₄)
for b₆ being State of b₃ st b₆ = b₅ | the carrier of b₁ holds
for b₇ being set st b₇ in the carrier of b₁ holds
for b₈ being Nat holds (Following b₅,b₈) . b₇ = (Following b₆,b₈) . b₇

proof end;

theorem Th33: :: FACIRC_1:33

for b₁, b₂ being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st InnerVertices b₁ misses InputVertices b₂ holds
for b₃ being gate`2=den Boolean Circuit of b₁
for b₄ being gate`2=den Boolean Circuit of b₂
for b₅ being State of (b₃ +* b₄)
for b₆ being State of b₄ st b₆ = b₅ | the carrier of b₂ holds
for b₇ being set st b₇ in the carrier of b₂ holds
for b₈ being Nat holds (Following b₅,b₈) . b₇ = (Following b₆,b₈) . b₇

proof end;

registration

let c₁ be non empty non void gate`2=den ManySortedSign ;
let c₂ be Gate of c₁;
cluster a₂ `2 -> Relation-like Function-like ;
coherence

proof end;

end;

theorem Th34: :: FACIRC_1:34

for b₁ being non empty non void Circuit-like gate`2=den ManySortedSign
for b₂ being non-empty Circuit of b₁ st b₂ is gate`2=den holds
for b₃ being State of b₂
for b₄ being Gate of b₁ holds (Following b₃) . (the_result_sort_of b₄) = (b₄ `2 ) . (b₃ * (the_arity_of b₄))

proof end;

theorem Th35: :: FACIRC_1:35

for b₁ being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign
for b₂ being non-empty gate`2=den Boolean Circuit of b₁
for b₃ being State of b₂
for b₄ being FinSequence
for b₅ being Function st [b₄,b₅] in the OperSymbols of b₁ holds
(Following b₃) . [b₄,b₅] = b₅ . (b₃ * b₄)

proof end;

theorem Th36: :: FACIRC_1:36

for b₁ being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign
for b₂ being non-empty gate`2=den Boolean Circuit of b₁
for b₃ being State of b₂
for b₄ being FinSequence
for b₅ being Function st [b₄,b₅] in the OperSymbols of b₁ & ( for b₆ being set st b₆ in rng b₄ holds
b₃ is_stable_at b₆ ) holds
Following b₃ is_stable_at [b₄,b₅]

proof end;

theorem Th37: :: FACIRC_1:37

for b₁ being non empty unsplit ManySortedSign holds InnerVertices b₁ = the OperSymbols of b₁

proof end;

theorem Th38: :: FACIRC_1:38

for b₁ being set
for b₂ being FinSequence holds InnerVertices (1GateCircStr b₂,b₁) is Relation

proof end;

theorem Th39: :: FACIRC_1:39

for b₁ being set
for b₂ being nonpair-yielding FinSequence holds not InputVertices (1GateCircStr b₂,b₁) is with_pair

proof end;

theorem Th40: :: FACIRC_1:40

for b₁, b₂, b₃ being set holds InputVertices (1GateCircStr <*b₂,b₃*>,b₁) = {b₂,b₃}

proof end;

theorem Th41: :: FACIRC_1:41

for b₁ being set
for b₂, b₃ being non pair set holds not InputVertices (1GateCircStr <*b₂,b₃*>,b₁) is with_pair

proof end;

theorem Th42: :: FACIRC_1:42

for b₁, b₂, b₃, b₄ being set holds InputVertices (1GateCircStr <*b₂,b₃,b₄*>,b₁) = {b₂,b₃,b₄}

proof end;

theorem Th43: :: FACIRC_1:43

for b₁, b₂, b₃ being set holds
( b₁ in the carrier of (1GateCircStr <*b₁,b₂*>,b₃) & b₂ in the carrier of (1GateCircStr <*b₁,b₂*>,b₃) & [<*b₁,b₂*>,b₃] in the carrier of (1GateCircStr <*b₁,b₂*>,b₃) )

proof end;

theorem Th44: :: FACIRC_1:44

for b₁, b₂, b₃, b₄ being set holds
( b₁ in the carrier of (1GateCircStr <*b₁,b₂,b₃*>,b₄) & b₂ in the carrier of (1GateCircStr <*b₁,b₂,b₃*>,b₄) & b₃ in the carrier of (1GateCircStr <*b₁,b₂,b₃*>,b₄) )

proof end;

theorem Th45: :: FACIRC_1:45

for b₁, b₂ being set
for b₃ being FinSequence holds
( b₂ in the carrier of (1GateCircStr b₃,b₁,b₂) & ( for b₄ being set st b₄ in rng b₃ holds
b₄ in the carrier of (1GateCircStr b₃,b₁,b₂) ) )

proof end;

theorem Th46: :: FACIRC_1:46

for b₁, b₂ being set
for b₃ being FinSequence holds
( 1GateCircStr b₃,b₁,b₂ is gate`1=arity & 1GateCircStr b₃,b₁,b₂ is Circuit-like )

proof end;

theorem Th47: :: FACIRC_1:47

for b₁ being FinSequence
for b₂ being set holds [b₁,b₂] in InnerVertices (1GateCircStr b₁,b₂)

proof end;

definition

let c₁, c₂ be set ;
let c₃ be Function of 2 -tuples_on BOOLEAN , BOOLEAN ;
func 1GateCircuit c₁,c₂,c₃ -> strict gate`2=den Boolean Circuit of 1GateCircStr <*a₁,a₂*>,a₃ equals :: FACIRC_1:def 10
1GateCircuit <*a₁,a₂*>,a₃;
coherence by CIRCCOMB:69;

end;

:: deftheorem Def10 defines 1GateCircuit FACIRC_1:def 10 :

theorem Th48: :: FACIRC_1:48

for b₁, b₂ being set
for b₃ being non empty finite set
for b₄ being Function of 2 -tuples_on b₃,b₃
for b₅ being State of (1GateCircuit <*b₁,b₂*>,b₄) holds
( (Following b₅) . [<*b₁,b₂*>,b₄] = b₄ . <*(b₅ . b₁),(b₅ . b₂)*> & (Following b₅) . b₁ = b₅ . b₁ & (Following b₅) . b₂ = b₅ . b₂ )

proof end;

theorem Th49: :: FACIRC_1:49

for b₁, b₂ being set
for b₃ being non empty finite set
for b₄ being Function of 2 -tuples_on b₃,b₃
for b₅ being State of (1GateCircuit <*b₁,b₂*>,b₄) holds Following b₅ is stable

proof end;

theorem Th50: :: FACIRC_1:50

for b₁, b₂ being set
for b₃ being Function of 2 -tuples_on BOOLEAN , BOOLEAN
for b₄ being State of (1GateCircuit b₁,b₂,b₃) holds
( (Following b₄) . [<*b₁,b₂*>,b₃] = b₃ . <*(b₄ . b₁),(b₄ . b₂)*> & (Following b₄) . b₁ = b₄ . b₁ & (Following b₄) . b₂ = b₄ . b₂ ) by Th48;

theorem Th51: :: FACIRC_1:51

for b₁, b₂ being set
for b₃ being Function of 2 -tuples_on BOOLEAN , BOOLEAN
for b₄ being State of (1GateCircuit b₁,b₂,b₃) holds Following b₄ is stable by Th49;

definition

let c₁, c₂, c₃ be set ;
let c₄ be Function of 3 -tuples_on BOOLEAN , BOOLEAN ;
func 1GateCircuit c₁,c₂,c₃,c₄ -> strict gate`2=den Boolean Circuit of 1GateCircStr <*a₁,a₂,a₃*>,a₄ equals :: FACIRC_1:def 11
1GateCircuit <*a₁,a₂,a₃*>,a₄;
coherence by CIRCCOMB:69;

end;

:: deftheorem Def11 defines 1GateCircuit FACIRC_1:def 11 :

theorem Th52: :: FACIRC_1:52

for b₁, b₂, b₃ being set
for b₄ being non empty finite set
for b₅ being Function of 3 -tuples_on b₄,b₄
for b₆ being State of (1GateCircuit <*b₁,b₂,b₃*>,b₅) holds
( (Following b₆) . [<*b₁,b₂,b₃*>,b₅] = b₅ . <*(b₆ . b₁),(b₆ . b₂),(b₆ . b₃)*> & (Following b₆) . b₁ = b₆ . b₁ & (Following b₆) . b₂ = b₆ . b₂ & (Following b₆) . b₃ = b₆ . b₃ )

proof end;

theorem Th53: :: FACIRC_1:53

for b₁, b₂, b₃ being set
for b₄ being non empty finite set
for b₅ being Function of 3 -tuples_on b₄,b₄
for b₆ being State of (1GateCircuit <*b₁,b₂,b₃*>,b₅) holds Following b₆ is stable

proof end;

theorem Th54: :: FACIRC_1:54

for b₁, b₂, b₃ being set
for b₄ being Function of 3 -tuples_on BOOLEAN , BOOLEAN
for b₅ being State of (1GateCircuit b₁,b₂,b₃,b₄) holds
( (Following b₅) . [<*b₁,b₂,b₃*>,b₄] = b₄ . <*(b₅ . b₁),(b₅ . b₂),(b₅ . b₃)*> & (Following b₅) . b₁ = b₅ . b₁ & (Following b₅) . b₂ = b₅ . b₂ & (Following b₅) . b₃ = b₅ . b₃ ) by Th52;

theorem Th55: :: FACIRC_1:55

for b₁, b₂, b₃ being set
for b₄ being Function of 3 -tuples_on BOOLEAN , BOOLEAN
for b₅ being State of (1GateCircuit b₁,b₂,b₃,b₄) holds Following b₅ is stable by Th53;

definition

let c₁, c₂, c₃ be set ;
let c₄ be Function of 2 -tuples_on BOOLEAN , BOOLEAN ;
func 2GatesCircStr c₁,c₂,c₃,c₄ -> non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: FACIRC_1:def 12
(1GateCircStr <*a₁,a₂*>,a₄) +* (1GateCircStr <*[<*a₁,a₂*>,a₄],a₃*>,a₄);
correctness ;

end;

:: deftheorem Def12 defines 2GatesCircStr FACIRC_1:def 12 :

definition

let c₁, c₂, c₃ be set ;
let c₄ be Function of 2 -tuples_on BOOLEAN , BOOLEAN ;
func 2GatesCircOutput c₁,c₂,c₃,c₄ -> Element of InnerVertices (2GatesCircStr a₁,a₂,a₃,a₄) equals :: FACIRC_1:def 13
[<*[<*a₁,a₂*>,a₄],a₃*>,a₄];
coherence

proof end;

correctness ;

end;

:: deftheorem Def13 defines 2GatesCircOutput FACIRC_1:def 13 :

registration

let c₁, c₂, c₃ be set ;
let c₄ be Function of 2 -tuples_on BOOLEAN , BOOLEAN ;
cluster 2GatesCircOutput a₁,a₂,a₃,a₄ -> non empty pair ;
coherence ;

end;

theorem Th56: :: FACIRC_1:56

for b₁, b₂, b₃ being set
for b₄ being Function of 2 -tuples_on BOOLEAN , BOOLEAN holds InnerVertices (2GatesCircStr b₁,b₂,b₃,b₄) = {[<*b₁,b₂*>,b₄],(2GatesCircOutput b₁,b₂,b₃,b₄)}

proof end;

theorem Th57: :: FACIRC_1:57

for b₁, b₂, b₃ being set
for b₄ being Function of 2 -tuples_on BOOLEAN , BOOLEAN st b₁ <> [<*b₂,b₃*>,b₄] holds
InputVertices (2GatesCircStr b₂,b₃,b₁,b₄) = {b₂,b₃,b₁}

proof end;

definition

let c₁, c₂, c₃ be set ;
let c₄ be Function of 2 -tuples_on BOOLEAN , BOOLEAN ;
func 2GatesCircuit c₁,c₂,c₃,c₄ -> strict gate`2=den Boolean Circuit of 2GatesCircStr a₁,a₂,a₃,a₄ equals :: FACIRC_1:def 14
(1GateCircuit a₁,a₂,a₄) +* (1GateCircuit [<*a₁,a₂*>,a₄],a₃,a₄);
coherence ;

end;

:: deftheorem Def14 defines 2GatesCircuit FACIRC_1:def 14 :

theorem Th58: :: FACIRC_1:58

for b₁, b₂, b₃ being set
for b₄ being Function of 2 -tuples_on BOOLEAN , BOOLEAN holds InnerVertices (2GatesCircStr b₁,b₂,b₃,b₄) is Relation

proof end;

theorem Th59: :: FACIRC_1:59

for b₁ being Function of 2 -tuples_on BOOLEAN , BOOLEAN
for b₂, b₃, b₄ being non pair set holds not InputVertices (2GatesCircStr b₂,b₃,b₄,b₁) is with_pair

proof end;

theorem Th60: :: FACIRC_1:60

for b₁, b₂, b₃ being set
for b₄ being Function of 2 -tuples_on BOOLEAN , BOOLEAN holds
( b₁ in the carrier of (2GatesCircStr b₁,b₂,b₃,b₄) & b₂ in the carrier of (2GatesCircStr b₁,b₂,b₃,b₄) & b₃ in the carrier of (2GatesCircStr b₁,b₂,b₃,b₄) )

proof end;

theorem Th61: :: FACIRC_1:61

for b₁, b₂, b₃ being set
for b₄ being Function of 2 -tuples_on BOOLEAN , BOOLEAN holds
( [<*b₁,b₂*>,b₄] in the carrier of (2GatesCircStr b₁,b₂,b₃,b₄) & [<*[<*b₁,b₂*>,b₄],b₃*>,b₄] in the carrier of (2GatesCircStr b₁,b₂,b₃,b₄) )

proof end;

definition

let c₁ be non empty non void unsplit ManySortedSign ;
let c₂ be Boolean Circuit of c₁;
let c₃ be State of c₂;
let c₄ be Vertex of c₁;
redefine func . as c₃ . c₄ -> Element of BOOLEAN ;
coherence

proof end;

end;

Lemma60: for b₁, b₂, b₃ being set
for b₄ being Function of 2 -tuples_on BOOLEAN , BOOLEAN
for b₅ being State of (2GatesCircuit b₂,b₃,b₁,b₄) st b₁ <> [<*b₂,b₃*>,b₄] holds
( (Following b₅) . (2GatesCircOutput b₂,b₃,b₁,b₄) = b₄ . <*(b₅ . [<*b₂,b₃*>,b₄]),(b₅ . b₁)*> & (Following b₅) . [<*b₂,b₃*>,b₄] = b₄ . <*(b₅ . b₂),(b₅ . b₃)*> & (Following b₅) . b₂ = b₅ . b₂ & (Following b₅) . b₃ = b₅ . b₃ & (Following b₅) . b₁ = b₅ . b₁ )

proof end;

theorem Th62: :: FACIRC_1:62

for b₁, b₂, b₃ being set
for b₄ being Function of 2 -tuples_on BOOLEAN , BOOLEAN
for b₅ being State of (2GatesCircuit b₂,b₃,b₁,b₄) st b₁ <> [<*b₂,b₃*>,b₄] holds
( (Following b₅,2) . (2GatesCircOutput b₂,b₃,b₁,b₄) = b₄ . <*(b₄ . <*(b₅ . b₂),(b₅ . b₃)*>),(b₅ . b₁)*> & (Following b₅,2) . [<*b₂,b₃*>,b₄] = b₄ . <*(b₅ . b₂),(b₅ . b₃)*> & (Following b₅,2) . b₂ = b₅ . b₂ & (Following b₅,2) . b₃ = b₅ . b₃ & (Following b₅,2) . b₁ = b₅ . b₁ )

proof end;

theorem Th63: :: FACIRC_1:63

for b₁, b₂, b₃ being set
for b₄ being Function of 2 -tuples_on BOOLEAN , BOOLEAN
for b₅ being State of (2GatesCircuit b₂,b₃,b₁,b₄) st b₁ <> [<*b₂,b₃*>,b₄] holds
Following b₅,2 is stable

proof end;

theorem Th64: :: FACIRC_1:64

for b₁, b₂, b₃ being set st b₁ <> [<*b₂,b₃*>,'xor' ] holds
for b₄ being State of (2GatesCircuit b₂,b₃,b₁,'xor' )
for b₅, b₆, b₇ being Element of BOOLEAN st b₅ = b₄ . b₂ & b₆ = b₄ . b₃ & b₇ = b₄ . b₁ holds
(Following b₄,2) . (2GatesCircOutput b₂,b₃,b₁,'xor' ) = (b₅ 'xor' b₆) 'xor' b₇

proof end;

theorem Th65: :: FACIRC_1:65

for b₁, b₂, b₃ being set st b₁ <> [<*b₂,b₃*>,'or' ] holds
for b₄ being State of (2GatesCircuit b₂,b₃,b₁,'or' )
for b₅, b₆, b₇ being Element of BOOLEAN st b₅ = b₄ . b₂ & b₆ = b₄ . b₃ & b₇ = b₄ . b₁ holds
(Following b₄,2) . (2GatesCircOutput b₂,b₃,b₁,'or' ) = (b₅ 'or' b₆) 'or' b₇

proof end;

theorem Th66: :: FACIRC_1:66

for b₁, b₂, b₃ being set st b₁ <> [<*b₂,b₃*>,'&' ] holds
for b₄ being State of (2GatesCircuit b₂,b₃,b₁,'&' )
for b₅, b₆, b₇ being Element of BOOLEAN st b₅ = b₄ . b₂ & b₆ = b₄ . b₃ & b₇ = b₄ . b₁ holds
(Following b₄,2) . (2GatesCircOutput b₂,b₃,b₁,'&' ) = (b₅ '&' b₆) '&' b₇

proof end;

definition

let c₁, c₂, c₃ be set ;
func BitAdderOutput c₁,c₂,c₃ -> Element of InnerVertices (2GatesCircStr a₁,a₂,a₃,'xor' ) equals :: FACIRC_1:def 15
2GatesCircOutput a₁,a₂,a₃,'xor' ;
coherence ;

end;

:: deftheorem Def15 defines BitAdderOutput FACIRC_1:def 15 :

definition

let c₁, c₂, c₃ be set ;
func BitAdderCirc c₁,c₂,c₃ -> strict gate`2=den Boolean Circuit of 2GatesCircStr a₁,a₂,a₃,'xor' equals :: FACIRC_1:def 16
2GatesCircuit a₁,a₂,a₃,'xor' ;
coherence ;

end;

:: deftheorem Def16 defines BitAdderCirc FACIRC_1:def 16 :

definition

let c₁, c₂, c₃ be set ;
func MajorityIStr c₁,c₂,c₃ -> non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: FACIRC_1:def 17
((1GateCircStr <*a₁,a₂*>,'&' ) +* (1GateCircStr <*a₂,a₃*>,'&' )) +* (1GateCircStr <*a₃,a₁*>,'&' );
correctness ;

end;

:: deftheorem Def17 defines MajorityIStr FACIRC_1:def 17 :

definition

let c₁, c₂, c₃ be set ;
func MajorityStr c₁,c₂,c₃ -> non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: FACIRC_1:def 18
(MajorityIStr a₁,a₂,a₃) +* (1GateCircStr <*[<*a₁,a₂*>,'&' ],[<*a₂,a₃*>,'&' ],[<*a₃,a₁*>,'&' ]*>,or3 );
correctness ;

end;

:: deftheorem Def18 defines MajorityStr FACIRC_1:def 18 :

definition

let c₁, c₂, c₃ be set ;
func MajorityICirc c₁,c₂,c₃ -> strict gate`2=den Boolean Circuit of MajorityIStr a₁,a₂,a₃ equals :: FACIRC_1:def 19
((1GateCircuit a₁,a₂,'&' ) +* (1GateCircuit a₂,a₃,'&' )) +* (1GateCircuit a₃,a₁,'&' );
coherence ;

end;

:: deftheorem Def19 defines MajorityICirc FACIRC_1:def 19 :

theorem Th67: :: FACIRC_1:67

for b₁, b₂, b₃ being set holds InnerVertices (MajorityStr b₁,b₂,b₃) is Relation

proof end;

theorem Th68: :: FACIRC_1:68

for b₁, b₂, b₃ being non pair set holds not InputVertices (MajorityStr b₁,b₂,b₃) is with_pair

proof end;

theorem Th69: :: FACIRC_1:69

for b₁, b₂, b₃ being set
for b₄ being State of (MajorityICirc b₁,b₂,b₃)
for b₅, b₆ being Element of BOOLEAN st b₅ = b₄ . b₁ & b₆ = b₄ . b₂ holds
(Following b₄) . [<*b₁,b₂*>,'&' ] = b₅ '&' b₆

proof end;

theorem Th70: :: FACIRC_1:70

for b₁, b₂, b₃ being set
for b₄ being State of (MajorityICirc b₁,b₂,b₃)
for b₅, b₆ being Element of BOOLEAN st b₅ = b₄ . b₂ & b₆ = b₄ . b₃ holds
(Following b₄) . [<*b₂,b₃*>,'&' ] = b₅ '&' b₆

proof end;

theorem Th71: :: FACIRC_1:71

for b₁, b₂, b₃ being set
for b₄ being State of (MajorityICirc b₁,b₂,b₃)
for b₅, b₆ being Element of BOOLEAN st b₅ = b₄ . b₃ & b₆ = b₄ . b₁ holds
(Following b₄) . [<*b₃,b₁*>,'&' ] = b₅ '&' b₆

proof end;

definition

let c₁, c₂, c₃ be set ;
func MajorityOutput c₁,c₂,c₃ -> Element of InnerVertices (MajorityStr a₁,a₂,a₃) equals :: FACIRC_1:def 20
[<*[<*a₁,a₂*>,'&' ],[<*a₂,a₃*>,'&' ],[<*a₃,a₁*>,'&' ]*>,or3 ];
coherence

proof end;

correctness ;

end;

:: deftheorem Def20 defines MajorityOutput FACIRC_1:def 20 :

definition

let c₁, c₂, c₃ be set ;
func MajorityCirc c₁,c₂,c₃ -> strict gate`2=den Boolean Circuit of MajorityStr a₁,a₂,a₃ equals :: FACIRC_1:def 21
(MajorityICirc a₁,a₂,a₃) +* (1GateCircuit [<*a₁,a₂*>,'&' ],[<*a₂,a₃*>,'&' ],[<*a₃,a₁*>,'&' ],or3 );
coherence ;

end;

:: deftheorem Def21 defines MajorityCirc FACIRC_1:def 21 :

theorem Th72: :: FACIRC_1:72

for b₁, b₂, b₃ being set holds
( b₁ in the carrier of (MajorityStr b₁,b₂,b₃) & b₂ in the carrier of (MajorityStr b₁,b₂,b₃) & b₃ in the carrier of (MajorityStr b₁,b₂,b₃) )

proof end;

theorem Th73: :: FACIRC_1:73

for b₁, b₂, b₃ being set holds
( [<*b₁,b₂*>,'&' ] in InnerVertices (MajorityStr b₁,b₂,b₃) & [<*b₂,b₃*>,'&' ] in InnerVertices (MajorityStr b₁,b₂,b₃) & [<*b₃,b₁*>,'&' ] in InnerVertices (MajorityStr b₁,b₂,b₃) )

proof end;

theorem Th74: :: FACIRC_1:74

for b₁, b₂, b₃ being non pair set holds
( b₁ in InputVertices (MajorityStr b₁,b₂,b₃) & b₂ in InputVertices (MajorityStr b₁,b₂,b₃) & b₃ in InputVertices (MajorityStr b₁,b₂,b₃) )

proof end;

theorem Th75: :: FACIRC_1:75

for b₁, b₂, b₃ being non pair set holds
( InputVertices (MajorityStr b₁,b₂,b₃) = {b₁,b₂,b₃} & InnerVertices (MajorityStr b₁,b₂,b₃) = {[<*b₁,b₂*>,'&' ],[<*b₂,b₃*>,'&' ],[<*b₃,b₁*>,'&' ]} \/ {(MajorityOutput b₁,b₂,b₃)} )

proof end;

Lemma70: for b₁, b₂, b₃ being non pair set
for b₄ being State of (MajorityCirc b₁,b₂,b₃)
for b₅, b₆, b₇ being Element of BOOLEAN st b₅ = b₄ . b₁ & b₆ = b₄ . b₂ & b₇ = b₄ . b₃ holds
( (Following b₄) . [<*b₁,b₂*>,'&' ] = b₅ '&' b₆ & (Following b₄) . [<*b₂,b₃*>,'&' ] = b₆ '&' b₇ & (Following b₄) . [<*b₃,b₁*>,'&' ] = b₇ '&' b₅ )

proof end;

theorem Th76: :: FACIRC_1:76

for b₁, b₂, b₃ being non pair set
for b₄ being State of (MajorityCirc b₁,b₂,b₃)
for b₅, b₆ being Element of BOOLEAN st b₅ = b₄ . b₁ & b₆ = b₄ . b₂ holds
(Following b₄) . [<*b₁,b₂*>,'&' ] = b₅ '&' b₆

proof end;

theorem Th77: :: FACIRC_1:77

for b₁, b₂, b₃ being non pair set
for b₄ being State of (MajorityCirc b₁,b₂,b₃)
for b₅, b₆ being Element of BOOLEAN st b₅ = b₄ . b₂ & b₆ = b₄ . b₃ holds
(Following b₄) . [<*b₂,b₃*>,'&' ] = b₅ '&' b₆

proof end;

theorem Th78: :: FACIRC_1:78

for b₁, b₂, b₃ being non pair set
for b₄ being State of (MajorityCirc b₁,b₂,b₃)
for b₅, b₆ being Element of BOOLEAN st b₅ = b₄ . b₁ & b₆ = b₄ . b₃ holds
(Following b₄) . [<*b₃,b₁*>,'&' ] = b₆ '&' b₅

proof end;

theorem Th79: :: FACIRC_1:79

for b₁, b₂, b₃ being non pair set
for b₄ being State of (MajorityCirc b₁,b₂,b₃)
for b₅, b₆, b₇ being Element of BOOLEAN st b₅ = b₄ . [<*b₁,b₂*>,'&' ] & b₆ = b₄ . [<*b₂,b₃*>,'&' ] & b₇ = b₄ . [<*b₃,b₁*>,'&' ] holds
(Following b₄) . (MajorityOutput b₁,b₂,b₃) = (b₅ 'or' b₆) 'or' b₇

proof end;

Lemma72: for b₁, b₂, b₃ being non pair set
for b₄ being State of (MajorityCirc b₁,b₂,b₃)
for b₅, b₆, b₇ being Element of BOOLEAN st b₅ = b₄ . b₁ & b₆ = b₄ . b₂ & b₇ = b₄ . b₃ holds
( (Following b₄,2) . (MajorityOutput b₁,b₂,b₃) = ((b₅ '&' b₆) 'or' (b₆ '&' b₇)) 'or' (b₇ '&' b₅) & (Following b₄,2) . [<*b₁,b₂*>,'&' ] = b₅ '&' b₆ & (Following b₄,2) . [<*b₂,b₃*>,'&' ] = b₆ '&' b₇ & (Following b₄,2) . [<*b₃,b₁*>,'&' ] = b₇ '&' b₅ )

proof end;

theorem Th80: :: FACIRC_1:80

for b₁, b₂, b₃ being non pair set
for b₄ being State of (MajorityCirc b₁,b₂,b₃)
for b₅, b₆ being Element of BOOLEAN st b₅ = b₄ . b₁ & b₆ = b₄ . b₂ holds
(Following b₄,2) . [<*b₁,b₂*>,'&' ] = b₅ '&' b₆

proof end;

theorem Th81: :: FACIRC_1:81

for b₁, b₂, b₃ being non pair set
for b₄ being State of (MajorityCirc b₁,b₂,b₃)
for b₅, b₆ being Element of BOOLEAN st b₅ = b₄ . b₂ & b₆ = b₄ . b₃ holds
(Following b₄,2) . [<*b₂,b₃*>,'&' ] = b₅ '&' b₆

proof end;

theorem Th82: :: FACIRC_1:82

for b₁, b₂, b₃ being non pair set
for b₄ being State of (MajorityCirc b₁,b₂,b₃)
for b₅, b₆ being Element of BOOLEAN st b₅ = b₄ . b₁ & b₆ = b₄ . b₃ holds
(Following b₄,2) . [<*b₃,b₁*>,'&' ] = b₆ '&' b₅

proof end;

theorem Th83: :: FACIRC_1:83

for b₁, b₂, b₃ being non pair set
for b₄ being State of (MajorityCirc b₁,b₂,b₃)
for b₅, b₆, b₇ being Element of BOOLEAN st b₅ = b₄ . b₁ & b₆ = b₄ . b₂ & b₇ = b₄ . b₃ holds
(Following b₄,2) . (MajorityOutput b₁,b₂,b₃) = ((b₅ '&' b₆) 'or' (b₆ '&' b₇)) 'or' (b₇ '&' b₅) by Lemma72;

theorem Th84: :: FACIRC_1:84

for b₁, b₂, b₃ being non pair set
for b₄ being State of (MajorityCirc b₁,b₂,b₃) holds Following b₄,2 is stable

proof end;

definition

let c₁, c₂, c₃ be set ;
func BitAdderWithOverflowStr c₁,c₂,c₃ -> non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: FACIRC_1:def 22
(2GatesCircStr a₁,a₂,a₃,'xor' ) +* (MajorityStr a₁,a₂,a₃);
coherence ;

end;

:: deftheorem Def22 defines BitAdderWithOverflowStr FACIRC_1:def 22 :

theorem Th85: :: FACIRC_1:85

for b₁, b₂, b₃ being non pair set holds InputVertices (BitAdderWithOverflowStr b₁,b₂,b₃) = {b₁,b₂,b₃}

proof end;

theorem Th86: :: FACIRC_1:86

for b₁, b₂, b₃ being non pair set holds InnerVertices (BitAdderWithOverflowStr b₁,b₂,b₃) = ({[<*b₁,b₂*>,'xor' ],(2GatesCircOutput b₁,b₂,b₃,'xor' )} \/ {[<*b₁,b₂*>,'&' ],[<*b₂,b₃*>,'&' ],[<*b₃,b₁*>,'&' ]}) \/ {(MajorityOutput b₁,b₂,b₃)}

proof end;

theorem Th87: :: FACIRC_1:87

for b₁, b₂, b₃ being set
for b₄ being non empty ManySortedSign st b₄ = BitAdderWithOverflowStr b₁,b₂,b₃ holds
( b₁ in the carrier of b₄ & b₂ in the carrier of b₄ & b₃ in the carrier of b₄ )

proof end;

definition

let c₁, c₂, c₃ be set ;
func BitAdderWithOverflowCirc c₁,c₂,c₃ -> strict gate`2=den Boolean Circuit of BitAdderWithOverflowStr a₁,a₂,a₃ equals :: FACIRC_1:def 23
(BitAdderCirc a₁,a₂,a₃) +* (MajorityCirc a₁,a₂,a₃);
coherence ;

end;

:: deftheorem Def23 defines BitAdderWithOverflowCirc FACIRC_1:def 23 :

theorem Th88: :: FACIRC_1:88

for b₁, b₂, b₃ being set holds InnerVertices (BitAdderWithOverflowStr b₁,b₂,b₃) is Relation

proof end;

theorem Th89: :: FACIRC_1:89

for b₁, b₂, b₃ being non pair set holds not InputVertices (BitAdderWithOverflowStr b₁,b₂,b₃) is with_pair

proof end;

theorem Th90: :: FACIRC_1:90

for b₁, b₂, b₃ being set holds
( BitAdderOutput b₁,b₂,b₃ in InnerVertices (BitAdderWithOverflowStr b₁,b₂,b₃) & MajorityOutput b₁,b₂,b₃ in InnerVertices (BitAdderWithOverflowStr b₁,b₂,b₃) ) by Th21;

theorem Th91: :: FACIRC_1:91

for b₁, b₂, b₃ being non pair set
for b₄ being State of (BitAdderWithOverflowCirc b₁,b₂,b₃)
for b₅, b₆, b₇ being Element of BOOLEAN st b₅ = b₄ . b₁ & b₆ = b₄ . b₂ & b₇ = b₄ . b₃ holds
( (Following b₄,2) . (BitAdderOutput b₁,b₂,b₃) = (b₅ 'xor' b₆) 'xor' b₇ & (Following b₄,2) . (MajorityOutput b₁,b₂,b₃) = ((b₅ '&' b₆) 'or' (b₆ '&' b₇)) 'or' (b₇ '&' b₅) )

proof end;

theorem Th92: :: FACIRC_1:92

for b₁, b₂, b₃ being non pair set
for b₄ being State of (BitAdderWithOverflowCirc b₁,b₂,b₃) holds Following b₄,2 is stable

proof end;