let x, y, c be set ; for s being State of (BorrowCirc (x,y,c))
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
( (Following s) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following s) . [<*y,c*>,and2] = a2 '&' a3 & (Following s) . [<*x,c*>,and2a] = ('not' a1) '&' a3 )
let s be State of (BorrowCirc (x,y,c)); for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
( (Following s) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following s) . [<*y,c*>,and2] = a2 '&' a3 & (Following s) . [<*x,c*>,and2a] = ('not' a1) '&' a3 )
let a1, a2, a3 be Element of BOOLEAN ; ( a1 = s . x & a2 = s . y & a3 = s . c implies ( (Following s) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following s) . [<*y,c*>,and2] = a2 '&' a3 & (Following s) . [<*x,c*>,and2a] = ('not' a1) '&' a3 ) )
assume that
A1:
a1 = s . x
and
A2:
a2 = s . y
and
A3:
a3 = s . c
; ( (Following s) . [<*x,y*>,and2a] = ('not' a1) '&' a2 & (Following s) . [<*y,c*>,and2] = a2 '&' a3 & (Following s) . [<*x,c*>,and2a] = ('not' a1) '&' a3 )
set S = BorrowStr (x,y,c);
A4:
InnerVertices (BorrowStr (x,y,c)) = the carrier' of (BorrowStr (x,y,c))
by FACIRC_1:37;
A5:
dom s = the carrier of (BorrowStr (x,y,c))
by CIRCUIT1:3;
A6:
x in the carrier of (BorrowStr (x,y,c))
by FSCIRC_1:6;
A7:
y in the carrier of (BorrowStr (x,y,c))
by FSCIRC_1:6;
A8:
c in the carrier of (BorrowStr (x,y,c))
by FSCIRC_1:6;
[<*x,y*>,and2a] in InnerVertices (BorrowStr (x,y,c))
by FSCIRC_1:7;
hence (Following s) . [<*x,y*>,and2a] =
and2a . (s * <*x,y*>)
by A4, FACIRC_1:35
.=
and2a . <*a1,a2*>
by A1, A2, A5, A6, A7, FINSEQ_2:125
.=
('not' a1) '&' a2
by TWOSCOMP:def 2
;
( (Following s) . [<*y,c*>,and2] = a2 '&' a3 & (Following s) . [<*x,c*>,and2a] = ('not' a1) '&' a3 )
[<*y,c*>,and2] in InnerVertices (BorrowStr (x,y,c))
by FSCIRC_1:7;
hence (Following s) . [<*y,c*>,and2] =
and2 . (s * <*y,c*>)
by A4, FACIRC_1:35
.=
and2 . <*a2,a3*>
by A2, A3, A5, A7, A8, FINSEQ_2:125
.=
a2 '&' a3
by FACIRC_1:def 6
;
(Following s) . [<*x,c*>,and2a] = ('not' a1) '&' a3
[<*x,c*>,and2a] in InnerVertices (BorrowStr (x,y,c))
by FSCIRC_1:7;
hence (Following s) . [<*x,c*>,and2a] =
and2a . (s * <*x,c*>)
by A4, FACIRC_1:35
.=
and2a . <*a1,a3*>
by A1, A3, A5, A6, A8, FINSEQ_2:125
.=
('not' a1) '&' a3
by TWOSCOMP:def 2
;
verum