defpred S1[ Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)), Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))] means for i being Nat st i in Seg 4 holds
ex xi being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( xi = $1 . i & $2 . i = Op-Shift (xi,(i - 1)) );
A1: for x being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ex z being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st S1[x,z]
proof
let x be Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)); :: thesis: ex z being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st S1[x,z]
x in 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
then Q01: ex s being Element of (4 -tuples_on (8 -tuples_on BOOLEAN)) * st
( x = s & len s = 4 ) ;
defpred S2[ Nat, set ] means ex xk being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( xk = x . $1 & $2 = Op-Shift (xk,($1 - 1)) );
Q1: for k being Nat st k in Seg 4 holds
ex zk being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st S2[k,zk]
proof
let k be Nat; :: thesis: ( k in Seg 4 implies ex zk being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st S2[k,zk] )
assume k in Seg 4 ; :: thesis: ex zk being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st S2[k,zk]
then k in dom x by Q01, FINSEQ_1:def 3;
then Q11: x . k in rng x by FUNCT_1:3;
then x . k in 4 -tuples_on (8 -tuples_on BOOLEAN) ;
then Q13: ex s being Element of (8 -tuples_on BOOLEAN) * st
( x . k = s & len s = 4 ) ;
then reconsider xk = x . k as Element of (8 -tuples_on BOOLEAN) * ;
reconsider xk1 = xk as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) by Q11;
reconsider zk = Op-Shift (xk,(k - 1)) as FinSequence of 8 -tuples_on BOOLEAN ;
Q15: len zk = 4 by Q13, DESCIP_1:def 3;
reconsider zk = zk as Element of (8 -tuples_on BOOLEAN) * by FINSEQ_1:def 11;
zk in 4 -tuples_on (8 -tuples_on BOOLEAN) by Q15;
then reconsider zk = zk as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) ;
ex xk being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( xk = x . k & zk = Op-Shift (xk1,(k - 1)) ) ;
hence ex zk being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st S2[k,zk] ; :: thesis: verum
end;
consider z being FinSequence of 4 -tuples_on (8 -tuples_on BOOLEAN) such that
Q2: ( dom z = Seg 4 & ( for i being Nat st i in Seg 4 holds
S2[i,z . i] ) ) from FINSEQ_1:sch 5(Q1);
 Q3: len z = 4 by Q2, FINSEQ_1:def 3;
reconsider z = z as Element of (4 -tuples_on (8 -tuples_on BOOLEAN)) * by FINSEQ_1:def 11;
z in 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) by Q3;
hence ex z being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st S1[x,z] by Q2; :: thesis: verum
end;
consider I being Function of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) such that
A2: for x being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds S1[x,I . x] from FUNCT_2:sch 3(A1);
 take I ; :: thesis: for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for i being Nat st i in Seg 4 holds
ex xi being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( xi = input . i & (I . input) . i = Op-Shift (xi,(i - 1)) )
thus for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for i being Nat st i in Seg 4 holds
ex xi being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( xi = input . i & (I . input) . i = Op-Shift (xi,(i - 1)) ) by A2; :: thesis: verum