for b₁ being set
for b₂ being non empty ManySortedSign st b₁ in the carrier of b₂ holds
(SingleMSS b₁) +* b₂ = ManySortedSign(# the carrier of b₂,the OperSymbols of b₂,the Arity of b₂,the ResultSort of b₂ #)

proof end;

theorem Th6: :: FACIRC_2:6

for b₁ being set
for b₂ being non empty strict ManySortedSign
for b₃ being Boolean MSAlgebra of b₂ st b₁ in the carrier of b₂ holds
(SingleMSA b₁) +* b₃ = MSAlgebra(# the Sorts of b₃,the Charact of b₃ #)

proof end;

notation

synonym <*> for {} ;

end;

definition

redefine func <*> as <*> -> FinSeqLen of 0;
coherence

proof end;

end;

definition

let c₁ be Nat;
let c₂, c₃ be FinSequence;
E4: ( 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) is unsplit & 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) is gate`1=arity & 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) is gate`2isBoolean & not 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) is void & not 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) is empty & 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) is strict ) ;
func c₁ -BitAdderStr c₂,c₃ -> non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign means :Def3: :: FACIRC_2:def 3
ex b₁, b₂ being ManySortedSet of NAT st
( a₄ = b₁ . a₁ & b₁ . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & b₂ . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for b₃ being Nat
for b₄ being non empty ManySortedSign
for b₅ being set st b₄ = b₁ . b₃ & b₅ = b₂ . b₃ holds
( b₁ . (b₃ + 1) = b₄ +* (BitAdderWithOverflowStr (a₂ . (b₃ + 1)),(a₃ . (b₃ + 1)),b₅) & b₂ . (b₃ + 1) = MajorityOutput (a₂ . (b₃ + 1)),(a₃ . (b₃ + 1)),b₅ ) ) );
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def3 defines -BitAdderStr FACIRC_2:def 3 :

definition

let c₁ be Nat;
let c₂, c₃ be FinSequence;
func c₁ -BitAdderCirc c₂,c₃ -> strict gate`2=den Boolean Circuit of a₁ -BitAdderStr a₂,a₃ means :Def4: :: FACIRC_2:def 4
ex b₁, b₂, b₃ being ManySortedSet of NAT st
( a₁ -BitAdderStr a₂,a₃ = b₁ . a₁ & a₄ = b₂ . a₁ & b₁ . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & b₂ . 0 = 1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & b₃ . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for b₄ being Nat
for b₅ being non empty ManySortedSign
for b₆ being non-empty MSAlgebra of b₅
for b₇ being set st b₅ = b₁ . b₄ & b₆ = b₂ . b₄ & b₇ = b₃ . b₄ holds
( b₁ . (b₄ + 1) = b₅ +* (BitAdderWithOverflowStr (a₂ . (b₄ + 1)),(a₃ . (b₄ + 1)),b₇) & b₂ . (b₄ + 1) = b₆ +* (BitAdderWithOverflowCirc (a₂ . (b₄ + 1)),(a₃ . (b₄ + 1)),b₇) & b₃ . (b₄ + 1) = MajorityOutput (a₂ . (b₄ + 1)),(a₃ . (b₄ + 1)),b₇ ) ) );
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def4 defines -BitAdderCirc FACIRC_2:def 4 :

definition

let c₁ be Nat;
let c₂, c₃ be FinSequence;
set c₄ = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )];
func c₁ -BitMajorityOutput c₂,c₃ -> Element of InnerVertices (a₁ -BitAdderStr a₂,a₃) means :Def5: :: FACIRC_2:def 5
ex b₁ being ManySortedSet of NAT st
( a₄ = b₁ . a₁ & b₁ . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for b₂ being Nat
for b₃ being set st b₃ = b₁ . b₂ holds
b₁ . (b₂ + 1) = MajorityOutput (a₂ . (b₂ + 1)),(a₃ . (b₂ + 1)),b₃ ) );
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def5 defines -BitMajorityOutput FACIRC_2:def 5 :

theorem Th7: :: FACIRC_2:7

for b₁, b₂ being FinSequence
for b₃, b₄, b₅ being ManySortedSet of NAT st b₃ . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & b₄ . 0 = 1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & b₅ . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] & ( for b₆ being Nat
for b₇ being non empty ManySortedSign
for b₈ being non-empty MSAlgebra of b₇
for b₉ being set st b₇ = b₃ . b₆ & b₈ = b₄ . b₆ & b₉ = b₅ . b₆ holds
( b₃ . (b₆ + 1) = b₇ +* (BitAdderWithOverflowStr (b₁ . (b₆ + 1)),(b₂ . (b₆ + 1)),b₉) & b₄ . (b₆ + 1) = b₈ +* (BitAdderWithOverflowCirc (b₁ . (b₆ + 1)),(b₂ . (b₆ + 1)),b₉) & b₅ . (b₆ + 1) = MajorityOutput (b₁ . (b₆ + 1)),(b₂ . (b₆ + 1)),b₉ ) ) holds
for b₆ being Nat holds
( b₆ -BitAdderStr b₁,b₂ = b₃ . b₆ & b₆ -BitAdderCirc b₁,b₂ = b₄ . b₆ & b₆ -BitMajorityOutput b₁,b₂ = b₅ . b₆ )

proof end;

theorem Th8: :: FACIRC_2:8

for b₁, b₂ being FinSequence holds
( 0 -BitAdderStr b₁,b₂ = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & 0 -BitAdderCirc b₁,b₂ = 1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) & 0 -BitMajorityOutput b₁,b₂ = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] )

proof end;

theorem Th9: :: FACIRC_2:9

for b₁, b₂ being FinSequence
for b₃ being set st b₃ = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] holds
( 1 -BitAdderStr b₁,b₂ = (1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE )) +* (BitAdderWithOverflowStr (b₁ . 1),(b₂ . 1),b₃) & 1 -BitAdderCirc b₁,b₂ = (1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> FALSE )) +* (BitAdderWithOverflowCirc (b₁ . 1),(b₂ . 1),b₃) & 1 -BitMajorityOutput b₁,b₂ = MajorityOutput (b₁ . 1),(b₂ . 1),b₃ )

proof end;

theorem Th10: :: FACIRC_2:10

for b₁, b₂, b₃ being set st b₃ = [<*> ,((0 -tuples_on BOOLEAN ) --> FALSE )] holds
( 1 -BitAdderStr <*b₁*>,<*b₂*> = (1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE )) +* (BitAdderWithOverflowStr b₁,b₂,b₃) & 1 -BitAdderCirc <*b₁*>,<*b₂*> = (1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> FALSE )) +* (BitAdderWithOverflowCirc b₁,b₂,b₃) & 1 -BitMajorityOutput <*b₁*>,<*b₂*> = MajorityOutput b₁,b₂,b₃ )

proof end;

theorem Th11: :: FACIRC_2:11

for b₁ being Nat
for b₂, b₃ being FinSeqLen of b₁
for b₄, b₅, b₆, b₇ being FinSequence holds
( b₁ -BitAdderStr (b₂ ^ b₄),(b₃ ^ b₆) = b₁ -BitAdderStr (b₂ ^ b₅),(b₃ ^ b₇) & b₁ -BitAdderCirc (b₂ ^ b₄),(b₃ ^ b₆) = b₁ -BitAdderCirc (b₂ ^ b₅),(b₃ ^ b₇) & b₁ -BitMajorityOutput (b₂ ^ b₄),(b₃ ^ b₆) = b₁ -BitMajorityOutput (b₂ ^ b₅),(b₃ ^ b₇) )

proof end;

theorem Th12: :: FACIRC_2:12

for b₁ being Nat
for b₂, b₃ being FinSeqLen of b₁
for b₄, b₅ being set holds
( (b₁ + 1) -BitAdderStr (b₂ ^ <*b₄*>),(b₃ ^ <*b₅*>) = (b₁ -BitAdderStr b₂,b₃) +* (BitAdderWithOverflowStr b₄,b₅,(b₁ -BitMajorityOutput b₂,b₃)) & (b₁ + 1) -BitAdderCirc (b₂ ^ <*b₄*>),(b₃ ^ <*b₅*>) = (b₁ -BitAdderCirc b₂,b₃) +* (BitAdderWithOverflowCirc b₄,b₅,(b₁ -BitMajorityOutput b₂,b₃)) & (b₁ + 1) -BitMajorityOutput (b₂ ^ <*b₄*>),(b₃ ^ <*b₅*>) = MajorityOutput b₄,b₅,(b₁ -BitMajorityOutput b₂,b₃) )

proof end;

theorem Th13: :: FACIRC_2:13

for b₁ being Nat
for b₂, b₃ being FinSequence holds
( (b₁ + 1) -BitAdderStr b₂,b₃ = (b₁ -BitAdderStr b₂,b₃) +* (BitAdderWithOverflowStr (b₂ . (b₁ + 1)),(b₃ . (b₁ + 1)),(b₁ -BitMajorityOutput b₂,b₃)) & (b₁ + 1) -BitAdderCirc b₂,b₃ = (b₁ -BitAdderCirc b₂,b₃) +* (BitAdderWithOverflowCirc (b₂ . (b₁ + 1)),(b₃ . (b₁ + 1)),(b₁ -BitMajorityOutput b₂,b₃)) & (b₁ + 1) -BitMajorityOutput b₂,b₃ = MajorityOutput (b₂ . (b₁ + 1)),(b₃ . (b₁ + 1)),(b₁ -BitMajorityOutput b₂,b₃) )

proof end;

theorem Th14: :: FACIRC_2:14

for b₁, b₂ being Nat st b₁ <= b₂ holds
for b₃, b₄ being FinSequence holds InnerVertices (b₁ -BitAdderStr b₃,b₄) c= InnerVertices (b₂ -BitAdderStr b₃,b₄)

proof end;

theorem Th15: :: FACIRC_2:15

for b₁ being Nat
for b₂, b₃ being FinSequence holds InnerVertices ((b₁ + 1) -BitAdderStr b₂,b₃) = (InnerVertices (b₁ -BitAdderStr b₂,b₃)) \/ (InnerVertices (BitAdderWithOverflowStr (b₂ . (b₁ + 1)),(b₃ . (b₁ + 1)),(b₁ -BitMajorityOutput b₂,b₃)))

proof end;

definition

let c₁, c₂ be Nat;
assume E13: ( c₁ >= 1 & c₁ <= c₂ ) ;
let c₃, c₄ be FinSequence;
func c₁,c₂ -BitAdderOutput c₃,c₄ -> Element of InnerVertices (a₂ -BitAdderStr a₃,a₄) means :Def6: :: FACIRC_2:def 6
ex b₁ being Nat st
( a₁ = b₁ + 1 & a₅ = BitAdderOutput (a₃ . a₁),(a₄ . a₁),(b₁ -BitMajorityOutput a₃,a₄) );
uniqueness ;
existence

proof end;

end;

:: deftheorem Def6 defines -BitAdderOutput FACIRC_2:def 6 :

theorem Th16: :: FACIRC_2:16

for b₁, b₂ being Nat st b₂ < b₁ holds
for b₃, b₄ being FinSequence holds (b₂ + 1),b₁ -BitAdderOutput b₃,b₄ = BitAdderOutput (b₃ . (b₂ + 1)),(b₄ . (b₂ + 1)),(b₂ -BitMajorityOutput b₃,b₄)

proof end;

E14: now

let c₁ be Nat;
let c₂ be FinSeqLen of c₁ + 1;
c₁ >= 0 by NAT_1:18;
then E15: ( c₁ + 1 <> 0 & len c₂ = c₁ + 1 ) by CIRCCOMB:def 12, NAT_1:38;
then c₂ <> <*> by FINSEQ_1:25;
then consider c₃ being FinSequence, c₄ being set such that
E16: c₂ = c₃ ^ <*c₄*> by FINSEQ_1:63;
len <*c₄*> = 1 by FINSEQ_1:57;
then c₁ + 1 = (len c₃) + 1 by E15, E16, FINSEQ_1:35;
then len c₃ = c₁ ;
then reconsider c₅ = c₃ as FinSeqLen of c₁ by CIRCCOMB:def 12;
take c₆ = c₅;
take c₇ = c₄;
thus c₂ = c₆ ^ <*c₇*> by E16;

end;

E15: now

let c₁ be Nat;
let c₂ be nonpair-yielding FinSeqLen of c₁ + 1;
consider c₃ being FinSeqLen of c₁, c₄ being set such that
E16: c₂ = c₃ ^ <*c₄*> by Lemma14;
E17: ( dom c₃ c= dom c₂ & c₃ = c₂ | (dom c₃) ) by E16, FINSEQ_1:33, FINSEQ_1:39;
c₃ is nonpair-yielding

proof

let c₅ be set ; :: according to FACIRC_1:def 3
assume c₅ in dom c₃ ;
then ( c₅ in dom c₂ & c₃ . c₅ = c₂ . c₅ ) by E17, FUNCT_1:70;
hence not c₃ . c₅ is pair by FACIRC_1:def 3;

end;

then reconsider c₅ = c₃ as nonpair-yielding FinSeqLen of c₁ ;
( c₁ + 1 in Seg (c₁ + 1) & dom c₂ = Seg (len c₂) ) by FINSEQ_1:6, FINSEQ_1:def 3;
then ( c₁ + 1 in dom c₂ & c₂ . ((len c₅) + 1) = c₄ & len c₅ = c₁ ) by E16, CIRCCOMB:def 12, FINSEQ_1:59;
then reconsider c₆ = c₄ as non pair set by FACIRC_1:def 3;
take c₇ = c₅;
take c₈ = c₆;
thus c₂ = c₇ ^ <*c₈*> by E16;

end;

theorem Th17: :: FACIRC_2:17

for b₁ being Nat
for b₂, b₃ being FinSequence holds InnerVertices (b₁ -BitAdderStr b₂,b₃) is Relation

proof end;

theorem Th18: :: FACIRC_2:18

for b₁, b₂, b₃ being set holds InnerVertices (MajorityIStr b₁,b₂,b₃) = {[<*b₁,b₂*>,'&' ],[<*b₂,b₃*>,'&' ],[<*b₃,b₁*>,'&' ]}

proof end;

theorem Th19: :: FACIRC_2:19

for b₁, b₂, b₃ being set st b₁ <> [<*b₂,b₃*>,'&' ] & b₂ <> [<*b₃,b₁*>,'&' ] & b₃ <> [<*b₁,b₂*>,'&' ] holds
InputVertices (MajorityIStr b₁,b₂,b₃) = {b₁,b₂,b₃}

proof end;

theorem Th20: :: FACIRC_2:20

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

proof end;

theorem Th21: :: FACIRC_2:21

for b₁, b₂, b₃ being set st b₁ <> [<*b₂,b₃*>,'&' ] & b₂ <> [<*b₃,b₁*>,'&' ] & b₃ <> [<*b₁,b₂*>,'&' ] holds
InputVertices (MajorityStr b₁,b₂,b₃) = {b₁,b₂,b₃}

proof end;

theorem Th22: :: FACIRC_2:22

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

proof end;

theorem Th23: :: FACIRC_2:23

for b₁, b₂, b₃ being set st b₁ <> [<*b₂,b₃*>,'&' ] & b₂ <> [<*b₃,b₁*>,'&' ] & b₃ <> [<*b₁,b₂*>,'&' ] & b₃ <> [<*b₁,b₂*>,'xor' ] holds
InputVertices (BitAdderWithOverflowStr b₁,b₂,b₃) = {b₁,b₂,b₃}

proof end;

theorem Th24: :: FACIRC_2:24

for b₁, b₂, b₃ being 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;

registration

cluster empty -> non pair set ;
coherence

proof end;

end;

registration

cluster <*> -> non pair nonpair-yielding ;
coherence

proof end;

let c₁ be nonpair-yielding Function;
let c₂ be set ;
cluster a₁ . a₂ -> non pair ;
coherence

proof end;

end;

registration

let c₁ be Nat;
let c₂, c₃ be FinSequence;
cluster a₁ -BitMajorityOutput a₂,a₃ -> pair ;
coherence

proof end;

end;

theorem Th25: :: FACIRC_2:25

for b₁, b₂ being FinSequence
for b₃ being Nat holds
( ( (b₃ -BitMajorityOutput b₁,b₂) `1 = <*> & (b₃ -BitMajorityOutput b₁,b₂) `2 = (0 -tuples_on BOOLEAN ) --> FALSE & proj1 ((b₃ -BitMajorityOutput b₁,b₂) `2 ) = 0 -tuples_on BOOLEAN ) or ( Card ((b₃ -BitMajorityOutput b₁,b₂) `1 ) = 3 & (b₃ -BitMajorityOutput b₁,b₂) `2 = or3 & proj1 ((b₃ -BitMajorityOutput b₁,b₂) `2 ) = 3 -tuples_on BOOLEAN ) )

proof end;

theorem Th26: :: FACIRC_2:26

for b₁ being Nat
for b₂, b₃ being FinSequence
for b₄ being set holds
( b₁ -BitMajorityOutput b₂,b₃ <> [b₄,'&' ] & b₁ -BitMajorityOutput b₂,b₃ <> [b₄,'xor' ] )

proof end;

theorem Th27: :: FACIRC_2:27

for b₁, b₂ being nonpair-yielding FinSequence
for b₃ being Nat holds
( InputVertices ((b₃ + 1) -BitAdderStr b₁,b₂) = (InputVertices (b₃ -BitAdderStr b₁,b₂)) \/ ((InputVertices (BitAdderWithOverflowStr (b₁ . (b₃ + 1)),(b₂ . (b₃ + 1)),(b₃ -BitMajorityOutput b₁,b₂))) \ {(b₃ -BitMajorityOutput b₁,b₂)}) & InnerVertices (b₃ -BitAdderStr b₁,b₂) is Relation & not InputVertices (b₃ -BitAdderStr b₁,b₂) is with_pair )

proof end;

theorem Th28: :: FACIRC_2:28

for b₁ being Nat
for b₂, b₃ being nonpair-yielding FinSeqLen of b₁ holds InputVertices (b₁ -BitAdderStr b₂,b₃) = (rng b₂) \/ (rng b₃)

proof end;

Lemma26: for b₁, b₂, b₃ being 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 Th29: :: FACIRC_2:29

for b₁, b₂, b₃ being 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;

Lemma28: for b₁, b₂, b₃ being set st b₁ <> [<*b₂,b₃*>,'&' ] & b₂ <> [<*b₃,b₁*>,'&' ] & b₃ <> [<*b₁,b₂*>,'&' ] holds
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 Th30: :: FACIRC_2:30

for b₁, b₂, b₃ being set st b₁ <> [<*b₂,b₃*>,'&' ] & b₂ <> [<*b₃,b₁*>,'&' ] & b₃ <> [<*b₁,b₂*>,'&' ] & b₃ <> [<*b₁,b₂*>,'xor' ] holds
for b₄ being State of (MajorityCirc b₁,b₂,b₃) holds Following b₄,2 is stable

proof end;

theorem Th31: :: FACIRC_2:31

for b₁, b₂, b₃ being set st b₁ <> [<*b₂,b₃*>,'&' ] & b₂ <> [<*b₃,b₁*>,'&' ] & b₃ <> [<*b₁,b₂*>,'&' ] & b₃ <> [<*b₁,b₂*>,'xor' ] holds
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 Th32: :: FACIRC_2:32

proof end;

Lemma31: for b₁ being Nat ex b₂ being Function of NAT , NAT st
( b₂ . 0 = 1 & b₂ . 1 = 2 & b₂ . 2 = b₁ )

proof end;

theorem Th33: :: FACIRC_2:33

for b₁ being Nat
for b₂, b₃ being nonpair-yielding FinSeqLen of b₁
for b₄ being State of (b₁ -BitAdderCirc b₂,b₃) holds Following b₄,(1 + (2 * b₁)) is stable

proof end;

theorem Th34: :: FACIRC_2:34

for b₁ being Nat
for b₂ being FinSeqLen of b₁ + 1 ex b₃ being FinSeqLen of b₁ex b₄ being set st b₂ = b₃ ^ <*b₄*> by Lemma14;

theorem Th35: :: FACIRC_2:35

canceled;

theorem Th36: :: FACIRC_2:36

for b₁ being Nat
for b₂ being nonpair-yielding FinSeqLen of b₁ + 1 ex b₃ being nonpair-yielding FinSeqLen of b₁ex b₄ being non pair set st b₂ = b₃ ^ <*b₄*> by Lemma15;

theorem Th37: :: FACIRC_2:37

for b₁ being Nat ex b₂ being Function of NAT , NAT st
( b₂ . 0 = 1 & b₂ . 1 = 2 & b₂ . 2 = b₁ ) by Lemma31;