proposition: Theorem dio_rel_seqs_of_ones l q u u1 : 𝔻F l -> 𝔻F q -> 𝔻F u -> 𝔻F u1 -> 𝔻R (fun v => seqs_of_ones (l v) (q v) (u v) (u1 v)).
proof: Proof. dio by lemma (fun v => seqs_of_ones_dio (l v) (q v) (u v) (u1 v)). Defined.
imports: Arith List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums bool_nat) Undecidability.H10.Matija(cipher) Undecidability.H10.Dio(dio_logic dio_expo dio_binary)