-->

This example is the algebraic part of Lagrange's theorem.

**Theorem: ***Let G be a group and H a subgroup of G. Let a be a member of G. Then there is a one-one correspondence between H and the coset Ha.*

This file constructs a map from a subgroup H of a group G
to the coset Ha, and also constructs its inverse.
The map in question takes *x* to *x*a*, and the inverse
takes *z* to *z*i(a)*, where *i(a)* denotes the inverse of *a*.
Otter-lambda uses lambda-unification to construct these maps,
which are given by the lambda terms lambda(x,x*a) and lambda(z,z*i(a))
respectively.

Answer literals (which use the symbol $ANS) are used in Otter and Otter-lambda just to provide information to the user. By using $ANS in the input file, we cause Otter-lambda to show us the lambda terms it constructed in find a proof.

We do not use a unary predicate for G(x). This is not an error or oversight. For an explanation
of why we do not need G(x), see *Implicit Typing*

The first axiom is always used when equality is involved: 1 [] x=x.

The next axiom is one way of formulating the axiom for group inverse, without a symbol for the identity element: 2 [] u*x=v|u!=v*i(x).

The next axiom defines the existential quantifier. It says "If the predicate Z holds of any object w then there exists an x such that Z(x)". Here "exists" is treated as a constant that applies to a predicate; predicates are given by lambda-terms. What we would usually write as "there exists an x such that P(x)" is written here in the form exists(lambda(x,Ap(P,x))). 3 [] -Ap(Z,w)|exists(lambda(x,Ap(Z,x))).

We now define f to be the characteristic function of the coset Ha: 4 [] f(w)=exists(lambda(x,and(H(x),x*a=w))).

Now, the theorem in question is that there exists an X such that X maps H into Ha, and an inverse map Y such that for a in H, we have Y(X(a)) = a. Using Ap to express function application, this would be "for all z in H, Ap(X,z) is in H and Ap(Y,Ap(X,u)) = z". As usual in a clause-based prover, we negate the goal, so the first z becomes a Skolem term g(X) and the second z becomes another Skolem term r(X,Y). We could equally well have made both occurrences of z into r(X,Y), but we didn't do that. X and Y are variables, and the negated goal says that g(X) is in H, and "either Ap(X,g(X)) is not in the coset H(g(X)), or it's not the case that Ap(Y,Ap(X,r(X,Y))) = r(X,Y)." But of course we use f(z) to express that z belongs to the coset Hz. Our negated goal then is expressed by the next two clauses:

5 [] H(g(X)).

6 [] -f(Ap(X,g(X)))|$ANS(X)|Ap(X,Ap(Y,r(X,Y)))!=r(X,Y)|$ANS(Y).

We put the answer literals in, as explained above, so we can see the values produced for X and Y.

Otter-lambda begins the proof by starting with line 6 and using line 4 to expand the definition of f:

9 [6,demod,4] -exists(lambda(x,and(H(x),x*a=Ap(y,g(y)))))|$ANS(y)|Ap(y,Ap(z,r(z)))!=r(z)|$ANS(z).

Then it uses the definition of "exists" from line 3. The variable Z in line 3 gets instantiated to lambda(x,and(H(x),x*a = Ap(X,g(X)))), and the first literal in line 3, which was -Ap(Z,w), then beta-reduces, now that Z is a lambda-term, to -and(H(w),w*a = Ap(X,g(X))). Otter-lambda renames the variables when producing a new clause, so in the following line, what was w becomes z and what was X becomes x:

21 [binary,9.1,3.2,demod,beta] $ANS(x)|Ap(x,Ap(y,r(y)))!=r(y)|$ANS(y)| -and(H(z),z*a=Ap(x,g(x))).

Now the literal containing a negated "and" is split into two literals. This is an inference rule that belongs to Otter-lambda, but not to Otter. It is activated by the set(lambda) command.

22 [split -and,21] $ANS(x)|Ap(x,Ap(y,r(y)))!=r(y)|$ANS(y)| -H(z)|z*a!=Ap(x,g(x)).

The literal -H(z) resolves with line 5, making z = g(X). The last literal in 22 then would become g(X) *a != Ap(x,g(x)). Otter-lambda tries to resolve this with the equality axiom 1, so it has to unify Ap(x,g(x)) with g(X)*a. Lambda-unification succeeds, taking x = lambda(u,u*a) and X = x. With that value of x, Ap(x,g(x)) beta-reduces to g(x)*a = g(lambda(u,u*a)) *a. So the last two literals of 22 disappear and x gets the value lambda(u,u*a). That leaves only one literal in 22 besides the answer literals, and since x has been instantiated to lambda(u,u*a), the left-hand side of that literal, namely Ap(x,Ap(y,r(y))), will now beta-reduce, becoming Ap(y,r(y))*a. As usual variables are renamed in the new clause:

25 [binary,22.3,1.1,demod,beta,unit_del,5] $ANS(lambda(x,x*a))|Ap(y,r(y))*a!=r(y)|$ANS(y).

Now, that last literal is resolved with first literal of axiom 2, the axiom for group inverse. Otter-lambda has to resolve Ap(y,r(y))*a = r(y) with u *x = v. This succeeds with the assignments u:= Ap(y,r(y)), x:= a, v:=r(y). The second literal of 2, u != v*i(x), then becomes Ap(y,r(y)) != r(y)*i(a) as seen in the next line of the proof: 27 [binary,25.1,2.1] $ANS(lambda(x,x*a))|$ANS(y)|Ap(y,r(y))!=r(y)*i(a). Using the equality axiom again, Otter-lambda unifies the two sides of this equality to reach the final contradiction, producing the map y := lambda(z,z*i(a)) as shown in the answer literal.

28 [binary,27.1,1.1] $ANS(lambda(x,x*a))|$ANS(lambda(z,z*i(a))). Since this clause contains only answer literals, it represents a contradiction, completing the proof.