let x, y, c be object ; :: thesis: for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds InnerVertices (2GatesCircStr (x,y,c,f)) = {[<*x,y*>,f],(2GatesCircOutput (x,y,c,f))}
let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN; :: thesis: InnerVertices (2GatesCircStr (x,y,c,f)) = {[<*x,y*>,f],(2GatesCircOutput (x,y,c,f))}
set p = <*[<*x,y*>,f],c*>;
set S1 = 1GateCircStr (<*x,y*>,f);
set S2 = 1GateCircStr (<*[<*x,y*>,f],c*>,f);
set S = 2GatesCircStr (x,y,c,f);
1GateCircStr (<*x,y*>,f) tolerates 1GateCircStr (<*[<*x,y*>,f],c*>,f) by CIRCCOMB:43;
hence InnerVertices (2GatesCircStr (x,y,c,f)) = (InnerVertices (1GateCircStr (<*x,y*>,f))) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,f],c*>,f))) by CIRCCOMB:11
.= {[<*x,y*>,f]} \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,f],c*>,f))) by CIRCCOMB:42
.= {[<*x,y*>,f]} \/ {[<*[<*x,y*>,f],c*>,f]} by CIRCCOMB:42
.= {[<*x,y*>,f],(2GatesCircOutput (x,y,c,f))} by ENUMSET1:1 ;
:: thesis: verum