:: FSCIRC_1 semantic presentation begin definition let x, y, c be set ; func BitSubtracterOutput (x,y,c) -> Element of InnerVertices (2GatesCircStr (x,y,c,'xor')) equals :: FSCIRC_1:def 1 2GatesCircOutput (x,y,c,'xor'); coherence 2GatesCircOutput (x,y,c,'xor') is Element of InnerVertices (2GatesCircStr (x,y,c,'xor')) ; end; :: deftheorem defines BitSubtracterOutput FSCIRC_1:def_1_:_ for x, y, c being set holds BitSubtracterOutput (x,y,c) = 2GatesCircOutput (x,y,c,'xor'); definition let x, y, c be set ; func BitSubtracterCirc (x,y,c) -> strict gate`2=den Boolean Circuit of 2GatesCircStr (x,y,c,'xor') equals :: FSCIRC_1:def 2 2GatesCircuit (x,y,c,'xor'); coherence 2GatesCircuit (x,y,c,'xor') is strict gate`2=den Boolean Circuit of 2GatesCircStr (x,y,c,'xor') ; end; :: deftheorem defines BitSubtracterCirc FSCIRC_1:def_2_:_ for x, y, c being set holds BitSubtracterCirc (x,y,c) = 2GatesCircuit (x,y,c,'xor'); definition let x, y, c be set ; func BorrowIStr (x,y,c) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: FSCIRC_1:def 3 ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)); correctness coherence ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ; ; end; :: deftheorem defines BorrowIStr FSCIRC_1:def_3_:_ for x, y, c being set holds BorrowIStr (x,y,c) = ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) +* (1GateCircStr (<*x,c*>,and2a)); definition let x, y, c be set ; func BorrowStr (x,y,c) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: FSCIRC_1:def 4 (BorrowIStr (x,y,c)) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)); correctness coherence (BorrowIStr (x,y,c)) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ; ; end; :: deftheorem defines BorrowStr FSCIRC_1:def_4_:_ for x, y, c being set holds BorrowStr (x,y,c) = (BorrowIStr (x,y,c)) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)); definition let x, y, c be set ; func BorrowICirc (x,y,c) -> strict gate`2=den Boolean Circuit of BorrowIStr (x,y,c) equals :: FSCIRC_1:def 5 ((1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2))) +* (1GateCircuit (x,c,and2a)); coherence ((1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2))) +* (1GateCircuit (x,c,and2a)) is strict gate`2=den Boolean Circuit of BorrowIStr (x,y,c) ; end; :: deftheorem defines BorrowICirc FSCIRC_1:def_5_:_ for x, y, c being set holds BorrowICirc (x,y,c) = ((1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2))) +* (1GateCircuit (x,c,and2a)); theorem Th1: :: FSCIRC_1:1 for x, y, c being set holds InnerVertices (BorrowStr (x,y,c)) is Relation proof let x, y, c be set ; ::_thesis: InnerVertices (BorrowStr (x,y,c)) is Relation ( InnerVertices (1GateCircStr (<*x,y*>,and2a)) is Relation & InnerVertices (1GateCircStr (<*y,c*>,and2)) is Relation ) by FACIRC_1:38; then ( InnerVertices (1GateCircStr (<*x,c*>,and2a)) is Relation & InnerVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) is Relation ) by FACIRC_1:3, FACIRC_1:38; then ( InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is Relation & InnerVertices (BorrowIStr (x,y,c)) is Relation ) by FACIRC_1:3, FACIRC_1:38; hence InnerVertices (BorrowStr (x,y,c)) is Relation by FACIRC_1:3; ::_thesis: verum end; theorem Th2: :: FSCIRC_1:2 for x, y, c being non pair set holds InputVertices (BorrowStr (x,y,c)) is without_pairs proof let x, y, c be non pair set ; ::_thesis: InputVertices (BorrowStr (x,y,c)) is without_pairs set M = BorrowStr (x,y,c); set MI = BorrowIStr (x,y,c); set S = 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3); given xx being pair set such that A1: xx in InputVertices (BorrowStr (x,y,c)) ; :: according to FACIRC_1:def_2 ::_thesis: contradiction A2: 1GateCircStr (<*x,y*>,and2a) tolerates 1GateCircStr (<*y,c*>,and2) by CIRCCOMB:47; A3: ( InnerVertices (1GateCircStr (<*x,c*>,and2a)) = {[<*x,c*>,and2a]} & (1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) tolerates 1GateCircStr (<*x,c*>,and2a) ) by CIRCCOMB:42, CIRCCOMB:47; ( InnerVertices (1GateCircStr (<*x,y*>,and2a)) = {[<*x,y*>,and2a]} & InnerVertices (1GateCircStr (<*y,c*>,and2)) = {[<*y,c*>,and2]} ) by CIRCCOMB:42; then InnerVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) = {[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]} by A2, CIRCCOMB:11; then A4: InnerVertices (BorrowIStr (x,y,c)) = ({[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]}) \/ {[<*x,c*>,and2a]} by A3, CIRCCOMB:11 .= {[<*x,y*>,and2a],[<*y,c*>,and2]} \/ {[<*x,c*>,and2a]} by ENUMSET1:1 .= {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} by ENUMSET1:3 ; InputVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) = {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} by FACIRC_1:42; then A5: (InputVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) \ (InnerVertices (BorrowIStr (x,y,c))) = {} by A4, XBOOLE_1:37; ( InputVertices (1GateCircStr (<*x,y*>,and2a)) is without_pairs & InputVertices (1GateCircStr (<*y,c*>,and2)) is without_pairs ) by FACIRC_1:41; then ( InputVertices (1GateCircStr (<*x,c*>,and2a)) is without_pairs & InputVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) is without_pairs ) by FACIRC_1:9, FACIRC_1:41; then A6: InputVertices (BorrowIStr (x,y,c)) is without_pairs by FACIRC_1:9; InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is Relation by FACIRC_1:38; then InputVertices (BorrowStr (x,y,c)) = (InputVertices (BorrowIStr (x,y,c))) \/ ((InputVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) \ (InnerVertices (BorrowIStr (x,y,c)))) by A6, FACIRC_1:6; hence contradiction by A6, A1, A5, FACIRC_1:def_2; ::_thesis: verum end; theorem :: FSCIRC_1:3 for x, y, c being set for s being State of (BorrowICirc (x,y,c)) for a, b being Element of BOOLEAN st a = s . x & b = s . y holds (Following s) . [<*x,y*>,and2a] = ('not' a) '&' b proof let x, y, c be set ; ::_thesis: for s being State of (BorrowICirc (x,y,c)) for a, b being Element of BOOLEAN st a = s . x & b = s . y holds (Following s) . [<*x,y*>,and2a] = ('not' a) '&' b set xy = <*x,y*>; set yc = <*y,c*>; set xc = <*x,c*>; set S1 = 1GateCircStr (<*x,y*>,and2a); set A1 = 1GateCircuit (x,y,and2a); set S2 = 1GateCircStr (<*y,c*>,and2); set A2 = 1GateCircuit (y,c,and2); set S3 = 1GateCircStr (<*x,c*>,and2a); set A3 = 1GateCircuit (x,c,and2a); set S = BorrowIStr (x,y,c); set A = BorrowICirc (x,y,c); set v1 = [<*x,y*>,and2a]; let s be State of (BorrowICirc (x,y,c)); ::_thesis: for a, b being Element of BOOLEAN st a = s . x & b = s . y holds (Following s) . [<*x,y*>,and2a] = ('not' a) '&' b let a, b be Element of BOOLEAN ; ::_thesis: ( a = s . x & b = s . y implies (Following s) . [<*x,y*>,and2a] = ('not' a) '&' b ) assume A1: ( a = s . x & b = s . y ) ; ::_thesis: (Following s) . [<*x,y*>,and2a] = ('not' a) '&' b reconsider xx = x, yy = y as Vertex of (1GateCircStr (<*x,y*>,and2a)) by FACIRC_1:43; reconsider v1 = [<*x,y*>,and2a] as Element of InnerVertices (1GateCircStr (<*x,y*>,and2a)) by FACIRC_1:47; A2: BorrowIStr (x,y,c) = (1GateCircStr (<*x,y*>,and2a)) +* ((1GateCircStr (<*y,c*>,and2)) +* (1GateCircStr (<*x,c*>,and2a))) by CIRCCOMB:6; then reconsider v = v1 as Element of InnerVertices (BorrowIStr (x,y,c)) by FACIRC_1:21; A3: BorrowICirc (x,y,c) = (1GateCircuit (x,y,and2a)) +* ((1GateCircuit (y,c,and2)) +* (1GateCircuit (x,c,and2a))) by FACIRC_1:25; then reconsider s1 = s | the carrier of (1GateCircStr (<*x,y*>,and2a)) as State of (1GateCircuit (x,y,and2a)) by FACIRC_1:26; reconsider xx = xx, yy = yy as Vertex of (BorrowIStr (x,y,c)) by A2, FACIRC_1:20; A4: dom s1 = the carrier of (1GateCircStr (<*x,y*>,and2a)) by CIRCUIT1:3; thus (Following s) . [<*x,y*>,and2a] = (Following s1) . v by A2, A3, CIRCCOMB:64 .= and2a . <*(s1 . xx),(s1 . yy)*> by FACIRC_1:50 .= and2a . <*(s . xx),(s1 . yy)*> by A4, FUNCT_1:47 .= and2a . <*(s . xx),(s . yy)*> by A4, FUNCT_1:47 .= ('not' a) '&' b by A1, TWOSCOMP:def_2 ; ::_thesis: verum end; theorem :: FSCIRC_1:4 for x, y, c being set for s being State of (BorrowICirc (x,y,c)) for a, b being Element of BOOLEAN st a = s . y & b = s . c holds (Following s) . [<*y,c*>,and2] = a '&' b proof let x, y, c be set ; ::_thesis: for s being State of (BorrowICirc (x,y,c)) for a, b being Element of BOOLEAN st a = s . y & b = s . c holds (Following s) . [<*y,c*>,and2] = a '&' b set xy = <*x,y*>; set yc = <*y,c*>; set xc = <*x,c*>; set S1 = 1GateCircStr (<*x,y*>,and2a); set A1 = 1GateCircuit (x,y,and2a); set S2 = 1GateCircStr (<*y,c*>,and2); set A2 = 1GateCircuit (y,c,and2); set S3 = 1GateCircStr (<*x,c*>,and2a); set A3 = 1GateCircuit (x,c,and2a); set S = BorrowIStr (x,y,c); set A = BorrowICirc (x,y,c); set v2 = [<*y,c*>,and2]; let s be State of (BorrowICirc (x,y,c)); ::_thesis: for a, b being Element of BOOLEAN st a = s . y & b = s . c holds (Following s) . [<*y,c*>,and2] = a '&' b let a, b be Element of BOOLEAN ; ::_thesis: ( a = s . y & b = s . c implies (Following s) . [<*y,c*>,and2] = a '&' b ) assume A1: ( a = s . y & b = s . c ) ; ::_thesis: (Following s) . [<*y,c*>,and2] = a '&' b reconsider yy = y, cc = c as Vertex of (1GateCircStr (<*y,c*>,and2)) by FACIRC_1:43; reconsider v2 = [<*y,c*>,and2] as Element of InnerVertices (1GateCircStr (<*y,c*>,and2)) by FACIRC_1:47; A2: (1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) = (1GateCircStr (<*y,c*>,and2)) +* (1GateCircStr (<*x,y*>,and2a)) by FACIRC_1:23; then A3: BorrowIStr (x,y,c) = (1GateCircStr (<*y,c*>,and2)) +* ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*x,c*>,and2a))) by CIRCCOMB:6; then reconsider v = v2 as Element of InnerVertices (BorrowIStr (x,y,c)) by FACIRC_1:21; (1GateCircuit (x,y,and2a)) +* (1GateCircuit (y,c,and2)) = (1GateCircuit (y,c,and2)) +* (1GateCircuit (x,y,and2a)) by FACIRC_1:24; then A4: BorrowICirc (x,y,c) = (1GateCircuit (y,c,and2)) +* ((1GateCircuit (x,y,and2a)) +* (1GateCircuit (x,c,and2a))) by A2, FACIRC_1:25; then reconsider s2 = s | the carrier of (1GateCircStr (<*y,c*>,and2)) as State of (1GateCircuit (y,c,and2)) by FACIRC_1:26; reconsider yy = yy, cc = cc as Vertex of (BorrowIStr (x,y,c)) by A3, FACIRC_1:20; A5: dom s2 = the carrier of (1GateCircStr (<*y,c*>,and2)) by CIRCUIT1:3; thus (Following s) . [<*y,c*>,and2] = (Following s2) . v by A3, A4, CIRCCOMB:64 .= and2 . <*(s2 . yy),(s2 . cc)*> by FACIRC_1:50 .= and2 . <*(s . yy),(s2 . cc)*> by A5, FUNCT_1:47 .= and2 . <*(s . yy),(s . cc)*> by A5, FUNCT_1:47 .= a '&' b by A1, TWOSCOMP:def_1 ; ::_thesis: verum end; theorem :: FSCIRC_1:5 for x, y, c being set for s being State of (BorrowICirc (x,y,c)) for a, b being Element of BOOLEAN st a = s . x & b = s . c holds (Following s) . [<*x,c*>,and2a] = ('not' a) '&' b proof let x, y, c be set ; ::_thesis: for s being State of (BorrowICirc (x,y,c)) for a, b being Element of BOOLEAN st a = s . x & b = s . c holds (Following s) . [<*x,c*>,and2a] = ('not' a) '&' b set xc = <*x,c*>; set S3 = 1GateCircStr (<*x,c*>,and2a); set A3 = 1GateCircuit (x,c,and2a); set S = BorrowIStr (x,y,c); set A = BorrowICirc (x,y,c); set v3 = [<*x,c*>,and2a]; let s be State of (BorrowICirc (x,y,c)); ::_thesis: for a, b being Element of BOOLEAN st a = s . x & b = s . c holds (Following s) . [<*x,c*>,and2a] = ('not' a) '&' b let a, b be Element of BOOLEAN ; ::_thesis: ( a = s . x & b = s . c implies (Following s) . [<*x,c*>,and2a] = ('not' a) '&' b ) assume A1: ( a = s . x & b = s . c ) ; ::_thesis: (Following s) . [<*x,c*>,and2a] = ('not' a) '&' b reconsider xx = x, cc = c as Vertex of (1GateCircStr (<*x,c*>,and2a)) by FACIRC_1:43; reconsider s3 = s | the carrier of (1GateCircStr (<*x,c*>,and2a)) as State of (1GateCircuit (x,c,and2a)) by FACIRC_1:26; reconsider v3 = [<*x,c*>,and2a] as Element of InnerVertices (1GateCircStr (<*x,c*>,and2a)) by FACIRC_1:47; reconsider v = v3 as Element of InnerVertices (BorrowIStr (x,y,c)) by FACIRC_1:21; A2: dom s3 = the carrier of (1GateCircStr (<*x,c*>,and2a)) by CIRCUIT1:3; reconsider xx = xx, cc = cc as Vertex of (BorrowIStr (x,y,c)) by FACIRC_1:20; thus (Following s) . [<*x,c*>,and2a] = (Following s3) . v by CIRCCOMB:64 .= and2a . <*(s3 . xx),(s3 . cc)*> by FACIRC_1:50 .= and2a . <*(s . xx),(s3 . cc)*> by A2, FUNCT_1:47 .= and2a . <*(s . xx),(s . cc)*> by A2, FUNCT_1:47 .= ('not' a) '&' b by A1, TWOSCOMP:def_2 ; ::_thesis: verum end; definition let x, y, c be set ; func BorrowOutput (x,y,c) -> Element of InnerVertices (BorrowStr (x,y,c)) equals :: FSCIRC_1:def 6 [<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3]; coherence [<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3] is Element of InnerVertices (BorrowStr (x,y,c)) proof [<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3] in InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) by FACIRC_1:47; hence [<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3] is Element of InnerVertices (BorrowStr (x,y,c)) by FACIRC_1:21; ::_thesis: verum end; correctness ; end; :: deftheorem defines BorrowOutput FSCIRC_1:def_6_:_ for x, y, c being set holds BorrowOutput (x,y,c) = [<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3]; definition let x, y, c be set ; func BorrowCirc (x,y,c) -> strict gate`2=den Boolean Circuit of BorrowStr (x,y,c) equals :: FSCIRC_1:def 7 (BorrowICirc (x,y,c)) +* (1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3)); coherence (BorrowICirc (x,y,c)) +* (1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3)) is strict gate`2=den Boolean Circuit of BorrowStr (x,y,c) ; end; :: deftheorem defines BorrowCirc FSCIRC_1:def_7_:_ for x, y, c being set holds BorrowCirc (x,y,c) = (BorrowICirc (x,y,c)) +* (1GateCircuit ([<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a],or3)); theorem Th6: :: FSCIRC_1:6 for x, y, c being set holds ( x in the carrier of (BorrowStr (x,y,c)) & y in the carrier of (BorrowStr (x,y,c)) & c in the carrier of (BorrowStr (x,y,c)) ) proof let x, y, c be set ; ::_thesis: ( x in the carrier of (BorrowStr (x,y,c)) & y in the carrier of (BorrowStr (x,y,c)) & c in the carrier of (BorrowStr (x,y,c)) ) c in the carrier of (1GateCircStr (<*x,c*>,and2a)) by FACIRC_1:43; then A1: c in the carrier of (BorrowIStr (x,y,c)) by FACIRC_1:20; y in the carrier of (1GateCircStr (<*x,y*>,and2a)) by FACIRC_1:43; then y in the carrier of ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) by FACIRC_1:20; then A2: y in the carrier of (BorrowIStr (x,y,c)) by FACIRC_1:20; x in the carrier of (1GateCircStr (<*x,c*>,and2a)) by FACIRC_1:43; then x in the carrier of (BorrowIStr (x,y,c)) by FACIRC_1:20; hence ( x in the carrier of (BorrowStr (x,y,c)) & y in the carrier of (BorrowStr (x,y,c)) & c in the carrier of (BorrowStr (x,y,c)) ) by A2, A1, FACIRC_1:20; ::_thesis: verum end; theorem Th7: :: FSCIRC_1:7 for x, y, c being set holds ( [<*x,y*>,and2a] in InnerVertices (BorrowStr (x,y,c)) & [<*y,c*>,and2] in InnerVertices (BorrowStr (x,y,c)) & [<*x,c*>,and2a] in InnerVertices (BorrowStr (x,y,c)) ) proof let x, y, c be set ; ::_thesis: ( [<*x,y*>,and2a] in InnerVertices (BorrowStr (x,y,c)) & [<*y,c*>,and2] in InnerVertices (BorrowStr (x,y,c)) & [<*x,c*>,and2a] in InnerVertices (BorrowStr (x,y,c)) ) [<*x,y*>,and2a] in InnerVertices (1GateCircStr (<*x,y*>,and2a)) by FACIRC_1:47; then [<*x,y*>,and2a] in InnerVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) by FACIRC_1:21; then A1: [<*x,y*>,and2a] in InnerVertices (BorrowIStr (x,y,c)) by FACIRC_1:21; [<*y,c*>,and2] in InnerVertices (1GateCircStr (<*y,c*>,and2)) by FACIRC_1:47; then [<*y,c*>,and2] in InnerVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) by FACIRC_1:21; then A2: [<*y,c*>,and2] in InnerVertices (BorrowIStr (x,y,c)) by FACIRC_1:21; [<*x,c*>,and2a] in InnerVertices (1GateCircStr (<*x,c*>,and2a)) by FACIRC_1:47; then [<*x,c*>,and2a] in InnerVertices (BorrowIStr (x,y,c)) by FACIRC_1:21; hence ( [<*x,y*>,and2a] in InnerVertices (BorrowStr (x,y,c)) & [<*y,c*>,and2] in InnerVertices (BorrowStr (x,y,c)) & [<*x,c*>,and2a] in InnerVertices (BorrowStr (x,y,c)) ) by A1, A2, FACIRC_1:21; ::_thesis: verum end; theorem Th8: :: FSCIRC_1:8 for x, y, c being non pair set holds ( x in InputVertices (BorrowStr (x,y,c)) & y in InputVertices (BorrowStr (x,y,c)) & c in InputVertices (BorrowStr (x,y,c)) ) proof let x, y, c be non pair set ; ::_thesis: ( x in InputVertices (BorrowStr (x,y,c)) & y in InputVertices (BorrowStr (x,y,c)) & c in InputVertices (BorrowStr (x,y,c)) ) assume A1: ( not x in InputVertices (BorrowStr (x,y,c)) or not y in InputVertices (BorrowStr (x,y,c)) or not c in InputVertices (BorrowStr (x,y,c)) ) ; ::_thesis: contradiction A2: c in the carrier of (BorrowStr (x,y,c)) by Th6; A3: InnerVertices (BorrowStr (x,y,c)) is Relation by Th1; ( x in the carrier of (BorrowStr (x,y,c)) & y in the carrier of (BorrowStr (x,y,c)) ) by Th6; then ( x in InnerVertices (BorrowStr (x,y,c)) or y in InnerVertices (BorrowStr (x,y,c)) or c in InnerVertices (BorrowStr (x,y,c)) ) by A2, A1, XBOOLE_0:def_5; then ( ex a1, b1 being set st x = [a1,b1] or ex a1, b1 being set st y = [a1,b1] or ex a1, b1 being set st c = [a1,b1] ) by A3, RELAT_1:def_1; hence contradiction ; ::_thesis: verum end; theorem Th9: :: FSCIRC_1:9 for x, y, c being non pair set holds ( InputVertices (BorrowStr (x,y,c)) = {x,y,c} & InnerVertices (BorrowStr (x,y,c)) = {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} \/ {(BorrowOutput (x,y,c))} ) proof let x, y, c be non pair set ; ::_thesis: ( InputVertices (BorrowStr (x,y,c)) = {x,y,c} & InnerVertices (BorrowStr (x,y,c)) = {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} \/ {(BorrowOutput (x,y,c))} ) set xy = <*x,y*>; set yc = <*y,c*>; set xc = <*x,c*>; set xy1 = [<*x,y*>,and2a]; set yc1 = [<*y,c*>,and2]; set xc1 = [<*x,c*>,and2a]; set MI = BorrowIStr (x,y,c); set S = 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3); set M = BorrowStr (x,y,c); A1: ( InputVertices (1GateCircStr (<*x,y*>,and2a)) = {x,y} & InputVertices (1GateCircStr (<*x,c*>,and2a)) = {x,c} ) by FACIRC_1:40; A2: InputVertices (1GateCircStr (<*y,c*>,and2)) = {y,c} by FACIRC_1:40; A3: ( InnerVertices (1GateCircStr (<*x,y*>,and2a)) = {[<*x,y*>,and2a]} & InnerVertices (1GateCircStr (<*y,c*>,and2)) = {[<*y,c*>,and2]} ) by CIRCCOMB:42; A4: InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is Relation by FACIRC_1:38; A5: ( InputVertices (1GateCircStr (<*x,y*>,and2a)) is without_pairs & InputVertices (1GateCircStr (<*y,c*>,and2)) is without_pairs ) by FACIRC_1:41; then A6: ( InputVertices (1GateCircStr (<*x,c*>,and2a)) is without_pairs & InputVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) is without_pairs ) by FACIRC_1:9, FACIRC_1:41; then InputVertices (BorrowIStr (x,y,c)) is without_pairs by FACIRC_1:9; then A7: InputVertices (BorrowStr (x,y,c)) = (InputVertices (BorrowIStr (x,y,c))) \/ ((InputVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) \ (InnerVertices (BorrowIStr (x,y,c)))) by A4, FACIRC_1:6; A8: InnerVertices (1GateCircStr (<*x,c*>,and2a)) = {[<*x,c*>,and2a]} by CIRCCOMB:42; 1GateCircStr (<*x,y*>,and2a) tolerates 1GateCircStr (<*y,c*>,and2) by CIRCCOMB:47; then A9: InnerVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) = {[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]} by A3, CIRCCOMB:11; (1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) tolerates 1GateCircStr (<*x,c*>,and2a) by CIRCCOMB:47; then A10: InnerVertices (BorrowIStr (x,y,c)) = ({[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]}) \/ {[<*x,c*>,and2a]} by A8, A9, CIRCCOMB:11 .= {[<*x,y*>,and2a],[<*y,c*>,and2]} \/ {[<*x,c*>,and2a]} by ENUMSET1:1 .= {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} by ENUMSET1:3 ; InputVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) = {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} by FACIRC_1:42; then A11: (InputVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) \ (InnerVertices (BorrowIStr (x,y,c))) = {} by A10, XBOOLE_1:37; InnerVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) = {[<*x,y*>,and2a],[<*y,c*>,and2]} by A9, ENUMSET1:1; hence InputVertices (BorrowStr (x,y,c)) = (InputVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)))) \/ (InputVertices (1GateCircStr (<*x,c*>,and2a))) by A6, A7, A8, A11, FACIRC_1:7 .= ((InputVertices (1GateCircStr (<*x,y*>,and2a))) \/ (InputVertices (1GateCircStr (<*y,c*>,and2)))) \/ (InputVertices (1GateCircStr (<*x,c*>,and2a))) by A5, A3, FACIRC_1:7 .= {x,y,y,c} \/ {c,x} by A1, A2, ENUMSET1:5 .= {y,y,x,c} \/ {c,x} by ENUMSET1:67 .= {y,x,c} \/ {c,x} by ENUMSET1:31 .= {x,y,c} \/ {c,x} by ENUMSET1:58 .= {x,y,c} \/ ({c} \/ {x}) by ENUMSET1:1 .= ({x,y,c} \/ {c}) \/ {x} by XBOOLE_1:4 .= ({c,x,y} \/ {c}) \/ {x} by ENUMSET1:59 .= {c,c,x,y} \/ {x} by ENUMSET1:4 .= {c,x,y} \/ {x} by ENUMSET1:31 .= {x,y,c} \/ {x} by ENUMSET1:59 .= {x,x,y,c} by ENUMSET1:4 .= {x,y,c} by ENUMSET1:31 ; ::_thesis: InnerVertices (BorrowStr (x,y,c)) = {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} \/ {(BorrowOutput (x,y,c))} BorrowIStr (x,y,c) tolerates 1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3) by CIRCCOMB:47; hence InnerVertices (BorrowStr (x,y,c)) = (InnerVertices (BorrowIStr (x,y,c))) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3))) by CIRCCOMB:11 .= {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} \/ {(BorrowOutput (x,y,c))} by A10, CIRCCOMB:42 ; ::_thesis: verum end; Lm1: for x, y, c being non pair set for s being State of (BorrowCirc (x,y,c)) for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds ( (Following s) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following s) . [<*y,c*>,and2] = a2 '&' a3 & (Following s) . [<*x,c*>,and2a] = ('not' a1) '&' a3 ) proof let x, y, c be non pair set ; ::_thesis: for s being State of (BorrowCirc (x,y,c)) for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds ( (Following s) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following s) . [<*y,c*>,and2] = a2 '&' a3 & (Following s) . [<*x,c*>,and2a] = ('not' a1) '&' a3 ) let s be State of (BorrowCirc (x,y,c)); ::_thesis: for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds ( (Following s) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following s) . [<*y,c*>,and2] = a2 '&' a3 & (Following s) . [<*x,c*>,and2a] = ('not' a1) '&' a3 ) let a1, a2, a3 be Element of BOOLEAN ; ::_thesis: ( a1 = s . x & a2 = s . y & a3 = s . c implies ( (Following s) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following s) . [<*y,c*>,and2] = a2 '&' a3 & (Following s) . [<*x,c*>,and2a] = ('not' a1) '&' a3 ) ) assume that A1: a1 = s . x and A2: a2 = s . y and A3: a3 = s . c ; ::_thesis: ( (Following s) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following s) . [<*y,c*>,and2] = a2 '&' a3 & (Following s) . [<*x,c*>,and2a] = ('not' a1) '&' a3 ) set S = BorrowStr (x,y,c); A4: InnerVertices (BorrowStr (x,y,c)) = the carrier' of (BorrowStr (x,y,c)) by FACIRC_1:37; A5: y in the carrier of (BorrowStr (x,y,c)) by Th6; A6: x in the carrier of (BorrowStr (x,y,c)) by Th6; A7: dom s = the carrier of (BorrowStr (x,y,c)) by CIRCUIT1:3; [<*x,y*>,and2a] in InnerVertices (BorrowStr (x,y,c)) by Th7; hence (Following s) . [<*x,y*>,and2a] = and2a . (s * <*x,y*>) by A4, FACIRC_1:35 .= and2a . <*a1,a2*> by A1, A2, A7, A6, A5, FINSEQ_2:125 .= ('not' a1) '&' a2 by TWOSCOMP:def_2 ; ::_thesis: ( (Following s) . [<*y,c*>,and2] = a2 '&' a3 & (Following s) . [<*x,c*>,and2a] = ('not' a1) '&' a3 ) A8: c in the carrier of (BorrowStr (x,y,c)) by Th6; [<*y,c*>,and2] in InnerVertices (BorrowStr (x,y,c)) by Th7; hence (Following s) . [<*y,c*>,and2] = and2 . (s * <*y,c*>) by A4, FACIRC_1:35 .= and2 . <*a2,a3*> by A2, A3, A7, A5, A8, FINSEQ_2:125 .= a2 '&' a3 by TWOSCOMP:def_1 ; ::_thesis: (Following s) . [<*x,c*>,and2a] = ('not' a1) '&' a3 [<*x,c*>,and2a] in InnerVertices (BorrowStr (x,y,c)) by Th7; hence (Following s) . [<*x,c*>,and2a] = and2a . (s * <*x,c*>) by A4, FACIRC_1:35 .= and2a . <*a1,a3*> by A1, A3, A7, A6, A8, FINSEQ_2:125 .= ('not' a1) '&' a3 by TWOSCOMP:def_2 ; ::_thesis: verum end; theorem :: FSCIRC_1:10 for x, y, c being non pair set for s being State of (BorrowCirc (x,y,c)) for a1, a2 being Element of BOOLEAN st a1 = s . x & a2 = s . y holds (Following s) . [<*x,y*>,and2a] = ('not' a1) '&' a2 proof let x, y, c be non pair set ; ::_thesis: for s being State of (BorrowCirc (x,y,c)) for a1, a2 being Element of BOOLEAN st a1 = s . x & a2 = s . y holds (Following s) . [<*x,y*>,and2a] = ('not' a1) '&' a2 reconsider a = c as Vertex of (BorrowStr (x,y,c)) by Th6; let s be State of (BorrowCirc (x,y,c)); ::_thesis: for a1, a2 being Element of BOOLEAN st a1 = s . x & a2 = s . y holds (Following s) . [<*x,y*>,and2a] = ('not' a1) '&' a2 s . a is Element of BOOLEAN ; hence for a1, a2 being Element of BOOLEAN st a1 = s . x & a2 = s . y holds (Following s) . [<*x,y*>,and2a] = ('not' a1) '&' a2 by Lm1; ::_thesis: verum end; theorem :: FSCIRC_1:11 for x, y, c being non pair set for s being State of (BorrowCirc (x,y,c)) for a2, a3 being Element of BOOLEAN st a2 = s . y & a3 = s . c holds (Following s) . [<*y,c*>,and2] = a2 '&' a3 proof let x, y, c be non pair set ; ::_thesis: for s being State of (BorrowCirc (x,y,c)) for a2, a3 being Element of BOOLEAN st a2 = s . y & a3 = s . c holds (Following s) . [<*y,c*>,and2] = a2 '&' a3 reconsider a = x as Vertex of (BorrowStr (x,y,c)) by Th6; let s be State of (BorrowCirc (x,y,c)); ::_thesis: for a2, a3 being Element of BOOLEAN st a2 = s . y & a3 = s . c holds (Following s) . [<*y,c*>,and2] = a2 '&' a3 s . a is Element of BOOLEAN ; hence for a2, a3 being Element of BOOLEAN st a2 = s . y & a3 = s . c holds (Following s) . [<*y,c*>,and2] = a2 '&' a3 by Lm1; ::_thesis: verum end; theorem :: FSCIRC_1:12 for x, y, c being non pair set for s being State of (BorrowCirc (x,y,c)) for a1, a3 being Element of BOOLEAN st a1 = s . x & a3 = s . c holds (Following s) . [<*x,c*>,and2a] = ('not' a1) '&' a3 proof let x, y, c be non pair set ; ::_thesis: for s being State of (BorrowCirc (x,y,c)) for a1, a3 being Element of BOOLEAN st a1 = s . x & a3 = s . c holds (Following s) . [<*x,c*>,and2a] = ('not' a1) '&' a3 reconsider a = y as Vertex of (BorrowStr (x,y,c)) by Th6; let s be State of (BorrowCirc (x,y,c)); ::_thesis: for a1, a3 being Element of BOOLEAN st a1 = s . x & a3 = s . c holds (Following s) . [<*x,c*>,and2a] = ('not' a1) '&' a3 s . a is Element of BOOLEAN ; hence for a1, a3 being Element of BOOLEAN st a1 = s . x & a3 = s . c holds (Following s) . [<*x,c*>,and2a] = ('not' a1) '&' a3 by Lm1; ::_thesis: verum end; theorem Th13: :: FSCIRC_1:13 for x, y, c being non pair set for s being State of (BorrowCirc (x,y,c)) for a1, a2, a3 being Element of BOOLEAN st a1 = s . [<*x,y*>,and2a] & a2 = s . [<*y,c*>,and2] & a3 = s . [<*x,c*>,and2a] holds (Following s) . (BorrowOutput (x,y,c)) = (a1 'or' a2) 'or' a3 proof let x, y, c be non pair set ; ::_thesis: for s being State of (BorrowCirc (x,y,c)) for a1, a2, a3 being Element of BOOLEAN st a1 = s . [<*x,y*>,and2a] & a2 = s . [<*y,c*>,and2] & a3 = s . [<*x,c*>,and2a] holds (Following s) . (BorrowOutput (x,y,c)) = (a1 'or' a2) 'or' a3 set xy = <*x,y*>; set yc = <*y,c*>; set xc = <*x,c*>; set xy1 = [<*x,y*>,and2a]; set yc1 = [<*y,c*>,and2]; set xc1 = [<*x,c*>,and2a]; set S = BorrowStr (x,y,c); reconsider xy1 = [<*x,y*>,and2a], yc1 = [<*y,c*>,and2], xc1 = [<*x,c*>,and2a] as Element of InnerVertices (BorrowStr (x,y,c)) by Th7; let s be State of (BorrowCirc (x,y,c)); ::_thesis: for a1, a2, a3 being Element of BOOLEAN st a1 = s . [<*x,y*>,and2a] & a2 = s . [<*y,c*>,and2] & a3 = s . [<*x,c*>,and2a] holds (Following s) . (BorrowOutput (x,y,c)) = (a1 'or' a2) 'or' a3 let a1, a2, a3 be Element of BOOLEAN ; ::_thesis: ( a1 = s . [<*x,y*>,and2a] & a2 = s . [<*y,c*>,and2] & a3 = s . [<*x,c*>,and2a] implies (Following s) . (BorrowOutput (x,y,c)) = (a1 'or' a2) 'or' a3 ) assume A1: ( a1 = s . [<*x,y*>,and2a] & a2 = s . [<*y,c*>,and2] & a3 = s . [<*x,c*>,and2a] ) ; ::_thesis: (Following s) . (BorrowOutput (x,y,c)) = (a1 'or' a2) 'or' a3 A2: dom s = the carrier of (BorrowStr (x,y,c)) by CIRCUIT1:3; InnerVertices (BorrowStr (x,y,c)) = the carrier' of (BorrowStr (x,y,c)) by FACIRC_1:37; hence (Following s) . (BorrowOutput (x,y,c)) = or3 . (s * <*xy1,yc1,xc1*>) by FACIRC_1:35 .= or3 . <*a1,a2,a3*> by A1, A2, FINSEQ_2:126 .= (a1 'or' a2) 'or' a3 by FACIRC_1:def_7 ; ::_thesis: verum end; Lm2: for x, y, c being non pair set for s being State of (BorrowCirc (x,y,c)) for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds ( (Following (s,2)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3) & (Following (s,2)) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following (s,2)) . [<*y,c*>,and2] = a2 '&' a3 & (Following (s,2)) . [<*x,c*>,and2a] = ('not' a1) '&' a3 ) proof let x, y, c be non pair set ; ::_thesis: for s being State of (BorrowCirc (x,y,c)) for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds ( (Following (s,2)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3) & (Following (s,2)) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following (s,2)) . [<*y,c*>,and2] = a2 '&' a3 & (Following (s,2)) . [<*x,c*>,and2a] = ('not' a1) '&' a3 ) set S = BorrowStr (x,y,c); reconsider x9 = x, y9 = y, c9 = c as Vertex of (BorrowStr (x,y,c)) by Th6; let s be State of (BorrowCirc (x,y,c)); ::_thesis: for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds ( (Following (s,2)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3) & (Following (s,2)) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following (s,2)) . [<*y,c*>,and2] = a2 '&' a3 & (Following (s,2)) . [<*x,c*>,and2a] = ('not' a1) '&' a3 ) set xy = <*x,y*>; set yc = <*y,c*>; set xc = <*x,c*>; set xy1 = [<*x,y*>,and2a]; set yc1 = [<*y,c*>,and2]; set xc1 = [<*x,c*>,and2a]; A1: Following (s,2) = Following (Following s) by FACIRC_1:15; let a1, a2, a3 be Element of BOOLEAN ; ::_thesis: ( a1 = s . x & a2 = s . y & a3 = s . c implies ( (Following (s,2)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3) & (Following (s,2)) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following (s,2)) . [<*y,c*>,and2] = a2 '&' a3 & (Following (s,2)) . [<*x,c*>,and2a] = ('not' a1) '&' a3 ) ) assume A2: ( a1 = s . x & a2 = s . y & a3 = s . c ) ; ::_thesis: ( (Following (s,2)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3) & (Following (s,2)) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following (s,2)) . [<*y,c*>,and2] = a2 '&' a3 & (Following (s,2)) . [<*x,c*>,and2a] = ('not' a1) '&' a3 ) A3: (Following s) . [<*x,c*>,and2a] = ('not' a1) '&' a3 by A2, Lm1; ( (Following s) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following s) . [<*y,c*>,and2] = a2 '&' a3 ) by A2, Lm1; hence (Following (s,2)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3) by A1, A3, Th13; ::_thesis: ( (Following (s,2)) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following (s,2)) . [<*y,c*>,and2] = a2 '&' a3 & (Following (s,2)) . [<*x,c*>,and2a] = ('not' a1) '&' a3 ) y in InputVertices (BorrowStr (x,y,c)) by Th8; then A4: (Following s) . y9 = s . y by CIRCUIT2:def_5; c in InputVertices (BorrowStr (x,y,c)) by Th8; then A5: (Following s) . c9 = s . c by CIRCUIT2:def_5; x in InputVertices (BorrowStr (x,y,c)) by Th8; then (Following s) . x9 = s . x by CIRCUIT2:def_5; hence ( (Following (s,2)) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following (s,2)) . [<*y,c*>,and2] = a2 '&' a3 & (Following (s,2)) . [<*x,c*>,and2a] = ('not' a1) '&' a3 ) by A2, A4, A5, A1, Lm1; ::_thesis: verum end; theorem :: FSCIRC_1:14 for x, y, c being non pair set for s being State of (BorrowCirc (x,y,c)) for a1, a2 being Element of BOOLEAN st a1 = s . x & a2 = s . y holds (Following (s,2)) . [<*x,y*>,and2a] = ('not' a1) '&' a2 proof let x, y, c be non pair set ; ::_thesis: for s being State of (BorrowCirc (x,y,c)) for a1, a2 being Element of BOOLEAN st a1 = s . x & a2 = s . y holds (Following (s,2)) . [<*x,y*>,and2a] = ('not' a1) '&' a2 reconsider a = c as Vertex of (BorrowStr (x,y,c)) by Th6; let s be State of (BorrowCirc (x,y,c)); ::_thesis: for a1, a2 being Element of BOOLEAN st a1 = s . x & a2 = s . y holds (Following (s,2)) . [<*x,y*>,and2a] = ('not' a1) '&' a2 s . a is Element of BOOLEAN ; hence for a1, a2 being Element of BOOLEAN st a1 = s . x & a2 = s . y holds (Following (s,2)) . [<*x,y*>,and2a] = ('not' a1) '&' a2 by Lm2; ::_thesis: verum end; theorem :: FSCIRC_1:15 for x, y, c being non pair set for s being State of (BorrowCirc (x,y,c)) for a2, a3 being Element of BOOLEAN st a2 = s . y & a3 = s . c holds (Following (s,2)) . [<*y,c*>,and2] = a2 '&' a3 proof let x, y, c be non pair set ; ::_thesis: for s being State of (BorrowCirc (x,y,c)) for a2, a3 being Element of BOOLEAN st a2 = s . y & a3 = s . c holds (Following (s,2)) . [<*y,c*>,and2] = a2 '&' a3 reconsider a = x as Vertex of (BorrowStr (x,y,c)) by Th6; let s be State of (BorrowCirc (x,y,c)); ::_thesis: for a2, a3 being Element of BOOLEAN st a2 = s . y & a3 = s . c holds (Following (s,2)) . [<*y,c*>,and2] = a2 '&' a3 s . a is Element of BOOLEAN ; hence for a2, a3 being Element of BOOLEAN st a2 = s . y & a3 = s . c holds (Following (s,2)) . [<*y,c*>,and2] = a2 '&' a3 by Lm2; ::_thesis: verum end; theorem :: FSCIRC_1:16 for x, y, c being non pair set for s being State of (BorrowCirc (x,y,c)) for a1, a3 being Element of BOOLEAN st a1 = s . x & a3 = s . c holds (Following (s,2)) . [<*x,c*>,and2a] = ('not' a1) '&' a3 proof let x, y, c be non pair set ; ::_thesis: for s being State of (BorrowCirc (x,y,c)) for a1, a3 being Element of BOOLEAN st a1 = s . x & a3 = s . c holds (Following (s,2)) . [<*x,c*>,and2a] = ('not' a1) '&' a3 reconsider a = y as Vertex of (BorrowStr (x,y,c)) by Th6; let s be State of (BorrowCirc (x,y,c)); ::_thesis: for a1, a3 being Element of BOOLEAN st a1 = s . x & a3 = s . c holds (Following (s,2)) . [<*x,c*>,and2a] = ('not' a1) '&' a3 s . a is Element of BOOLEAN ; hence for a1, a3 being Element of BOOLEAN st a1 = s . x & a3 = s . c holds (Following (s,2)) . [<*x,c*>,and2a] = ('not' a1) '&' a3 by Lm2; ::_thesis: verum end; theorem :: FSCIRC_1:17 for x, y, c being non pair set for s being State of (BorrowCirc (x,y,c)) for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds (Following (s,2)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3) by Lm2; theorem Th18: :: FSCIRC_1:18 for x, y, c being non pair set for s being State of (BorrowCirc (x,y,c)) holds Following (s,2) is stable proof let x, y, c be non pair set ; ::_thesis: for s being State of (BorrowCirc (x,y,c)) holds Following (s,2) is stable set S = BorrowStr (x,y,c); reconsider xx = x, yy = y, cc = c as Vertex of (BorrowStr (x,y,c)) by Th6; let s be State of (BorrowCirc (x,y,c)); ::_thesis: Following (s,2) is stable set a1 = s . xx; set a2 = s . yy; set a3 = s . cc; set ffs = Following (s,2); set fffs = Following (Following (s,2)); A1: Following (s,2) = Following (Following s) by FACIRC_1:15; A2: y in InputVertices (BorrowStr (x,y,c)) by Th8; then (Following s) . y = s . yy by CIRCUIT2:def_5; then A3: (Following (s,2)) . y = s . yy by A1, A2, CIRCUIT2:def_5; s . yy = s . y ; then A4: (Following (s,2)) . [<*x,c*>,and2a] = ('not' (s . xx)) '&' (s . cc) by Lm2; A5: x in InputVertices (BorrowStr (x,y,c)) by Th8; then (Following s) . x = s . xx by CIRCUIT2:def_5; then A6: (Following (s,2)) . x = s . xx by A1, A5, CIRCUIT2:def_5; s . xx = s . x ; then A7: (Following (s,2)) . [<*y,c*>,and2] = (s . yy) '&' (s . cc) by Lm2; A8: c in InputVertices (BorrowStr (x,y,c)) by Th8; then (Following s) . c = s . cc by CIRCUIT2:def_5; then A9: (Following (s,2)) . c = s . cc by A1, A8, CIRCUIT2:def_5; s . cc = s . c ; then A10: (Following (s,2)) . [<*x,y*>,and2a] = ('not' (s . xx)) '&' (s . yy) by Lm2; A11: (Following (s,2)) . (BorrowOutput (x,y,c)) = ((('not' (s . xx)) '&' (s . yy)) 'or' ((s . yy) '&' (s . cc))) 'or' (('not' (s . xx)) '&' (s . cc)) by Lm2; A12: now__::_thesis:_for_a_being_set_st_a_in_the_carrier_of_(BorrowStr_(x,y,c))_holds_ (Following_(s,2))_._a_=_(Following_(Following_(s,2)))_._a let a be set ; ::_thesis: ( a in the carrier of (BorrowStr (x,y,c)) implies (Following (s,2)) . a = (Following (Following (s,2))) . a ) assume A13: a in the carrier of (BorrowStr (x,y,c)) ; ::_thesis: (Following (s,2)) . a = (Following (Following (s,2))) . a then reconsider v = a as Vertex of (BorrowStr (x,y,c)) ; A14: v in (InputVertices (BorrowStr (x,y,c))) \/ (InnerVertices (BorrowStr (x,y,c))) by A13, XBOOLE_1:45; thus (Following (s,2)) . a = (Following (Following (s,2))) . a ::_thesis: verum proof percases ( v in InputVertices (BorrowStr (x,y,c)) or v in InnerVertices (BorrowStr (x,y,c)) ) by A14, XBOOLE_0:def_3; suppose v in InputVertices (BorrowStr (x,y,c)) ; ::_thesis: (Following (s,2)) . a = (Following (Following (s,2))) . a hence (Following (s,2)) . a = (Following (Following (s,2))) . a by CIRCUIT2:def_5; ::_thesis: verum end; suppose v in InnerVertices (BorrowStr (x,y,c)) ; ::_thesis: (Following (s,2)) . a = (Following (Following (s,2))) . a then v in {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} \/ {(BorrowOutput (x,y,c))} by Th9; then ( v in {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} or v in {(BorrowOutput (x,y,c))} ) by XBOOLE_0:def_3; then ( v = [<*x,y*>,and2a] or v = [<*y,c*>,and2] or v = [<*x,c*>,and2a] or v = BorrowOutput (x,y,c) ) by ENUMSET1:def_1, TARSKI:def_1; hence (Following (s,2)) . a = (Following (Following (s,2))) . a by A11, A10, A7, A4, A6, A3, A9, Lm1, Th13; ::_thesis: verum end; end; end; end; ( dom (Following (Following (s,2))) = the carrier of (BorrowStr (x,y,c)) & dom (Following (s,2)) = the carrier of (BorrowStr (x,y,c)) ) by CIRCUIT1:3; hence Following (s,2) = Following (Following (s,2)) by A12, FUNCT_1:2; :: according to CIRCUIT2:def_6 ::_thesis: verum end; begin definition let x, y, c be set ; func BitSubtracterWithBorrowStr (x,y,c) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: FSCIRC_1:def 8 (2GatesCircStr (x,y,c,'xor')) +* (BorrowStr (x,y,c)); coherence (2GatesCircStr (x,y,c,'xor')) +* (BorrowStr (x,y,c)) is non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ; end; :: deftheorem defines BitSubtracterWithBorrowStr FSCIRC_1:def_8_:_ for x, y, c being set holds BitSubtracterWithBorrowStr (x,y,c) = (2GatesCircStr (x,y,c,'xor')) +* (BorrowStr (x,y,c)); theorem Th19: :: FSCIRC_1:19 for x, y, c being non pair set holds InputVertices (BitSubtracterWithBorrowStr (x,y,c)) = {x,y,c} proof let x, y, c be non pair set ; ::_thesis: InputVertices (BitSubtracterWithBorrowStr (x,y,c)) = {x,y,c} set S = BitSubtracterWithBorrowStr (x,y,c); set S1 = 2GatesCircStr (x,y,c,'xor'); set S2 = BorrowStr (x,y,c); A1: ( InputVertices (2GatesCircStr (x,y,c,'xor')) = {x,y,c} & InputVertices (BorrowStr (x,y,c)) = {x,y,c} ) by Th9, FACIRC_1:57; ( InnerVertices (2GatesCircStr (x,y,c,'xor')) is Relation & InnerVertices (BorrowStr (x,y,c)) is Relation ) by Th1, FACIRC_1:58; hence InputVertices (BitSubtracterWithBorrowStr (x,y,c)) = {x,y,c} \/ {x,y,c} by A1, FACIRC_1:7 .= {x,y,c} ; ::_thesis: verum end; theorem :: FSCIRC_1:20 for x, y, c being non pair set holds InnerVertices (BitSubtracterWithBorrowStr (x,y,c)) = ({[<*x,y*>,'xor'],(2GatesCircOutput (x,y,c,'xor'))} \/ {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]}) \/ {(BorrowOutput (x,y,c))} proof let x, y, c be non pair set ; ::_thesis: InnerVertices (BitSubtracterWithBorrowStr (x,y,c)) = ({[<*x,y*>,'xor'],(2GatesCircOutput (x,y,c,'xor'))} \/ {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]}) \/ {(BorrowOutput (x,y,c))} set S1 = 2GatesCircStr (x,y,c,'xor'); set S2 = BorrowStr (x,y,c); A1: ( ({[<*x,y*>,'xor'],(2GatesCircOutput (x,y,c,'xor'))} \/ {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]}) \/ {(BorrowOutput (x,y,c))} = {[<*x,y*>,'xor'],(2GatesCircOutput (x,y,c,'xor'))} \/ ({[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} \/ {(BorrowOutput (x,y,c))}) & InnerVertices (2GatesCircStr (x,y,c,'xor')) = {[<*x,y*>,'xor'],(2GatesCircOutput (x,y,c,'xor'))} ) by FACIRC_1:56, XBOOLE_1:4; InnerVertices (BorrowStr (x,y,c)) = {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} \/ {(BorrowOutput (x,y,c))} by Th9; hence InnerVertices (BitSubtracterWithBorrowStr (x,y,c)) = ({[<*x,y*>,'xor'],(2GatesCircOutput (x,y,c,'xor'))} \/ {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]}) \/ {(BorrowOutput (x,y,c))} by A1, FACIRC_1:27; ::_thesis: verum end; theorem :: FSCIRC_1:21 for x, y, c being set for S being non empty ManySortedSign st S = BitSubtracterWithBorrowStr (x,y,c) holds ( x in the carrier of S & y in the carrier of S & c in the carrier of S ) proof let x, y, c be set ; ::_thesis: for S being non empty ManySortedSign st S = BitSubtracterWithBorrowStr (x,y,c) holds ( x in the carrier of S & y in the carrier of S & c in the carrier of S ) set S1 = 2GatesCircStr (x,y,c,'xor'); let S be non empty ManySortedSign ; ::_thesis: ( S = BitSubtracterWithBorrowStr (x,y,c) implies ( x in the carrier of S & y in the carrier of S & c in the carrier of S ) ) A1: ( x in the carrier of (2GatesCircStr (x,y,c,'xor')) & y in the carrier of (2GatesCircStr (x,y,c,'xor')) ) by FACIRC_1:60; A2: c in the carrier of (2GatesCircStr (x,y,c,'xor')) by FACIRC_1:60; assume S = BitSubtracterWithBorrowStr (x,y,c) ; ::_thesis: ( x in the carrier of S & y in the carrier of S & c in the carrier of S ) hence ( x in the carrier of S & y in the carrier of S & c in the carrier of S ) by A1, A2, FACIRC_1:20; ::_thesis: verum end; definition let x, y, c be set ; func BitSubtracterWithBorrowCirc (x,y,c) -> strict gate`2=den Boolean Circuit of BitSubtracterWithBorrowStr (x,y,c) equals :: FSCIRC_1:def 9 (BitSubtracterCirc (x,y,c)) +* (BorrowCirc (x,y,c)); coherence (BitSubtracterCirc (x,y,c)) +* (BorrowCirc (x,y,c)) is strict gate`2=den Boolean Circuit of BitSubtracterWithBorrowStr (x,y,c) ; end; :: deftheorem defines BitSubtracterWithBorrowCirc FSCIRC_1:def_9_:_ for x, y, c being set holds BitSubtracterWithBorrowCirc (x,y,c) = (BitSubtracterCirc (x,y,c)) +* (BorrowCirc (x,y,c)); theorem :: FSCIRC_1:22 for x, y, c being set holds InnerVertices (BitSubtracterWithBorrowStr (x,y,c)) is Relation proof let x, y, c be set ; ::_thesis: InnerVertices (BitSubtracterWithBorrowStr (x,y,c)) is Relation ( InnerVertices (2GatesCircStr (x,y,c,'xor')) is Relation & InnerVertices (BorrowStr (x,y,c)) is Relation ) by Th1, FACIRC_1:58; hence InnerVertices (BitSubtracterWithBorrowStr (x,y,c)) is Relation by FACIRC_1:3; ::_thesis: verum end; theorem :: FSCIRC_1:23 for x, y, c being non pair set holds InputVertices (BitSubtracterWithBorrowStr (x,y,c)) is without_pairs proof let x, y, c be non pair set ; ::_thesis: InputVertices (BitSubtracterWithBorrowStr (x,y,c)) is without_pairs InputVertices (BitSubtracterWithBorrowStr (x,y,c)) = {x,y,c} by Th19; hence InputVertices (BitSubtracterWithBorrowStr (x,y,c)) is without_pairs ; ::_thesis: verum end; theorem :: FSCIRC_1:24 for x, y, c being non pair set for s being State of (BitSubtracterWithBorrowCirc (x,y,c)) for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds ( (Following (s,2)) . (BitSubtracterOutput (x,y,c)) = (a1 'xor' a2) 'xor' a3 & (Following (s,2)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3) ) proof set f = 'xor' ; let x, y, c be non pair set ; ::_thesis: for s being State of (BitSubtracterWithBorrowCirc (x,y,c)) for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds ( (Following (s,2)) . (BitSubtracterOutput (x,y,c)) = (a1 'xor' a2) 'xor' a3 & (Following (s,2)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3) ) set S1 = 2GatesCircStr (x,y,c,'xor'); set S2 = BorrowStr (x,y,c); set A = BitSubtracterWithBorrowCirc (x,y,c); set A1 = BitSubtracterCirc (x,y,c); set A2 = BorrowCirc (x,y,c); let s be State of (BitSubtracterWithBorrowCirc (x,y,c)); ::_thesis: for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds ( (Following (s,2)) . (BitSubtracterOutput (x,y,c)) = (a1 'xor' a2) 'xor' a3 & (Following (s,2)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3) ) let a1, a2, a3 be Element of BOOLEAN ; ::_thesis: ( a1 = s . x & a2 = s . y & a3 = s . c implies ( (Following (s,2)) . (BitSubtracterOutput (x,y,c)) = (a1 'xor' a2) 'xor' a3 & (Following (s,2)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3) ) ) assume that A1: a1 = s . x and A2: a2 = s . y and A3: a3 = s . c ; ::_thesis: ( (Following (s,2)) . (BitSubtracterOutput (x,y,c)) = (a1 'xor' a2) 'xor' a3 & (Following (s,2)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3) ) reconsider s1 = s | the carrier of (2GatesCircStr (x,y,c,'xor')) as State of (BitSubtracterCirc (x,y,c)) by FACIRC_1:26; A4: dom s1 = the carrier of (2GatesCircStr (x,y,c,'xor')) by CIRCUIT1:3; c in the carrier of (2GatesCircStr (x,y,c,'xor')) by FACIRC_1:60; then A5: a3 = s1 . c by A3, A4, FUNCT_1:47; y in the carrier of (2GatesCircStr (x,y,c,'xor')) by FACIRC_1:60; then A6: a2 = s1 . y by A2, A4, FUNCT_1:47; reconsider t = s as State of ((BitSubtracterCirc (x,y,c)) +* (BorrowCirc (x,y,c))) ; InputVertices (2GatesCircStr (x,y,c,'xor')) is without_pairs by FACIRC_1:59; then InnerVertices (BorrowStr (x,y,c)) misses InputVertices (2GatesCircStr (x,y,c,'xor')) by Th1, FACIRC_1:5; then A7: (Following (t,2)) . (2GatesCircOutput (x,y,c,'xor')) = (Following (s1,2)) . (2GatesCircOutput (x,y,c,'xor')) by FACIRC_1:32; reconsider s2 = s | the carrier of (BorrowStr (x,y,c)) as State of (BorrowCirc (x,y,c)) by FACIRC_1:26; A8: dom s2 = the carrier of (BorrowStr (x,y,c)) by CIRCUIT1:3; x in the carrier of (2GatesCircStr (x,y,c,'xor')) by FACIRC_1:60; then a1 = s1 . x by A1, A4, FUNCT_1:47; hence (Following (s,2)) . (BitSubtracterOutput (x,y,c)) = (a1 'xor' a2) 'xor' a3 by A6, A5, A7, FACIRC_1:64; ::_thesis: (Following (s,2)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3) InputVertices (BorrowStr (x,y,c)) is without_pairs by Th2; then InnerVertices (2GatesCircStr (x,y,c,'xor')) misses InputVertices (BorrowStr (x,y,c)) by FACIRC_1:5, FACIRC_1:58; then A9: (Following (t,2)) . (BorrowOutput (x,y,c)) = (Following (s2,2)) . (BorrowOutput (x,y,c)) by FACIRC_1:33; c in the carrier of (BorrowStr (x,y,c)) by Th6; then A10: a3 = s2 . c by A3, A8, FUNCT_1:47; y in the carrier of (BorrowStr (x,y,c)) by Th6; then A11: a2 = s2 . y by A2, A8, FUNCT_1:47; x in the carrier of (BorrowStr (x,y,c)) by Th6; then a1 = s2 . x by A1, A8, FUNCT_1:47; hence (Following (s,2)) . (BorrowOutput (x,y,c)) = ((('not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (('not' a1) '&' a3) by A11, A10, A9, Lm2; ::_thesis: verum end; theorem :: FSCIRC_1:25 for x, y, c being non pair set for s being State of (BitSubtracterWithBorrowCirc (x,y,c)) holds Following (s,2) is stable proof let x, y, c be non pair set ; ::_thesis: for s being State of (BitSubtracterWithBorrowCirc (x,y,c)) holds Following (s,2) is stable set S = BitSubtracterWithBorrowStr (x,y,c); set S1 = 2GatesCircStr (x,y,c,'xor'); set S2 = BorrowStr (x,y,c); set A = BitSubtracterWithBorrowCirc (x,y,c); set A1 = BitSubtracterCirc (x,y,c); set A2 = BorrowCirc (x,y,c); let s be State of (BitSubtracterWithBorrowCirc (x,y,c)); ::_thesis: Following (s,2) is stable reconsider s1 = s | the carrier of (2GatesCircStr (x,y,c,'xor')) as State of (BitSubtracterCirc (x,y,c)) by FACIRC_1:26; reconsider s2 = s | the carrier of (BorrowStr (x,y,c)) as State of (BorrowCirc (x,y,c)) by FACIRC_1:26; reconsider t = s as State of ((BitSubtracterCirc (x,y,c)) +* (BorrowCirc (x,y,c))) ; A1: dom (Following (s,3)) = the carrier of (BitSubtracterWithBorrowStr (x,y,c)) by CIRCUIT1:3; A2: the carrier of (BitSubtracterWithBorrowStr (x,y,c)) = the carrier of (2GatesCircStr (x,y,c,'xor')) \/ the carrier of (BorrowStr (x,y,c)) by CIRCCOMB:def_2; InputVertices (2GatesCircStr (x,y,c,'xor')) is without_pairs by FACIRC_1:59; then InnerVertices (BorrowStr (x,y,c)) misses InputVertices (2GatesCircStr (x,y,c,'xor')) by Th1, FACIRC_1:5; then A3: ( Following (s1,2) = (Following (t,2)) | the carrier of (2GatesCircStr (x,y,c,'xor')) & Following (s1,3) = (Following (t,3)) | the carrier of (2GatesCircStr (x,y,c,'xor')) ) by FACIRC_1:30; Following (s1,2) is stable by FACIRC_1:63; then A4: Following (s1,2) = Following (Following (s1,2)) by CIRCUIT2:def_6 .= Following (s1,(2 + 1)) by FACIRC_1:12 ; InputVertices (BorrowStr (x,y,c)) is without_pairs by Th2; then InnerVertices (2GatesCircStr (x,y,c,'xor')) misses InputVertices (BorrowStr (x,y,c)) by FACIRC_1:5, FACIRC_1:58; then A5: ( Following (s2,2) = (Following (t,2)) | the carrier of (BorrowStr (x,y,c)) & Following (s2,3) = (Following (t,3)) | the carrier of (BorrowStr (x,y,c)) ) by FACIRC_1:31; Following (s2,2) is stable by Th18; then A6: Following (s2,2) = Following (Following (s2,2)) by CIRCUIT2:def_6 .= Following (s2,(2 + 1)) by FACIRC_1:12 ; A7: ( dom (Following (s1,2)) = the carrier of (2GatesCircStr (x,y,c,'xor')) & dom (Following (s2,2)) = the carrier of (BorrowStr (x,y,c)) ) by CIRCUIT1:3; A8: now__::_thesis:_for_a_being_set_st_a_in_the_carrier_of_(BitSubtracterWithBorrowStr_(x,y,c))_holds_ (Following_(s,2))_._a_=_(Following_(Following_(s,2)))_._a let a be set ; ::_thesis: ( a in the carrier of (BitSubtracterWithBorrowStr (x,y,c)) implies (Following (s,2)) . a = (Following (Following (s,2))) . a ) assume a in the carrier of (BitSubtracterWithBorrowStr (x,y,c)) ; ::_thesis: (Following (s,2)) . a = (Following (Following (s,2))) . a then ( a in the carrier of (2GatesCircStr (x,y,c,'xor')) or a in the carrier of (BorrowStr (x,y,c)) ) by A2, XBOOLE_0:def_3; then ( ( (Following (s,2)) . a = (Following (s1,2)) . a & (Following (s,3)) . a = (Following (s1,3)) . a ) or ( (Following (s,2)) . a = (Following (s2,2)) . a & (Following (s,3)) . a = (Following (s2,3)) . a ) ) by A3, A5, A4, A6, A7, FUNCT_1:47; hence (Following (s,2)) . a = (Following (Following (s,2))) . a by A4, A6, FACIRC_1:12; ::_thesis: verum end; ( Following (s,(2 + 1)) = Following (Following (s,2)) & dom (Following (s,2)) = the carrier of (BitSubtracterWithBorrowStr (x,y,c)) ) by CIRCUIT1:3, FACIRC_1:12; hence Following (s,2) = Following (Following (s,2)) by A1, A8, FUNCT_1:2; :: according to CIRCUIT2:def_6 ::_thesis: verum end;