:: FSCIRC_2 semantic presentation

definition

let c₁ be Nat;
let c₂, c₃ be FinSequence;
E1: ( 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) is unsplit & 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) is gate`1=arity & 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) is gate`2isBoolean & not 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) is void & not 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) is empty & 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) is strict ) ;
func c₁ -BitSubtracterStr c₂,c₃ -> non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign means :Def1: :: FSCIRC_2:def 1
ex b₁, b₂ being ManySortedSet of NAT st
( a₄ = b₁ . a₁ & b₁ . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & b₂ . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( 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₄ +* (BitSubtracterWithBorrowStr (a₂ . (b₃ + 1)),(a₃ . (b₃ + 1)),b₅) & b₂ . (b₃ + 1) = BorrowOutput (a₂ . (b₃ + 1)),(a₃ . (b₃ + 1)),b₅ ) ) );
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def1 defines -BitSubtracterStr FSCIRC_2:def 1 :

definition

let c₁ be Nat;
let c₂, c₃ be FinSequence;
func c₁ -BitSubtracterCirc c₂,c₃ -> strict gate`2=den Boolean Circuit of a₁ -BitSubtracterStr a₂,a₃ means :Def2: :: FSCIRC_2:def 2
ex b₁, b₂, b₃ being ManySortedSet of NAT st
( a₁ -BitSubtracterStr a₂,a₃ = b₁ . a₁ & a₄ = b₂ . a₁ & b₁ . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & b₂ . 0 = 1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & b₃ . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( 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₅ +* (BitSubtracterWithBorrowStr (a₂ . (b₄ + 1)),(a₃ . (b₄ + 1)),b₇) & b₂ . (b₄ + 1) = b₆ +* (BitSubtracterWithBorrowCirc (a₂ . (b₄ + 1)),(a₃ . (b₄ + 1)),b₇) & b₃ . (b₄ + 1) = BorrowOutput (a₂ . (b₄ + 1)),(a₃ . (b₄ + 1)),b₇ ) ) );
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def2 defines -BitSubtracterCirc FSCIRC_2:def 2 :

definition

let c₁ be Nat;
let c₂, c₃ be FinSequence;
set c₄ = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )];
func c₁ -BitBorrowOutput c₂,c₃ -> Element of InnerVertices (a₁ -BitSubtracterStr a₂,a₃) means :Def3: :: FSCIRC_2:def 3
ex b₁ being ManySortedSet of NAT st
( a₄ = b₁ . a₁ & b₁ . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( for b₂ being Nat holds b₁ . (b₂ + 1) = BorrowOutput (a₂ . (b₂ + 1)),(a₃ . (b₂ + 1)),(b₁ . b₂) ) );
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def3 defines -BitBorrowOutput FSCIRC_2:def 3 :

theorem Th1: :: FSCIRC_2:1

for b₁, b₂ being FinSequence
for b₃, b₄, b₅ being ManySortedSet of NAT st b₃ . 0 = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & b₄ . 0 = 1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & b₅ . 0 = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] & ( 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₇ +* (BitSubtracterWithBorrowStr (b₁ . (b₆ + 1)),(b₂ . (b₆ + 1)),b₉) & b₄ . (b₆ + 1) = b₈ +* (BitSubtracterWithBorrowCirc (b₁ . (b₆ + 1)),(b₂ . (b₆ + 1)),b₉) & b₅ . (b₆ + 1) = BorrowOutput (b₁ . (b₆ + 1)),(b₂ . (b₆ + 1)),b₉ ) ) holds
for b₆ being Nat holds
( b₆ -BitSubtracterStr b₁,b₂ = b₃ . b₆ & b₆ -BitSubtracterCirc b₁,b₂ = b₄ . b₆ & b₆ -BitBorrowOutput b₁,b₂ = b₅ . b₆ )

proof end;

theorem Th2: :: FSCIRC_2:2

for b₁, b₂ being FinSequence holds
( 0 -BitSubtracterStr b₁,b₂ = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & 0 -BitSubtracterCirc b₁,b₂ = 1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> TRUE ) & 0 -BitBorrowOutput b₁,b₂ = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] )

proof end;

theorem Th3: :: FSCIRC_2:3

for b₁, b₂ being FinSequence
for b₃ being set st b₃ = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] holds
( 1 -BitSubtracterStr b₁,b₂ = (1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE )) +* (BitSubtracterWithBorrowStr (b₁ . 1),(b₂ . 1),b₃) & 1 -BitSubtracterCirc b₁,b₂ = (1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> TRUE )) +* (BitSubtracterWithBorrowCirc (b₁ . 1),(b₂ . 1),b₃) & 1 -BitBorrowOutput b₁,b₂ = BorrowOutput (b₁ . 1),(b₂ . 1),b₃ )

proof end;

theorem Th4: :: FSCIRC_2:4

for b₁, b₂, b₃ being set st b₃ = [<*> ,((0 -tuples_on BOOLEAN ) --> TRUE )] holds
( 1 -BitSubtracterStr <*b₁*>,<*b₂*> = (1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> TRUE )) +* (BitSubtracterWithBorrowStr b₁,b₂,b₃) & 1 -BitSubtracterCirc <*b₁*>,<*b₂*> = (1GateCircuit <*> ,((0 -tuples_on BOOLEAN ) --> TRUE )) +* (BitSubtracterWithBorrowCirc b₁,b₂,b₃) & 1 -BitBorrowOutput <*b₁*>,<*b₂*> = BorrowOutput b₁,b₂,b₃ )

proof end;

theorem Th5: :: FSCIRC_2:5

for b₁ being Nat
for b₂, b₃ being FinSeqLen of b₁
for b₄, b₅, b₆, b₇ being FinSequence holds
( b₁ -BitSubtracterStr (b₂ ^ b₄),(b₃ ^ b₆) = b₁ -BitSubtracterStr (b₂ ^ b₅),(b₃ ^ b₇) & b₁ -BitSubtracterCirc (b₂ ^ b₄),(b₃ ^ b₆) = b₁ -BitSubtracterCirc (b₂ ^ b₅),(b₃ ^ b₇) & b₁ -BitBorrowOutput (b₂ ^ b₄),(b₃ ^ b₆) = b₁ -BitBorrowOutput (b₂ ^ b₅),(b₃ ^ b₇) )

proof end;

theorem Th6: :: FSCIRC_2:6

for b₁ being Nat
for b₂, b₃ being FinSeqLen of b₁
for b₄, b₅ being set holds
( (b₁ + 1) -BitSubtracterStr (b₂ ^ <*b₄*>),(b₃ ^ <*b₅*>) = (b₁ -BitSubtracterStr b₂,b₃) +* (BitSubtracterWithBorrowStr b₄,b₅,(b₁ -BitBorrowOutput b₂,b₃)) & (b₁ + 1) -BitSubtracterCirc (b₂ ^ <*b₄*>),(b₃ ^ <*b₅*>) = (b₁ -BitSubtracterCirc b₂,b₃) +* (BitSubtracterWithBorrowCirc b₄,b₅,(b₁ -BitBorrowOutput b₂,b₃)) & (b₁ + 1) -BitBorrowOutput (b₂ ^ <*b₄*>),(b₃ ^ <*b₅*>) = BorrowOutput b₄,b₅,(b₁ -BitBorrowOutput b₂,b₃) )

proof end;

theorem Th7: :: FSCIRC_2:7

for b₁ being Nat
for b₂, b₃ being FinSequence holds
( (b₁ + 1) -BitSubtracterStr b₂,b₃ = (b₁ -BitSubtracterStr b₂,b₃) +* (BitSubtracterWithBorrowStr (b₂ . (b₁ + 1)),(b₃ . (b₁ + 1)),(b₁ -BitBorrowOutput b₂,b₃)) & (b₁ + 1) -BitSubtracterCirc b₂,b₃ = (b₁ -BitSubtracterCirc b₂,b₃) +* (BitSubtracterWithBorrowCirc (b₂ . (b₁ + 1)),(b₃ . (b₁ + 1)),(b₁ -BitBorrowOutput b₂,b₃)) & (b₁ + 1) -BitBorrowOutput b₂,b₃ = BorrowOutput (b₂ . (b₁ + 1)),(b₃ . (b₁ + 1)),(b₁ -BitBorrowOutput b₂,b₃) )

proof end;

theorem Th8: :: FSCIRC_2:8

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

proof end;

theorem Th9: :: FSCIRC_2:9

for b₁ being Nat
for b₂, b₃ being FinSequence holds InnerVertices ((b₁ + 1) -BitSubtracterStr b₂,b₃) = (InnerVertices (b₁ -BitSubtracterStr b₂,b₃)) \/ (InnerVertices (BitSubtracterWithBorrowStr (b₂ . (b₁ + 1)),(b₃ . (b₁ + 1)),(b₁ -BitBorrowOutput b₂,b₃)))

proof end;

definition

let c₁, c₂ be Nat;
assume E10: ( c₁ >= 1 & c₁ <= c₂ ) ;
let c₃, c₄ be FinSequence;
func c₁,c₂ -BitSubtracterOutput c₃,c₄ -> Element of InnerVertices (a₂ -BitSubtracterStr a₃,a₄) means :Def4: :: FSCIRC_2:def 4
ex b₁ being Nat st
( a₁ = b₁ + 1 & a₅ = BitSubtracterOutput (a₃ . a₁),(a₄ . a₁),(b₁ -BitBorrowOutput a₃,a₄) );
uniqueness ;
existence

proof end;

end;

:: deftheorem Def4 defines -BitSubtracterOutput FSCIRC_2:def 4 :

theorem Th10: :: FSCIRC_2:10

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

proof end;

theorem Th11: :: FSCIRC_2:11

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

proof end;

theorem Th12: :: FSCIRC_2:12

for b₁, b₂, b₃ being set holds InnerVertices (BorrowIStr b₁,b₂,b₃) = {[<*b₁,b₂*>,and2a ],[<*b₂,b₃*>,and2 ],[<*b₁,b₃*>,and2a ]}

proof end;

theorem Th13: :: FSCIRC_2:13

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

proof end;

theorem Th14: :: FSCIRC_2:14

for b₁, b₂, b₃ being set holds InnerVertices (BorrowStr b₁,b₂,b₃) = {[<*b₁,b₂*>,and2a ],[<*b₂,b₃*>,and2 ],[<*b₁,b₃*>,and2a ]} \/ {(BorrowOutput b₁,b₂,b₃)}

proof end;

theorem Th15: :: FSCIRC_2:15

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

proof end;

theorem Th16: :: FSCIRC_2:16

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

proof end;

theorem Th17: :: FSCIRC_2:17

for b₁, b₂, b₃ being set holds InnerVertices (BitSubtracterWithBorrowStr b₁,b₂,b₃) = ({[<*b₁,b₂*>,'xor' ],(2GatesCircOutput b₁,b₂,b₃,'xor' )} \/ {[<*b₁,b₂*>,and2a ],[<*b₂,b₃*>,and2 ],[<*b₁,b₃*>,and2a ]}) \/ {(BorrowOutput b₁,b₂,b₃)}

proof end;

registration

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

proof end;

end;

theorem Th18: :: FSCIRC_2:18

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

proof end;

theorem Th19: :: FSCIRC_2:19

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

proof end;

theorem Th20: :: FSCIRC_2:20

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

proof end;

theorem Th21: :: FSCIRC_2:21

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

proof end;

Lemma20: for b₁, b₂, b₃ being set
for b₄ being State of (BorrowCirc 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₂*>,and2a ] = ('not' b₅) '&' b₆ & (Following b₄) . [<*b₂,b₃*>,and2 ] = b₆ '&' b₇ & (Following b₄) . [<*b₁,b₃*>,and2a ] = ('not' b₅) '&' b₇ )

proof end;

theorem Th22: :: FSCIRC_2:22

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

proof end;

Lemma22: for b₁, b₂, b₃ being set st b₁ <> [<*b₂,b₃*>,and2 ] & b₂ <> [<*b₁,b₃*>,and2a ] & b₃ <> [<*b₁,b₂*>,and2a ] holds
for b₄ being State of (BorrowCirc 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) . (BorrowOutput b₁,b₂,b₃) = ((('not' b₅) '&' b₆) 'or' (b₆ '&' b₇)) 'or' (('not' b₅) '&' b₇) & (Following b₄,2) . [<*b₁,b₂*>,and2a ] = ('not' b₅) '&' b₆ & (Following b₄,2) . [<*b₂,b₃*>,and2 ] = b₆ '&' b₇ & (Following b₄,2) . [<*b₁,b₃*>,and2a ] = ('not' b₅) '&' b₇ )

proof end;

theorem Th23: :: FSCIRC_2:23

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

proof end;

theorem Th24: :: FSCIRC_2:24

for b₁, b₂, b₃ being set st b₁ <> [<*b₂,b₃*>,and2 ] & b₂ <> [<*b₁,b₃*>,and2a ] & b₃ <> [<*b₁,b₂*>,and2a ] & b₃ <> [<*b₁,b₂*>,'xor' ] holds
for b₄ being State of (BitSubtracterWithBorrowCirc 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) . (BitSubtracterOutput b₁,b₂,b₃) = (b₅ 'xor' b₆) 'xor' b₇ & (Following b₄,2) . (BorrowOutput b₁,b₂,b₃) = ((('not' b₅) '&' b₆) 'or' (b₆ '&' b₇)) 'or' (('not' b₅) '&' b₇) )

proof end;

theorem Th25: :: FSCIRC_2:25

proof end;

theorem Th26: :: FSCIRC_2:26

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

proof end;