deffunc H1( set ) -> non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign = F1($1);
A7:
for n being Nat
for S being non empty ManySortedSign
for x being set st S = H1(n) & x = F2() . n holds
( H1(n + 1) = S +* F3(x,n) & F2() . (n + 1) = F4(x,n) & x in InputVertices F3(x,n) & F4(x,n) in InnerVertices F3(x,n) )
by A6;
let n be Nat; ( InputVertices F1((n + 1)) = (InputVertices F1(n)) \/ ((InputVertices F3((F2() . n),n)) \ {(F2() . n)}) & InnerVertices F1(n) is Relation & InputVertices F1(n) is without_pairs )
A8:
for n being Nat
for x being set st x = F2() . n holds
(InputVertices F3(x,n)) \ {x} is without_pairs
by A5;
A9:
( H1( 0 ) = H1( 0 ) & F2() . 0 in InnerVertices H1( 0 ) )
by A3;
A10:
for n being Nat
for x being set holds InnerVertices F3(x,n) is Relation
by A4;
for n being Nat ex S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st
( S1 = H1(n) & S2 = H1(n + 1) & InputVertices S2 = (InputVertices S1) \/ ((InputVertices F3((F2() . n),n)) \ {(F2() . n)}) & InnerVertices S1 is Relation & InputVertices S1 is without_pairs )
from CIRCCMB2:sch 10(A1, A2, A9, A10, A8, A7);
then
ex S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st
( S1 = F1(n) & S2 = F1((n + 1)) & InputVertices S2 = (InputVertices S1) \/ ((InputVertices F3((F2() . n),n)) \ {(F2() . n)}) & InnerVertices S1 is Relation & InputVertices S1 is without_pairs )
;
hence
( InputVertices F1((n + 1)) = (InputVertices F1(n)) \/ ((InputVertices F3((F2() . n),n)) \ {(F2() . n)}) & InnerVertices F1(n) is Relation & InputVertices F1(n) is without_pairs )
; verum