let x, y, z be set ; :: thesis: ( x <> [<*y,z*>,and2b ] & y <> [<*z,x*>,and2b ] & z <> [<*x,y*>,and2b ] implies InputVertices (GFA3CarryIStr x,y,z) = {x,y,z} )
set f1 = and2b ;
set f2 = and2b ;
set f3 = and2b ;
set xy = [<*x,y*>,and2b ];
set yz = [<*y,z*>,and2b ];
set zx = [<*z,x*>,and2b ];
set Cxy = 1GateCircStr <*x,y*>,and2b ;
set Cyz = 1GateCircStr <*y,z*>,and2b ;
set Czx = 1GateCircStr <*z,x*>,and2b ;
assume that
A1: x <> [<*y,z*>,and2b ] and
A2: ( y <> [<*z,x*>,and2b ] & z <> [<*x,y*>,and2b ] ) ; :: thesis: InputVertices (GFA3CarryIStr x,y,z) = {x,y,z}
A3: not [<*x,y*>,and2b ] in {y,z} by A1, A2, Lm1;
A4: not [<*z,x*>,and2b ] in {x,y,z} by A1, A2, Lm1;
A5: y <> [<*y,z*>,and2b ] by FACIRC_2:3;
A6: ( not z in {[<*x,y*>,and2b ],[<*y,z*>,and2b ]} & not x in {[<*x,y*>,and2b ],[<*y,z*>,and2b ]} ) by A1, A2, Lm1;
A7: 1GateCircStr <*x,y*>,and2b tolerates 1GateCircStr <*y,z*>,and2b by CIRCCOMB:55;
InputVertices (GFA3CarryIStr x,y,z) = ((InputVertices ((1GateCircStr <*x,y*>,and2b ) +* (1GateCircStr <*y,z*>,and2b ))) \ (InnerVertices (1GateCircStr <*z,x*>,and2b ))) \/ ((InputVertices (1GateCircStr <*z,x*>,and2b )) \ (InnerVertices ((1GateCircStr <*x,y*>,and2b ) +* (1GateCircStr <*y,z*>,and2b )))) by CIRCCMB2:6, CIRCCOMB:55
.= ((((InputVertices (1GateCircStr <*x,y*>,and2b )) \ (InnerVertices (1GateCircStr <*y,z*>,and2b ))) \/ ((InputVertices (1GateCircStr <*y,z*>,and2b )) \ (InnerVertices (1GateCircStr <*x,y*>,and2b )))) \ (InnerVertices (1GateCircStr <*z,x*>,and2b ))) \/ ((InputVertices (1GateCircStr <*z,x*>,and2b )) \ (InnerVertices ((1GateCircStr <*x,y*>,and2b ) +* (1GateCircStr <*y,z*>,and2b )))) by CIRCCMB2:6, CIRCCOMB:55
.= ((((InputVertices (1GateCircStr <*x,y*>,and2b )) \ (InnerVertices (1GateCircStr <*y,z*>,and2b ))) \/ ((InputVertices (1GateCircStr <*y,z*>,and2b )) \ (InnerVertices (1GateCircStr <*x,y*>,and2b )))) \ (InnerVertices (1GateCircStr <*z,x*>,and2b ))) \/ ((InputVertices (1GateCircStr <*z,x*>,and2b )) \ ((InnerVertices (1GateCircStr <*x,y*>,and2b )) \/ (InnerVertices (1GateCircStr <*y,z*>,and2b )))) by A7, CIRCCOMB:15
.= ((((InputVertices (1GateCircStr <*x,y*>,and2b )) \ {[<*y,z*>,and2b ]}) \/ ((InputVertices (1GateCircStr <*y,z*>,and2b )) \ (InnerVertices (1GateCircStr <*x,y*>,and2b )))) \ (InnerVertices (1GateCircStr <*z,x*>,and2b ))) \/ ((InputVertices (1GateCircStr <*z,x*>,and2b )) \ ((InnerVertices (1GateCircStr <*x,y*>,and2b )) \/ (InnerVertices (1GateCircStr <*y,z*>,and2b )))) by CIRCCOMB:49
.= ((((InputVertices (1GateCircStr <*x,y*>,and2b )) \ {[<*y,z*>,and2b ]}) \/ ((InputVertices (1GateCircStr <*y,z*>,and2b )) \ {[<*x,y*>,and2b ]})) \ (InnerVertices (1GateCircStr <*z,x*>,and2b ))) \/ ((InputVertices (1GateCircStr <*z,x*>,and2b )) \ ((InnerVertices (1GateCircStr <*x,y*>,and2b )) \/ (InnerVertices (1GateCircStr <*y,z*>,and2b )))) by CIRCCOMB:49
.= ((((InputVertices (1GateCircStr <*x,y*>,and2b )) \ {[<*y,z*>,and2b ]}) \/ ((InputVertices (1GateCircStr <*y,z*>,and2b )) \ {[<*x,y*>,and2b ]})) \ {[<*z,x*>,and2b ]}) \/ ((InputVertices (1GateCircStr <*z,x*>,and2b )) \ ((InnerVertices (1GateCircStr <*x,y*>,and2b )) \/ (InnerVertices (1GateCircStr <*y,z*>,and2b )))) by CIRCCOMB:49
.= ((((InputVertices (1GateCircStr <*x,y*>,and2b )) \ {[<*y,z*>,and2b ]}) \/ ((InputVertices (1GateCircStr <*y,z*>,and2b )) \ {[<*x,y*>,and2b ]})) \ {[<*z,x*>,and2b ]}) \/ ((InputVertices (1GateCircStr <*z,x*>,and2b )) \ ({[<*x,y*>,and2b ]} \/ (InnerVertices (1GateCircStr <*y,z*>,and2b )))) by CIRCCOMB:49
.= ((((InputVertices (1GateCircStr <*x,y*>,and2b )) \ {[<*y,z*>,and2b ]}) \/ ((InputVertices (1GateCircStr <*y,z*>,and2b )) \ {[<*x,y*>,and2b ]})) \ {[<*z,x*>,and2b ]}) \/ ((InputVertices (1GateCircStr <*z,x*>,and2b )) \ ({[<*x,y*>,and2b ]} \/ {[<*y,z*>,and2b ]})) by CIRCCOMB:49
.= ((({x,y} \ {[<*y,z*>,and2b ]}) \/ ((InputVertices (1GateCircStr <*y,z*>,and2b )) \ {[<*x,y*>,and2b ]})) \ {[<*z,x*>,and2b ]}) \/ ((InputVertices (1GateCircStr <*z,x*>,and2b )) \ ({[<*x,y*>,and2b ]} \/ {[<*y,z*>,and2b ]})) by FACIRC_1:40
.= ((({x,y} \ {[<*y,z*>,and2b ]}) \/ ({y,z} \ {[<*x,y*>,and2b ]})) \ {[<*z,x*>,and2b ]}) \/ ((InputVertices (1GateCircStr <*z,x*>,and2b )) \ ({[<*x,y*>,and2b ]} \/ {[<*y,z*>,and2b ]})) by FACIRC_1:40
.= ((({x,y} \ {[<*y,z*>,and2b ]}) \/ ({y,z} \ {[<*x,y*>,and2b ]})) \ {[<*z,x*>,and2b ]}) \/ ({z,x} \ ({[<*x,y*>,and2b ]} \/ {[<*y,z*>,and2b ]})) by FACIRC_1:40
.= ((({x,y} \ {[<*y,z*>,and2b ]}) \/ ({y,z} \ {[<*x,y*>,and2b ]})) \ {[<*z,x*>,and2b ]}) \/ ({z,x} \ {[<*x,y*>,and2b ],[<*y,z*>,and2b ]}) by ENUMSET1:41
.= (({x,y} \/ ({y,z} \ {[<*x,y*>,and2b ]})) \ {[<*z,x*>,and2b ]}) \/ ({z,x} \ {[<*x,y*>,and2b ],[<*y,z*>,and2b ]}) by A1, A5, FACIRC_2:1
.= (({x,y} \/ {y,z}) \ {[<*z,x*>,and2b ]}) \/ ({z,x} \ {[<*x,y*>,and2b ],[<*y,z*>,and2b ]}) by A3, ZFMISC_1:65
.= (({x,y} \/ {y,z}) \ {[<*z,x*>,and2b ]}) \/ {z,x} by A6, ZFMISC_1:72
.= ({x,y,y,z} \ {[<*z,x*>,and2b ]}) \/ {z,x} by ENUMSET1:45
.= ({y,y,x,z} \ {[<*z,x*>,and2b ]}) \/ {z,x} by ENUMSET1:110
.= ({y,x,z} \ {[<*z,x*>,and2b ]}) \/ {z,x} by ENUMSET1:71
.= ({x,y,z} \ {[<*z,x*>,and2b ]}) \/ {z,x} by ENUMSET1:99
.= {x,y,z} \/ {z,x} by A4, ZFMISC_1:65
.= {x,y,z,z,x} by ENUMSET1:49
.= {x,y,z,z} \/ {x} by ENUMSET1:50
.= {z,z,x,y} \/ {x} by ENUMSET1:118
.= {z,x,y} \/ {x} by ENUMSET1:71
.= {z,x,y,x} by ENUMSET1:46
.= {x,x,y,z} by ENUMSET1:113
.= {x,y,z} by ENUMSET1:71 ;
hence InputVertices (GFA3CarryIStr x,y,z) = {x,y,z} ; :: thesis: verum