proposition: Lemma Representable2Expressible : forall (n : nat) (R : naryRel n) (A : Formula), Representable n (charFunction n R) A -> Expressible n R (substF A 0 (natToTerm 1)).
proof: Proof. intros n R A [H H0]; split. - intros v H1; induction (freeVarSubFormula3 _ _ _ _ _ H1). split. + apply H. eapply in_remove. apply H2. + eapply in_remove_neq. apply H2. + elim H2. - clear H. generalize H0 as H. generalize A; clear H0 A. induction n as [| n Hrecn]; intros. + simpl in H |- *. induction R. * simpl in H. apply impE with (substF (v#0 = Succ Zero)%fol 0 (Succ Zero)). -- apply iffE2. rewrite <- (subFormulaIff LNN). apply forallE. apply forallI. ++ apply closedT. ++ apply H. -- rewrite (subFormulaEqual LNN). simpl in |- *. apply eqRefl. * simpl in H. apply impE with (~ (substF (v#0 = Zero) 0 (Succ Zero)))%fol. -- apply cp2. apply iffE1. rewrite <- (subFormulaIff LNN). apply forallE. apply forallI. ++ apply closedT. ++ apply H. -- rewrite (subFormulaEqual LNN); simpl in |- *. replace (apply LNN Languages.Zero_ (Tnil)) with (natToTerm 0) by reflexivity. replace (Succ Zero) with (natToTerm 1) by reflexivity. simpl; apply nn1. + simpl in H |- *. intros a; apply expressibleAlternate with (substF (substF A (S n) (natToTerm a)) 0 (Succ Zero)). * apply (subFormulaExch LNN). -- discriminate. -- apply closedNatToTerm. -- auto. * apply Hrecn; apply H. Qed.
imports: Coq(Arith List) hydras.Ackermann(ListExt folProp subProp extEqualNat Languages LNN NewNotations)