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. eapply in_map_iff. 1:eexists; repeat split. 2:in_collect psi... 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 t) as [m2], (el_T phi) as [m3]. exists (1 + m1 + m2 + m3). cbn. in_app 6. in_collect (phi, t)... + destruct IHprv1 as [m1], IHprv2 as [m2], (el_T phi) as [m4], (el_T psi) as [m5]. exists (1 + m1 + m2 + m4 + m5). cbn. in_app 7. cbn. in_collect (phi, psi)... + destruct IHprv as [m1], (el_T phi) as [m2]. exists (1 + m1 + m2). cbn. in_app 8. in_collect phi... + now exists 0. + destruct IHprv1 as [m1], IHprv2 as [m2]. exists (1 + m1 + m2). cbn. in_app 10. in_collect (phi, psi)... + destruct IHprv as [m1], (el_T phi) as [m2], (el_T psi) as [m3]. exists (1 + m1 + m2 + m3). cbn. in_app 11. in_collect (phi, psi)... + destruct IHprv as [m1], (el_T phi) as [m2], (el_T psi) as [m3]. exists (1 + m1 + m2 + m3). cbn. in_app 12. in_collect (phi, psi)... + destruct IHprv as [m1], (el_T phi) as [m2], (el_T psi) as [m3]. exists (1 + m1 + m2 + m3). cbn. in_app 13. in_collect (phi, psi)... + destruct IHprv as [m1], (el_T phi) as [m2], (el_T psi) as [m3]. exists (1 + m1 + m2 + m3). cbn. in_app 14. in_collect (phi, psi)... + destruct IHprv1 as [m1], IHprv2 as [m2], IHprv3 as [m3], (el_T phi) as [m4], (el_T psi) as [m5], (el_T theta) as [m6]. exists (1 + m1 + m2 + m3 + m4 + m5 + m6). cbn. in_app 15. cbn. in_collect (phi, (psi, theta))... + destruct (el_T phi) as [m1], (el_T psi) as [m2]. exists (1 + m1 + m2). cbn. in_app 9. in_collect (phi, psi)... - intros [m]; induction m in A, x, H |-*; cbn in *. + now apply Ctx. + invert_list_in. * now eapply IHm. * eapply II; eapply IHm; eauto. * eapply IE; eapply IHm; eauto. * eapply AllI; eapply IHm; eauto. * eapply AllE; eapply IHm; eauto. * eapply ExI; eapply IHm; eauto. * eapply ExE; eapply IHm; destruct a; eauto. * destruct b; invert_list_in. eapply Exp; eapply IHm; eauto. * destruct p; invert_list_in. eapply Pc. * eapply CI; eapply IHm; eauto. * eapply CE1; eapply IHm; eauto. * eapply CE2; eapply IHm; eauto. * eapply DI1; eapply IHm; eauto. * eapply DI2; eapply IHm; eauto. * destruct a; invert_list_in. destruct H4. eapply DE; eapply IHm; eauto. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(FOL.Syntax.Facts FOL.Syntax.Theories) Undecidability(Shared.ListAutomation) Lia