proposition: Lemma PAdec : forall x : Formula, decidable (In _ PA x).
proof: Proof. intros x. unfold PA in |- *. induction (formula_eqdec LNT LNT_eqdec x PA6). - rewrite a; left; right; constructor. - induction (formula_eqdec LNT LNT_eqdec x PA5). + rewrite a; left; left; right; constructor. + induction (formula_eqdec LNT LNT_eqdec x PA4). * rewrite a; left; do 2 left; right; constructor. * induction (formula_eqdec LNT LNT_eqdec x PA3). -- rewrite a; left; do 3 left; right; constructor. -- induction (formula_eqdec LNT LNT_eqdec x PA2). ++ rewrite a; left; do 4 left; right; constructor. ++ induction (formula_eqdec LNT LNT_eqdec x PA1). ** rewrite a; left; do 5 left; right; constructor. ** cut (In Formula InductionSchema x \/ ~ In Formula InductionSchema x). { intros [H| H]. - left; do 6 left; assumption. - right; intro H0. repeat tauto || induction H0. } clear b b0 b1 b2 b3 b4. assert (H: forall y : Formula, (decidable (exists (f : Formula) (v : nat), (substF f v Zero -> (allH v, f -> substF f v (Succ v#v)) -> allH v, f)%nt = y))). { intros y; destruct y as [t t0| r t| f f0| f| n f]; try (right; unfold not in |- *; intros; decompose record H; discriminate ). destruct f0 as [t t0| r t| f0 f1| f0| n f0]; try (right; unfold not in |- *; intros; decompose record H; discriminate). destruct f0 as [t t0| r t| f0 f2| f0| n f0]; try (right; unfold not in |- *; intros; decompose record H; discriminate). destruct f1 as [t t0| r t| f1 f2| f1| n0 f1]; try (right; unfold not in |- *; intros; decompose record H; discriminate). destruct (formula_eqdec LNT LNT_eqdec (substF f1 n0 Zero) f) as [a | b]. - rewrite <- a; clear a f. destruct f0 as [t t0| r t| f f0| f| n1 f]; try (right; unfold not in |- *; intros; decompose record H; discriminate). induction (formula_eqdec LNT LNT_eqdec f1 f) as [a | b]. + rewrite <- a; clear a f. induction (formula_eqdec LNT LNT_eqdec (substF f1 n0 (Succ (v#n0))%nt) f0). * rewrite <- a; clear a f0. induction (eq_nat_dec n n0) as [a | b]. -- rewrite a; left. exists f1. exists n0. reflexivity. -- right; unfold not in |- *; intros; apply b; decompose record H /r. intros H x0 x1 H1; inversion H1; auto. * right; unfold not in |- *; intros; apply b; decompose record H /r. intros H x0 x1 H1; inversion H1; reflexivity. + right; unfold not in |- *; intros; apply b; decompose record H /r. intros H x0 x1 H1; inversion H1; auto. - right; unfold not in |- *; intros; apply b; decompose record H /r. intros H x0 x1 H1; inversion H1; auto. } induction (formula_eqdec LNT LNT_eqdec x (close LNT (open x))) as [a | b]. --- induction (H (open x)). left. unfold In, InductionSchema, PA7 in |- *. decompose record H0 /r. intros x0 x1 H2; exists x0, x1; now rewrite H2. right. intros H1; apply H0. unfold In, InductionSchema, PA7 in H1. decompose record H1 /r. intros x0 x1 H3; exists x0, x1; rewrite H3. unfold close. induction (List.nodup eq_nat_dec (freeVarF (substF x0 x1 Zero -> (allH x1, x0 -> substF x0 x1 (Succ (v#x1))) -> allH x1, x0)%nt)). simpl; reflexivity. simpl; assumption. --- right; intros H0; apply b. unfold In, InductionSchema, PA7 in H0. decompose record H0 /r. intros x0 x1 H2; rewrite H2. replace (open (close LNT (substF x0 x1 Zero -> (allH x1, x0 -> substF x0 x1 (Succ v#x1)) -> allH x1, x0)%nt)) with (substF x0 x1 Zero -> (allH x1, x0 -> substF x0 x1 (Succ v#x1)) -> allH x1, x0)%nt; [reflexivity |]. unfold close in |- *. induction (List.nodup eq_nat_dec (freeVarF (substF x0 x1 Zero -> (allH x1, x0 -> substF x0 x1 (Succ (v#x1))) -> (allH x1, x0)))%nt). simpl; reflexivity. simpl; auto. Qed.
imports: Coq(Arith Lia Ensembles Decidable) hydras.Ackermann(folProp subAll folLogic3) hydras.Ackermann(NewNotations)