# Re: [tlaplus] Arity of NEW operator in tlapm
 Hi Ioannis,On 9 May 2017, at 08:09, Ioannis Filippidis wrote:I am trying to prove that the image of a finite set under an operator is finite (relevant to [1]),to reuse it at multiple places. thanks, this is a useful corollary to FS_Surjection (please also note the comment in FiniteSetTheorems indicating that the theorem implies that the image of a finite set under any function is finite).If I write a proof similar to that of ImageOfFinite belowfor some specific operator Op, for example:<2> DEFINE    Op(u, a, b) == u    f == [u \in S |-> Op(u, arg1, arg2)]<2>1. f \in Surjection(S, H)    BY DEF Surjection, Hdef<2> QED    BY <2>1, ..., FS_Surjectionthen tlapm -v -C proves it, and I don't see any intermediate errors (using version 1.4.3).tlapm proves correct also the module test2 below, but with an error from the SMT backend (see below),which can probably be ignored, because only the Isabelle backend supports the declaration NEW Op(_) [2].Yes: the message from the SMT backend indicates a limitation of the backend, which stumbles over the apparent "mismatch" of arities. This is one of the situations where the Isabelle backend is useful, due to higher-order unification.However, if I change the assumption to NEW Op(_, _) in ImageOfFinite,or the operator application to Op(x) in ImageOfFinite2,then the proof is again successful, but SANY detects the errors.This is indeed a syntax error and should be rejected. Our working hypothesis is that the prover is called only on input that has been checked by SANY (if you use the Toolbox, the prover will not be started on modules that contain a syntax error). The next (major) release of TLAPS will be based on the SANY parser, so you will not be able to run the prover on that module anymore.Question 1: If SANY detects no errors and tlapm proves module test2 correct,should I assume that the arity of operator declarations as those in module test2has been taken into account correctly?Yes.Question 2: Is there an approach simpler/better than a couple of theorems for different arities toprove that IsFiniteSet(S) implies IsFiniteSet( { Op(x, ...):  x \in S } )as a theorem that we can reuse?In fact, I'd simply apply ImageOfFinite, just as you do in the proofs of the theorems for operators of different arities. Since the other arguments must be fixed, the operator is effectively unary. For example:LEMMA  ASSUME NEW S \in SUBSET Nat, IsFiniteSet(S), NEW n \in Nat  PROVE  IsFiniteSet({x+n : x \in S})BY ImageOfFiniteHowever, this again requires higher-order unification, so only Isabelle will prove the step, and you may have to "isolate" the application of the theorem and not combine it with, say, arithmetic reasoning.Sidenote: To invoke ImageOfFinite3 successfully, I had to hide the definition of S,but at least I didn't rewrite a proof like that of ImageOfFinite.Indeed, if S is a complex _expression_, there may be some rewriting going on before Isabelle's classical prover gets to see the term, preventing successful unification. In such cases, you may be successful using "BY IsaM("blast")", which essentially disables rewriting. We'd like to hide these backend-specific idiosyncrasies from users, but we're not there yet.*** Fatal exception:Type Checking error: Expected function type for:a_Opunde_1a but got this: u in function application:(_APPLY {a_Opunde_1a} x)test2.tlaps/tlapm_d7953c.smt:50: this is the location of the error...As mentioned above, this only indicates a failure of the backend and doesn't mean that there is something wrong with your input.Checking the proofs with Isabelle. This may take a long time.(* Isabelle interaction log in "test2.tlaps/isabelle.log" *)(* Isabelle parsing "test2.tlaps/test2.thy" ... done *)(* Obligation checking trace follows. *)(* +5 -5 +7 -7 *)Proof checking done. No errors found.Please note that at this point we can only check proofs found by Zenon, not those found by SMT.Regards,Stephan