fact: Fixpoint bounded_func ar n (phi : form) := match phi with | atom _ v => Forall (bounded_func_term ar n) v | fal => True | bin _ phi psi => bounded_func ar n phi /\ bounded_func ar n psi | quant_indi _ phi => bounded_func ar n phi | quant_func _ ar' phi => (ar = ar' /\ bounded_func ar (S n) phi) \/ (ar <> ar' /\ bounded_func ar n phi) | quant_pred _ _ phi => bounded_func ar n phi end.
imports: Undecidability.SOL.SOL Undecidability.Shared.Dec Undecidability.Shared.Libs.PSL(Vectors) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) EqdepFacts Eqdep_dec