proposition: Lemma decode_nat_app_depth_r xs s : decode_nat xs s (app_depth_r (flatten (closure xs s))).
proof: Proof. move E: (closure xs s) => y. elim /(induction_ltof1 _ eterm_size) : y xs s E. rewrite /ltof. move=> [xs [n|s t|s]] IH ?? [-> ->]. - move: xs IH => [|x xs]. + move=> ?. rewrite flatten_term. by apply: decode_nat_var. + move: n => [|n]. * move: x => [xs' x'] IH. apply: decode_nat_var0. rewrite flatten_var. apply: IH; [|done]. rewrite /=. lia. * move=> IH. apply: decode_nat_varS. rewrite app_depth_r_var_S. apply: IH; [|done]. rewrite /=. lia. - rewrite flatten_app /=. apply: decode_nat_app. apply: IH; [|done]. rewrite /=. lia. - apply: decode_nat_lam. rewrite app_depth_r_lam. apply: IH; [|done]. rewrite /=. lia. Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA L.L) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss Code.subcode) Undecidability(MinskyMachines.Util.MMA_pairing L.AbstractMachines.wCBV) PeanoNat List Lia Wf_nat ssreflect ssrbool ssrfun