Theory Exploration 
Versus
Theorem Proving

Bruno Buchberger
RISC
Research Institute for Symbolic Computation
A4232 Castle of Hagenberg, Austria

Invited Talk at the Calculemus Meeting, Trento, July 11, 1999.

Copyright Bruno Buchberger: Copying, storing in data bases etc. is granted under the condition that the file is kept unchanged and this copyright note is included in the copy. Usage of the material contained in this talk hast be cited appropriately.

Acknowledgements: This research is partially supported by the Austrian Science Foundation (FWF-SFB-project FO-1302) and the Upper Austrian Government  (project ``PROVE'').

A Rough Distinction

Theorem Proving

The two essential parameters of a prover:

Knowledge–Base      (Overscript[⊢, ?])  Goal

Power of theorem provers is measured by the class of goals and knowledge bases for which proofs can be generated (efficiently, naturally, ...).

Correspondingly, in Theorema, the basic call is

Prove[expression,  using -> knowledge–base,  
      by -> proof–method]

Similarly, in Theorema, we have the calls

Solve[expression,  using -> knowledge–base,  
      by -> solution–method]

Compute[expression,  using -> knowledge–base,  
      by -> evaluation–method]

Remark: Prove, Solve, Compute intimately interact with each other, see B. Buchberger, Proving, Solving, Computing: A Language Environment Based on Mathematica, invited talk at the  Multi-Paradigm Logic Programming Conference, Schloss Dagstuhl, September 1996; http://www.risc.uni-linz.ac.at/people/buchberg/papers/B-Buchberger-1999-Talk- MPLP96.zip

Theory Exploration

In normal math research, teaching, and application, we do not consider individual theorems.

Rather, we explore an entire 'theory', i.e. we

we proceed in proving 'layers' of more and more complex propositions

in each layer, we consider (try to prove or disprove) the propositions as an ensemble and not isolated

in each layer, we prove by reduction to the (immediately) preceding layer(s) and not by reduction to 'first principles'.

in each layer, we apply specific proof techniques that are 'appropriate' to the layer considered.

The thesis of this talk:

Organized theory exploration instead of isolated theorem proving has a drastic influence on the feasibility, power, naturalness and practical attractiveness of automated theorem proving.

Hence, future mathematical software systems that integrate theorem proving should support theory generation in various ways.

Exploration Situations

The Parameters of an Exploration Situation

An 'exploration situation' in mathematical research is characterized by the following parameters:

a collection C of known concepts

a collection K of facts that (are thought  to) "completely" describe the interrelations among the known concepts

a new concept N

axioms A (definitions) that relate the new concept with the known concepts

a collection G of goal propositions that (are thought to) "completely" explore the relation between the new concept and the known concepts.

Note that, here, the notion of a "complete" knowledge on concepts is not a formal notion. In certain contexts, for example in rewriting, "complete" knowledge may well be conceived as a "completed system" in the technical sense, which entails that the truth of sentences can be decided w.r.t. to such a system. However, although we do not give a formal definition of "completeness", the intuitive ingredient of the notion of  "complete knowledge" is that, as with formally complete systems,  it should be "relatively easy" (i.e. by "symbolic computing" and not by handling quantifiers) to prove or disprove all other statements on the given notions as soon as we have "complete knowledge" about them. We will make this clearer in the examples below.

The Proof Method Appropriate for an Exploration Situation

We believe that

the parameters K (known facts), A (axioms), and G (goals)  of an exploration situation determine an "appropriate" proof method for proving the "routine" propositions in G and

"often", the appropriate proof method can be derived from the syntactical structure of K , A , and G.

Layers of sophistication in (present and future) computer-supported theory exploration systems:

For many typical exploration situations, the system provides an appropriate proof method in a library of proof methods which the user may choose according this hir analysis of the situation ("\!\(\*
StyleBox[\(Theorema\),
FontSlant->"Italic"]\), present Version 1").

For any  exploration situation, the system allows the user to formulate, in an easy "prover programming language", using also basic proof methods from a library, his/her proposal for what she believes is an appropriate proof method for the given situation ("\!\(\*
StyleBox[\(Theorema\),
FontSlant->"Italic"]\), future Version 2").

The system provides a "proof method composer" that composes
        , for (m) any exploration situations, an appropriate proof method automatically from a library of basic proof methods ("\!\(\*
StyleBox[\(Theorema\),
FontSlant->"Italic"]\), future Version 3).

An Example of an Exploration Situation

Needs["Theorema`"]

Known concepts: 0 (zero), \(TraditionalForm\`\(□\^+\)\) (successor function).

Fact(s) about known concepts: induction axiom(s)

\(∀ \+A\((
        \((A[0] ∧ 
              ∀ \+x\((A[x]⟹A[\(x\^+\)])\))
            \)⟹\(∀ \+x A[x]\))\)\)

New concept: '+' (addition).

Axioms (definition) that relate new concept with known concepts:

Definition["Addition",any[m, n],
	({{m + 0 = m, " +0"}, {\(m + \(n\^+\) = \(\((m + n)\)\^+\)\), " +succ"}})]

Goal propositions: all formulae of the form

(Underscript[∀ , (Subscript[x, 1]), …, (Subscript[x, n])])L = R

where L and R are terms in '0', '\(TraditionalForm\`\(□\^+\)\)', and '+' and the variables ' (Subscript[x, 1])', …, ' (Subscript[x, n])'.

An Appropriate Proof Method

A proof method that is appropriate for this proof situation (and many others):

Take all (Subscript[x, 1]), …, (Subscript[x, n]) "arbitrary but fixed" and try to prove 'L=R' by rewriting both L and R modulo the assumed equalities (in the definition).

If this proof succeeds, report success (and show the proof).

If this proof fails, organize induction on (Subscript[x, 1]):

The induction base is a proof situation of the same type but with one variable less. 
         Hence call the proof method recursively.

The induction step is a proof situation of the same type but with one variable less. 
         Hence call the proof method recursively.

In Theorema, this proof method has the name 'NNEqIndProver'.

An Example of a Proof

SetGlobals[TraceLevel -> 0]; $RecursionLimit = 1024;

Proposition["Addition of Zero from Left",any[n],
	({{0 + n = n, "0+ "}})]

Prove[Proposition["Addition of Zero from Left"],
	using -> Definition["Addition"],
    by -> NNEqIndProver]

(If you are a Theorema alpha tester you can execute the above Prove-call and you obtain the proof generated by Theorema in a notebook with name 'Untitled-...'. If you don't have Theorema available but you have Mathematica 3.0 installed you can read the proof in the notebook Proof-Addition-0-From-Left-All-Branches.nb. If you don't have Mathematica available you can read the proof in the postscript file Proof-Addition-0-From-Left-All-Branches.nb.)

Prove[Proposition["Addition of Zero from Left"],
	using -> Definition["Addition"],
    by -> NNEqIndProver,proof–object -> "SuccessBranch"]

(You can read the proof in the notebook Proof-Addition-0-From-Left.nb  or ...ps.)

An Attempt at Complete Exploration

Let's now try to prove other equalities on 0, \(TraditionalForm\`\(□\^+\)\), + by the same method:

SetGlobals[Prover -> NNEqIndProver]

Proposition["Addition from Left",any[m, n],
	({{\(\(m\^+\) + n = \(\((m + n)\)\^+\)\), "succ+ "}})]

Prove[Proposition["Addition from Left"],using -> Definition["Addition"],proof–object -> "SuccessBranch"]

(You can read the proof in the notebook Proof-Addition-From-Left-All-Branches.nb or ...ps.)

Proposition["Associativity of Addition",any[m, n, p],
	({{(m + n) + p = m + (n + p), "( + )+ "}})]

Prove[Proposition["Associativity of Addition"],using -> Definition["Addition"],
proof–object -> "SuccessBranch"]

(You can read the proof in the notebook Proof-Addition-Associativity.nb or ...ps.)

Proposition["Commutativity of Addition",any[m, n],
	({{m + n = n + m, " + "}})]

Prove[Proposition["Commutativity of Addition"],using -> Definition["Addition"]]

This proof fails. The failure will be analyzed below. (You can read the proof attempt in the notebook Proof-Addition- Commutativity.nb or ...ps.)

Complete Exploration: Bottom-Up

Observation

A fixed prover determines, of course, for every fixed knowledge base a fixed set of provable formulae.

However, without changing the prover, the collection of provable formula can increase drastically if we add proved formulae to the knowledge base. Similarly, the length of proofs may decrease drastically by the same measure.

Also, the order in which formulae are proved (and, if proved, are added to the knowledge base) may drastically influence the proving power of the prover.

Hence, we should add a mechanism to the proof system that automatically adds proved formulae to the knowledge if sequences of goal propositions are given to a prover of the system instead of isolated goal propositions.

An Example of Adding Proved Formulae to the Knowledge Base

SetGlobals[LabelStyle -> "Alpha"]

Propositions["Equational Properties of Addition",any[m, n, p],
	({{0 + n = n, "0+ "}, {\(\(m\^+\) + n = \(\((m + n)\)\^+\)\), "^++ "}, {m + n = n + m, " + "}, {(m + n) + p = m + (n + p), "( + ) + "}})]

By setting the option 'ExpandKnowledge->True' (which forces every proved goal to be added to the knowledge base) in the Prove-call, all above propositions can be proved without changing the prover.

Prove[\(Propositions["Equational Properties of Addition"], 
	
        using -> Definition["Addition"], 
\ \ \ \ \ 
        by -> NNEqIndProver, 
        proof–object -> "SuccessBranch", 
        ExpandKnowledge -> True\)]

(The four proofs generated are stored in Proof-Sequence-Expanding-KB-1.nb through ...-4.nb and the corresponding .ps files.)

Which and How Many Formulae should we Prove for a 'Complete' Exploration?

Answer:

All propositions (in our case, equalities) that describe all interactions of the new concept with the known concepts (and with itself) are interesting goals.

Interactions that can be described in the form of rewrite rules are particular useful because they 'algorithmize' the branch of mathematics under exploration. (90 % of the mathematical knowledge is of this nature.)

Only the 'immediate' interactions need to be explored because the compound interactions are iterations of immediate interactions.

This does not yet give conjectures about the 'result' of the interactions, however!

Example Addition: immediate interactions

0 + 0 =  ?

0 + n = ?

m + 0 = ?

\(\(m\^+\) + n = ?\)

\(m + \(n\^+\) = ?\)

m + m = ?

m + n = ?

m + (n + p) = ?

(m + n) + p = ?

All other interactions are 'compound'.

One Syntactical Class At A Time

A Suggestion

An Example:

Definition["limit",
	({{(Underscript[∀ , f, a, ϵ, N])(
                  limit[f] := 
                    (Underscript[æ, a]) 
                      (Underscript[∀ 
                          , ϵ])(Underscript[∃ , N])(Underscript[( ∀ ), n]) 
                            (n ≥ N)
                                ⟹(
                                \[LeftBracketingBar]f[n] - a
                                      \[RightBracketingBar] < ϵ)
                                ), "l1:"}})]

Exploration situation:

known concepts: +, -, *, | |, <, ... on numbers,  ⊕, ⊖, ... on sequences,
          known facts: 'complete' knowledge about mutual interaction of these operations,
          new concept: limit
          axioms: the above definition
          goals: all interactions of limit with ⊕, ⊖, ...

Example of a goal:

Proposition["limit",
	({{(Underscript[∀ , f, g])(
                  limit[f⊕g] = limit[f] + limit[g]), "limit[ ⊕ ] "}})]

Proposition["limit",
	({{(Underscript[((Underscript[∀ , f, g])), is–convergent[f], is–convergent[g]])(limit[f⊕g] = limit[f] + limit[g]), "limit[ ⊕ ] "}})]

Definition[\("convergence", 
	
      ∀ \+\(f, a, ϵ, N\)\((
          is–convergent[f] := 
            \(∃ \+a\) 
              \(∀ 
                  \+ϵ\(∃ \+N\(\(\ ∀ \)\+n\) 
                    \((n ≥ N)\)⟹\((
                        \[LeftBracketingBar]f[n] - a\[RightBracketingBar] < 
                          ϵ)\)\)\))\)\)]

Suggestion: Consider one "syntactical class" at a time! In other words, apply "structured programming" principles!

Split New Notion

Definition["1-ary limit",
	({{(Underscript[∀ , f, a, ϵ, N])(
                  limit[f] := (Underscript[æ, a]) limit[f, a]), "l1:"}})]

Definition["2-ary limit",
	({{(Underscript[∀ , f, a])(
                  (limit[f, a])  := 
                    ( (Underscript[∀ , ϵ]) limit[f, a, ϵ]))
                  , "l2:"}})]

Definition["3-ary limit",
	({{(Underscript[∀ , f, a, ϵ])(
                  (limit[f, a, ϵ]) :=  
                    (Underscript[∃ , N]) limit[f, a, ϵ, N]), "l3:"}})]

Definition["4-ary limit",
	({{(Underscript[∀ , f, a, ϵ, N])(
                  (limit[f, a, ϵ, N]) := 
                    ((Underscript[( ∀ ), n]) 
                        (n ≥ N)⟹(
                            \[LeftBracketingBar]f[n] - a
                                  \[RightBracketingBar] < ϵ)))
                  , "l4:"}})]

Some Knowledge on Known Notions

Definition["sum of sequences",any[f, g, x],
	({{((f⊕g)[x]) = (f[x] + g[x]), "⊕:"}})]

Proposition["distance of sum",any[x, y, a, b, δ, ϵ],
	({{(\[LeftBracketingBar]x - a\[RightBracketingBar] < δ 
                    ∧ \[LeftBracketingBar]y - b\[RightBracketingBar] < 
                      ϵ)⟹(
                  \[LeftBracketingBar](x + y) - 
                        (a + b)\[RightBracketingBar] < 
                    δ + ϵ), "\[LeftBracketingBar]++\[RightBracketingBar]"}})]

Proposition["max",any[M, m, n],
	({{(M ≥ max[m, n])⟹(
                  M ≥ m ∧ M ≥ n), "max:"}})]

Explore Lowest Layer

Now we explore each of the "layers" separately:

Theory["4-ary limit",
	({{Definition["4-ary limit"]}, {Definition["sum of sequences"]}, {Proposition["distance of sum"]}, {Proposition["max"]}})]

Proposition["4-ary limit of sum",
	({{\(∀ \+\(f, a, δ, M, g, b, ϵ, N\)\((
                  \((limit[f, a, δ, M] ∧ 
                        limit[g, b, ϵ, N])\)
	
                    ⟹limit[f⊕g, a + b, 
                      δ + ϵ, max[M, N]])\)\), "l4+"}})]

\(SetGlobals[Prover -> PredicateProver]; $RecursionLimit = 1024; 
    SetGlobals[LabelStyle -> "Alphanumeric"]; 

    SetGlobals[SearchDepth -> 200]; SetGlobals[DebugLevel -> 0]; 
    SetGlobals[TraceLevel -> 0]\)

Prove[\(Proposition["4-ary limit of sum"], 
        using -> Theory["4-ary limit"], 
	
        ProverOptions -> {BackChaining -> True}, 
        SearchDepth -> 250\)] //Timing

(The proof is stored in Proof-Sum-4-ary-Limit.nb and ...ps.)

Explore Next Layer

Theory["3-ary limit",
	({{Definition["3-ary limit"]}, {Proposition["4-ary limit of sum"]}})]

Proposition["3-ary limit of sum",
	({{\(∀ \+\(f, a, δ, g, b, ϵ\)\((
                  \((limit[f, a, δ] ∧ limit[g, b, ϵ])\)

                    	⟹limit[f⊕g, a + b, 
                      δ + ϵ])\)\), "l3+"}})]

Prove[Proposition["3-ary limit of sum"], 
        using -> Theory["3-ary limit"], 
        ProverOptions 
          -> {BackChaining -> True, PNDLevel -> 0}, 
        SearchDepth -> 200]//Timing

Explore Next Layer

Proposition["3-ary limit of sum: variant",
	({{\(∀ \+\(f, a, g, b, ϵ\)\((
                  \((limit[f, a, ϵ/2] ∧ 
                        limit[g, b, ϵ/2])\)
	
                    ⟹limit[f⊕g, a + b, 
                      ϵ])\)\), "l3+"}})]

Theory["2-ary limit",
	({{Definition["2-ary limit"]}, {Proposition["3-ary limit of sum: variant"]}})]

Proposition["2-ary limit of sum",
	({{\(∀ \+\(f, a, g, b\)\((
                  \((limit[f, a] ∧ limit[g, b])\)
	
                    ⟹limit[f⊕g, a + b])
                  \)\), "l2+"}})]

Prove[Proposition["2-ary limit of sum"], 
        using -> Theory["2-ary limit"], 
        ProverOptions -> {BackChaining -> True}, 
        SearchDepth -> 200]//Timing

Explore Next Layer

The last layer, at this stage, cannot yet be handled in Theorema.

Theory["1-ary limit",
	({{Definition["1-ary limit"]}, {Definition["convergence"]}, {Proposition["2-ary limit of sum"]}})]

Proposition["limit",
	({{(Underscript[((Underscript[∀ , f, g])), is–convergent[f], 
                  is–convergent[g]])(
                  limit[f⊕g] = limit[f] + limit[g]), "limit[ ⊕ ] "}})]

Prove[\(Proposition[
        "limit'],using->Theory[" 1 - 
          ary\ limit 
            \*""],
					ProverOptions->{BackChaining->True},SearchDepth->200]"\)

Complete Exploration: Top-Down

Let's Be Unsystematic

Start with Higher Level Conjecture as a Challenge

In contrast to the bottom-up approach, we now start with a "challenge" for the natural induction prover for equalities that cannot yet be handled because, at this stage, some intermediate knowledge is not yet proved:

Propositions["Equational Properties of Addition",any[m, n, p],
	({{m + 0 = m, " +0"}, {\(m + \(n\^+\) = \(\((m + n)\)\^+\)\), " + ^+"}, {0 + n = n, "0+ "}, {\(\(m\^+\) + n = \(\((m + n)\)\^+\)\), "^++ "}, {(m + n) + p = m + (n + p), "( + ) + "}})]

Definition["Multiplication",any[m, n],
	({{m*0 = 0, " *0"}, {\(m*\(n\^+\) = \((m*n)\) + m\), " * ^+"}})]

Proposition["Commutativity of Multiplication",any[m, n],
	({{m*n = n*m, " * "}})]

Prove[\(Proposition["Commutativity of Multiplication"], 
	
        using -> {Definition["Multiplication"], 
            Propositions["Equational Properties of Addition"]}, \ 
	
        by -> NNEqIndProver\)]// Timing

The proof fails. (See the notebook Proof-Attempt-1-Multiplication-Commutativity.nb or ....ps.)

Failure Analysis Leads to Conjectures

An anlysis of the proof shows that, for a constant (Subscript[m, 1]), the prover would have needed the knowledge :

0=0*(Subscript[m, 1]).

Let's first prove this for arbitrary  (Subscript[m, 1]):

Proposition["Multiplication of Zero from Left",any[n],
	({{0*n = 0, "0* "}})]

Prove[\(Proposition["Multiplication of Zero from Left"], 
	
        using -> {Definition["Multiplication"], 
            Propositions["Equational Properties of Addition"]}, \ 
	
        by -> NNEqIndProver\)]// Timing

(See the notebook Proof-Multiplication-0-From-Left.nb or ...ps.)

After expansion of the knowledge base, we return to the main proof:

Prove[\(Proposition["Commutativity of Multiplication"], 
	
        using -> {Definition["Multiplication"], 
            Propositions["Equational Properties of Addition"], 
            Proposition["Multiplication of Zero from Left"]}, \ 
	
        by -> NNEqIndProver\)]// Timing

The prover fails again but at some later point. (See the notebook Proof-Attempt-2-Multiplication-Commutativity.nb or ...ps.)

An anlysis of the proof shows that, for  constants  (Subscript[m, 1]),(Subscript[n, 3])   it would have needed the knowledge :

(SuperPlus[((Subscript[m, 1])*(Subscript[n, 3])+((Subscript[n, 3])+(Subscript[m, 1])))])=(SuperPlus[((Subscript[m, 1])*(Subscript[n, 3])+((Subscript[m, 1])+(Subscript[n, 3])))])

In fact, the lhs and rhs are identical except for:

(Subscript[n, 3])+(Subscript[m, 1])=(Subscript[m, 1])+(Subscript[n, 3])

Let's, hence, first prove this for arbitrary  (Subscript[m, 1]), (Subscript[n, 3]):

Proposition["Commutativity of Addition",any[m, n],
	({{m + n = n + m, " + "}})]

In fact, we already know that this proof works with the prover NNEqIndProver.

After expansion of the knowledge base, we return to the main proof:

Prove[\(Proposition["Commutativity of Multiplication"], 
	
        using -> {Definition["Multiplication"], 
            Propositions["Equational Properties of Addition"], 
			
            Proposition["Commutativity of Addition"], 
            Proposition["Multiplication of Zero from Left"]}, \ 
	
        by -> NNEqIndProver\)]// Timing

Now, the proof works. (See the notebook Proof-Multiplication-Commutativity.nb or ...ps.)

What we can Learn From This

Given a prover and an exploration situation,

instead of exploring all possible interactions of new and old concepts systematically bottom-up (with a high chance to obtain successful proofs immediately but with the necessity of already having conjectures for the propositions to be proved),

we can "challenge" the prover with a top conjecture and analyze the failing proof, which may lead to a conjecture for a lower level proposition,   a n d   s o   o n.

A Theory Generation Cascade

Given a prover P, a fixed knowledge base K and a statement G which we want to prove, the function "Theory–Generation–Cascade" produces a theory consisting of statements that comprise all statements of K plus possibly some (hopefully many) other statements that are provable from K by P.

Theory–Generation–Cascade[G,K,P]:

Prove[G, using->K,by->P].

If proof succeeds then  resulting theory is  K⋃{G}else  (i . e .  if proof fails) analyze the points where the proof fails         and derive a conjecture C such that G might be provable by P using K⋃{C}.

        T:=Theory–Generation–Cascade[C, K, P].

        If   T=K  (i . e .  no additional theorems were provable by P 
                using K) 	            then  resulting theory is  K            else    Prove[G, using->T,by->P].

                If  proof succeeds  	                      then  resulting theory is T⋃{G} 		                 else   resulting theory is  T.

Note: Importance of displaying failing proofs!

If we have an algorithmic failure analyzer for P then the theory generation cascade turns the prover P into a more powerful prover P', which is also a theorem generator:

Prove[G,using->K,by->P']:=Theory–Generation–Cascade[G,K,P].

In the current version of Theorema this cascade is implemented, see the paper B-Buchberger-1999-Paper-Theorema-Demo which can be loaded from the home page www.risc.uni-linz.ac.at/people/buchberg/papers

The Transfer of Knowledge to the Status of Inference Rule

Let's Look to a Successful Proof

Consider the following scenario:

Complete exploration of + over 0, \(TraditionalForm\`\(□\^+\)\): Done.

Next exploration situation: * inductively defined over +.

Let's prove, for example, associativity of *, knowing already some facts about + and *:

Propositions["Equational Properties of Addition",any[m, n, p],
	({{m + 0 = m, " +0"}, {\(m + \(n\^+\) = \(\((m + n)\)\^+\)\), " + ^+"}, {0 + n = n, "0+ "}, {\(\(m\^+\) + n = \(\((m + n)\)\^+\)\), "^++ "}, {m + n = n + m, " + "}, {(m + n) + p = m + (n + p), "( + ) + "}})]

Propositions["Some Equational Properties of Multiplication",any[m, n],
	({{m*0 = 0, " *0"}, {\(m*\(n\^+\) = \((m*n)\) + m\), " *  ^+"}, {0*n = 0, "0*"}, {\(\(m\^+\)*n = \((m*n)\) + n\), " ^+*"}})]

Proposition["Associativity of Multiplication",any[m, n, p],
	({{(m*n)*p = m*(n*p), "( * ) * "}})]

Prove[\(Proposition["Associativity of Multiplication"], 
	
        using -> {
            Propositions["Some Equational Properties of Multiplication"], 
            Propositions["Equational Properties of Addition"]}, \ 
	
        by -> NNEqIndProver\)]// Timing

(See the notebook Proof-Multiplication-Associativity-with-AddAC-in-KB.nb or ...ps.)

Let's Analyze the Longest Part of the Proof

Now we analyze the longest part of the proof:

Simplification of the lhs term:

((SuperPlus[(Subscript[n, 3])])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(SuperPlus[(Subscript[p, 6])]) =   by ( *  ^+)

((SuperPlus[(Subscript[n, 3])])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 6])+((SuperPlus[(Subscript[n, 3])])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])])) =   by (( * ) * .IS.S.IS.IH)

((SuperPlus[(Subscript[n, 3])])*(Subscript[p, 6])+((Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 6]))+((SuperPlus[(Subscript[n, 3])])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])])) =   by ( *  ^+)

((SuperPlus[(Subscript[n, 3])])*(Subscript[p, 6])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6]))+((SuperPlus[(Subscript[n, 3])])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])])) =   by ( *  ^+)

((SuperPlus[(Subscript[n, 3])])*(Subscript[p, 6])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6]))+((SuperPlus[(Subscript[n, 3])])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))) =   by ( ^+*)

(((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6]))+((SuperPlus[(Subscript[n, 3])])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))) =   by (^++ )

(((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6]))+(SuperPlus[((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1])))]) =   by ( + ^+)

(SuperPlus[((((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6]))+((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))))]) =   by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1])))+(((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])))]) =   by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+(((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])))]) =   by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+(((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])))]) =   by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+(((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 6])))]) =   by (( + ) + )

(SuperPlus[((((Subscript[n, 3])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6])))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 6]))])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[n, 3])])*(SuperPlus[(Subscript[p, 6])])+((Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(SuperPlus[(Subscript[p, 6])]) =   by ( *  ^+)

((SuperPlus[(Subscript[n, 3])])*(Subscript[p, 6])+(SuperPlus[(Subscript[n, 3])]))+((Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(SuperPlus[(Subscript[p, 6])]) =   by ( *  ^+)

((SuperPlus[(Subscript[n, 3])])*(Subscript[p, 6])+(SuperPlus[(Subscript[n, 3])]))+(((Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 6])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])])) =   by ( *  ^+)

((SuperPlus[(Subscript[n, 3])])*(Subscript[p, 6])+(SuperPlus[(Subscript[n, 3])]))+(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])])) =   by ( *  ^+)

((SuperPlus[(Subscript[n, 3])])*(Subscript[p, 6])+(SuperPlus[(Subscript[n, 3])]))+(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))) =   by ( ^+*)

(((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6]))+(SuperPlus[(Subscript[n, 3])]))+(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))) =   by ( + ^+)

(SuperPlus[(((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6]))+(Subscript[n, 3]))])+(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))) =   by (^++ )

(SuperPlus[((((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6]))+(Subscript[n, 3]))+(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))))]) =   by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6])))+(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))))]) =   by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6])))+(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))))]) =   by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6])))+(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])))]) =   by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6])))+(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])))]) =   by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6])))+(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 6])))]) =   by (( + ) + )

(SuperPlus[((((Subscript[n, 3])+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6])))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 6]))]) =   by ( + )

(SuperPlus[((((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))+((Subscript[n, 3])+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6]))))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 6]))]) =   by (( + ) + )

(SuperPlus[(((((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))+(Subscript[n, 3]))+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6])))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 6]))]) =   by ( + )

(SuperPlus[((((Subscript[n, 3])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6])))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 6]))])⌋

We see that, in fact, most of the time is spent in applying associativity and commutativity of +. Furthermore, "it is clear" what the outcome of these AC-simplification steps is, i.e. we can predict the outcome, i.e. we can invent an easy algorithm that produces the outcome of these AC-simplification steps a priori:

view the term as composed of  '+' on the highest level and 'elementary terms' that start with a symbol other than '+'

put all paretheses to the left

order the elementary terms according to some fixed ordering.

Note that this algorithm is not just a reformulation of the AC-steps. "Prediction algorithms" can be arbitrarily far away from the inference rules whose effect is predicted and may involve some high-level nontrivial mathematics. (Examples: Groebner bases simplification for boolean combination of equalities over the complex numbers; Collins' algorithm for arbitrary formulae of the theory of real closed fields; etc.)

Consequence: Transfer of Knowledge to the Status of Inference Rule

Consequence: In this exploration situation, an appropriate prover should use a special "black box" inference rule for '+' applying the above prediction algorithm and not show details of applying this inference rule because this is "uninteresting" in the present exploration situation, in which our attention is on exploring '*'. In contrast, '+' is already supposed to be "completely explored".

Hence, we cancel AC for '+' in the knowledge base

Propositions["Equational Properties of Addition",any[m, n, p],
	({{m + 0 = m, " +0"}, {\(m + \(n\^+\) = \(\((m + n)\)\^+\)\), " + ^+"}, {0 + n = n, "0+ "}, {\(\(m\^+\) + n = \(\((m + n)\)\^+\)\), "^++ "}})]

and, instead, add AC of addition as a special inference rule:

Prove[\(Proposition["Associativity of Multiplication"], 
	
        using -> {
            Propositions["Some Equational Properties of Multiplication"], 
            Propositions["Equational Properties of Addition"]}, \ 
	
        built–in -> {
            Property[\(+\( -> {Associative, Commutative}\)\)]}, 
	
        by -> NNEqIndProver, 
        proof–object -> "SuccessBranch"\)]// Timing

(See the notebook Proof-Multiplication-Associativity-with-AddAC-as-Inference-Rule.nb or ...ps.)

Of course, adding AC for addition as an inference rule needs extra programming work in the prover, it does not "come for free". The critical part of the proof now looks as follows:

Simplification of the lhs term:

(SuperPlus[(Subscript[p, 5])])+((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*(SuperPlus[(Subscript[p, 5])]) =   by (Special Simpl)

((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*(SuperPlus[(Subscript[p, 5])])+(SuperPlus[(Subscript[p, 5])]) =   by ( *  ^+)

(((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*(Subscript[p, 5])+((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3]))))+(SuperPlus[(Subscript[p, 5])]) =   by (Special Simpl)

((Subscript[m, 1])+((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*(Subscript[p, 5]))))+(SuperPlus[(Subscript[p, 5])]) =   by ( + ^+)

(SuperPlus[(((Subscript[m, 1])+((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*(Subscript[p, 5]))))+(Subscript[p, 5]))]) =   by (Special Simpl)

(SuperPlus[((Subscript[m, 1])+((Subscript[n, 3])+(((Subscript[p, 5])+((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*(Subscript[p, 5]))+(Subscript[m, 1])*(Subscript[n, 3]))))]) =   by (( * ) * .IS.S.IS.S.IH)

(SuperPlus[((Subscript[m, 1])+((Subscript[n, 3])+(((Subscript[p, 5])+((Subscript[n, 3])*(Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5])))+(Subscript[m, 1])*(Subscript[n, 3]))))]) =   by (Special Simpl )

(SuperPlus[((Subscript[m, 1])+((Subscript[n, 3])+((Subscript[p, 5])+((Subscript[m, 1])*(Subscript[n, 3])+((Subscript[n, 3])*(Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))))))])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[p, 5])])+((Subscript[n, 3])*(SuperPlus[(Subscript[p, 5])])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(SuperPlus[(Subscript[p, 5])])) =   by (Special Simpl)

(Subscript[n, 3])*(SuperPlus[(Subscript[p, 5])])+(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(SuperPlus[(Subscript[p, 5])])+(SuperPlus[(Subscript[p, 5])])) =   by ( *  ^+)

((Subscript[n, 3])*(Subscript[p, 5])+(Subscript[n, 3]))+(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(SuperPlus[(Subscript[p, 5])])+(SuperPlus[(Subscript[p, 5])])) =   by (Special Simpl)

(Subscript[n, 3])+(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(SuperPlus[(Subscript[p, 5])])+((SuperPlus[(Subscript[p, 5])])+(Subscript[n, 3])*(Subscript[p, 5]))) =   by ( *  ^+)

(Subscript[n, 3])+((((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+((SuperPlus[(Subscript[p, 5])])+(Subscript[n, 3])*(Subscript[p, 5]))) =   by (Special Simpl)

((Subscript[m, 1])+((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+((Subscript[n, 3])*(Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5])))))+(SuperPlus[(Subscript[p, 5])]) =   by ( + ^+)

(SuperPlus[(((Subscript[m, 1])+((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+((Subscript[n, 3])*(Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5])))))+(Subscript[p, 5]))]) =   by (Special Simpl )

(SuperPlus[((Subscript[m, 1])+((Subscript[n, 3])+((Subscript[p, 5])+((Subscript[m, 1])*(Subscript[n, 3])+((Subscript[n, 3])*(Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))))))])⌋

One sees that long sequences of AC-steps for addition have been replaced by one invocation of the AC-simplifier for addition (marked by '(Special Simpl)').  The proof becomes faster, shorter and easier to read.

This Transfer Principle is Ubiquitous in Human Practical Proving

If one ananlyzes lots of "real-life" exploration situations, one detects that this transfer principle is not an exotic and special happening but, rather, the main principle by which human exploration of entire theories in the definition-proposition-proof style becomes practically feasible.

Other examples:

In fact, we already tacitly applied this principle right at the beginning when we formulated induction as a proof method instead of putting induction axioms to the knowledge base and using a general predicate logic prover.

Explore properties of Σ as a function, then introduce Σ as a quantifier and transfer the properties proved about the function Σ into special inference rules for the quantifier Σ.

Go further and develop an algebraic theory and a corresponding algorithm for checking the identity of Σ-expressions, see the Zeilberger-Paule-... theory. Call to this algorithm "whenever appropriate". (See the demo of the Zeilberger-Paule-method in the paper B-Buchberger-1999-Paper-Theorema-Demo which can be loaded from the home page www.risc.uni-linz.ac.at /people/buchberg/papers.)

Explore rewrite properties of 'lim', 'df/dx', '∫' first for these functions. Then introduce the corresponding quantifiers and transfer the properties proved about the functions into special inference rules for the quantifiers.

Go further and develop an algebraic theory and a corresponding algorithm for checking the integrability of certain classes of functions defined by certain classes of expressions, see Risch, ... . Call to this algorithm "whenever appropriate".

Develop a theory of polynomial ideal membership and a membership (congruence, ...) algorithm based on it, see the author's Groebner bases theory. Call this algorithm "whenever appropriate". (See the demo of the Groebner-bases-method below and in the paper B-Buchberger-1999-Paper-Theorema-Demo which can be downloaded from the home page www.risc.uni-linz.ac.at /people/buchberg/papers.)

Develop a theory of "cylindric algebraic decompositions" of the real space w.r.t. systems of polynomials and develop an algorithm based on it for checking the truth of arbitrary formulae of the theory of real closed fields, see Collins, .... Call this algorithm "whenever appropriate".

Needs["Theorema`Provers`UserProvers`GroebnerBasesProver`"]

Formula["GB-Test",any[x, y],
	({{\(\((\((\(x\^3\) y\^4 + 27  xy\^3 - 15  x\^3 = 0)\) ∧ 
                    \((\(1\/5\) \(x\^2\) y - 23  x\ y + 17 = 0)\))\) 
                \[Implies] 
	
                \((225\ x\^3 + \(-405\)\ xy\^3 + 255\ x\ y + 
                      \(-15\)\ x\^4\ y + 27\ x\ xy\^3\ y + 
                      \(-328\)\ x\^2\ y\^2 + 3\ x\^3\ y\^2 + 
                      \(-23\)\ x\^3\ y\^3 + \(x\^4\ y\^3\)\/5 + 
                      \(-15\)\ x\^3\ y\^4 + x\^4\ y\^5 = 0)\)\), "f=0"}})]

Prove[Formula["GB-Test"], by -> GroebnerBasesProver] // Timing

(See the notebook Proof-by-Groebner-Bases.nb or ...ps.)

There is a seamless transition from near-at-hand special inference rules to gigantic black box decision procedures for special classes of formulae. However, the logics of integrating special inference mechanisms is always the same.

A Logically Sound Integration of Special Inferencing

We start from one logic system, e.g. a variant of higher order predicate logic. For this system we have a semantical notion of logical consequence.

Whenever we establish a special prover P, we must specify two essential things:

the class of knowledge bases and goals for which P can be applied

the "tacit (implicit, built-in, ...) theory" T under which correctness of P is guaranteed.

In more detail: For a correct special prover P for the theory T the following correctness theorem for T must be proved:

If P proves G from K, then G must be a logical consequence of K and T.

The correctness theorem for T is a meta-theorem.

For many important special provers (various special simplifiers, Collins' method, Groebner Bases method, Zeilberger method, ...) the correctness theorem is well established in the mathematical literature.

These proofs could also be given using a formalization of (parts of) logic within the proof system itself. (A challenge! Example: Formal proof of Groebner bases theory is one of the motivations for Theorema.)

However, note that the proof of the correctness theorem for the special prover P will normally be much harder then the proofs of the theorems that are automatically proved by P. ("A practical version of Goedel's second theorem".)

Avoiding Correctness Proofs for Special Provers

Formal proofs of the correctness theorem for provers (as for any other algorithms) - and their implementation ! -  may be difficult.

Most people just "trust" the correctness of special proof technique proved "manually" in the literature and "carefully implemented" using the literature.

One can, however, also consider a special proof technique as a "conjecture generating black box". For each "proof" π generated by a prover relying on the special proof technique one would then have to check the correctness of each black box step by proving it by a prover that does not rely on the special proof technique but on a general proof technique with the corresponding implicit theory T in the knowledge base.

Conclusion

We argued that, for "real-life" application of proving / solving / computing systems, these systems should support the "theory exploration" paradigm rather than concentrate only on the "isolated theorem proving" paradigm.   (Example: At CADE, we need a "Computer-supported theory exploration" competition in addition to the "single theorem proving" competition!)

We discussed some strategies and approaches to facilitate theory exploration:

Practical facilities for manipulating large amounts of formal text.

Establishing provers that are "appropriate" for a given exploration situation.

Complete exploration by bottom-up analysis of all possible interactions (hopefully in the form of algorithmic formulae)  of new concepts with given concepts.

Decomposition of goals with nested alternating quantifiers.

Top-down conjectures generation by challenging provers and (automated) analysis of failing proofs (the "cascade").

Transfer of knowledge to the status of proof methods as the main principle for "human-like" exploration and generation of short proofs.

Importance of a uniform semantics for a clear understanding and manipulation of the correctness of special provers.

Appendix: Proofs

Proof Addition 0 From Left - All Branches

Prove:

under the assumptions:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: failed

The proof of (0+ ) fails.(The Simplifier was unable to transform the proof situation.)

Alternative proof 2: proved

We prove (0+ ) by  induction on n.

Induction Base:

A proof by simplification of (1) works.

Simplification of the lhs term:

0 + 0 =  by ( +0)

0⌋

Simplification of the rhs term:

0⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

A proof by simplification of (3) works.

Simplification of the lhs term:

0+(SuperPlus[(Subscript[n, 1])]) =  by ( +succ)

(SuperPlus[(0+(Subscript[n, 1]))]) =  by (2)

(SuperPlus[(Subscript[n, 1])])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[n, 1])])⌋

Proof Addition 0 From Left

Prove:

under the assumptions:

We prove (0+ ) by  induction on n.

Induction Base:

A proof by simplification of (1) works.

Simplification of the lhs term:

0 + 0 =  by ( +0)

0⌋

Simplification of the rhs term:

0⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

A proof by simplification of (3) works.

Simplification of the lhs term:

0+(SuperPlus[(Subscript[n, 1])]) =  by ( +succ)

(SuperPlus[(0+(Subscript[n, 1]))]) =  by (2)

(SuperPlus[(Subscript[n, 1])])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[n, 1])])⌋

Proof Addition From Left

Prove:

under the assumptions:

We prove (succ+ ) by  induction on m.

Induction Base:

We prove (1) by  induction on n.

Induction Base:

A proof by simplification of (4) works.

Simplification of the lhs term:

\(\(0\^+\) + 0\) =  by ( +0)

\(\(0\^+\)\)⌋

Simplification of the rhs term:

\(\(\((0 + 0)\)\^+\)\) =  by ( +0)

\(\(0\^+\)\)⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

A proof by simplification of (6) works.

Simplification of the lhs term:

\(0\^+\)+(SuperPlus[(Subscript[n, 2])]) =  by ( +succ)

(SuperPlus[(\(0\^+\)+(Subscript[n, 2]))]) =  by (5)

(SuperPlus[((SuperPlus[(0+(Subscript[n, 2]))]))])⌋

Simplification of the rhs term:

(SuperPlus[(0+(SuperPlus[(Subscript[n, 2])]))]) =  by ( +succ)

(SuperPlus[((SuperPlus[(0+(Subscript[n, 2]))]))])⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

We take in (3) all variables arbitrary but fixed:

and simplify it.

Simplification of the lhs term:

(SuperPlus[((SuperPlus[(Subscript[m, 1])]))])+(Subscript[n, 3])⌋

Simplification of the rhs term:

(SuperPlus[((SuperPlus[(Subscript[m, 1])])+(Subscript[n, 3]))]) =  by (2)

(SuperPlus[((SuperPlus[((Subscript[m, 1])+(Subscript[n, 3]))]))])⌋

Hence, it is sufficient to prove:

We prove (8) by  induction on n.

Induction Base:

A proof by simplification of (9) works.

Simplification of the lhs term:

(SuperPlus[((SuperPlus[(Subscript[m, 1])]))])+0 =  by ( +0)

(SuperPlus[((SuperPlus[(Subscript[m, 1])]))])⌋

Simplification of the rhs term:

(SuperPlus[((SuperPlus[((Subscript[m, 1])+0)]))]) =  by ( +0)

(SuperPlus[((SuperPlus[(Subscript[m, 1])]))])⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

A proof by simplification of (11) works.

Simplification of the lhs term:

(SuperPlus[((SuperPlus[(Subscript[m, 1])]))])+(SuperPlus[(Subscript[n, 4])]) =  by ( +succ)

(SuperPlus[((SuperPlus[((SuperPlus[(Subscript[m, 1])]))])+(Subscript[n, 4]))]) =  by (10)

(SuperPlus[((SuperPlus[((SuperPlus[((Subscript[m, 1])+(Subscript[n, 4]))]))]))])⌋

Simplification of the rhs term:

(SuperPlus[((SuperPlus[((Subscript[m, 1])+(SuperPlus[(Subscript[n, 4])]))]))]) =  by ( +succ)

(SuperPlus[((SuperPlus[((SuperPlus[((Subscript[m, 1])+(Subscript[n, 4]))]))]))])⌋

Proof Addition Associativity

Prove:

under the assumptions:

We prove (( + )+ ) by  induction on m.

Induction Base:

We prove (1) by  induction on n.

Induction Base:

We take in (4) all variables arbitrary but fixed:

and simplify it.

Simplification of the lhs term:

(0 + 0)+(Subscript[p, 2]) =  by ( +0)

0+(Subscript[p, 2])⌋

Simplification of the rhs term:

0+(0+(Subscript[p, 2]))⌋

Hence, it is sufficient to prove:

We prove (8) by  induction on p.

Induction Base:

A proof by simplification of (9) works.

Simplification of the lhs term:

0 + 0⌋

Simplification of the rhs term:

0 + (0 + 0) =  by ( +0)

0 + 0⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

A proof by simplification of (11) works.

Simplification of the lhs term:

0+(SuperPlus[(Subscript[p, 3])]) =  by ( +succ)

(SuperPlus[(0+(Subscript[p, 3]))])⌋

Simplification of the rhs term:

0+(0+(SuperPlus[(Subscript[p, 3])])) =  by ( +succ)

0+(SuperPlus[(0+(Subscript[p, 3]))]) =  by ( +succ)

(SuperPlus[(0+(0+(Subscript[p, 3])))]) =  by (10)

(SuperPlus[(0+(Subscript[p, 3]))])⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

We take in (6) all variables arbitrary but fixed:

and simplify it.

Simplification of the lhs term:

(0+(SuperPlus[(Subscript[n, 2])]))+(Subscript[p, 4]) =  by ( +succ)

(SuperPlus[(0+(Subscript[n, 2]))])+(Subscript[p, 4])⌋

Simplification of the rhs term:

0+((SuperPlus[(Subscript[n, 2])])+(Subscript[p, 4]))⌋

Hence, it is sufficient to prove:

We prove (13) by  induction on p.

Induction Base:

A proof by simplification of (14) works.

Simplification of the lhs term:

(SuperPlus[(0+(Subscript[n, 2]))])+0 =  by ( +0)

(SuperPlus[(0+(Subscript[n, 2]))])⌋

Simplification of the rhs term:

0+((SuperPlus[(Subscript[n, 2])])+0) =  by ( +0)

0+(SuperPlus[(Subscript[n, 2])]) =  by ( +succ)

(SuperPlus[(0+(Subscript[n, 2]))])⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

A proof by simplification of (16) works.

Simplification of the lhs term:

(SuperPlus[(0+(Subscript[n, 2]))])+(SuperPlus[(Subscript[p, 5])]) =  by ( +succ)

(SuperPlus[((SuperPlus[(0+(Subscript[n, 2]))])+(Subscript[p, 5]))])⌋

Simplification of the rhs term:

0+((SuperPlus[(Subscript[n, 2])])+(SuperPlus[(Subscript[p, 5])])) =  by ( +succ)

0+(SuperPlus[((SuperPlus[(Subscript[n, 2])])+(Subscript[p, 5]))]) =  by ( +succ)

(SuperPlus[(0+((SuperPlus[(Subscript[n, 2])])+(Subscript[p, 5])))]) =  by (15)

(SuperPlus[((SuperPlus[(0+(Subscript[n, 2]))])+(Subscript[p, 5]))])⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

We prove (3) by  induction on n.

Induction Base:

We take in (17) all variables arbitrary but fixed:

and simplify it.

Simplification of the lhs term:

((SuperPlus[(Subscript[m, 1])])+0)+(Subscript[p, 7]) =  by ( +0)

(SuperPlus[(Subscript[m, 1])])+(Subscript[p, 7])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[m, 1])])+(0+(Subscript[p, 7]))⌋

Hence, it is sufficient to prove:

We prove (21) by  induction on p.

Induction Base:

A proof by simplification of (22) works.

Simplification of the lhs term:

(SuperPlus[(Subscript[m, 1])])+0⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[m, 1])])+(0 + 0) =  by ( +0)

(SuperPlus[(Subscript[m, 1])])+0⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

A proof by simplification of (24) works.

Simplification of the lhs term:

(SuperPlus[(Subscript[m, 1])])+(SuperPlus[(Subscript[p, 8])]) =  by ( +succ)

(SuperPlus[((SuperPlus[(Subscript[m, 1])])+(Subscript[p, 8]))])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[m, 1])])+(0+(SuperPlus[(Subscript[p, 8])])) =  by ( +succ)

(SuperPlus[(Subscript[m, 1])])+(SuperPlus[(0+(Subscript[p, 8]))]) =  by ( +succ)

(SuperPlus[((SuperPlus[(Subscript[m, 1])])+(0+(Subscript[p, 8])))]) =  by (23)

(SuperPlus[((SuperPlus[(Subscript[m, 1])])+(Subscript[p, 8]))])⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

We take in (19) all variables arbitrary but fixed:

and simplify it.

Simplification of the lhs term:

((SuperPlus[(Subscript[m, 1])])+(SuperPlus[(Subscript[n, 4])]))+(Subscript[p, 9]) =  by ( +succ)

(SuperPlus[((SuperPlus[(Subscript[m, 1])])+(Subscript[n, 4]))])+(Subscript[p, 9])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[m, 1])])+((SuperPlus[(Subscript[n, 4])])+(Subscript[p, 9]))⌋

Hence, it is sufficient to prove:

We prove (26) by  induction on p.

Induction Base:

A proof by simplification of (27) works.

Simplification of the lhs term:

(SuperPlus[((SuperPlus[(Subscript[m, 1])])+(Subscript[n, 4]))])+0 =  by ( +0)

(SuperPlus[((SuperPlus[(Subscript[m, 1])])+(Subscript[n, 4]))])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[m, 1])])+((SuperPlus[(Subscript[n, 4])])+0) =  by ( +0)

(SuperPlus[(Subscript[m, 1])])+(SuperPlus[(Subscript[n, 4])]) =  by ( +succ)

(SuperPlus[((SuperPlus[(Subscript[m, 1])])+(Subscript[n, 4]))])⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

A proof by simplification of (29) works.

Simplification of the lhs term:

(SuperPlus[((SuperPlus[(Subscript[m, 1])])+(Subscript[n, 4]))])+(SuperPlus[(Subscript[p, 10])]) =  by ( +succ)

(SuperPlus[((SuperPlus[((SuperPlus[(Subscript[m, 1])])+(Subscript[n, 4]))])+(Subscript[p, 10]))])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[m, 1])])+((SuperPlus[(Subscript[n, 4])])+(SuperPlus[(Subscript[p, 10])])) =  by ( +succ)

(SuperPlus[(Subscript[m, 1])])+(SuperPlus[((SuperPlus[(Subscript[n, 4])])+(Subscript[p, 10]))]) =  by ( +succ)

(SuperPlus[((SuperPlus[(Subscript[m, 1])])+((SuperPlus[(Subscript[n, 4])])+(Subscript[p, 10])))]) =  by (28)

(SuperPlus[((SuperPlus[((SuperPlus[(Subscript[m, 1])])+(Subscript[n, 4]))])+(Subscript[p, 10]))])⌋

Proof  Attempt Addition Commutativity

Prove:

under the assumptions:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: failed

The proof of ( + )  fails.(The Simplifier was unable to transform the proof situation.)

Alternative proof 2: failed

We try to prove ( + ) by  induction on m.

Induction Base:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: proved

We take in (1) all variables arbitrary but fixed:

and simplify it.

Simplification of the lhs term:

0+(Subscript[n, 1])⌋

Simplification of the rhs term:

(Subscript[n, 1])+0 =  by ( +0)

(Subscript[n, 1])⌋

Hence, it is sufficient to prove:

We prove (5) by  induction on n.

Induction Base:

A proof by simplification of (6) works.

Simplification of the lhs term:

0 + 0 =  by ( +0)

0⌋

Simplification of the rhs term:

0⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

A proof by simplification of (8) works.

Simplification of the lhs term:

0+(SuperPlus[(Subscript[n, 2])]) =  by ( +succ)

(SuperPlus[(0+(Subscript[n, 2]))]) =  by (7)

(SuperPlus[(Subscript[n, 2])])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[n, 2])])⌋

Alternative proof 2: pending

Pending proof of (1).

Induction Step:

Induction Hypothesis:

Induction Conclusion:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: failed

We take in (3) all variables arbitrary but fixed:

and simplify it.

Simplification of the lhs term:

(SuperPlus[(Subscript[m, 1])])+(Subscript[n, 3])⌋

Simplification of the rhs term:

(Subscript[n, 3])+(SuperPlus[(Subscript[m, 1])]) =  by ( +succ)

(SuperPlus[((Subscript[n, 3])+(Subscript[m, 1]))]) =  by (2)

(SuperPlus[((Subscript[m, 1])+(Subscript[n, 3]))])⌋

Hence, it is sufficient to prove:

We try to prove (10) by  induction on n.

Induction Base:

We simplify (11).

Simplification of the lhs term:

(SuperPlus[(Subscript[m, 1])])+0 =  by ( +0)

(SuperPlus[(Subscript[m, 1])])⌋

Simplification of the rhs term:

(SuperPlus[((Subscript[m, 1])+0)]) = by (2)

(SuperPlus[(0+(Subscript[m, 1]))])⌋

Hence, it is sufficient to prove:

The proof of (14) fails.(No applicable inference rule was found.)

Induction Step:

Induction Hypothesis:

Induction Conclusion:

Pending proof of (13).

Alternative proof 2: failed

We try to prove (3) by  induction on n.

Induction Base:

We simplify (15).

Simplification of the lhs term:

(SuperPlus[(Subscript[m, 1])])+0 =  by ( +0)

(SuperPlus[(Subscript[m, 1])])⌋

Simplification of the rhs term:

0+(SuperPlus[(Subscript[m, 1])]) =  by ( +succ)

(SuperPlus[(0+(Subscript[m, 1]))])⌋

Hence, it is sufficient to prove:

The proof of (18)fails.(No applicable inference rule was found.)

Induction Step:

Induction Hypothesis:

Induction Conclusion:

Pending proof of (17).

Proof  Sequence Expanding KB - 1

Prove:

under the assumptions:

We prove (0+ ) by  induction on n.

Induction Base:

A proof by simplification of (0+ .IB) works.

Simplification of the lhs term:

0 + 0 =  by ( +0)

0⌋

Simplification of the rhs term:

0⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

A proof by simplification of (0+ .IS) works.

Simplification of the lhs term:

0+(SuperPlus[(Subscript[n, 1])]) =  by ( +succ)

(SuperPlus[(0+(Subscript[n, 1]))]) =  by (0+ .IH)

(SuperPlus[(Subscript[n, 1])])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[n, 1])])⌋

Proof  Sequence Expanding KB - 2

Prove:

under the assumptions:

We prove (^++ ) by  induction on m.

Induction Base:

We take in (^++ .IB) all variables arbitrary but fixed:

and simplify it.

Simplification of the lhs term:

\(0\^+\)+(Subscript[n, 1])⌋

Simplification of the rhs term:

(SuperPlus[(0+(Subscript[n, 1]))]) =  by (0+ )

(SuperPlus[(Subscript[n, 1])])⌋

Hence, it is sufficient to prove:

We prove (^++ .IB.S) by  induction on n.

Induction Base:

A proof by simplification of (^++ .IB.S.IB) works.

Simplification of the lhs term:

\(\(0\^+\) + 0\) =  by ( +0)

\(\(0\^+\)\)⌋

Simplification of the rhs term:

\(\(0\^+\)\)⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

A proof by simplification of (^++ .IB.S.IS) works.

Simplification of the lhs term:

\(0\^+\)+(SuperPlus[(Subscript[n, 2])]) =  by ( +succ)

(SuperPlus[(\(0\^+\)+(Subscript[n, 2]))]) =  by (^++ .IB.S.IH)

(SuperPlus[((SuperPlus[(Subscript[n, 2])]))])⌋

Simplification of the rhs term:

(SuperPlus[((SuperPlus[(Subscript[n, 2])]))])⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

We take in (^++ .IS) all variables arbitrary but fixed:

and simplify it.

Simplification of the lhs term:

(SuperPlus[((SuperPlus[(Subscript[m, 1])]))])+(Subscript[n, 3])⌋

Simplification of the rhs term:

(SuperPlus[((SuperPlus[(Subscript[m, 1])])+(Subscript[n, 3]))]) =  by (^++ .IH)

(SuperPlus[((SuperPlus[((Subscript[m, 1])+(Subscript[n, 3]))]))])⌋

Hence, it is sufficient to prove:

We prove (^++ .IS.S) by  induction on n.

Induction Base:

A proof by simplification of (^++ .IS.S.IB) works.

Simplification of the lhs term:

(SuperPlus[((SuperPlus[(Subscript[m, 1])]))])+0 =  by ( +0)

(SuperPlus[((SuperPlus[(Subscript[m, 1])]))])⌋

Simplification of the rhs term:

(SuperPlus[((SuperPlus[((Subscript[m, 1])+0)]))]) =  by ( +0)

(SuperPlus[((SuperPlus[(Subscript[m, 1])]))])⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

A proof by simplification of (^++ .IS.S.IS) works.

Simplification of the lhs term:

(SuperPlus[((SuperPlus[(Subscript[m, 1])]))])+(SuperPlus[(Subscript[n, 4])]) =  by ( +succ)

(SuperPlus[((SuperPlus[((SuperPlus[(Subscript[m, 1])]))])+(Subscript[n, 4]))]) =  by (^++ .IS.S.IH)

(SuperPlus[((SuperPlus[((SuperPlus[((Subscript[m, 1])+(Subscript[n, 4]))]))]))])⌋

Simplification of the rhs term:

(SuperPlus[((SuperPlus[((Subscript[m, 1])+(SuperPlus[(Subscript[n, 4])]))]))]) =  by ( +succ)

(SuperPlus[((SuperPlus[((SuperPlus[((Subscript[m, 1])+(Subscript[n, 4]))]))]))])⌋

Proof  Sequence Expanding KB - 3

Prove:

under the assumptions:

We prove ( + ) by  induction on m.

Induction Base:

We take in ( + .IB) all variables arbitrary but fixed and prove:

A proof by simplification of ( + .IB.F) works.

Simplification of the lhs term:

0+(Subscript[n, 1]) =  by (0+ )

(Subscript[n, 1])⌋

Simplification of the rhs term:

(Subscript[n, 1])+0 =  by ( +0)

(Subscript[n, 1])⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

We take in ( + .IS) all variables arbitrary but fixed and prove:

A proof by simplification of ( + .IS.F) works.

Simplification of the lhs term:

(SuperPlus[(Subscript[m, 1])])+(Subscript[n, 2]) =  by (^++ )

(SuperPlus[((Subscript[m, 1])+(Subscript[n, 2]))])⌋

Simplification of the rhs term:

(Subscript[n, 2])+(SuperPlus[(Subscript[m, 1])]) =  by ( +succ)

(SuperPlus[((Subscript[n, 2])+(Subscript[m, 1]))]) =  by ( + .IH)

(SuperPlus[((Subscript[m, 1])+(Subscript[n, 2]))])⌋

Proof  Sequence Expanding KB - 4

Prove:

under the assumptions:

We take in (( + ) + ) all variables arbitrary but fixed:

and simplify it.

Simplification of the lhs term:

((Subscript[m, 0])+(Subscript[n, 0]))+(Subscript[p, 0]) =  by ( + )

(Subscript[p, 0])+((Subscript[m, 0])+(Subscript[n, 0]))⌋

Simplification of the rhs term:

(Subscript[m, 0])+((Subscript[n, 0])+(Subscript[p, 0]))⌋

Hence, it is sufficient to prove:

We prove (( + ) + .S) by  induction on m.

Induction Base:

We take in (( + ) + .S.IB) all variables arbitrary but fixed and prove:

A proof by simplification of (( + ) + .S.IB.F) works.

Simplification of the lhs term:

(Subscript[p, 1])+(0+(Subscript[n, 1])) =  by (0+ )

(Subscript[p, 1])+(Subscript[n, 1]) =  by ( + )

(Subscript[n, 1])+(Subscript[p, 1])⌋

Simplification of the rhs term:

0+((Subscript[n, 1])+(Subscript[p, 1])) =  by (0+ )

(Subscript[n, 1])+(Subscript[p, 1])⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

We take in (( + ) + .S.IS) all variables arbitrary but fixed and prove:

A proof by simplification of (( + ) + .S.IS.F) works.

Simplification of the lhs term:

(Subscript[p, 2])+((SuperPlus[(Subscript[m, 1])])+(Subscript[n, 2])) =  by ( + )

(Subscript[p, 2])+((Subscript[n, 2])+(SuperPlus[(Subscript[m, 1])])) =  by ( +succ)

(Subscript[p, 2])+(SuperPlus[((Subscript[n, 2])+(Subscript[m, 1]))]) =  by ( + )

(Subscript[p, 2])+(SuperPlus[((Subscript[m, 1])+(Subscript[n, 2]))]) =  by ( +succ)

(SuperPlus[((Subscript[p, 2])+((Subscript[m, 1])+(Subscript[n, 2])))])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[m, 1])])+((Subscript[n, 2])+(Subscript[p, 2])) =  by (^++ )

(SuperPlus[((Subscript[m, 1])+((Subscript[n, 2])+(Subscript[p, 2])))]) =  by (( + ) + .S.IH)

(SuperPlus[((Subscript[p, 2])+((Subscript[m, 1])+(Subscript[n, 2])))])⌋

Proof  Sum 4-ary Limit

Prove:

under the assumptions:

For proving (l4+) we take all variables arbitrary but fixed and prove:

We prove (l4+') by the deduction rule.

We assume

and show

The conjunction (l4+'.A) splits into (l4+'.A.1), (l4+'.A.2).

For proving (l4+'.C), by the definition (l4:), it suffices to prove:

The formula (l4+'.A.1) is expanded by the definition (l4:) into:

The formula (l4+'.A.2) is expanded by the definition (l4:) into:

For proving (l4+'.C') we take all variables arbitrary but fixed and prove:

We prove (l4+'.C'') by the deduction rule.

We assume

and show

Using (⊕:), the goal (l4+'.C''.C) is transformed into:

For proving (l4+'.C''.C'), by (|++|), it suffices to prove

We prove the individual conjunctive parts of (l4+'.C''.C'.A):

Proof of (l4+'.C''.C'.A.1) |(Subscript[f, 0])[(Subscript[n, 0])]-(Subscript[a, 0])|<(Subscript[δ, 0]):

For proving (l4+'.C''.C'.A.1), by (l4+'.A.1'), it suffices to prove

From (l4+'.C''.A), by (max:), we obtain:

The conjunction (max:/1) splits into (max:/1.1), (max:/1.2).

Formula (l4+'.C''.C'.A.1.A) is true because it is identical to (max:/1.1).

Proof of (l4+'.C''.C'.A.2) |(Subscript[g, 0])[(Subscript[n, 0])]-(Subscript[b, 0])|<(Subscript[ϵ, 0]):

For proving (l4+'.C''.C'.A.2), by (l4+'.A.2'), it suffices to prove

From (l4+'.C''.A), by (max:), we obtain:

The conjunction (max:/13) splits into (max:/13.1), (max:/13.2).

Formula (l4+'.C''.C'.A.2.A) is true because it is identical to (max:/13.2).

Proof  Sum 3-ary Limit

Prove:

under the assumptions:

For proving (l3+) we take all variables arbitrary but fixed and prove:

We prove (l3+') by the deduction rule.

We assume

and show

The conjunction (l3+'.A) splits into (l3+'.A.1), (l3+'.A.2).

For proving (l3+'.C), by the definition (l3:), it suffices to prove:

The formula (l3+'.A.1) is expanded by the definition (l3:) into:

By (l3+'.A.1') we can take appropriate values such that:

The formula (l3+'.A.2) is expanded by the definition (l3:) into:

By (l3+'.A.2') we can take appropriate values such that:

Because a literal of the formula (l4+) matches the goal (l3+'.C'), we specialize it to:

For proving (l3+'.C'), by (l3+'.C''), it suffices to prove

Because (l3+'.A.1'') matches a part of (l3+'.C'.A), we can proceed in several ways.

Alternative proof 1: proved

For proving (l3+'.C'.A) it is sufficient to prove:

Because (l3+'.A.2'') matches a part of (l3+'.C'.A/2), we can proceed in several ways.

Alternative proof 1: proved

For proving (l3+'.C'.A/2) it is sufficient to prove:

We prove the individual conjunctive parts of (l3+'.C'.A/2/1):

Proof of (l3+'.C'.A/2/1.1) limit[(Subscript[f, 0]),(Subscript[a, 0]),(Subscript[δ, 0]),(Subscript[N, 0])]:

Formula (l3+'.C'.A/2/1.1) is true because it is identical to (l3+'.A.1'').

Proof of (l3+'.C'.A/2/1.2) limit[(Subscript[g, 0]),(Subscript[b, 0]),(Subscript[ϵ, 0]),(Subscript[N, 1])]:

Formula (l3+'.C'.A/2/1.2) is true because it is identical to (l3+'.A.2'').

Alternative proof 2: pending

Pending proof of (l3+'.C'.A/2).

Alternative proof 2: pending

Pending proof of (l3+'.C'.A).

Proof  Sum 2-ary Limit

Prove:

under the assumptions:

For proving (l2+) we take all variables arbitrary but fixed and prove:

We prove (l2+') by the deduction rule.

We assume

and show

The conjunction (l2+'.A) splits into (l2+'.A.1), (l2+'.A.2).

For proving (l2+'.C), by the definition (l2:), it suffices to prove:

The formula (l2+'.A.1) is expanded by the definition (l2:) into:

The formula (l2+'.A.2) is expanded by the definition (l2:) into:

For proving (l2+'.C') we take all variables arbitrary but fixed and prove:

For proving (l2+'.C''), by (l3+), it suffices to prove

We prove the individual conjunctive parts of (l2+'.C''.A):

Proof of (l2+'.C''.A.1) limit[(Subscript[f, 0]),(Subscript[a, 0]),(((Subscript[ϵ, 0]))/2)]:

Formula (l2+'.C''.A.1) is proved because it is an instance of (l2+'.A.1').

Proof of (l2+'.C''.A.2) limit[(Subscript[g, 0]),(Subscript[b, 0]),(((Subscript[ϵ, 0]))/2)]:

Formula (l2+'.C''.A.2) is proved because it is an instance of (l2+'.A.2').

Proof  Attempt 1- Multiplication Commutativity

Prove:

under the assumptions:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: failed

The proof of ( * ) fails.(The Simplifier was unable to transform the proof situation.)

Alternative proof 2: failed

We try to prove ( * ) by  induction on m.

Induction Base:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: proved

We take in ( * .IB) all variables arbitrary but fixed:

and simplify it.

Simplification of the lhs term:

0*(Subscript[n, 1])⌋

Simplification of the rhs term:

(Subscript[n, 1])*0 =  by ( *0)

0⌋

Hence, it is sufficient to prove:

We prove ( * .IB.S) by  induction on n.

Induction Base:

A proof by simplification of ( * .IB.S.IB) works.

Simplification of the lhs term:

0*0 =  by ( *0)

0⌋

Simplification of the rhs term:

0⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

A proof by simplification of ( * .IB.S.IS) works.

Simplification of the lhs term:

0*(SuperPlus[(Subscript[n, 2])]) =  by ( * ^+)

0*(Subscript[n, 2])+0 =  by ( * .IB.S.IH)

0 + 0 =  by ( +0)

0⌋

Simplification of the rhs term:

0⌋

Alternative proof 2: pending

Pending proof of ( * .IB).

Induction Step:

Induction Hypothesis:

Induction Conclusion:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: failed

We take in ( * .IS) all variables arbitrary but fixed:

and simplify it.

Simplification of the lhs term:

(SuperPlus[(Subscript[m, 1])])*(Subscript[n, 3])⌋

Simplification of the rhs term:

(Subscript[n, 3])*(SuperPlus[(Subscript[m, 1])]) =  by ( * ^+)

(Subscript[n, 3])*(Subscript[m, 1])+(Subscript[n, 3]) =  by ( * .IH)

(Subscript[m, 1])*(Subscript[n, 3])+(Subscript[n, 3])⌋

Hence, it is sufficient to prove:

We try to prove ( * .IS.S) by  induction on n.

Induction Base:

We simplify ( * .IS.S.IB).

Simplification of the lhs term:

(SuperPlus[(Subscript[m, 1])])*0 =  by ( *0)

0⌋

Simplification of the rhs term:

(Subscript[m, 1])*0+0 =  by ( * .IH)

0*(Subscript[m, 1])+0 =  by ( +0)

0*(Subscript[m, 1])⌋

Hence, it is sufficient to prove:

The proof of ( * .IS.S.IB.S) fails.(No applicable inference rule was found.)

Induction Step:

Induction Hypothesis:

Induction Conclusion:

Pending proof of ( * .IS.S.IS).

Alternative proof 2: failed

We try to prove ( * .IS) by  induction on n.

Induction Base:

We simplify ( * .IS.IB).

Simplification of the lhs term:

(SuperPlus[(Subscript[m, 1])])*0 =  by ( *0)

0⌋

Simplification of the rhs term:

0*(SuperPlus[(Subscript[m, 1])]) =  by ( * ^+)

0*(Subscript[m, 1])+0 =  by ( +0)

0*(Subscript[m, 1])⌋

Hence, it is sufficient to prove:

The proof of ( * .IS.IB.S) fails.(No applicable inference rule was found.)

Induction Step:

Induction Hypothesis:

Induction Conclusion:

Pending proof of ( * .IS.IS).

Proof   Multiplication 0 From Left

Prove:

under the assumptions:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: failed

The proof of (0* ) fails.(The Simplifier was unable to transform the proof situation.)

Alternative proof 2: proved

We prove (0* ) by  induction on n.

Induction Base:

A proof by simplification of (0* .IB) works.

Simplification of the lhs term:

0*0 =  by ( *0)

0⌋

Simplification of the rhs term:

0⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

A proof by simplification of (0* .IS) works.

Simplification of the lhs term:

0*(SuperPlus[(Subscript[n, 1])]) =  by ( * ^+)

0*(Subscript[n, 1])+0 =  by (0* .IH)

0 + 0 =  by ( +0)

0⌋

Simplification of the rhs term:

0⌋

Proof  Attempt 2- Multiplication Commutativity

Prove:

under the assumptions:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: failed

The proof of ( * ) fails.(The Simplifier was unable to transform the proof situation.)

Alternative proof 2: failed

We try to prove ( * ) by  induction on m.

Induction Base:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: proved

We take in ( * .IB) all variables arbitrary but fixed and prove:

A proof by simplification of ( * .IB.F) works.

Simplification of the lhs term:

0*(Subscript[n, 1]) =  by (0* )

0⌋

Simplification of the rhs term:

(Subscript[n, 1])*0 =  by ( *0)

0⌋

Alternative proof 2: pending

Pending proof of ( * .IB).

Induction Step:

Induction Hypothesis:

Induction Conclusion:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: failed

We take in ( * .IS) all variables arbitrary but fixed:

and simplify it.

Simplification of the lhs term:

(SuperPlus[(Subscript[m, 1])])*(Subscript[n, 2])⌋

Simplification of the rhs term:

(Subscript[n, 2])*(SuperPlus[(Subscript[m, 1])]) =  by ( * ^+)

(Subscript[n, 2])*(Subscript[m, 1])+(Subscript[n, 2]) =  by ( * .IH)

(Subscript[m, 1])*(Subscript[n, 2])+(Subscript[n, 2])⌋

Hence, it is sufficient to prove:

We try to prove ( * .IS.S) by  induction on n.

Induction Base:

A proof by simplification of ( * .IS.S.IB) works.

Simplification of the lhs term:

(SuperPlus[(Subscript[m, 1])])*0 =  by ( *0)

0⌋

Simplification of the rhs term:

(Subscript[m, 1])*0+0 =  by ( * .IH)

0*(Subscript[m, 1])+0 =  by ( +0)

0*(Subscript[m, 1]) =  by (0* )

0⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

We simplify ( * .IS.S.IS).

Simplification of the lhs term:

(SuperPlus[(Subscript[m, 1])])*(SuperPlus[(Subscript[n, 3])]) =  by ( * ^+)

(SuperPlus[(Subscript[m, 1])])*(Subscript[n, 3])+(SuperPlus[(Subscript[m, 1])]) =  by ( * .IS.S.IH)

((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[n, 3]))+(SuperPlus[(Subscript[m, 1])]) =  by ( + ^+)

(SuperPlus[(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[n, 3]))+(Subscript[m, 1]))]) =  by (( + ) + )

(SuperPlus[((Subscript[m, 1])*(Subscript[n, 3])+((Subscript[n, 3])+(Subscript[m, 1])))])⌋

Simplification of the rhs term:

(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])])+(SuperPlus[(Subscript[n, 3])]) =  by ( * ^+)

((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))+(SuperPlus[(Subscript[n, 3])]) =  by ( + ^+)

(SuperPlus[(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))+(Subscript[n, 3]))]) =  by (( + ) + )

(SuperPlus[((Subscript[m, 1])*(Subscript[n, 3])+((Subscript[m, 1])+(Subscript[n, 3])))])⌋

Hence, it is sufficient to prove:

The proof of ( * .IS.S.IS.S) fails.(No applicable inference rule was found.)

Alternative proof 2: failed

We try to prove ( * .IS) by  induction on n.

Induction Base:

A proof by simplification of ( * .IS.IB) works.

Simplification of the lhs term:

(SuperPlus[(Subscript[m, 1])])*0 =  by ( *0)

0⌋

Simplification of the rhs term:

0*(SuperPlus[(Subscript[m, 1])]) =  by ( * ^+)

0*(Subscript[m, 1])+0 =  by ( +0)

0*(Subscript[m, 1]) =  by (0* )

0⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

We simplify ( * .IS.IS).

Simplification of the lhs term:

(SuperPlus[(Subscript[m, 1])])*(SuperPlus[(Subscript[n, 4])]) =  by ( * ^+)

(SuperPlus[(Subscript[m, 1])])*(Subscript[n, 4])+(SuperPlus[(Subscript[m, 1])]) =  by ( * .IS.IH)

(Subscript[n, 4])*(SuperPlus[(Subscript[m, 1])])+(SuperPlus[(Subscript[m, 1])]) =  by ( * ^+)

((Subscript[n, 4])*(Subscript[m, 1])+(Subscript[n, 4]))+(SuperPlus[(Subscript[m, 1])]) =  by ( * .IH)

((Subscript[m, 1])*(Subscript[n, 4])+(Subscript[n, 4]))+(SuperPlus[(Subscript[m, 1])]) =  by ( + ^+)

(SuperPlus[(((Subscript[m, 1])*(Subscript[n, 4])+(Subscript[n, 4]))+(Subscript[m, 1]))]) =  by (( + ) + )

(SuperPlus[((Subscript[m, 1])*(Subscript[n, 4])+((Subscript[n, 4])+(Subscript[m, 1])))])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[n, 4])])*(SuperPlus[(Subscript[m, 1])]) =  by ( * ^+)

(SuperPlus[(Subscript[n, 4])])*(Subscript[m, 1])+(SuperPlus[(Subscript[n, 4])]) =  by ( * .IH)

(Subscript[m, 1])*(SuperPlus[(Subscript[n, 4])])+(SuperPlus[(Subscript[n, 4])]) =  by ( * ^+)

((Subscript[m, 1])*(Subscript[n, 4])+(Subscript[m, 1]))+(SuperPlus[(Subscript[n, 4])]) =  by ( + ^+)

(SuperPlus[(((Subscript[m, 1])*(Subscript[n, 4])+(Subscript[m, 1]))+(Subscript[n, 4]))]) =  by (( + ) + )

(SuperPlus[((Subscript[m, 1])*(Subscript[n, 4])+((Subscript[m, 1])+(Subscript[n, 4])))])⌋

Hence, it is sufficient to prove:

The proof of ( * .IS.IS.S) fails.(No applicable inference rule was found.)

Proof  Multiplication Commutativity

Prove:

under the assumptions:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: failed

The proof of ( * ) fails.(The Simplifier was unable to transform the proof situation.)

Alternative proof 2: proved

We prove ( * ) by  induction on m.

Induction Base:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: proved

We take in ( * .IB) all variables arbitrary but fixed and prove:

A proof by simplification of ( * .IB.F) works.

Simplification of the lhs term:

0*(Subscript[n, 1]) =  by (0* )

0⌋

Simplification of the rhs term:

(Subscript[n, 1])*0 =  by ( *0)

0⌋

Alternative proof 2: pending

Pending proof of ( * .IB).

Induction Step:

Induction Hypothesis:

Induction Conclusion:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: proved

We take in ( * .IS) all variables arbitrary but fixed:

and simplify it.

Simplification of the lhs term:

(SuperPlus[(Subscript[m, 1])])*(Subscript[n, 2])⌋

Simplification of the rhs term:

(Subscript[n, 2])*(SuperPlus[(Subscript[m, 1])]) =  by ( * ^+)

(Subscript[n, 2])*(Subscript[m, 1])+(Subscript[n, 2]) =  by ( * .IH)

(Subscript[m, 1])*(Subscript[n, 2])+(Subscript[n, 2]) =  by ( + )

(Subscript[n, 2])+(Subscript[m, 1])*(Subscript[n, 2])⌋

Hence, it is sufficient to prove:

We prove ( * .IS.S) by  induction on n.

Induction Base:

A proof by simplification of ( * .IS.S.IB) works.

Simplification of the lhs term:

(SuperPlus[(Subscript[m, 1])])*0 =  by ( *0)

0⌋

Simplification of the rhs term:

0+(Subscript[m, 1])*0 =  by ( * .IH)

0+0*(Subscript[m, 1]) =  by (0+ )

0*(Subscript[m, 1]) =  by (0* )

0⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

A proof by simplification of ( * .IS.S.IS) works.

Simplification of the lhs term:

(SuperPlus[(Subscript[m, 1])])*(SuperPlus[(Subscript[n, 3])]) =  by ( * ^+)

(SuperPlus[(Subscript[m, 1])])*(Subscript[n, 3])+(SuperPlus[(Subscript[m, 1])]) =  by ( * .IS.S.IH)

((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3]))+(SuperPlus[(Subscript[m, 1])]) =  by ( + ^+)

(SuperPlus[(((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3]))+(Subscript[m, 1]))]) =  by (( + ) + )

(SuperPlus[((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1])))])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[n, 3])])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]) =  by ( * ^+)

(SuperPlus[(Subscript[n, 3])])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1])) =  by (^++ )

(SuperPlus[((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1])))])⌋

Alternative proof 2: pending

Pending proof of ( * .IS).

Proof  Multiplication Associativity with Addition AC in KB

Prove:

under the assumptions:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: failed

The proof of (( * ) * ) fails.(The Simplifier was unable to transform the proof situation.)

Alternative proof 2: proved

We prove (( * ) * ) by  induction on m.

Induction Base:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: proved

We take in (( * ) * .IB) all variables arbitrary but fixed and prove:

A proof by simplification of (( * ) * .IB.F) works.

Simplification of the lhs term:

(0*(Subscript[n, 1]))*(Subscript[p, 1]) =  by (0*)

0*(Subscript[p, 1]) =  by (0*)

0⌋

Simplification of the rhs term:

0*((Subscript[n, 1])*(Subscript[p, 1])) =  by (0*)

0⌋

Alternative proof 2: pending

Pending proof of (( * ) * .IB).

Induction Step:

Induction Hypothesis:

Induction Conclusion:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: proved

We take in (( * ) * .IS) all variables arbitrary but fixed:

and simplify it.

Simplification of the lhs term:

((SuperPlus[(Subscript[m, 1])])*(Subscript[n, 2]))*(Subscript[p, 2]) =  by ( ^+*)

((Subscript[m, 1])*(Subscript[n, 2])+(Subscript[n, 2]))*(Subscript[p, 2]) =  by ( + )

((Subscript[n, 2])+(Subscript[m, 1])*(Subscript[n, 2]))*(Subscript[p, 2])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[m, 1])])*((Subscript[n, 2])*(Subscript[p, 2])) =  by ( ^+*)

(Subscript[m, 1])*((Subscript[n, 2])*(Subscript[p, 2]))+(Subscript[n, 2])*(Subscript[p, 2]) =  by (( * ) * .IH)

((Subscript[m, 1])*(Subscript[n, 2]))*(Subscript[p, 2])+(Subscript[n, 2])*(Subscript[p, 2]) =  by ( + )

(Subscript[n, 2])*(Subscript[p, 2])+((Subscript[m, 1])*(Subscript[n, 2]))*(Subscript[p, 2])⌋

Hence, it is sufficient to prove:

We prove (( * ) * .IS.S) by  induction on n.

Induction Base:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: proved

We take in (( * ) * .IS.S.IB) all variables arbitrary but fixed and prove:

A proof by simplification of (( * ) * .IS.S.IB.F) works.

Simplification of the lhs term:

(0+(Subscript[m, 1])*0)*(Subscript[p, 3]) =  by ( *0)

(0 + 0)*(Subscript[p, 3]) =  by ( +0)

0*(Subscript[p, 3]) =  by (0*)

0⌋

Simplification of the rhs term:

0*(Subscript[p, 3])+((Subscript[m, 1])*0)*(Subscript[p, 3]) =  by ( *0)

0*(Subscript[p, 3])+0*(Subscript[p, 3]) =  by (0*)

0+0*(Subscript[p, 3]) =  by (0*)

0 + 0 =  by ( +0)

0⌋

Alternative proof 2: pending

Pending proof of (( * ) * .IS.S.IB).

Induction Step:

Induction Hypothesis:

Induction Conclusion:

As there are several methods which can be applied, we have different choices to proceed with the proof.

Alternative proof 1: failed

We take in (( * ) * .IS.S.IS) all variables arbitrary but fixed:

and simplify it.

Simplification of the lhs term:

((SuperPlus[(Subscript[n, 3])])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 4]) =  by ( *  ^+)

((SuperPlus[(Subscript[n, 3])])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1])))*(Subscript[p, 4]) =  by (^++ )

(SuperPlus[((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1])))])*(Subscript[p, 4]) =  by ( ^+*)

((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1])))*(Subscript[p, 4])+(Subscript[p, 4]) =  by ( + )

(Subscript[p, 4])+((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1])))*(Subscript[p, 4]) =  by ( + )

(Subscript[p, 4])+((Subscript[n, 3])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))*(Subscript[p, 4]) =  by (( + ) + )

(Subscript[p, 4])+(((Subscript[n, 3])+(Subscript[m, 1]))+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 4]) =  by ( + )

(Subscript[p, 4])+(((Subscript[m, 1])+(Subscript[n, 3]))+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 4])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[n, 3])])*(Subscript[p, 4])+((Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 4]) =  by ( *  ^+)

(SuperPlus[(Subscript[n, 3])])*(Subscript[p, 4])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 4]) =  by ( ^+*)

((Subscript[n, 3])*(Subscript[p, 4])+(Subscript[p, 4]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 4]) =  by ( + )

((Subscript[p, 4])+(Subscript[n, 3])*(Subscript[p, 4]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 4]) =  by ( + )

((Subscript[p, 4])+(Subscript[n, 3])*(Subscript[p, 4]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 4])⌋

Hence, it is sufficient to prove:

We try to prove (( * ) * .IS.S.IS.S) by  induction on p.

Induction Base:

A proof by simplification of (( * ) * .IS.S.IS.S.IB) works.

Simplification of the lhs term:

0+(((Subscript[m, 1])+(Subscript[n, 3]))+(Subscript[m, 1])*(Subscript[n, 3]))*0 =  by ( *0)

0 + 0⌋

Simplification of the rhs term:

(0+(Subscript[n, 3])*0)+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*0 =  by ( *0)

(0 + 0)+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*0 =  by ( *0)

(0 + 0) + 0 =  by ( +0)

0 + 0⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

We simplify (( * ) * .IS.S.IS.S.IS).

Simplification of the lhs term:

(SuperPlus[(Subscript[p, 5])])+(((Subscript[m, 1])+(Subscript[n, 3]))+(Subscript[m, 1])*(Subscript[n, 3]))*(SuperPlus[(Subscript[p, 5])]) =  by ( *  ^+)

(SuperPlus[(Subscript[p, 5])])+((((Subscript[m, 1])+(Subscript[n, 3]))+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5])+(((Subscript[m, 1])+(Subscript[n, 3]))+(Subscript[m, 1])*(Subscript[n, 3]))) =  by (^++ )

(SuperPlus[((Subscript[p, 5])+((((Subscript[m, 1])+(Subscript[n, 3]))+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5])+(((Subscript[m, 1])+(Subscript[n, 3]))+(Subscript[m, 1])*(Subscript[n, 3]))))]) =  by ( + )

(SuperPlus[((Subscript[p, 5])+((((Subscript[m, 1])+(Subscript[n, 3]))+(Subscript[m, 1])*(Subscript[n, 3]))+(((Subscript[m, 1])+(Subscript[n, 3]))+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5])))]) =  by (( + ) + )

(SuperPlus[(((Subscript[p, 5])+(((Subscript[m, 1])+(Subscript[n, 3]))+(Subscript[m, 1])*(Subscript[n, 3])))+(((Subscript[m, 1])+(Subscript[n, 3]))+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))]) =  by (( + ) + )

(SuperPlus[((((Subscript[p, 5])+((Subscript[m, 1])+(Subscript[n, 3])))+(Subscript[m, 1])*(Subscript[n, 3]))+(((Subscript[m, 1])+(Subscript[n, 3]))+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))])⌋

Simplification of the rhs term:

((SuperPlus[(Subscript[p, 5])])+(Subscript[n, 3])*(SuperPlus[(Subscript[p, 5])]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(SuperPlus[(Subscript[p, 5])]) =  by ( *  ^+)

((SuperPlus[(Subscript[p, 5])])+((Subscript[n, 3])*(Subscript[p, 5])+(Subscript[n, 3])))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(SuperPlus[(Subscript[p, 5])]) =  by ( *  ^+)

((SuperPlus[(Subscript[p, 5])])+((Subscript[n, 3])*(Subscript[p, 5])+(Subscript[n, 3])))+(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))) =  by (^++ )

(SuperPlus[((Subscript[p, 5])+((Subscript[n, 3])*(Subscript[p, 5])+(Subscript[n, 3])))])+(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))) =  by (^++ )

(SuperPlus[(((Subscript[p, 5])+((Subscript[n, 3])*(Subscript[p, 5])+(Subscript[n, 3])))+(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))))]) =  by ( + )

(SuperPlus[(((Subscript[p, 5])+((Subscript[n, 3])+(Subscript[n, 3])*(Subscript[p, 5])))+(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))))]) =  by ( + )

(SuperPlus[(((Subscript[p, 5])+((Subscript[n, 3])+(Subscript[n, 3])*(Subscript[p, 5])))+(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5])))]) =  by (( + ) + )

(SuperPlus[((((Subscript[p, 5])+((Subscript[n, 3])+(Subscript[n, 3])*(Subscript[p, 5])))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))]) =  by ( + )

(SuperPlus[((((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))+((Subscript[p, 5])+((Subscript[n, 3])+(Subscript[n, 3])*(Subscript[p, 5]))))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))]) =  by (( + ) + )

(SuperPlus[(((((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))+(Subscript[p, 5]))+((Subscript[n, 3])+(Subscript[n, 3])*(Subscript[p, 5])))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))]) =  by ( + )

(SuperPlus[((((Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+((Subscript[n, 3])+(Subscript[n, 3])*(Subscript[p, 5])))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))]) =  by (( + ) + )

(SuperPlus[(((((Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+(Subscript[n, 3]))+(Subscript[n, 3])*(Subscript[p, 5]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))]) =  by ( + )

(SuperPlus[((((Subscript[n, 3])+((Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))))+(Subscript[n, 3])*(Subscript[p, 5]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))]) =  by (( + ) + )

(SuperPlus[(((((Subscript[n, 3])+(Subscript[p, 5]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+(Subscript[n, 3])*(Subscript[p, 5]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))]) =  by (( + ) + )

(SuperPlus[((((((Subscript[n, 3])+(Subscript[p, 5]))+(Subscript[m, 1]))+(Subscript[m, 1])*(Subscript[n, 3]))+(Subscript[n, 3])*(Subscript[p, 5]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))]) =  by ( + )

(SuperPlus[(((((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[p, 5])))+(Subscript[m, 1])*(Subscript[n, 3]))+(Subscript[n, 3])*(Subscript[p, 5]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))]) =  by (( + ) + )

(SuperPlus[((((((Subscript[m, 1])+(Subscript[n, 3]))+(Subscript[p, 5]))+(Subscript[m, 1])*(Subscript[n, 3]))+(Subscript[n, 3])*(Subscript[p, 5]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))]) =  by ( + )

(SuperPlus[(((((Subscript[p, 5])+((Subscript[m, 1])+(Subscript[n, 3])))+(Subscript[m, 1])*(Subscript[n, 3]))+(Subscript[n, 3])*(Subscript[p, 5]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))])⌋

Hence, it is sufficient to prove:

The proof of (( * ) * .IS.S.IS.S.IS.S) fails.(No applicable inference rule was found.)

Alternative proof 2: proved

We prove (( * ) * .IS.S.IS) by  induction on p.

Induction Base:

A proof by simplification of (( * ) * .IS.S.IS.IB) works.

Simplification of the lhs term:

((SuperPlus[(Subscript[n, 3])])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*0 =  by ( *0)

0⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[n, 3])])*0+((Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*0 =  by (( * ) * .IH)

(SuperPlus[(Subscript[n, 3])])*0+(Subscript[m, 1])*((SuperPlus[(Subscript[n, 3])])*0) =  by ( *0)

0+(Subscript[m, 1])*((SuperPlus[(Subscript[n, 3])])*0) =  by ( *0)

0+(Subscript[m, 1])*0 =  by ( *0)

0 + 0 =  by ( +0)

0⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

A proof by simplification of (( * ) * .IS.S.IS.IS) works.

Simplification of the lhs term:

((SuperPlus[(Subscript[n, 3])])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(SuperPlus[(Subscript[p, 6])]) =  by ( *  ^+)

((SuperPlus[(Subscript[n, 3])])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 6])+((SuperPlus[(Subscript[n, 3])])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])])) =  by (( * ) * .IS.S.IS.IH)

((SuperPlus[(Subscript[n, 3])])*(Subscript[p, 6])+((Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 6]))+((SuperPlus[(Subscript[n, 3])])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])])) =  by ( *  ^+)

((SuperPlus[(Subscript[n, 3])])*(Subscript[p, 6])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6]))+((SuperPlus[(Subscript[n, 3])])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])])) =  by ( *  ^+)

((SuperPlus[(Subscript[n, 3])])*(Subscript[p, 6])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6]))+((SuperPlus[(Subscript[n, 3])])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))) =  by ( ^+*)

(((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6]))+((SuperPlus[(Subscript[n, 3])])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))) =  by (^++ )

(((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6]))+(SuperPlus[((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1])))]) =  by ( + ^+)

(SuperPlus[((((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6]))+((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))))]) =  by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1])))+(((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])))]) =  by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+(((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])))]) =  by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+(((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])))]) =  by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+(((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 6])))]) =  by (( + ) + )

(SuperPlus[((((Subscript[n, 3])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6])))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 6]))])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[n, 3])])*(SuperPlus[(Subscript[p, 6])])+((Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(SuperPlus[(Subscript[p, 6])]) =  by ( *  ^+)

((SuperPlus[(Subscript[n, 3])])*(Subscript[p, 6])+(SuperPlus[(Subscript[n, 3])]))+((Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(SuperPlus[(Subscript[p, 6])]) =  by ( *  ^+)

((SuperPlus[(Subscript[n, 3])])*(Subscript[p, 6])+(SuperPlus[(Subscript[n, 3])]))+(((Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 6])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])])) =  by ( *  ^+)

((SuperPlus[(Subscript[n, 3])])*(Subscript[p, 6])+(SuperPlus[(Subscript[n, 3])]))+(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])])) =  by ( *  ^+)

((SuperPlus[(Subscript[n, 3])])*(Subscript[p, 6])+(SuperPlus[(Subscript[n, 3])]))+(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))) =  by ( ^+*)

(((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6]))+(SuperPlus[(Subscript[n, 3])]))+(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))) =  by ( + ^+)

(SuperPlus[(((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6]))+(Subscript[n, 3]))])+(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))) =  by (^++ )

(SuperPlus[((((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6]))+(Subscript[n, 3]))+(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))))]) =  by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[n, 3])*(Subscript[p, 6])+(Subscript[p, 6])))+(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))))]) =  by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6])))+(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))))]) =  by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6])))+(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])))]) =  by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6])))+(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))+((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 6])))]) =  by ( + )

(SuperPlus[(((Subscript[n, 3])+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6])))+(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 6])))]) =  by (( + ) + )

(SuperPlus[((((Subscript[n, 3])+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6])))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 6]))]) =  by ( + )

(SuperPlus[((((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))+((Subscript[n, 3])+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6]))))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 6]))]) =  by (( + ) + )

(SuperPlus[(((((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))+(Subscript[n, 3]))+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6])))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 6]))]) =  by ( + )

(SuperPlus[((((Subscript[n, 3])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+((Subscript[p, 6])+(Subscript[n, 3])*(Subscript[p, 6])))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 6]))])⌋

Alternative proof 2: pending

Pending proof of (( * ) * .IS).

Proof  Multiplication Associativity with Addition AC  as Iference Rule

Prove:

under the assumptions:

We prove (( * ) * ) by  induction on m.

Induction Base:

We take in (( * ) * .IB) all variables arbitrary but fixed and prove:

A proof by simplification of (( * ) * .IB.F) works.

Simplification of the lhs term:

(0*(Subscript[n, 1]))*(Subscript[p, 1]) = by (0*)

0*(Subscript[p, 1]) =  by (0*)

0⌋

Simplification of the rhs term:

0*((Subscript[n, 1])*(Subscript[p, 1])) =  by (0*)

0⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

We take in (( * ) * .IS) all variables arbitrary but fixed:

and simplify it.

Simplification of the lhs term:

((SuperPlus[(Subscript[m, 1])])*(Subscript[n, 2]))*(Subscript[p, 2]) =  by ( ^+*)

((Subscript[m, 1])*(Subscript[n, 2])+(Subscript[n, 2]))*(Subscript[p, 2]) =  by (Special Simpl )

((Subscript[n, 2])+(Subscript[m, 1])*(Subscript[n, 2]))*(Subscript[p, 2])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[m, 1])])*((Subscript[n, 2])*(Subscript[p, 2])) =  by ( ^+*)

(Subscript[m, 1])*((Subscript[n, 2])*(Subscript[p, 2]))+(Subscript[n, 2])*(Subscript[p, 2]) =  by (( * ) * .IH)

((Subscript[m, 1])*(Subscript[n, 2]))*(Subscript[p, 2])+(Subscript[n, 2])*(Subscript[p, 2]) =  by (Special Simpl )

(Subscript[n, 2])*(Subscript[p, 2])+((Subscript[m, 1])*(Subscript[n, 2]))*(Subscript[p, 2])⌋

Hence, it is sufficient to prove:

We prove (( * ) * .IS.S) by  induction on n.

Induction Base:

We take in (( * ) * .IS.S.IB) all variables arbitrary but fixed and prove:

A proof by simplification of (( * ) * .IS.S.IB.F) works.

Simplification of the lhs term:

(0+(Subscript[m, 1])*0)*(Subscript[p, 3]) =  by ( *0)

(0 + 0)*(Subscript[p, 3]) =  by ( +0)

0*(Subscript[p, 3]) =  by (0*)

0⌋

Simplification of the rhs term:

0*(Subscript[p, 3])+((Subscript[m, 1])*0)*(Subscript[p, 3]) =  by ( *0)

0*(Subscript[p, 3])+0*(Subscript[p, 3]) =  by (0*)

0+0*(Subscript[p, 3]) =  by (0*)

0 + 0 =  by ( +0)

0⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

We take in (( * ) * .IS.S.IS) all variables arbitrary but fixed:

and simplify it.

Simplification of the lhs term:

((SuperPlus[(Subscript[n, 3])])+(Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 4]) =  by (Special Simpl)

((Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])])+(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 4]) =  by ( *  ^+)

(((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))+(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 4]) =  by (Special Simpl)

(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))+(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 4]) =  by ( + ^+)

(SuperPlus[(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))+(Subscript[n, 3]))])*(Subscript[p, 4]) =  by (Special Simpl)

(SuperPlus[((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))])*(Subscript[p, 4]) =  by ( ^+*)

((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*(Subscript[p, 4])+(Subscript[p, 4]) =  by (Special Simpl )

(Subscript[p, 4])+((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*(Subscript[p, 4])⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[n, 3])])*(Subscript[p, 4])+((Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 4]) =  by (Special Simpl)

((Subscript[m, 1])*(SuperPlus[(Subscript[n, 3])]))*(Subscript[p, 4])+(SuperPlus[(Subscript[n, 3])])*(Subscript[p, 4]) =  by ( *  ^+)

((Subscript[m, 1])*(Subscript[n, 3])+(Subscript[m, 1]))*(Subscript[p, 4])+(SuperPlus[(Subscript[n, 3])])*(Subscript[p, 4]) =  by (Special Simpl)

(SuperPlus[(Subscript[n, 3])])*(Subscript[p, 4])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 4]) =  by ( ^+*)

((Subscript[n, 3])*(Subscript[p, 4])+(Subscript[p, 4]))+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 4]) =  by (Special Simpl )

(Subscript[p, 4])+((Subscript[n, 3])*(Subscript[p, 4])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 4]))⌋

Hence, it is sufficient to prove:

We prove (( * ) * .IS.S.IS.S) by  induction on p.

Induction Base:

A proof by simplification of (( * ) * .IS.S.IS.S.IB) works.

Simplification of the lhs term:

0+((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*0 =  by ( *0)

0 + 0⌋

Simplification of the rhs term:

0+((Subscript[n, 3])*0+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*0) =  by ( *0)

0+(0+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*0) =  by ( *0)

0 + (0 + 0) =  by (Special Simpl)

(0 + 0) + 0 =  by ( +0)

0 + 0⌋

Induction Step:

Induction Hypothesis:

Induction Conclusion:

A proof by simplification of (( * ) * .IS.S.IS.S.IS) works.

Simplification of the lhs term:

(SuperPlus[(Subscript[p, 5])])+((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*(SuperPlus[(Subscript[p, 5])]) =  by (Special Simpl)

((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*(SuperPlus[(Subscript[p, 5])])+(SuperPlus[(Subscript[p, 5])]) =  by ( *  ^+)

(((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*(Subscript[p, 5])+((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3]))))+(SuperPlus[(Subscript[p, 5])]) =  by (Special Simpl)

((Subscript[m, 1])+((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*(Subscript[p, 5]))))+(SuperPlus[(Subscript[p, 5])]) =  by ( + ^+)

(((Subscript[m, 1])+((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*(Subscript[p, 5]))))+(Subscript[p, 5]))^+ =  by (Special Simpl)

((Subscript[m, 1])+((Subscript[n, 3])+(((Subscript[p, 5])+((Subscript[m, 1])+((Subscript[n, 3])+(Subscript[m, 1])*(Subscript[n, 3])))*(Subscript[p, 5]))+(Subscript[m, 1])*(Subscript[n, 3]))))^+ =  by (( * ) * .IS.S.IS.S.IH)

((Subscript[m, 1])+((Subscript[n, 3])+(((Subscript[p, 5])+((Subscript[n, 3])*(Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5])))+(Subscript[m, 1])*(Subscript[n, 3]))))^+ =  by (Special Simpl )

((Subscript[m, 1])+((Subscript[n, 3])+((Subscript[p, 5])+((Subscript[m, 1])*(Subscript[n, 3])+((Subscript[n, 3])*(Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))))))^+⌋

Simplification of the rhs term:

(SuperPlus[(Subscript[p, 5])])+((Subscript[n, 3])*(SuperPlus[(Subscript[p, 5])])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(SuperPlus[(Subscript[p, 5])])) =  by (Special Simpl)

(Subscript[n, 3])*(SuperPlus[(Subscript[p, 5])])+(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(SuperPlus[(Subscript[p, 5])])+(SuperPlus[(Subscript[p, 5])])) =  by ( *  ^+)

((Subscript[n, 3])*(Subscript[p, 5])+(Subscript[n, 3]))+(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(SuperPlus[(Subscript[p, 5])])+(SuperPlus[(Subscript[p, 5])])) =  by (Special Simpl)

(Subscript[n, 3])+(((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(SuperPlus[(Subscript[p, 5])])+((SuperPlus[(Subscript[p, 5])])+(Subscript[n, 3])*(Subscript[p, 5]))) =  by ( *  ^+)

(Subscript[n, 3])+((((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3])))+((SuperPlus[(Subscript[p, 5])])+(Subscript[n, 3])*(Subscript[p, 5]))) =  by (Special Simpl)

((Subscript[m, 1])+((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+((Subscript[n, 3])*(Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5])))))+(SuperPlus[(Subscript[p, 5])]) =  by ( + ^+)

(((Subscript[m, 1])+((Subscript[n, 3])+((Subscript[m, 1])*(Subscript[n, 3])+((Subscript[n, 3])*(Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5])))))+(Subscript[p, 5]))^+ =  by (Special Simpl )

((Subscript[m, 1])+((Subscript[n, 3])+((Subscript[p, 5])+((Subscript[m, 1])*(Subscript[n, 3])+((Subscript[n, 3])*(Subscript[p, 5])+((Subscript[m, 1])+(Subscript[m, 1])*(Subscript[n, 3]))*(Subscript[p, 5]))))))^+⌋

Proof  by Groebner Bases

Prove:

with no assumptions.

Proved.

The Theorem is proved by the Groebner Bases method.      

      The formula in the scope of the universal quantifier is transformed into an equivalent formula that is a conjunction of disjunctions of equalities and negated equalities. The universal quantifier can then be distributed over the individual parts of the conjunction. By this, we obtain:

Independent proof problems:

We now prove the above individual problems separately:

Proof of (f=0.1):

This proof problem has the following structure:

where

({{Poly[1] =, 17+-23*x*y+(1/5)*(x^2)*y}, {Poly[2] =, 27*(xy^3)+-15*(x^3)+(x^3)*(y^4)}, {Poly[3] =, -405*(xy^3)+225*(x^3)+255*x*y+27*(xy^3)*x*y+-15*(x^4)*y+-328*(x^2)*(y^2)+3*(x^3)*(y^2)+-23*(x^3)*(y^3)+(1/5)*(x^4)*(y^3)+-15*(x^3)*(y^4)+(x^4)*(y^5)}})

(f=0.1.structure) is equivalent to

(f=0.1.implication) is equivalent to

By introducing the slack variable(s)

{ξ}

(f=0.1.not-exists) is transformed into the equivalent formula

Hence, we see that the proof problem is transformed into the question on whether or not a system of polynomial equations has a solution or not. This question can be answered by checking whether or not the (reduced) Groebner basis of

{Poly[1], Poly[2], -1 + ξ Poly[3]}

is exactly {1}.                  

Hence, we compute the Groebner basis for the following polynomial list:

{-1 + 225 (x^3) ξ + -405 (xy^3) ξ + 
        255 x y ξ + -15 (x^4) y ξ + 
        27 x (xy^3) y ξ + -328 (x^2) (y^2) ξ + 
        3 (x^3) (y^2) ξ + -23 (x^3) (y^3) ξ + 
        (1/5) (x^4) (y^3) ξ + -15 (x^3) (y^4) ξ + 
        (x^4) (y^5) ξ, -15 (x^3) + 27 (xy^3) + (x^3) (y^4), 
      17 + -23 x y + (((x^2) y)/5)}

The Groebner basis:

{1}

Hence, (f=0.1) is proved.

Since all of the individual subtheorems are proved, the original formula is proved.