let x, y, c be object ; :: thesis: for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN st c <> [<*x,y*>,f] holds

InputVertices (2GatesCircStr (x,y,c,f)) = {x,y,c}

let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN; :: thesis: ( c <> [<*x,y*>,f] implies InputVertices (2GatesCircStr (x,y,c,f)) = {x,y,c} )

assume A1: c <> [<*x,y*>,f] ; :: thesis: InputVertices (2GatesCircStr (x,y,c,f)) = {x,y,c}

set S = 2GatesCircStr (x,y,c,f);

set S1 = 1GateCircStr (<*x,y*>,f);

set p = <*[<*x,y*>,f],c*>;

set S2 = 1GateCircStr (<*[<*x,y*>,f],c*>,f);

set R = the ResultSort of (2GatesCircStr (x,y,c,f));

A2: the carrier of (2GatesCircStr (x,y,c,f)) = the carrier of (1GateCircStr (<*x,y*>,f)) \/ the carrier of (1GateCircStr (<*[<*x,y*>,f],c*>,f)) by CIRCCOMB:def 2;

A3: rng <*x,y*> = {x,y} by FINSEQ_2:127;

then A4: the carrier of (1GateCircStr (<*x,y*>,f)) = {x,y} \/ {[<*x,y*>,f]} by CIRCCOMB:def 6;

A5: rng the ResultSort of (2GatesCircStr (x,y,c,f)) = {[<*x,y*>,f],(2GatesCircOutput (x,y,c,f))} by Th56

.= {[<*x,y*>,f],[<*[<*x,y*>,f],c*>,f]} ;

A6: rng <*[<*x,y*>,f],c*> = {[<*x,y*>,f],c} by FINSEQ_2:127;

then A7: the carrier of (1GateCircStr (<*[<*x,y*>,f],c*>,f)) = {[<*x,y*>,f],c} \/ {[<*[<*x,y*>,f],c*>,f]} by CIRCCOMB:def 6;

thus InputVertices (2GatesCircStr (x,y,c,f)) c= {x,y,c} :: according to XBOOLE_0:def 10 :: thesis: {x,y,c} c= InputVertices (2GatesCircStr (x,y,c,f))

reconsider zz = z as set by TARSKI:1;

assume z in {x,y,c} ; :: thesis: z in InputVertices (2GatesCircStr (x,y,c,f))

then A10: ( z = x or z = y or z = c ) by ENUMSET1:def 1;

then ( z in {x,y} or z in rng <*[<*x,y*>,f],c*> ) by A6, TARSKI:def 2;

then ( z in InputVertices (1GateCircStr (<*x,y*>,f)) or z in InputVertices (1GateCircStr (<*[<*x,y*>,f],c*>,f)) ) by A3, CIRCCOMB:42;

then A11: z in the carrier of (2GatesCircStr (x,y,c,f)) by A2, XBOOLE_0:def 3;

( ( z in {x,y} & [<*x,y*>,f] in rng <*[<*x,y*>,f],c*> ) or z in {c} ) by A6, A10, TARSKI:def 1, TARSKI:def 2;

then A12: ( ( the_rank_of zz in the_rank_of [<*x,y*>,f] & the_rank_of [<*x,y*>,f] in the_rank_of [<*[<*x,y*>,f],c*>,f] ) or ( z = c & c in rng <*[<*x,y*>,f],c*> ) ) by A3, A6, CLASSES1:82, TARSKI:def 1, TARSKI:def 2;

then the_rank_of zz in the_rank_of [<*[<*x,y*>,f],c*>,f] by CLASSES1:82, ORDINAL1:10;

then A13: z <> [<*[<*x,y*>,f],c*>,f] ;

z <> [<*x,y*>,f] by A1, A12;

then not z in rng the ResultSort of (2GatesCircStr (x,y,c,f)) by A5, A13, TARSKI:def 2;

hence z in InputVertices (2GatesCircStr (x,y,c,f)) by A11, XBOOLE_0:def 5; :: thesis: verum

InputVertices (2GatesCircStr (x,y,c,f)) = {x,y,c}

let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN; :: thesis: ( c <> [<*x,y*>,f] implies InputVertices (2GatesCircStr (x,y,c,f)) = {x,y,c} )

assume A1: c <> [<*x,y*>,f] ; :: thesis: InputVertices (2GatesCircStr (x,y,c,f)) = {x,y,c}

set S = 2GatesCircStr (x,y,c,f);

set S1 = 1GateCircStr (<*x,y*>,f);

set p = <*[<*x,y*>,f],c*>;

set S2 = 1GateCircStr (<*[<*x,y*>,f],c*>,f);

set R = the ResultSort of (2GatesCircStr (x,y,c,f));

A2: the carrier of (2GatesCircStr (x,y,c,f)) = the carrier of (1GateCircStr (<*x,y*>,f)) \/ the carrier of (1GateCircStr (<*[<*x,y*>,f],c*>,f)) by CIRCCOMB:def 2;

A3: rng <*x,y*> = {x,y} by FINSEQ_2:127;

then A4: the carrier of (1GateCircStr (<*x,y*>,f)) = {x,y} \/ {[<*x,y*>,f]} by CIRCCOMB:def 6;

A5: rng the ResultSort of (2GatesCircStr (x,y,c,f)) = {[<*x,y*>,f],(2GatesCircOutput (x,y,c,f))} by Th56

.= {[<*x,y*>,f],[<*[<*x,y*>,f],c*>,f]} ;

A6: rng <*[<*x,y*>,f],c*> = {[<*x,y*>,f],c} by FINSEQ_2:127;

then A7: the carrier of (1GateCircStr (<*[<*x,y*>,f],c*>,f)) = {[<*x,y*>,f],c} \/ {[<*[<*x,y*>,f],c*>,f]} by CIRCCOMB:def 6;

thus InputVertices (2GatesCircStr (x,y,c,f)) c= {x,y,c} :: according to XBOOLE_0:def 10 :: thesis: {x,y,c} c= InputVertices (2GatesCircStr (x,y,c,f))

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in {x,y,c} or z in InputVertices (2GatesCircStr (x,y,c,f)) )
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in InputVertices (2GatesCircStr (x,y,c,f)) or z in {x,y,c} )

assume A8: z in InputVertices (2GatesCircStr (x,y,c,f)) ; :: thesis: z in {x,y,c}

then ( z in the carrier of (1GateCircStr (<*x,y*>,f)) or z in the carrier of (1GateCircStr (<*[<*x,y*>,f],c*>,f)) ) by A2, XBOOLE_0:def 3;

then ( z in {x,y} or z in {[<*x,y*>,f]} or z in {[<*x,y*>,f],c} or z in {[<*[<*x,y*>,f],c*>,f]} ) by A4, A7, XBOOLE_0:def 3;

then A9: ( z = x or z = y or z = [<*x,y*>,f] or z = c or z = [<*[<*x,y*>,f],c*>,f] ) by TARSKI:def 1, TARSKI:def 2;

not z in rng the ResultSort of (2GatesCircStr (x,y,c,f)) by A8, XBOOLE_0:def 5;

hence z in {x,y,c} by A5, A9, ENUMSET1:def 1, TARSKI:def 2; :: thesis: verum

end;assume A8: z in InputVertices (2GatesCircStr (x,y,c,f)) ; :: thesis: z in {x,y,c}

then ( z in the carrier of (1GateCircStr (<*x,y*>,f)) or z in the carrier of (1GateCircStr (<*[<*x,y*>,f],c*>,f)) ) by A2, XBOOLE_0:def 3;

then ( z in {x,y} or z in {[<*x,y*>,f]} or z in {[<*x,y*>,f],c} or z in {[<*[<*x,y*>,f],c*>,f]} ) by A4, A7, XBOOLE_0:def 3;

then A9: ( z = x or z = y or z = [<*x,y*>,f] or z = c or z = [<*[<*x,y*>,f],c*>,f] ) by TARSKI:def 1, TARSKI:def 2;

not z in rng the ResultSort of (2GatesCircStr (x,y,c,f)) by A8, XBOOLE_0:def 5;

hence z in {x,y,c} by A5, A9, ENUMSET1:def 1, TARSKI:def 2; :: thesis: verum

reconsider zz = z as set by TARSKI:1;

assume z in {x,y,c} ; :: thesis: z in InputVertices (2GatesCircStr (x,y,c,f))

then A10: ( z = x or z = y or z = c ) by ENUMSET1:def 1;

then ( z in {x,y} or z in rng <*[<*x,y*>,f],c*> ) by A6, TARSKI:def 2;

then ( z in InputVertices (1GateCircStr (<*x,y*>,f)) or z in InputVertices (1GateCircStr (<*[<*x,y*>,f],c*>,f)) ) by A3, CIRCCOMB:42;

then A11: z in the carrier of (2GatesCircStr (x,y,c,f)) by A2, XBOOLE_0:def 3;

( ( z in {x,y} & [<*x,y*>,f] in rng <*[<*x,y*>,f],c*> ) or z in {c} ) by A6, A10, TARSKI:def 1, TARSKI:def 2;

then A12: ( ( the_rank_of zz in the_rank_of [<*x,y*>,f] & the_rank_of [<*x,y*>,f] in the_rank_of [<*[<*x,y*>,f],c*>,f] ) or ( z = c & c in rng <*[<*x,y*>,f],c*> ) ) by A3, A6, CLASSES1:82, TARSKI:def 1, TARSKI:def 2;

then the_rank_of zz in the_rank_of [<*[<*x,y*>,f],c*>,f] by CLASSES1:82, ORDINAL1:10;

then A13: z <> [<*[<*x,y*>,f],c*>,f] ;

z <> [<*x,y*>,f] by A1, A12;

then not z in rng the ResultSort of (2GatesCircStr (x,y,c,f)) by A5, A13, TARSKI:def 2;

hence z in InputVertices (2GatesCircStr (x,y,c,f)) by A11, XBOOLE_0:def 5; :: thesis: verum