let x, y, c be set ; for s being State of (BorrowICirc (x,y,c))
for a, b being Element of BOOLEAN st a = s . x & b = s . y holds
(Following s) . [<*x,y*>,and2a] = ('not' a) '&' b
set xy = <*x,y*>;
set yc = <*y,c*>;
set xc = <*x,c*>;
set S1 = 1GateCircStr (<*x,y*>,and2a);
set A1 = 1GateCircuit (x,y,and2a);
set S2 = 1GateCircStr (<*y,c*>,and2);
set A2 = 1GateCircuit (y,c,and2);
set S3 = 1GateCircStr (<*x,c*>,and2a);
set A3 = 1GateCircuit (x,c,and2a);
set S = BorrowIStr (x,y,c);
set A = BorrowICirc (x,y,c);
set v1 = [<*x,y*>,and2a];
let s be State of (BorrowICirc (x,y,c)); for a, b being Element of BOOLEAN st a = s . x & b = s . y holds
(Following s) . [<*x,y*>,and2a] = ('not' a) '&' b
let a, b be Element of BOOLEAN ; ( a = s . x & b = s . y implies (Following s) . [<*x,y*>,and2a] = ('not' a) '&' b )
assume A1:
( a = s . x & b = s . y )
; (Following s) . [<*x,y*>,and2a] = ('not' a) '&' b
reconsider xx = x, yy = y as Vertex of (1GateCircStr (<*x,y*>,and2a)) by FACIRC_1:43;
reconsider v1 = [<*x,y*>,and2a] as Element of InnerVertices (1GateCircStr (<*x,y*>,and2a)) by FACIRC_1:47;
A2:
BorrowIStr (x,y,c) = (1GateCircStr (<*x,y*>,and2a)) +* ((1GateCircStr (<*y,c*>,and2)) +* (1GateCircStr (<*x,c*>,and2a)))
by CIRCCOMB:6;
then reconsider v = v1 as Element of InnerVertices (BorrowIStr (x,y,c)) by FACIRC_1:21;
A3:
BorrowICirc (x,y,c) = (1GateCircuit (x,y,and2a)) +* ((1GateCircuit (y,c,and2)) +* (1GateCircuit (x,c,and2a)))
by FACIRC_1:25;
then reconsider s1 = s | the carrier of (1GateCircStr (<*x,y*>,and2a)) as State of (1GateCircuit (x,y,and2a)) by FACIRC_1:26;
reconsider xx = xx, yy = yy as Vertex of (BorrowIStr (x,y,c)) by A2, FACIRC_1:20;
A4:
dom s1 = the carrier of (1GateCircStr (<*x,y*>,and2a))
by CIRCUIT1:3;
thus (Following s) . [<*x,y*>,and2a] =
(Following s1) . v
by A2, A3, CIRCCOMB:64
.=
and2a . <*(s1 . xx),(s1 . yy)*>
by FACIRC_1:50
.=
and2a . <*(s . xx),(s1 . yy)*>
by A4, FUNCT_1:47
.=
and2a . <*(s . xx),(s . yy)*>
by A4, FUNCT_1:47
.=
('not' a) '&' b
by A1, TWOSCOMP:def 2
; verum