let x, y, c be set ; :: 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:51;
hence InnerVertices (2GatesCircStr x,y,c,f) = (InnerVertices (1GateCircStr <*x,y*>,f)) \/ (InnerVertices (1GateCircStr <*[<*x,y*>,f],c*>,f)) by CIRCCOMB:15
.= {[<*x,y*>,f]} \/ (InnerVertices (1GateCircStr <*[<*x,y*>,f],c*>,f)) by CIRCCOMB:49
.= {[<*x,y*>,f]} \/ {[<*[<*x,y*>,f],c*>,f]} by CIRCCOMB:49
.= {[<*x,y*>,f],(2GatesCircOutput x,y,c,f)} by ENUMSET1:41 ;
:: thesis: verum