let x, y, c be set ; ( 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*>,'&' ]
; InputVertices (MajorityIStr x,y,c) = {x,y,c}
A4:
1GateCircStr <*x,y*>,'&' tolerates 1GateCircStr <*y,c*>,'&'
by CIRCCOMB:55;
A5:
y in {1,y}
by TARSKI:def 2;
A6:
y in {2,y}
by TARSKI:def 2;
A7:
{1,y} in [1,y]
by TARSKI:def 2;
A8:
{2,y} in [2,y]
by TARSKI:def 2;
<*y,c*> = <*y*> ^ <*c*>
by FINSEQ_1:def 9;
then A9:
<*y*> c= <*y,c*>
by FINSEQ_6:12;
<*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*>,'&' ]
by TARSKI:def 2;
then A13:
y <> [<*y,c*>,'&' ]
by A5, A7, A9, A10, A11, ORDINAL1:5;
A14:
c in {2,c}
by TARSKI:def 2;
A15:
{2,c} in [2,c]
by TARSKI:def 2;
dom <*y,c*> = Seg 2
by FINSEQ_1:110;
then A18:
2 in dom <*y,c*>
by FINSEQ_1:3;
<*y,c*> . 2 = c
by FINSEQ_1:61;
then
[2,c] in <*y,c*>
by A18, FUNCT_1:8;
then A19:
c <> [<*y,c*>,'&' ]
by A11, A12, A14, A15, ORDINAL1:5;
dom <*x,y*> = Seg 2
by FINSEQ_1:110;
then A22:
2 in dom <*x,y*>
by FINSEQ_1:3;
<*x,y*> . 2 = y
by FINSEQ_1:61;
then A23:
[2,y] in <*x,y*>
by A22, FUNCT_1:8;
A24:
<*x,y*> in {<*x,y*>}
by TARSKI:def 1;
{<*x,y*>} in [<*x,y*>,'&' ]
by TARSKI:def 2;
then
y <> [<*x,y*>,'&' ]
by A6, A8, A23, A24, ORDINAL1:5;
then A25:
not [<*x,y*>,'&' ] in {y,c}
by A3, TARSKI:def 2;
A26:
x in {1,x}
by TARSKI:def 2;
A27:
{1,x} in [1,x]
by TARSKI:def 2;
<*x,y*> = <*x*> ^ <*y*>
by FINSEQ_1:def 9;
then A28:
<*x*> c= <*x,y*>
by FINSEQ_6:12;
<*x*> = {[1,x]}
by FINSEQ_1:def 5;
then A29:
[1,x] in <*x*>
by TARSKI:def 1;
A30:
<*x,y*> in {<*x,y*>}
by TARSKI:def 1;
{<*x,y*>} in [<*x,y*>,'&' ]
by TARSKI:def 2;
then A31:
x <> [<*x,y*>,'&' ]
by A26, A27, A28, A29, A30, ORDINAL1:5;
A32:
not c in {[<*x,y*>,'&' ],[<*y,c*>,'&' ]}
by A3, A19, TARSKI:def 2;
A33:
not x in {[<*x,y*>,'&' ],[<*y,c*>,'&' ]}
by A1, A31, TARSKI:def 2;
A34:
x in {2,x}
by TARSKI:def 2;
A35:
{2,x} in [2,x]
by TARSKI:def 2;
dom <*c,x*> = Seg 2
by FINSEQ_1:110;
then A38:
2 in dom <*c,x*>
by FINSEQ_1:3;
<*c,x*> . 2 = x
by FINSEQ_1:61;
then A39:
[2,x] in <*c,x*>
by A38, FUNCT_1:8;
A40:
<*c,x*> in {<*c,x*>}
by TARSKI:def 1;
{<*c,x*>} in [<*c,x*>,'&' ]
by TARSKI:def 2;
then A41:
x <> [<*c,x*>,'&' ]
by A34, A35, A39, A40, ORDINAL1:5;
A42:
c in {1,c}
by TARSKI:def 2;
A43:
{1,c} in [1,c]
by TARSKI:def 2;
<*c,x*> = <*c*> ^ <*x*>
by FINSEQ_1:def 9;
then A44:
<*c*> c= <*c,x*>
by FINSEQ_6:12;
<*c*> = {[1,c]}
by FINSEQ_1:def 5;
then A45:
[1,c] in <*c*>
by TARSKI:def 1;
A46:
<*c,x*> in {<*c,x*>}
by TARSKI:def 1;
{<*c,x*>} in [<*c,x*>,'&' ]
by TARSKI:def 2;
then
c <> [<*c,x*>,'&' ]
by A42, A43, A44, A45, A46, ORDINAL1:5;
then A47:
not [<*c,x*>,'&' ] in {x,y,c}
by A2, A41, 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:6, CIRCCOMB:55
.=
((((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:6, CIRCCOMB:55
.=
((((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:15
.=
((((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:49
.=
((((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:49
.=
((((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:49
.=
((((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:49
.=
((((InputVertices (1GateCircStr <*x,y*>,'&' )) \ {[<*y,c*>,'&' ]}) \/ ((InputVertices (1GateCircStr <*y,c*>,'&' )) \ {[<*x,y*>,'&' ]})) \ {[<*c,x*>,'&' ]}) \/ ((InputVertices (1GateCircStr <*c,x*>,'&' )) \ ({[<*x,y*>,'&' ]} \/ {[<*y,c*>,'&' ]}))
by CIRCCOMB:49
.=
((({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:41
.=
(({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 A25, ZFMISC_1:65
.=
(({x,y} \/ {y,c}) \ {[<*c,x*>,'&' ]}) \/ {c,x}
by A32, A33, ZFMISC_1:72
.=
({x,y,y,c} \ {[<*c,x*>,'&' ]}) \/ {c,x}
by ENUMSET1:45
.=
({y,y,x,c} \ {[<*c,x*>,'&' ]}) \/ {c,x}
by ENUMSET1:110
.=
({y,x,c} \ {[<*c,x*>,'&' ]}) \/ {c,x}
by ENUMSET1:71
.=
({x,y,c} \ {[<*c,x*>,'&' ]}) \/ {c,x}
by ENUMSET1:99
.=
{x,y,c} \/ {c,x}
by A47, ZFMISC_1:65
.=
{x,y,c,c,x}
by ENUMSET1:49
.=
{x,y,c,c} \/ {x}
by ENUMSET1:50
.=
{c,c,x,y} \/ {x}
by ENUMSET1:118
.=
{c,x,y} \/ {x}
by ENUMSET1:71
.=
{c,x,y,x}
by ENUMSET1:46
.=
{x,x,y,c}
by ENUMSET1:113
.=
{x,y,c}
by ENUMSET1:71
;
hence
InputVertices (MajorityIStr x,y,c) = {x,y,c}
; verum