:: FSCIRC_1 semantic presentation

definition

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

end;

:: deftheorem Def1 defines BitSubtracterOutput FSCIRC_1:def 1 :

definition

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

end;

:: deftheorem Def2 defines BitSubtracterCirc FSCIRC_1:def 2 :

definition

let c₁, c₂, c₃ be set ;
func BorrowIStr c₁,c₂,c₃ -> non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: FSCIRC_1:def 3
((1GateCircStr <*a₁,a₂*>,and2a ) +* (1GateCircStr <*a₂,a₃*>,and2 )) +* (1GateCircStr <*a₁,a₃*>,and2a );
correctness ;

end;

:: deftheorem Def3 defines BorrowIStr FSCIRC_1:def 3 :

definition

let c₁, c₂, c₃ be set ;
func BorrowStr c₁,c₂,c₃ -> non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: FSCIRC_1:def 4
(BorrowIStr a₁,a₂,a₃) +* (1GateCircStr <*[<*a₁,a₂*>,and2a ],[<*a₂,a₃*>,and2 ],[<*a₁,a₃*>,and2a ]*>,or3 );
correctness ;

end;

:: deftheorem Def4 defines BorrowStr FSCIRC_1:def 4 :

definition

let c₁, c₂, c₃ be set ;
func BorrowICirc c₁,c₂,c₃ -> strict gate`2=den Boolean Circuit of BorrowIStr a₁,a₂,a₃ equals :: FSCIRC_1:def 5
((1GateCircuit a₁,a₂,and2a ) +* (1GateCircuit a₂,a₃,and2 )) +* (1GateCircuit a₁,a₃,and2a );
coherence ;

end;

:: deftheorem Def5 defines BorrowICirc FSCIRC_1:def 5 :

theorem Th1: :: FSCIRC_1:1

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

proof end;

theorem Th2: :: FSCIRC_1:2

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

proof end;

theorem Th3: :: FSCIRC_1:3

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

proof end;

theorem Th4: :: FSCIRC_1:4

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

proof end;

theorem Th5: :: FSCIRC_1:5

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

proof end;

definition

let c₁, c₂, c₃ be set ;
func BorrowOutput c₁,c₂,c₃ -> Element of InnerVertices (BorrowStr a₁,a₂,a₃) equals :: FSCIRC_1:def 6
[<*[<*a₁,a₂*>,and2a ],[<*a₂,a₃*>,and2 ],[<*a₁,a₃*>,and2a ]*>,or3 ];
coherence

proof end;

correctness ;

end;

:: deftheorem Def6 defines BorrowOutput FSCIRC_1:def 6 :

definition

let c₁, c₂, c₃ be set ;
func BorrowCirc c₁,c₂,c₃ -> strict gate`2=den Boolean Circuit of BorrowStr a₁,a₂,a₃ equals :: FSCIRC_1:def 7
(BorrowICirc a₁,a₂,a₃) +* (1GateCircuit [<*a₁,a₂*>,and2a ],[<*a₂,a₃*>,and2 ],[<*a₁,a₃*>,and2a ],or3 );
coherence ;

end;

:: deftheorem Def7 defines BorrowCirc FSCIRC_1:def 7 :

theorem Th6: :: FSCIRC_1:6

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

proof end;

theorem Th7: :: FSCIRC_1:7

for b₁, b₂, b₃ being set holds
( [<*b₁,b₂*>,and2a ] in InnerVertices (BorrowStr b₁,b₂,b₃) & [<*b₂,b₃*>,and2 ] in InnerVertices (BorrowStr b₁,b₂,b₃) & [<*b₁,b₃*>,and2a ] in InnerVertices (BorrowStr b₁,b₂,b₃) )

proof end;

theorem Th8: :: FSCIRC_1:8

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

proof end;

theorem Th9: :: FSCIRC_1:9

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

proof end;

Lemma7: for b₁, b₂, b₃ being non pair 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 Th10: :: FSCIRC_1:10

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

proof end;

theorem Th11: :: FSCIRC_1:11

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

proof end;

theorem Th12: :: FSCIRC_1:12

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

proof end;

theorem Th13: :: FSCIRC_1:13

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

Lemma9: for b₁, b₂, b₃ being non pair 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₄,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 Th14: :: FSCIRC_1:14

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

proof end;

theorem Th15: :: FSCIRC_1:15

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

proof end;

theorem Th16: :: FSCIRC_1:16

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

proof end;

theorem Th17: :: FSCIRC_1:17

for b₁, b₂, b₃ being non pair 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₄,2) . (BorrowOutput b₁,b₂,b₃) = ((('not' b₅) '&' b₆) 'or' (b₆ '&' b₇)) 'or' (('not' b₅) '&' b₇) by Lemma9;

theorem Th18: :: FSCIRC_1:18

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

proof end;

definition

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

end;

:: deftheorem Def8 defines BitSubtracterWithBorrowStr FSCIRC_1:def 8 :

theorem Th19: :: FSCIRC_1:19

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

proof end;

theorem Th20: :: FSCIRC_1:20

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

theorem Th21: :: FSCIRC_1:21

for b₁, b₂, b₃ being set
for b₄ being non empty ManySortedSign st b₄ = BitSubtracterWithBorrowStr 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 BitSubtracterWithBorrowCirc c₁,c₂,c₃ -> strict gate`2=den Boolean Circuit of BitSubtracterWithBorrowStr a₁,a₂,a₃ equals :: FSCIRC_1:def 9
(BitSubtracterCirc a₁,a₂,a₃) +* (BorrowCirc a₁,a₂,a₃);
coherence ;

end;

:: deftheorem Def9 defines BitSubtracterWithBorrowCirc FSCIRC_1:def 9 :

theorem Th22: :: FSCIRC_1:22

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

proof end;

theorem Th23: :: FSCIRC_1:23

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

proof end;

theorem Th24: :: FSCIRC_1:24

for b₁, b₂, b₃ being set holds
( BitSubtracterOutput b₁,b₂,b₃ in InnerVertices (BitSubtracterWithBorrowStr b₁,b₂,b₃) & BorrowOutput b₁,b₂,b₃ in InnerVertices (BitSubtracterWithBorrowStr b₁,b₂,b₃) ) by FACIRC_1:21;

theorem Th25: :: FSCIRC_1:25

for b₁, b₂, b₃ being non pair set
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 Th26: :: FSCIRC_1:26

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

proof end;