proposition: Theorem dio_fun_expo q r : 𝔻F q -> 𝔻F r -> 𝔻F (fun ν => expo (r ν) (q ν)).
proof: Proof. dio by lemma (fun v => expo_diophantine (v 0) (q v⭳) (r v⭳)). Defined.
imports: Arith ZArith List Undecidability.Shared.Libs.DLW.Utils(utils_tac sums rel_iter gcd) Undecidability.H10.Matija(alpha expo_diophantine) Undecidability.H10.Dio(dio_logic)