proposition: Theorem dio_rel_fall_lt a (R : nat -> (nat -> nat) -> Prop) : 𝔻F a -> 𝔻R (fun ν => R (ν 0) ν⭳) -> 𝔻R (fun ν => forall x, x < a ν -> R x ν).
proof: Proof. intros Ha H. by dio equiv (fun ν => exists y, y = a ν /\ forall x, x < y -> R x ν). + abstract(intros v; split; [ exists (a v); auto | intros (? & -> & ?); auto ]). + set (T v := R (v 0) v⭳⭳). by dio equiv (fun v => forall x, x < v 0 -> T (x·v)). * abstract (intros v; unfold T; simpl; tauto). * apply dio_rel_bounded_fall; unfold T; simpl. revert H; apply dio_rel_ren with (ρ := fun n => match n with 0 => 0 | S n => S (S n) end). Defined.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list sums bounded_quantification) Undecidability.H10.Matija(cipher) Undecidability.H10.Dio(dio_logic dio_cipher dio_elem)