let x, y, c be set ; :: thesis: ( x <> [<*y,c*>,'&'] & y <> [<*c,x*>,'&'] & c <> [<*x,y*>,'&'] implies InputVertices (MajorityIStr (x,y,c)) = {x,y,c} )
assume that
A1: x <> [<*y,c*>,'&'] and
A2: y <> [<*c,x*>,'&'] and
A3: c <> [<*x,y*>,'&'] ; :: thesis: InputVertices (MajorityIStr (x,y,c)) = {x,y,c}
A4: 1GateCircStr (<*x,y*>,'&') tolerates 1GateCircStr (<*y,c*>,'&') by CIRCCOMB:47;
A5: y in {1,y} by TARSKI:def 2;
A6: y in {2,y} by TARSKI:def 2;
A7: {1,y} in {{1},{1,y}} by TARSKI:def 2;
A8: {2,y} in {{2},{2,y}} by TARSKI:def 2;
<*y,c*> = <*y*> ^ <*c*> by FINSEQ_1:def 9;
then A9: <*y*> c= <*y,c*> by FINSEQ_6:10;
<*y*> = {[1,y]} by FINSEQ_1:def 5;
then A10: [1,y] in <*y*> by TARSKI:def 1;
A11: <*y,c*> in {<*y,c*>} by TARSKI:def 1;
A12: {<*y,c*>} in {{<*y,c*>},{<*y,c*>,'&'}} by TARSKI:def 2;
then A13: y <> [<*y,c*>,'&'] by A5, A7, A9, A10, A11, XREGULAR:9;
A14: c in {2,c} by TARSKI:def 2;
A15: {2,c} in {{2},{2,c}} by TARSKI:def 2;
dom <*y,c*> = Seg 2 by FINSEQ_1:89;
then A16: 2 in dom <*y,c*> by FINSEQ_1:1;
<*y,c*> . 2 = c by FINSEQ_1:44;
then [2,c] in <*y,c*> by A16, FUNCT_1:1;
then A17: c <> [<*y,c*>,'&'] by A11, A12, A14, A15, XREGULAR:9;
dom <*x,y*> = Seg 2 by FINSEQ_1:89;
then A18: 2 in dom <*x,y*> by FINSEQ_1:1;
<*x,y*> . 2 = y by FINSEQ_1:44;
then A19: [2,y] in <*x,y*> by A18, FUNCT_1:1;
A20: <*x,y*> in {<*x,y*>} by TARSKI:def 1;
{<*x,y*>} in {{<*x,y*>},{<*x,y*>,'&'}} by TARSKI:def 2;
then y <> [<*x,y*>,'&'] by A6, A8, A19, A20, XREGULAR:9;
then A21: not [<*x,y*>,'&'] in {y,c} by A3, TARSKI:def 2;
A22: x in {1,x} by TARSKI:def 2;
A23: {1,x} in {{1},{1,x}} by TARSKI:def 2;
<*x,y*> = <*x*> ^ <*y*> by FINSEQ_1:def 9;
then A24: <*x*> c= <*x,y*> by FINSEQ_6:10;
<*x*> = {[1,x]} by FINSEQ_1:def 5;
then A25: [1,x] in <*x*> by TARSKI:def 1;
A26: <*x,y*> in {<*x,y*>} by TARSKI:def 1;
{<*x,y*>} in {{<*x,y*>},{<*x,y*>,'&'}} by TARSKI:def 2;
then A27: x <> [<*x,y*>,'&'] by A22, A23, A24, A25, A26, XREGULAR:9;
A28: not c in {[<*x,y*>,'&'],[<*y,c*>,'&']} by A3, A17, TARSKI:def 2;
A29: not x in {[<*x,y*>,'&'],[<*y,c*>,'&']} by A1, A27, TARSKI:def 2;
A30: x in {2,x} by TARSKI:def 2;
A31: {2,x} in {{2},{2,x}} by TARSKI:def 2;
dom <*c,x*> = Seg 2 by FINSEQ_1:89;
then A32: 2 in dom <*c,x*> by FINSEQ_1:1;
<*c,x*> . 2 = x by FINSEQ_1:44;
then A33: [2,x] in <*c,x*> by A32, FUNCT_1:1;
A34: <*c,x*> in {<*c,x*>} by TARSKI:def 1;
{<*c,x*>} in {{<*c,x*>},{<*c,x*>,'&'}} by TARSKI:def 2;
then A35: x <> [<*c,x*>,'&'] by A30, A31, A33, A34, XREGULAR:9;
A36: c in {1,c} by TARSKI:def 2;
A37: {1,c} in {{1},{1,c}} by TARSKI:def 2;
<*c,x*> = <*c*> ^ <*x*> by FINSEQ_1:def 9;
then A38: <*c*> c= <*c,x*> by FINSEQ_6:10;
<*c*> = {[1,c]} by FINSEQ_1:def 5;
then A39: [1,c] in <*c*> by TARSKI:def 1;
A40: <*c,x*> in {<*c,x*>} by TARSKI:def 1;
{<*c,x*>} in {{<*c,x*>},{<*c,x*>,'&'}} by TARSKI:def 2;
then c <> [<*c,x*>,'&'] by A36, A37, A38, A39, A40, XREGULAR:9;
then A41: not [<*c,x*>,'&'] in {x,y,c} by A2, A35, ENUMSET1:def 1;
InputVertices (MajorityIStr (x,y,c)) = ((InputVertices ((1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&')))) \ (InnerVertices (1GateCircStr (<*c,x*>,'&')))) \/ ((InputVertices (1GateCircStr (<*c,x*>,'&'))) \ (InnerVertices ((1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&'))))) by CIRCCMB2:5, CIRCCOMB:47
.= ((((InputVertices (1GateCircStr (<*x,y*>,'&'))) \ (InnerVertices (1GateCircStr (<*y,c*>,'&')))) \/ ((InputVertices (1GateCircStr (<*y,c*>,'&'))) \ (InnerVertices (1GateCircStr (<*x,y*>,'&'))))) \ (InnerVertices (1GateCircStr (<*c,x*>,'&')))) \/ ((InputVertices (1GateCircStr (<*c,x*>,'&'))) \ (InnerVertices ((1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&'))))) by CIRCCMB2:5, CIRCCOMB:47
.= ((((InputVertices (1GateCircStr (<*x,y*>,'&'))) \ (InnerVertices (1GateCircStr (<*y,c*>,'&')))) \/ ((InputVertices (1GateCircStr (<*y,c*>,'&'))) \ (InnerVertices (1GateCircStr (<*x,y*>,'&'))))) \ (InnerVertices (1GateCircStr (<*c,x*>,'&')))) \/ ((InputVertices (1GateCircStr (<*c,x*>,'&'))) \ ((InnerVertices (1GateCircStr (<*x,y*>,'&'))) \/ (InnerVertices (1GateCircStr (<*y,c*>,'&'))))) by A4, CIRCCOMB:11
.= ((((InputVertices (1GateCircStr (<*x,y*>,'&'))) \ {[<*y,c*>,'&']}) \/ ((InputVertices (1GateCircStr (<*y,c*>,'&'))) \ (InnerVertices (1GateCircStr (<*x,y*>,'&'))))) \ (InnerVertices (1GateCircStr (<*c,x*>,'&')))) \/ ((InputVertices (1GateCircStr (<*c,x*>,'&'))) \ ((InnerVertices (1GateCircStr (<*x,y*>,'&'))) \/ (InnerVertices (1GateCircStr (<*y,c*>,'&'))))) by CIRCCOMB:42
.= ((((InputVertices (1GateCircStr (<*x,y*>,'&'))) \ {[<*y,c*>,'&']}) \/ ((InputVertices (1GateCircStr (<*y,c*>,'&'))) \ {[<*x,y*>,'&']})) \ (InnerVertices (1GateCircStr (<*c,x*>,'&')))) \/ ((InputVertices (1GateCircStr (<*c,x*>,'&'))) \ ((InnerVertices (1GateCircStr (<*x,y*>,'&'))) \/ (InnerVertices (1GateCircStr (<*y,c*>,'&'))))) by CIRCCOMB:42
.= ((((InputVertices (1GateCircStr (<*x,y*>,'&'))) \ {[<*y,c*>,'&']}) \/ ((InputVertices (1GateCircStr (<*y,c*>,'&'))) \ {[<*x,y*>,'&']})) \ {[<*c,x*>,'&']}) \/ ((InputVertices (1GateCircStr (<*c,x*>,'&'))) \ ((InnerVertices (1GateCircStr (<*x,y*>,'&'))) \/ (InnerVertices (1GateCircStr (<*y,c*>,'&'))))) by CIRCCOMB:42
.= ((((InputVertices (1GateCircStr (<*x,y*>,'&'))) \ {[<*y,c*>,'&']}) \/ ((InputVertices (1GateCircStr (<*y,c*>,'&'))) \ {[<*x,y*>,'&']})) \ {[<*c,x*>,'&']}) \/ ((InputVertices (1GateCircStr (<*c,x*>,'&'))) \ ({[<*x,y*>,'&']} \/ (InnerVertices (1GateCircStr (<*y,c*>,'&'))))) by CIRCCOMB:42
.= ((((InputVertices (1GateCircStr (<*x,y*>,'&'))) \ {[<*y,c*>,'&']}) \/ ((InputVertices (1GateCircStr (<*y,c*>,'&'))) \ {[<*x,y*>,'&']})) \ {[<*c,x*>,'&']}) \/ ((InputVertices (1GateCircStr (<*c,x*>,'&'))) \ ({[<*x,y*>,'&']} \/ {[<*y,c*>,'&']})) by CIRCCOMB:42
.= ((({x,y} \ {[<*y,c*>,'&']}) \/ ((InputVertices (1GateCircStr (<*y,c*>,'&'))) \ {[<*x,y*>,'&']})) \ {[<*c,x*>,'&']}) \/ ((InputVertices (1GateCircStr (<*c,x*>,'&'))) \ ({[<*x,y*>,'&']} \/ {[<*y,c*>,'&']})) by FACIRC_1:40
.= ((({x,y} \ {[<*y,c*>,'&']}) \/ ({y,c} \ {[<*x,y*>,'&']})) \ {[<*c,x*>,'&']}) \/ ((InputVertices (1GateCircStr (<*c,x*>,'&'))) \ ({[<*x,y*>,'&']} \/ {[<*y,c*>,'&']})) by FACIRC_1:40
.= ((({x,y} \ {[<*y,c*>,'&']}) \/ ({y,c} \ {[<*x,y*>,'&']})) \ {[<*c,x*>,'&']}) \/ ({c,x} \ ({[<*x,y*>,'&']} \/ {[<*y,c*>,'&']})) by FACIRC_1:40
.= ((({x,y} \ {[<*y,c*>,'&']}) \/ ({y,c} \ {[<*x,y*>,'&']})) \ {[<*c,x*>,'&']}) \/ ({c,x} \ {[<*x,y*>,'&'],[<*y,c*>,'&']}) by ENUMSET1:1
.= (({x,y} \/ ({y,c} \ {[<*x,y*>,'&']})) \ {[<*c,x*>,'&']}) \/ ({c,x} \ {[<*x,y*>,'&'],[<*y,c*>,'&']}) by A1, A13, Th1
.= (({x,y} \/ {y,c}) \ {[<*c,x*>,'&']}) \/ ({c,x} \ {[<*x,y*>,'&'],[<*y,c*>,'&']}) by A21, ZFMISC_1:57
.= (({x,y} \/ {y,c}) \ {[<*c,x*>,'&']}) \/ {c,x} by A28, A29, ZFMISC_1:63
.= ({x,y,y,c} \ {[<*c,x*>,'&']}) \/ {c,x} by ENUMSET1:5
.= ({y,y,x,c} \ {[<*c,x*>,'&']}) \/ {c,x} by ENUMSET1:67
.= ({y,x,c} \ {[<*c,x*>,'&']}) \/ {c,x} by ENUMSET1:31
.= ({x,y,c} \ {[<*c,x*>,'&']}) \/ {c,x} by ENUMSET1:58
.= {x,y,c} \/ {c,x} by A41, ZFMISC_1:57
.= {x,y,c,c,x} by ENUMSET1:9
.= {x,y,c,c} \/ {x} by ENUMSET1:10
.= {c,c,x,y} \/ {x} by ENUMSET1:73
.= {c,x,y} \/ {x} by ENUMSET1:31
.= {c,x,y,x} by ENUMSET1:6
.= {x,x,y,c} by ENUMSET1:70
.= {x,y,c} by ENUMSET1:31 ;
hence InputVertices (MajorityIStr (x,y,c)) = {x,y,c} ; :: thesis: verum