:: 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;