% A proof of the totality of the Ackermann function using muMALL.
% This proof development is a formal version of the informal proof given
% in the paper Peano Arithmetic and muMALL by Matteo Manighetti and Dale
% Miller, which has been accepted to Fundamenta Informaticae in March
% 2025. This paper is also available at https://hal.science/hal-04824175.
% The use of Abella in this development is unusual since a different
% logic, muMALL, is presented here by encoding the inference rules of
% that logic as axioms in Abella. Since Abella was not intended to be
% used in this fashion, the resulting proof was rather tedious to
% complete.
Specification "dual".
Set subgoals off.
% Splitting relation on multisets
Define split : list pol -> list pol -> list pol -> prop by
split nil nil nil
; split (X::L) (X::K) M := split L K M
; split (X::L) K (X::M) := split L K M.
% The member-and-rest relation on context
Define mnr : pol -> list pol -> list pol -> prop by
mnr X (X::L) L
; mnr X (Y::L) (Y::K) := mnr X L K.
% The relation that holds when all members of a context start with the ? modal
Define modals : list pol -> prop by
modals nil
; modals ((? B)::C) := modals C.
% Predicate used for induction over lists.
Define list_pol : list pol -> prop by
list_pol nil
; list_pol (B::L) := list_pol L.
Theorem split_nil : forall L, list_pol L -> split L nil L.
induction on 1. intros. case H1. search. apply IH to H2. search.
% The judgment that a context is provable in muMALL.
% This predicate is not defined by it is axiomatized.
Type ts list pol -> prop. % Turnstile
% The inference rules of muMALL as axioms (unproven theorems in Abella).
Theorem exchange : forall P Q L, ts (P::Q::L) -> ts (Q::P::L). skip.
Theorem parI : forall P Q C C', mnr (par P Q) C C' -> ts (P::Q::C') -> ts C. skip.
Theorem botI : forall C C', mnr bot C C' -> ts C' -> ts C. skip.
Theorem neqI : forall T S C C', mnr (neq T S) C C' -> ((T = S) -> ts C') -> ts C. skip.
Theorem withI : forall P Q C C', mnr (with P Q) C C' -> (ts (P::C') /\ (ts (Q::C'))) -> ts C. skip.
Theorem allI : forall B C C', mnr (all B) C C' -> (forall x, ts (B x::C')) -> ts C. skip.
Theorem nu1I : forall B T C C', mnr (nu1 B T) C C' ->
(exists S, ts ((S T)::C') /\
(forall S', ({dual (all S) (some S')}) -> (forall x, ts ((B S x)::(S' x)::nil)))) -> ts C. skip.
Theorem nu3I : forall B T R U C C', mnr (nu3 B T R U) C C' -> (exists S, ts ((S T R U)::C') /\
(forall S', {dual (all x\ all y\ all u\ S x y u) (all x\ all y\ all u\ S' x y u)} ->
(forall x y u, ts ((B S x y u)::(S' x y u)::nil)))) -> ts C. skip.
Theorem unfold1 : forall B T1 C C', mnr (nu1 B T1) C C' -> ts ((B (nu1 B) T1 )::C') -> ts C. skip.
Theorem unfold2 : forall B T1 T2 C C', mnr (nu2 B T1 T2) C C' -> ts ((B (nu2 B) T1 T2 )::C') -> ts C. skip.
Theorem unfold3 : forall B T1 T2 T3 C C', mnr (nu3 B T1 T2 T3) C C' -> ts ((B (nu3 B) T1 T2 T3)::C') -> ts C. skip.
Theorem mu1I : forall B T1 C C', mnr (mu1 B T1) C C' -> ts ((B (mu1 B) T1 )::C') -> ts C. skip.
Theorem mu2I : forall B T1 T2 C C', mnr (mu2 B T1 T2) C C' -> ts ((B (mu2 B) T1 T2 )::C') -> ts C. skip.
Theorem mu3I : forall B T1 T2 T3 C C', mnr (mu3 B T1 T2 T3) C C' -> ts ((B (mu3 B) T1 T2 T3)::C') -> ts C. skip.
Theorem tensorI : forall P Q C C' D D', mnr (tensor P Q) C C' -> split C' D D' -> ts (P::D) -> ts (Q::D') -> ts C. skip.
Theorem tensorIx : forall P Q C C', mnr (tensor P Q) C C' -> (exists D D', split C' D D' /\ ts (P::D) /\ ts (Q::D')) -> ts C. skip.
Theorem oplusI : forall P Q C C', mnr (oplus P Q) C C' -> (ts (P::C') \/ (ts (Q::C'))) -> ts C. skip.
Theorem someI : forall B C C', mnr (some B) C C' -> (exists x, ts (B x::C')) -> ts C. skip.
Theorem oneI : ts (one::nil). skip.
Theorem eqI : forall T, ts ((eq T T)::nil). skip.
Theorem mu0nu0a : forall B B', {dual (mu0 B) (nu0 B')} -> ts ((mu0 B)::(nu0 B')::nil). skip.
Theorem mu0nu0b : forall B B', {dual (nu0 B) (mu0 B')} -> ts ((nu0 B)::(mu0 B')::nil). skip.
Theorem mu1nu1a : forall B B' T, {dual (mu1 B T) (nu1 B' T)} -> ts ((mu1 B T)::(nu1 B' T)::nil). skip.
Theorem mu1nu1b : forall B B' T, {dual (mu1 B T) (nu1 B' T)} -> ts ((nu1 B T)::(mu1 B' T)::nil). skip.
Theorem mu2nu2a : forall B B' T1 T2, {dual (mu2 B T1 T2) (nu2 B' T1 T2)} -> ts ((mu2 B T1 T2)::(nu2 B' T1 T2)::nil). skip.
Theorem mu2nu2b : forall B B' T1 T2, {dual (mu2 B T1 T2) (nu2 B' T1 T2)} -> ts ((nu2 B T1 T2)::(mu2 B' T1 T2)::nil). skip.
Theorem mu3nu3a : forall B B' T1 T2 T3, {dual (mu3 B T1 T2 T3) (nu3 B' T1 T2 T3)} -> ts ((mu3 B T1 T2 T3)::(nu3 B' T1 T2 T3)::nil). skip.
Theorem mu3nu3b : forall B B' T1 T2 T3, {dual (nu3 B T1 T2 T3) (mu3 B' T1 T2 T3)} -> ts ((nu3 B T1 T2 T3)::(mu3 B' T1 T2 T3)::nil). skip.
Theorem ginit : forall B B', {dual B B'} -> ts (B::B'::nil). skip.
Theorem weaken : forall B C C', mnr (? B) C C' -> ts C' -> ts C. skip.
Theorem derelict : forall B C C', mnr (? B) C C' -> ts (B::C') -> ts C. skip.
Theorem contract : forall B C C', mnr (? B) C C' -> ts ((? B)::(? B)::C') -> ts C. skip.
Theorem promote : forall B C C', mnr (bang B) C C' -> modals C' -> ts (B::C') -> ts C. skip.
Theorem promotex : forall C, (exists B C', mnr (bang B) C C' /\ modals C' /\ ts (B::C')) -> ts C. skip.
% Enter the dual expression directly - skip the computation of the dual
Theorem nu1Ix : forall B T C C', mnr (nu1 B T) C C' -> (exists S S', ts ((S T)::C') /\ (forall x, ts ((B S x)::(S' x)::nil))) -> ts C. skip.
Theorem nu3Ix : forall B T R U C C', mnr (nu3 B T R U) C C' ->
(exists S S', ts ((S T R U)::C') /\ (forall x y u, ts ((B S x y u)::(S' x y u)::nil))) -> ts C. skip.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Some derived rules of inference
Theorem par_neq : forall L T S B, (T = S -> ts (B::L)) -> ts ((par (neq T S) B) :: L).
intros. backchain parI. backchain neqI.
Theorem tensor_eq : forall L T B, list_pol L -> ts (B::L) -> ts ((tensor (eq T T) B) :: L).
intros. backchain tensorIx. witness nil. witness L. split. apply split_nil to H1. search.
backchain eqI. search.
%% The general form of the initial rule is admissible.
Theorem initial : forall A B, {dual A B} -> ts (A :: B :: nil).
induction on 1. intros. case H1.
backchain botI. backchain oneI.
backchain botI. backchain oneI.
backchain neqI. intros. case H2. backchain eqI.
backchain neqI. intros. case H2. backchain eqI.
backchain parI. backchain tensorIx. witness D::nil. witness E::nil. split.
search. apply IH to H2. search. apply IH to H3. search.
backchain parI. backchain tensorIx. witness B1::nil. witness C::nil. split.
search. apply IH to H2. backchain exchange. apply IH to H3. backchain exchange.
backchain withI. split. backchain oplusI. left. apply IH to H2. search.
backchain oplusI. right. apply IH to H3. search.
backchain withI. split. backchain oplusI. left. apply IH to H2. backchain exchange.
backchain oplusI. right. apply IH to H3. backchain exchange.
backchain allI. intros. backchain someI. witness x. inst H2 with n1 = x. apply IH to H3. search.
backchain allI. intros. backchain someI. witness x. inst H2 with n1 = x. apply IH to H3. backchain exchange.
backchain mu0nu0a. backchain mu0nu0b. backchain mu1nu1a. backchain mu1nu1b.
backchain mu2nu2a. backchain mu2nu2b. backchain mu3nu3a. backchain mu3nu3b.
backchain promote. backchain derelict. apply IH to H2. search.
backchain promote. backchain derelict. apply IH to H2. backchain exchange.
% An example of how to prove a theorem.
Theorem excluded-middle-multi : ts ((all x\ all y\ par (eq x y) (neq x y))::nil).
backchain allI. intros. backchain allI. intros. backchain parI. backchain neqI. intros. case H1.
backchain eqI.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Define the fixed point expressions for the natural number predicate
% and the Ackermann predicate. Also defined their De Morgan dual for
% convenient.
Define nat : (i -> pol) -> prop by
nat (mu1 (N\ x\ (oplus (eq x z) (some y\ (tensor (eq x (s y)) (N y)))))).
Define dnat : (i -> pol) -> prop by
dnat (nu1 (N\ x\ (with (neq x z) (all y\ (par (neq x (s y)) (N y)))))).
Define ack : (i -> i -> i -> pol) -> prop by
ack (mu3 (A\ x\ y\ a\ (oplus (tensor (eq x z) (eq a (s y)))
(oplus (some (p\ (tensor (eq x (s p)) (tensor (eq y z) (A p (s z) a)))))
(some p\ some q\ some b\ (tensor (eq x (s p))
(tensor (eq y (s q)) (tensor (A x q b) (A p b a))))))))).
Define dack : (i -> i -> i -> pol) -> prop by
dack (nu3 (A\ x\ y\ a\ (with (par (neq x z) (neq a (s y)))
(with (all (p\ (par (neq x (s p)) (par (neq y z) (A p (s z) a)))))
(all p\ all q\ all b\ (par (neq x (s p))
(par (neq y (s q)) (par (A x q b) (A p b a))))))))).
%%%%
%%%% Complete proof of the totality of Ackermann's function
%%%%
Theorem ack_first_induction_is_invariant:
forall N DN A DA x y, nat N -> dnat DN -> ack A -> dack DA ->
ts ((? (some (z\ tensor (N z) (all (a\ par (DA x z a) (DN a)))))) ::
DN y ::
some (a\ tensor (A x y a) (N a)) :: nil).
intros.
backchain derelict. backchain someI. witness y.
backchain tensorIx. witness (DN y :: nil).
witness (some a\ tensor (A x y a) (N a)) :: nil. split. search.
%% Tensor and splitting bureaucracy
case H1. case H2.
%Preserve: split invariant: nat and dual nat
backchain mu1nu1a.
%Preserve: split invariant: ack /\ nat and dual ack /\ dual nat
backchain allI. intros. backchain someI. witness x1.
backchain initial. case H3. case H4. case H1. case H2. search 20.
%%unfold all defs and find out the two are duals
Theorem ack_first_induction_base_case :
forall DN A N x1, ack A -> dnat DN -> nat N ->
ts (neq x1 z ::
bang (all (x\par (DN x) (some (a\tensor (A x1 x a) (N a))))) :: nil).
intros.
backchain neqI. intros. case H4. backchain promote. backchain allI. intros.
backchain parI. backchain someI. witness (s x).
backchain tensorIx. witness nil. witness (DN x :: nil). split. search.
case H1. backchain mu3I.
% Select base case of ack
backchain oplusI. left.
%% prove for ack: 0=0 and s 0 = s 0
backchain tensorI. backchain eqI. backchain eqI.
%% proving that nat x -> nat (s x) by unfolding nat (s x)
case H3. backchain mu1I. backchain oplusI. right. backchain someI. witness x.
backchain tensorIx. witness nil. witness (DN x :: nil). split. search.
backchain eqI. backchain initial. case H2. search 20.
Theorem ack_second_invariant_is_invariant :
forall DN N A DA x2 x3, ack A -> nat N -> dnat DN -> dack DA ->
ts (tensor (bang (all (x\par (DN x) (some (a\tensor (A x2 x a) (N a))))))
(all (a\par (DA (s x2) x3 a) (DN a))) ::
some (a\tensor (A (s x2) x3 a) (N a)) ::
? (some (x\tensor (N x) (all (a\ par (DA x2 x a) (DN a))))) :: nil).
intros.
backchain tensorIx.
witness (? (some (x\tensor (N x) (all (a\par (DA x2 x a) (DN a))))) :: nil).
witness (some (a\tensor (A (s x2) x3 a) (N a)) ::nil). split. search.
backchain initial. case H1. case H2. case H3. case H4. search 50.
backchain initial. case H1. case H2. case H3. case H4. search 50.
Theorem ack_second_induction_base:
forall N A DA DN x2 x4, ack A -> nat N -> dack DA -> dnat DN ->
ts (neq x4 z ::
par (? (some (x\tensor (N x) (all (a\par (DA x2 x a) (DN a))))))
(some (a\tensor (A (s x2) x4 a) (N a))) :: nil).
intros.
backchain neqI. intros. case H5. backchain parI. backchain derelict.
backchain someI. witness (s z). backchain tensorIx. witness nil.
witness (some (a\ tensor (A (s x2) z a) (N a)) :: nil). split. search.
%% one is nat
case H2. backchain mu1I. backchain oplusI. right. backchain someI. witness z.
backchain tensorI. backchain eqI. backchain mu1I. backchain oplusI. left. backchain eqI.
%% More base case: computing exists a (ack (s x2) 0 a (X) nat a) given forall a (ack x2 1 a (X) nat a)
backchain allI. intros. backchain someI. witness x.
backchain parI. backchain tensorIx. witness DA x2 (s z) x :: nil. witness DN x :: nil. split. search.
%% After introducing quantifiers and splitting: compute ack (s x2) 0 given ack x2 1
case H1. backchain mu3I. backchain oplusI. right. backchain oplusI. left. % select appropriate case of ack
backchain someI. witness x2. backchain tensorIx. witness nil.
witness (DA x2 (s z) x :: nil). split. search.
backchain eqI. backchain tensorIx. witness nil. witness DA x2 (s z) x :: nil. split. search.
backchain eqI. case H3. backchain mu3nu3a. search 10.
%% Finally, the other branch of the tensor where we prove nat x |- nat x
backchain initial. case H2. case H4. search 20.
Theorem ack_total :
forall N DN A DA, dnat DN -> ack A -> nat N -> dack DA -> forall x y,
ts ((DN x)::(DN y)::(some a\ tensor (A x y a) (N a)) ::nil).
intros. case H1.
backchain nu1Ix.
witness (y\ ? (some x \ tensor (N x) (all a\ par (DA y x a) (DN a)))).
witness (y\ bang (all x \ par (DN x) (some a\ tensor (A y x a) (N a)))).
split.
% Lemma: the chosen invariant is an invariant
backchain ack_first_induction_is_invariant with N = N, DN = DN, A = A, DA = DA.
% Induction!
intros. backchain withI. split.
% Base case in a lemma (easy but has some bureaucracy)
backchain ack_first_induction_base_case with DN = DN, A = A, N = N.
% Inductive step of main proof (we do it here since it is short)
backchain allI. intros. backchain parI. backchain neqI. intros. case H5.
backchain promote. backchain allI. intros. backchain parI.
% Time for the second induction!
backchain nu1Ix.
witness (y\ (tensor (bang (all x \ par (DN x) (some a\ tensor (A x2 x a) (N a))))
(all a\ par (DA (s x2) y a) (DN a)))).
witness (y\ (par (? (some x \ tensor (N x) (all a\ par (DA x2 x a) (DN a))))
(some a\tensor (A (s x2) y a) (N a)))).
split.
% Preserve
backchain ack_second_invariant_is_invariant with A = A, DA = DA, N = N, DN = DN.
% The second induction starts!
intros. backchain withI. split.
% Base case
backchain ack_second_induction_base with A = A, DN = DN, DA = DA, N = N.
%% Finally, the second inductive case
backchain allI. intros. backchain parI. backchain neqI. intros. case H6. backchain parI.
%% The crucial contraction and the following tensor split (corresponding to the imp-left rule in two sides)
backchain contract. backchain tensorIx.
witness (? (some (x\tensor (N x) (all (a\par (DA x2 x a) (DN a)))))) :: nil.
witness (? (some (x\tensor (N x) (all (a\par (DA x2 x a) (DN a)))))) ::
some (a\tensor (A (s x2) (s x5) a) (N a)) :: nil.
split. search.
%% Thanks to the careful splitting, we can promote here
backchain promote. backchain derelict. backchain allI. intros. backchain someI. witness x6.
%% Left hand side premise of the main imp-left rule
backchain parI. backchain tensorIx. witness DN x6 :: nil.
witness some (a\tensor (A x2 x6 a) (N a)) :: nil. split. search. case H3. backchain mu1nu1a.
backchain initial. case H2. case H4. case H3. search 20.
%% Finally, the main branch of the main imp-left rule of the second induction
backchain derelict. backchain allI. intros. backchain someI. witness x6.
backchain parI.
%% Use the tensor (i.e., imp left) to use the inductive hypothesis
backchain tensorIx. witness DN x6 :: nil.
witness DA (s x2) x5 x6 :: some (a\tensor (A (s x2) (s x5) a) (N a)) :: nil. split. search.
%% left branch of imp-left : nat x6 |- nat x6
backchain initial. case H3. search 20.
%% Finally, computing the appropriate value of ack.
%% Instantiate quantifiers (the return value is the one returned by the second call in ctx)
backchain allI. intros. backchain someI. witness x7.
%% split the two goals: the final return value x7 is a nat, and it is ack (s x2) (s x5)
backchain parI. backchain tensorIx. witness DA x2 x6 x7 :: DA (s x2) x5 x6 :: nil.
witness DN x7 :: nil. split. search.
%% main branch of the split: prove that x7 is the correct result
%%% unfolding the corresponding case of ack
case H2. backchain mu3I. backchain oplusI. right. backchain oplusI. right.
%%% the witnesses for the final ack unfolding
backchain someI. witness x2. backchain someI. witness x5. backchain someI. witness x6.
%%% verify the assignments for the unfolding
backchain tensorIx. witness nil. witness DA x2 x6 x7 :: DA (s x2) x5 x6 :: nil. split. search.
backchain eqI.
backchain tensorIx. witness nil. witness DA x2 x6 x7 :: DA (s x2) x5 x6 :: nil. split. search.
backchain eqI.
%%% split the two final calls to ack. Send the right premise to each branch.
backchain tensorIx.
witness DA (s x2) x5 x6 :: nil. witness DA x2 x6 x7 :: nil. split.search.
case H4. backchain mu3nu3a. search 10.
case H4. backchain mu3nu3a. search 10.
%% The other final goal: the computed value is nat
backchain initial. case H3. search 20.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Define the fixed point expressions for the plus (addition) predicate.
% Also defined their De Morgan dual for convenient.
Define plus : (i -> i -> i -> pol) -> prop by
plus (mu3 (P\ x\ y\ a\
(oplus (tensor (eq x z) (eq y a))
(some p\ some q\ (tensor (eq x (s p)) (tensor (eq a (s q)) (P p y q))))))).
Define dplus : (i -> i -> i -> pol) -> prop by
dplus (nu3 (P\ x\ y\ a\
(with (par (neq x z) (neq y a))
(all p\ all q\ (par (neq x (s p)) (par (neq a (s q)) (P p y q))))))).
%%%%
%%%% Prove that plus is commutative.
%%%%
%%%% First prove that 0 + x = x by induction on the natural number x.
Theorem plus_zero :
forall N DN P DP, nat N -> dnat DN -> plus P -> dplus DP ->
forall x, ts ((DN x):: (P x z x) :: nil).
intros. case H2.
backchain nu1Ix.
% The co-invariant is a purely negative formula.
witness (x\ DP x z x). witness (x\ P x z x).
%
case H3. case H4. split.
backchain mu3nu3b. search 20.
intros. backchain withI. split.
backchain neqI. intros. case H5. backchain mu3I. backchain oplusI. left.
backchain tensorIx. witness nil. witness nil. split. unfold. search.
backchain eqI. backchain eqI.
backchain allI. intros. backchain parI. backchain neqI. intros. case H5.
backchain mu3I. backchain oplusI. right. backchain someI. witness x2.
backchain someI. witness x2. backchain tensorIx. witness nil.
witness (nu3
(P\x\y\a\with (par (neq x z) (neq y a))
(all
(p\all
(q\par (neq x (s p))
(par (neq a (s q)) (P p y q))))))
x2 z x2 :: nil).
split. search.
backchain eqI.
backchain tensorIx. witness nil.
witness (nu3
(P\x\y\a\with (par (neq x z) (neq y a))
(all
(p\all
(q\par (neq x (s p))
(par (neq a (s q)) (P p y q))))))
x2 z x2 :: nil).
split. search. backchain eqI.
backchain mu3nu3a. search 20.
%%%% Second prove that if x + y = u then x + (s y) = (s u)
%%%% (by induction on the addition judgment: x + y = u).
Theorem plus_succ :
forall P DP, plus P -> dplus DP -> forall x y u, ts ((DP x y u):: (P x (s y) (s u)) :: nil).
intros plusH dplusH. case plusH. case dplusH. % Set up sequent, remove definitions.
backchain nu3Ix.% State the inductive hypothesis
% Enter the invariant.
witness (x\y\u\ (nu3 (P\ x\ y\ a\ (with (par (neq x z) (neq y a))
(all p\ all q\ (par (neq x (s p)) (par (neq a (s q)) (P p y q))))))) x (s y) (s u)).
% Enter the negation of the invariant.
witness (x\y\u\ (mu3 (P\ x\ y\ a\ (oplus (tensor (eq x z) (eq y a))
(some p\ some q\ (tensor (eq x (s p)) (tensor (eq a (s q)) (P p y q))))))) x (s y) (s u)).
split.
% Subgoal 1: The easy "identity case".
backchain mu3nu3b. search 20.
% Subgoal 2:
intros. backchain withI. split.
% Subgoal 2.1: The easy base case
backchain par_neq. intros eqH. case eqH. % Set two variables.
backchain neqI. intros eqH. case eqH.
backchain mu3I. backchain oplusI. left.
backchain tensor_eq.
backchain eqI.
% Subgoal 2.1: The harder inductive case
backchain allI. intros. backchain allI. intros.
backchain par_neq. intros eqH. case eqH.
backchain par_neq. intros eqH. case eqH.
% Now unfold the left-hand side case.
backchain unfold3. backchain withI. split.
backchain par_neq. intros eqH. case eqH.
backchain neqI. intros eqH. case eqH.
% open definition of plus
backchain mu3I. backchain oplusI. right.
backchain someI. witness z.
backchain someI. witness (s x3).
backchain tensor_eq. backchain tensor_eq.
backchain mu3I. backchain oplusI. left.
backchain tensor_eq. backchain eqI.
backchain allI. intros. backchain allI. intros.
backchain par_neq. intros eqH. case eqH.
backchain par_neq. intros eqH. case eqH.
% Here, we are left with x4 + (s y1) = x5 implies (s (s x4)) + (s y1) = (s (s x5)).
% Prove this by two unfolding of plus's definition.
% First unfolding:
backchain mu3I. backchain oplusI. right. backchain someI. witness (s x4).
backchain someI. witness (s x5). backchain tensor_eq. backchain tensor_eq.
% Second unfolding:
backchain mu3I. backchain oplusI. right. backchain someI. witness x4.
backchain someI. witness x5. backchain tensor_eq. backchain tensor_eq.
backchain mu3nu3a. search 20.
