proposition: Lemma enum_prv {p : peirce} {b : falsity_flag} A : list_enumerator (L_ded A) (prv A).
proof: Proof. Proof with try (eapply cum_ge'; eauto; lia). split. - rename x into phi. induction 1; try congruence; subst. + destruct IHprv as [m1], (el_T phi) as [m2]. exists (1 + m1 + m2). cbn. in_app 2. eapply in_concat. eexists. split. 1: eapply in_map. 2: eapply in_map. 1:idtac... idtac... + destruct IHprv1 as [m1], IHprv2 as [m2], (el_T psi) as [m3]; eauto. exists (1 + m1 + m2 + m3). cbn. in_app 3. in_collect (phi, psi)... + destruct IHprv as [m]. exists (1 + m). cbn. in_app 4. in_collect phi... + destruct IHprv as [m1], (el_T t) as [m2], (el_T phi) as [m3]. exists (1 + m1 + m2 + m3). cbn. in_app 5. in_collect (phi, t)... + destruct IHprv as [m1], (el_T phi) as [m2]. exists (1 + m1 + m2). cbn. in_app 6. in_collect phi... + now exists 0. + destruct (el_T phi) as [m1], (el_T psi) as [m2]. exists (1 + m1 + m2). cbn. in_app 7. in_collect (phi, psi)... - intros [m H]; induction m in A, x, H |-*; cbn in *. + now apply Ctx. + repeat invert_list_in. * eauto. * eapply II; eauto. * eapply IE; eapply IHm; eauto. * eapply AllI; eapply IHm; eauto. * eapply AllE; eapply IHm; eauto. * destruct b; repeat invert_list_in. eapply Exp, IHm; eauto. * destruct p; repeat invert_list_in. eapply Pc. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.FOL(Syntax.Facts Syntax.Theories Syntax.Asimpl) Undecidability(Shared.ListAutomation) Lia EqdepFacts