fact: Definition env_contains_PA2 (rho rho' : env D) xO xS xA xEq := (forall n, get_indi rho n = get_indi rho' n) /\ (forall n ar, get_func rho' n ar = match ar with | 0 => insert xO (fun n => get_func rho n 0) (@i_f _ _ D I Zero) n | 1 => insert xS (fun n => get_func rho n 1) (@i_f _ _ D I Succ) n | 2 => insert xA (insert xA (fun n => get_func rho n 2) (@i_f _ _ D I Mult)) (@i_f _ _ D I Plus) n | ar => get_func rho n ar end) /\ (forall n ar, get_pred rho' n ar = match ar with | 2 => insert xEq (fun n => get_pred rho n 2) (@i_P _ _ D I Eq) n | ar => get_pred rho n ar end).
imports: PeanoNat Lia Vector Undecidability.SOL(SOL PA2) Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax Subst Tarski) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.Shared.Dec