let f be set ; :: thesis: for p, q being FinSequence holds 1GateCircStr (p,f) tolerates 1GateCircStr (q,f)
let p, q be FinSequence; :: thesis: 1GateCircStr (p,f) tolerates 1GateCircStr (q,f)
set S1 = 1GateCircStr (p,f);
set S2 = 1GateCircStr (q,f);
A1: ( [p,f] <> [q,f] implies {[p,f]} misses {[q,f]} ) by ZFMISC_1:11;
A2: the Arity of (1GateCircStr (q,f)) = (q,f) .--> q by Th40;
the Arity of (1GateCircStr (p,f)) = (p,f) .--> p by Th40;
hence the Arity of (1GateCircStr (p,f)) tolerates the Arity of (1GateCircStr (q,f)) by A2, A1, XTUPLE_0:1; :: according to CIRCCOMB:def 1 :: thesis: the ResultSort of (1GateCircStr (p,f)) tolerates the ResultSort of (1GateCircStr (q,f))
A3: the ResultSort of (1GateCircStr (q,f)) = (q,f) .--> [q,f] by Th40;
the ResultSort of (1GateCircStr (p,f)) = (p,f) .--> [p,f] by Th40;
hence the ResultSort of (1GateCircStr (p,f)) tolerates the ResultSort of (1GateCircStr (q,f)) by A3, A1; :: thesis: verum