fscirc_1.miz

    begin

    reserve x,y,c for set;

    definition

      let x,y,c be set;

      :: FSCIRC_1:def1

      func BitSubtracterOutput (x,y,c) -> Element of ( InnerVertices ( 2GatesCircStr (x,y,c, 'xor' ))) equals ( 2GatesCircOutput (x,y,c, 'xor' ));

      coherence ;

    end

    definition

      let x,y,c be set;

      :: FSCIRC_1:def2

      func BitSubtracterCirc (x,y,c) -> strict Boolean gate`2=den Circuit of ( 2GatesCircStr (x,y,c, 'xor' )) equals ( 2GatesCircuit (x,y,c, 'xor' ));

      coherence ;

    end

    definition

      let x,y,c be set;

      :: FSCIRC_1:def3

      func BorrowIStr (x,y,c) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign equals ((( 1GateCircStr ( <*x, y*>, and2a )) +* ( 1GateCircStr ( <*y, c*>, and2 ))) +* ( 1GateCircStr ( <*x, c*>, and2a )));

      correctness ;

    end

    definition

      let x,y,c be set;

      :: FSCIRC_1:def4

      func BorrowStr (x,y,c) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign equals (( BorrowIStr (x,y,c)) +* ( 1GateCircStr ( <* [ <*x, y*>, and2a ], [ <*y, c*>, and2 ], [ <*x, c*>, and2a ]*>, or3 )));

      correctness ;

    end

    definition

      let x,y,c be set;

      :: FSCIRC_1:def5

      func BorrowICirc (x,y,c) -> strict Boolean gate`2=den Circuit of ( BorrowIStr (x,y,c)) equals ((( 1GateCircuit (x,y, and2a )) +* ( 1GateCircuit (y,c, and2 ))) +* ( 1GateCircuit (x,c, and2a )));

      coherence ;

    end

    theorem :: FSCIRC_1:1



     Th1: ( InnerVertices ( BorrowStr (x,y,c))) is Relation

    proof

      ( 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 thesis by FACIRC_1: 3;

    end;

    theorem :: FSCIRC_1:2



     Th2: for x,y,c be non pair set holds ( InputVertices ( BorrowStr (x,y,c))) is without_pairs

    proof

      let x,y,c be non pair set;

      set M = ( BorrowStr (x,y,c)), MI = ( BorrowIStr (x,y,c));

      set S = ( 1GateCircStr ( <* [ <*x, y*>, and2a ], [ <*y, c*>, and2 ], [ <*x, c*>, and2a ]*>, or3 ));

      given xx be pair object such that

       A1: xx in ( InputVertices M);



       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 MI) = (( { [ <*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 S) = { [ <*x, y*>, and2a ], [ <*y, c*>, and2 ], [ <*x, c*>, and2a ]} by FACIRC_1: 42;

      then

       A5: (( InputVertices S) \ ( InnerVertices MI)) = {} 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 MI) is without_pairs by FACIRC_1: 9;

      ( InnerVertices S) is Relation by FACIRC_1: 38;

      then ( InputVertices M) = (( InputVertices MI) \/ (( InputVertices S) \ ( InnerVertices MI))) by A6, FACIRC_1: 6;

      hence thesis by A6, A1, A5;

    end;

    theorem :: FSCIRC_1:3

    for s be State of ( BorrowICirc (x,y,c)), a,b be Element of BOOLEAN st a = (s . x) & b = (s . y) holds (( Following s) . [ <*x, y*>, and2a ]) = (( 'not' a) '&' b)

    proof

      set xy = <*x, y*>, yc = <*y, c*>, xc = <*x, c*>;

      set S1 = ( 1GateCircStr (xy, and2a )), A1 = ( 1GateCircuit (x,y, and2a ));

      set S2 = ( 1GateCircStr (yc, and2 )), A2 = ( 1GateCircuit (y,c, and2 ));

      set S3 = ( 1GateCircStr (xc, and2a )), A3 = ( 1GateCircuit (x,c, and2a ));

      set S = ( BorrowIStr (x,y,c)), A = ( BorrowICirc (x,y,c));

      set v1 = [xy, and2a ];

      let s be State of A;

      let a,b be Element of BOOLEAN such that

       A1: a = (s . x) & b = (s . y);

      reconsider xx = x, yy = y as Vertex of S1 by FACIRC_1: 43;

      reconsider v1 as Element of ( InnerVertices S1) by FACIRC_1: 47;



       A2: S = (S1 +* (S2 +* S3)) by CIRCCOMB: 6;

      then

      reconsider v = v1 as Element of ( InnerVertices S) by FACIRC_1: 21;



       A3: A = (A1 +* (A2 +* A3)) by FACIRC_1: 25;

      then

      reconsider s1 = (s | the carrier of S1) as State of A1 by FACIRC_1: 26;

      reconsider xx, yy as Vertex of S by A2, FACIRC_1: 20;



       A4: ( dom s1) = the carrier of S1 by CIRCUIT1: 3;



      thus (( Following s) . [xy, 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;

    end;

    theorem :: FSCIRC_1:4

    for s be State of ( BorrowICirc (x,y,c)), a,b be Element of BOOLEAN st a = (s . y) & b = (s . c) holds (( Following s) . [ <*y, c*>, and2 ]) = (a '&' b)

    proof

      set xy = <*x, y*>, yc = <*y, c*>, xc = <*x, c*>;

      set S1 = ( 1GateCircStr (xy, and2a )), A1 = ( 1GateCircuit (x,y, and2a ));

      set S2 = ( 1GateCircStr (yc, and2 )), A2 = ( 1GateCircuit (y,c, and2 ));

      set S3 = ( 1GateCircStr (xc, and2a )), A3 = ( 1GateCircuit (x,c, and2a ));

      set S = ( BorrowIStr (x,y,c)), A = ( BorrowICirc (x,y,c));

      set v2 = [yc, and2 ];

      let s be State of A;

      let a,b be Element of BOOLEAN such that

       A1: a = (s . y) & b = (s . c);

      reconsider yy = y, cc = c as Vertex of S2 by FACIRC_1: 43;

      reconsider v2 as Element of ( InnerVertices S2) by FACIRC_1: 47;



       A2: (S1 +* S2) = (S2 +* S1) by FACIRC_1: 23;

      then

       A3: S = (S2 +* (S1 +* S3)) by CIRCCOMB: 6;

      then

      reconsider v = v2 as Element of ( InnerVertices S) by FACIRC_1: 21;

      (A1 +* A2) = (A2 +* A1) by FACIRC_1: 24;

      then

       A4: A = (A2 +* (A1 +* A3)) by A2, FACIRC_1: 25;

      then

      reconsider s2 = (s | the carrier of S2) as State of A2 by FACIRC_1: 26;

      reconsider yy, cc as Vertex of S by A3, FACIRC_1: 20;



       A5: ( dom s2) = the carrier of S2 by CIRCUIT1: 3;



      thus (( Following s) . [yc, 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, FACIRC_1:def 6;

    end;

    theorem :: FSCIRC_1:5

    for s be State of ( BorrowICirc (x,y,c)), a,b be Element of BOOLEAN st a = (s . x) & b = (s . c) holds (( Following s) . [ <*x, c*>, and2a ]) = (( 'not' a) '&' b)

    proof

      set xc = <*x, c*>;

      set S3 = ( 1GateCircStr (xc, and2a )), A3 = ( 1GateCircuit (x,c, and2a ));

      set S = ( BorrowIStr (x,y,c)), A = ( BorrowICirc (x,y,c));

      set v3 = [xc, and2a ];

      let s be State of A;

      let a,b be Element of BOOLEAN such that

       A1: a = (s . x) & b = (s . c);

      reconsider xx = x, cc = c as Vertex of S3 by FACIRC_1: 43;

      reconsider s3 = (s | the carrier of S3) as State of A3 by FACIRC_1: 26;

      reconsider v3 as Element of ( InnerVertices S3) by FACIRC_1: 47;

      reconsider v = v3 as Element of ( InnerVertices S) by FACIRC_1: 21;



       A2: ( dom s3) = the carrier of S3 by CIRCUIT1: 3;

      reconsider xx, cc as Vertex of S by FACIRC_1: 20;



      thus (( Following s) . [xc, 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;

    end;

    definition

      let x,y,c be set;

      :: FSCIRC_1:def6

      func BorrowOutput (x,y,c) -> Element of ( InnerVertices ( BorrowStr (x,y,c))) equals [ <* [ <*x, y*>, and2a ], [ <*y, c*>, and2 ], [ <*x, c*>, and2a ]*>, or3 ];

      coherence

      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 thesis by FACIRC_1: 21;

      end;

      correctness ;

    end

    definition

      let x,y,c be set;

      :: FSCIRC_1:def7

      func BorrowCirc (x,y,c) -> strict Boolean gate`2=den Circuit of ( BorrowStr (x,y,c)) equals (( BorrowICirc (x,y,c)) +* ( 1GateCircuit ( [ <*x, y*>, and2a ], [ <*y, c*>, and2 ], [ <*x, c*>, and2a ], or3 )));

      coherence ;

    end

    theorem :: FSCIRC_1:6



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

      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 thesis by A2, A1, FACIRC_1: 20;

    end;

    theorem :: FSCIRC_1:7



     Th7: [ <*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

       [ <*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 thesis by A1, A2, FACIRC_1: 21;

    end;

    theorem :: FSCIRC_1:8



     Th8: for x,y,c be 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;

      assume

       A1: not thesis;



       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 be object st x = [a1, b1]) or (ex a1,b1 be object st y = [a1, b1]) or ex a1,b1 be object st c = [a1, b1] by A3, RELAT_1:def 1;

      hence contradiction;

    end;

    theorem :: FSCIRC_1:9



     Th9: for x,y,c be 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;

      set xy = <*x, y*>, yc = <*y, c*>, xc = <*x, c*>;

      set xy1 = [xy, and2a ], yc1 = [yc, and2 ], xc1 = [xc, and2a ];

      set MI = ( BorrowIStr (x,y,c)), S = ( 1GateCircStr ( <*xy1, yc1, xc1*>, 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 S) 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 MI) is without_pairs by FACIRC_1: 9;

      then

       A7: ( InputVertices M) = (( InputVertices MI) \/ (( InputVertices S) \ ( InnerVertices MI))) 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 MI) = (( { [ <*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 S) = { [ <*x, y*>, and2a ], [ <*y, c*>, and2 ], [ <*x, c*>, and2a ]} by FACIRC_1: 42;

      then

       A11: (( InputVertices S) \ ( InnerVertices MI)) = {} 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 M) = (( 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;

      MI tolerates S by CIRCCOMB: 47;



      hence ( InnerVertices M) = (( InnerVertices MI) \/ ( InnerVertices S)) by CIRCCOMB: 11

      .= ( { [ <*x, y*>, and2a ], [ <*y, c*>, and2 ], [ <*x, c*>, and2a ]} \/ {( BorrowOutput (x,y,c))}) by A10, CIRCCOMB: 42;

    end;



     Lm1: for x,y,c be non pair set holds for s be State of ( BorrowCirc (x,y,c)) holds for a1,a2,a3 be 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;

      let s be State of ( BorrowCirc (x,y,c));

      let a1,a2,a3 be Element of BOOLEAN such that

       A1: a1 = (s . x) and

       A2: a2 = (s . y) and

       A3: a3 = (s . c);

      set S = ( BorrowStr (x,y,c));



       A4: ( InnerVertices S) = the carrier' of S by FACIRC_1: 37;



       A5: y in the carrier of S by Th6;



       A6: x in the carrier of S by Th6;



       A7: ( dom s) = the carrier of S 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;



       A8: c in the carrier of S 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 FACIRC_1:def 6;

       [ <*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;

    end;

    theorem :: FSCIRC_1:10

    for x,y,c be non pair set holds for s be State of ( BorrowCirc (x,y,c)) holds for a1,a2 be 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;

      reconsider a = c as Vertex of ( BorrowStr (x,y,c)) by Th6;

      let s be State of ( BorrowCirc (x,y,c));

      (s . a) is Element of BOOLEAN ;

      hence thesis by Lm1;

    end;

    theorem :: FSCIRC_1:11

    for x,y,c be non pair set holds for s be State of ( BorrowCirc (x,y,c)) holds for a2,a3 be 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;

      reconsider a = x as Vertex of ( BorrowStr (x,y,c)) by Th6;

      let s be State of ( BorrowCirc (x,y,c));

      (s . a) is Element of BOOLEAN ;

      hence thesis by Lm1;

    end;

    theorem :: FSCIRC_1:12

    for x,y,c be non pair set holds for s be State of ( BorrowCirc (x,y,c)) holds for a1,a3 be 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;

      reconsider a = y as Vertex of ( BorrowStr (x,y,c)) by Th6;

      let s be State of ( BorrowCirc (x,y,c));

      (s . a) is Element of BOOLEAN ;

      hence thesis by Lm1;

    end;

    theorem :: FSCIRC_1:13



     Th13: for x,y,c be non pair set holds for s be State of ( BorrowCirc (x,y,c)) holds for a1,a2,a3 be 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;

      set xy = <*x, y*>, yc = <*y, c*>, xc = <*x, c*>;

      set xy1 = [xy, and2a ], yc1 = [yc, and2 ], xc1 = [xc, and2a ];

      set S = ( BorrowStr (x,y,c));

      reconsider xy1, yc1, xc1 as Element of ( InnerVertices S) by Th7;

      let s be State of ( BorrowCirc (x,y,c));

      let a1,a2,a3 be Element of BOOLEAN such that

       A1: a1 = (s . [ <*x, y*>, and2a ]) & a2 = (s . [ <*y, c*>, and2 ]) & a3 = (s . [ <*x, c*>, and2a ]);



       A2: ( dom s) = the carrier of S by CIRCUIT1: 3;

      ( InnerVertices S) = the carrier' of S 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;

    end;



     Lm2: for x,y,c be non pair set holds for s be State of ( BorrowCirc (x,y,c)) holds for a1,a2,a3 be 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;

      set S = ( BorrowStr (x,y,c));

      reconsider x9 = x, y9 = y, c9 = c as Vertex of S by Th6;

      let s be State of ( BorrowCirc (x,y,c));

      set xy = <*x, y*>, yc = <*y, c*>, xc = <*x, c*>;

      set xy1 = [xy, and2a ], yc1 = [yc, and2 ], xc1 = [xc, and2a ];



       A1: ( Following (s,2)) = ( Following ( Following s)) by FACIRC_1: 15;

      let a1,a2,a3 be Element of BOOLEAN such that

       A2: a1 = (s . x) & a2 = (s . y) & a3 = (s . c);



       A3: (( Following s) . xc1) = (( 'not' a1) '&' a3) by A2, Lm1;

      (( Following s) . xy1) = (( 'not' a1) '&' a2) & (( Following s) . yc1) = (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;

      y in ( InputVertices S) by Th8;

      then

       A4: (( Following s) . y9) = (s . y) by CIRCUIT2:def 5;

      c in ( InputVertices S) by Th8;

      then

       A5: (( Following s) . c9) = (s . c) by CIRCUIT2:def 5;

      x in ( InputVertices S) by Th8;

      then (( Following s) . x9) = (s . x) by CIRCUIT2:def 5;

      hence thesis by A2, A4, A5, A1, Lm1;

    end;

    theorem :: FSCIRC_1:14

    for x,y,c be non pair set holds for s be State of ( BorrowCirc (x,y,c)) holds for a1,a2 be 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;

      reconsider a = c as Vertex of ( BorrowStr (x,y,c)) by Th6;

      let s be State of ( BorrowCirc (x,y,c));

      (s . a) is Element of BOOLEAN ;

      hence thesis by Lm2;

    end;

    theorem :: FSCIRC_1:15

    for x,y,c be non pair set holds for s be State of ( BorrowCirc (x,y,c)) holds for a2,a3 be 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;

      reconsider a = x as Vertex of ( BorrowStr (x,y,c)) by Th6;

      let s be State of ( BorrowCirc (x,y,c));

      (s . a) is Element of BOOLEAN ;

      hence thesis by Lm2;

    end;

    theorem :: FSCIRC_1:16

    for x,y,c be non pair set holds for s be State of ( BorrowCirc (x,y,c)) holds for a1,a3 be 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;

      reconsider a = y as Vertex of ( BorrowStr (x,y,c)) by Th6;

      let s be State of ( BorrowCirc (x,y,c));

      (s . a) is Element of BOOLEAN ;

      hence thesis by Lm2;

    end;

    theorem :: FSCIRC_1:17

    for x,y,c be non pair set holds for s be State of ( BorrowCirc (x,y,c)) holds for a1,a2,a3 be 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 :: FSCIRC_1:18



     Th18: for x,y,c be non pair set holds for s be State of ( BorrowCirc (x,y,c)) holds ( Following (s,2)) is stable

    proof

      let x,y,c be non pair set;

      set S = ( BorrowStr (x,y,c));

      reconsider xx = x, yy = y, cc = c as Vertex of S by Th6;

      let s be State of ( BorrowCirc (x,y,c));

      set a1 = (s . xx), a2 = (s . yy), a3 = (s . cc);

      set ffs = ( Following (s,2)), fffs = ( Following ffs);



       A1: ffs = ( Following ( Following s)) by FACIRC_1: 15;



       A2: y in ( InputVertices S) by Th8;

      then (( Following s) . y) = a2 by CIRCUIT2:def 5;

      then

       A3: (ffs . y) = a2 by A1, A2, CIRCUIT2:def 5;

      a2 = (s . y);

      then

       A4: (ffs . [ <*x, c*>, and2a ]) = (( 'not' a1) '&' a3) by Lm2;



       A5: x in ( InputVertices S) by Th8;

      then (( Following s) . x) = a1 by CIRCUIT2:def 5;

      then

       A6: (ffs . x) = a1 by A1, A5, CIRCUIT2:def 5;

      a1 = (s . x);

      then

       A7: (ffs . [ <*y, c*>, and2 ]) = (a2 '&' a3) by Lm2;



       A8: c in ( InputVertices S) by Th8;

      then (( Following s) . c) = a3 by CIRCUIT2:def 5;

      then

       A9: (ffs . c) = a3 by A1, A8, CIRCUIT2:def 5;

      a3 = (s . c);

      then

       A10: (ffs . [ <*x, y*>, and2a ]) = (( 'not' a1) '&' a2) by Lm2;



       A11: (ffs . ( BorrowOutput (x,y,c))) = (((( 'not' a1) '&' a2) 'or' (a2 '&' a3)) 'or' (( 'not' a1) '&' a3)) by Lm2;

       A12:

      now

        let a be object;

        assume

         A13: a in the carrier of S;

        then

        reconsider v = a as Vertex of S;



         A14: v in (( InputVertices S) \/ ( InnerVertices S)) by A13, XBOOLE_1: 45;

        thus (ffs . a) = (fffs . a)

        proof

          per cases by A14, XBOOLE_0:def 3;

            suppose v in ( InputVertices S);

            hence thesis by CIRCUIT2:def 5;

          end;

            suppose v in ( InnerVertices S);

            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 thesis by A11, A10, A7, A4, A6, A3, A9, Lm1, Th13;

          end;

        end;

      end;

      ( dom ( Following ( Following (s,2)))) = the carrier of S & ( dom ( Following (s,2))) = the carrier of S by CIRCUIT1: 3;

      hence ffs = fffs by A12, FUNCT_1: 2;

    end;

    begin

    definition

      let x,y,c be set;

      :: FSCIRC_1:def8

      func BitSubtracterWithBorrowStr (x,y,c) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign equals (( 2GatesCircStr (x,y,c, 'xor' )) +* ( BorrowStr (x,y,c)));

      coherence ;

    end

    theorem :: FSCIRC_1:19



     Th19: for x,y,c be non pair set holds ( InputVertices ( BitSubtracterWithBorrowStr (x,y,c))) = {x, y, c}

    proof

      let x,y,c be non pair set;

      set S = ( BitSubtracterWithBorrowStr (x,y,c));

      set S1 = ( 2GatesCircStr (x,y,c, 'xor' )), S2 = ( BorrowStr (x,y,c));



       A1: ( InputVertices S1) = {x, y, c} & ( InputVertices S2) = {x, y, c} by Th9, FACIRC_1: 57;

      ( InnerVertices S1) is Relation & ( InnerVertices S2) is Relation by Th1, FACIRC_1: 58;



      hence ( InputVertices S) = ( {x, y, c} \/ {x, y, c}) by A1, FACIRC_1: 7

      .= {x, y, c};

    end;

    theorem :: FSCIRC_1:20

    for x,y,c be 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;

      set S1 = ( 2GatesCircStr (x,y,c, 'xor' )), 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 S1) = { [ <*x, y*>, 'xor' ], ( 2GatesCircOutput (x,y,c, 'xor' ))} by FACIRC_1: 56, XBOOLE_1: 4;

      ( InnerVertices S2) = ( { [ <*x, y*>, and2a ], [ <*y, c*>, and2 ], [ <*x, c*>, and2a ]} \/ {( BorrowOutput (x,y,c))}) by Th9;

      hence thesis by A1, FACIRC_1: 27;

    end;

    theorem :: FSCIRC_1:21

    for S be 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

      set S1 = ( 2GatesCircStr (x,y,c, 'xor' ));

      let S be non empty ManySortedSign;



       A1: x in the carrier of S1 & y in the carrier of S1 by FACIRC_1: 60;



       A2: c in the carrier of S1 by FACIRC_1: 60;

      assume S = ( BitSubtracterWithBorrowStr (x,y,c));

      hence thesis by A1, A2, FACIRC_1: 20;

    end;

    definition

      let x,y,c be set;

      :: FSCIRC_1:def9

      func BitSubtracterWithBorrowCirc (x,y,c) -> strict Boolean gate`2=den Circuit of ( BitSubtracterWithBorrowStr (x,y,c)) equals (( BitSubtracterCirc (x,y,c)) +* ( BorrowCirc (x,y,c)));

      coherence ;

    end

    theorem :: FSCIRC_1:22

    ( InnerVertices ( BitSubtracterWithBorrowStr (x,y,c))) is Relation

    proof

      ( InnerVertices ( 2GatesCircStr (x,y,c, 'xor' ))) is Relation & ( InnerVertices ( BorrowStr (x,y,c))) is Relation by Th1, FACIRC_1: 58;

      hence thesis by FACIRC_1: 3;

    end;

    theorem :: FSCIRC_1:23

    for x,y,c be non pair set holds ( InputVertices ( BitSubtracterWithBorrowStr (x,y,c))) is without_pairs

    proof

      let x,y,c be non pair set;

      ( InputVertices ( BitSubtracterWithBorrowStr (x,y,c))) = {x, y, c} by Th19;

      hence thesis;

    end;

    theorem :: FSCIRC_1:24

    for x,y,c be non pair set holds for s be State of ( BitSubtracterWithBorrowCirc (x,y,c)) holds for a1,a2,a3 be 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;

      set S1 = ( 2GatesCircStr (x,y,c, 'xor' )), S2 = ( BorrowStr (x,y,c));

      set A = ( BitSubtracterWithBorrowCirc (x,y,c));

      set A1 = ( BitSubtracterCirc (x,y,c)), A2 = ( BorrowCirc (x,y,c));

      let s be State of A;

      let a1,a2,a3 be Element of BOOLEAN ;

      assume that

       A1: a1 = (s . x) and

       A2: a2 = (s . y) and

       A3: a3 = (s . c);

      reconsider s1 = (s | the carrier of S1) as State of A1 by FACIRC_1: 26;



       A4: ( dom s1) = the carrier of S1 by CIRCUIT1: 3;

      c in the carrier of S1 by FACIRC_1: 60;

      then

       A5: a3 = (s1 . c) by A3, A4, FUNCT_1: 47;

      y in the carrier of S1 by FACIRC_1: 60;

      then

       A6: a2 = (s1 . y) by A2, A4, FUNCT_1: 47;

      reconsider t = s as State of (A1 +* A2);

      ( InputVertices S1) is without_pairs by FACIRC_1: 59;

      then ( InnerVertices S2) misses ( InputVertices S1) by Th1, FACIRC_1: 5;

      then

       A7: (( Following (t,2)) . ( 2GatesCircOutput (x,y,c,f))) = (( Following (s1,2)) . ( 2GatesCircOutput (x,y,c,f))) by FACIRC_1: 32;

      reconsider s2 = (s | the carrier of S2) as State of A2 by FACIRC_1: 26;



       A8: ( dom s2) = the carrier of S2 by CIRCUIT1: 3;

      x in the carrier of S1 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;

      ( InputVertices S2) is without_pairs by Th2;

      then ( InnerVertices S1) misses ( InputVertices S2) 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 S2 by Th6;

      then

       A10: a3 = (s2 . c) by A3, A8, FUNCT_1: 47;

      y in the carrier of S2 by Th6;

      then

       A11: a2 = (s2 . y) by A2, A8, FUNCT_1: 47;

      x in the carrier of S2 by Th6;

      then a1 = (s2 . x) by A1, A8, FUNCT_1: 47;

      hence thesis by A11, A10, A9, Lm2;

    end;

    theorem :: FSCIRC_1:25

    for x,y,c be non pair set holds for s be State of ( BitSubtracterWithBorrowCirc (x,y,c)) holds ( Following (s,2)) is stable

    proof

      let x,y,c be non pair set;

      set S = ( BitSubtracterWithBorrowStr (x,y,c));

      set S1 = ( 2GatesCircStr (x,y,c, 'xor' )), S2 = ( BorrowStr (x,y,c));

      set A = ( BitSubtracterWithBorrowCirc (x,y,c));

      set A1 = ( BitSubtracterCirc (x,y,c)), A2 = ( BorrowCirc (x,y,c));

      let s be State of A;

      reconsider s1 = (s | the carrier of S1) as State of A1 by FACIRC_1: 26;

      reconsider s2 = (s | the carrier of S2) as State of A2 by FACIRC_1: 26;

      reconsider t = s as State of (A1 +* A2);



       A1: ( dom ( Following (s,3))) = the carrier of S by CIRCUIT1: 3;



       A2: the carrier of S = (the carrier of S1 \/ the carrier of S2) by CIRCCOMB:def 2;

      ( InputVertices S1) is without_pairs by FACIRC_1: 59;

      then ( InnerVertices S2) misses ( InputVertices S1) by Th1, FACIRC_1: 5;

      then

       A3: ( Following (s1,2)) = (( Following (t,2)) | the carrier of S1) & ( Following (s1,3)) = (( Following (t,3)) | the carrier of S1) by FACIRC_1: 30;

      ( Following (s1,2)) is stable by FACIRC_1: 63;



      then

       A4: ( Following (s1,2)) = ( Following ( Following (s1,2)))

      .= ( Following (s1,(2 + 1))) by FACIRC_1: 12;

      ( InputVertices S2) is without_pairs by Th2;

      then ( InnerVertices S1) misses ( InputVertices S2) by FACIRC_1: 5, FACIRC_1: 58;

      then

       A5: ( Following (s2,2)) = (( Following (t,2)) | the carrier of S2) & ( Following (s2,3)) = (( Following (t,3)) | the carrier of S2) by FACIRC_1: 31;

      ( Following (s2,2)) is stable by Th18;



      then

       A6: ( Following (s2,2)) = ( Following ( Following (s2,2)))

      .= ( Following (s2,(2 + 1))) by FACIRC_1: 12;



       A7: ( dom ( Following (s1,2))) = the carrier of S1 & ( dom ( Following (s2,2))) = the carrier of S2 by CIRCUIT1: 3;

       A8:

      now

        let a be object;

        assume a in the carrier of S;

        then a in the carrier of S1 or a in the carrier of S2 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;

      end;

      ( Following (s,(2 + 1))) = ( Following ( Following (s,2))) & ( dom ( Following (s,2))) = the carrier of S by CIRCUIT1: 3, FACIRC_1: 12;

      hence ( Following (s,2)) = ( Following ( Following (s,2))) by A1, A8, FUNCT_1: 2;

    end;