[2/3] Main Proof That n : Nat then f ? n is decidable FVal FVar [0/4] FOp (Splitting of Cases) |+| |*| |&| |^| [2/3] Solve Above That for any n : Nat exists y . (f ? y , y >= n) FVal Simple case (decide on gte) FVar Trivial case (just y = x) [0/4] FOp Firstly, we assume that f, g are formulas, and f ? x, g ? y are always decidable |+| |*| |&| |^|