Newbie questions

[Haitao Zhang]

Hi! I have some questions regarding metamath and mmj2:

1) What is the best way to export a subset of set.mm? Should I just use a text editor like vim? Does a compressed proof get affected by insertions and deletions of theorems  it does not use?

2) Is there a specification of the compression/decompression scheme? mmverify.py's was very helpful in helping me understand how the proof stack works but its decompression code is not easy to understand.

3) Is mmj2 specialized to set.mm? That is do constants like |- and wff have special meanings for mmj2?

4) It is my understanding that one can not enter new $c, $v, $f in mmj2. So one needs to modify the database file with an external editor and then restart mmj2 if such a need arises?

Thanks,

Haitao

[David A. Wheeler]

On February 10, 2019 2:39:33 PM EST, Haitao Zhang <zht...@gmail.com> wrote:
>Hi! I have some questions regarding metamath and mmj2:
>
>1) What is the best way to export a subset of set.mm? Should I just use
>a
>text editor like vim? Does a compressed proof get affected by
>insertions
>and deletions of theorems it does not use?

You can certainly use a text editor. Every proof will depend on at least some axioms or definitions, and almost certainly some other proofs. If proof C depends on proof B, and you delete proof B, then clearly proof C will not be provable. You can certainly create a subset, you simply need to decide what subset you want, and then include all the proofs transitively that they require.

>2) Is there a specification of the compression/decompression scheme?
>mmverify.py's was very helpful in helping me understand how the proof
>stack
>works but its decompression code is not easy to understand.

Yes, the metamath book expressly explains it. We are about to release an update to that book, nothing substantive changed about its spec, but there are a few minor clarifications that might be helpful. I think you will see an announcement in a day or two (Norm?)

>3) Is mmj2 specialized to set.mm? That is do constants like |- and wff
>have
>special meanings for mmj2?

Sort of. mmj2 has a number of enhancements that focus on set.mm. but you can use it for other databases. I exclusively use mmj2 when I create proofs for iset.mm.

>4) It is my understanding that one can not enter new $c, $v, $f in
>mmj2. So
>one needs to modify the database file with an external editor and then
>restart mmj2 if such a need arises?

I have never tried, but I believe that is correct. In practice, that is not a significant issue.


--- David A.Wheeler

[Haitao Zhang]

David,

Thank you for your responses. I enjoyed your video showing mmj2 and found it very helpful. Right now I am having trouble getting the mmj2 off the ground on a tiny file that is proved and saved from metamath. I suspect it has something to do what mmj2 expects from set.mm. I am not sure here is the right forum to ask detailed questions on mmj2. I will try mmj2 github issues tracker first.

Haitao

[Mario Carneiro]

This is probably a better place to ask mmj2 questions than the issue tracker. I admit that the tutorial is long out of date, but I haven't had much time to revisit it. When writing theorems in set.mm, I usually have a text editor open to do the structural work (creating theorem statements, arranging hypotheses and scoping, theorem comments, putting in $c/$f/$v although these are not really needed in set.mm since they are all set up already), and use mmj2 only for loading set.mm with a theorem stub, navigating to it, proving the theorem, getting the compressed proofs, and copy/pasting into the file.

Mario

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[Haitao Zhang]

I see internally things are marked into sections. Is there a tool to break out these sections into files so I can manage imports with $[ $]? The commented markers seem to hint at the existence of something like this. I did this by hand for now. I think in the beginning I will need to restart mmj2 quite a bit to experiment with $c/$f/$v for some syntax I am thinking of using. By importing only till the internally marked "end of set.mm" mmj2 starts quite responsively.

Haitao

[Norman Megill]

On Sunday, February 10, 2019 at 11:27:53 PM UTC-5, Haitao Zhang wrote:

I see internally things are marked into sections. Is there a tool to break out these sections into files so I can manage imports with $[ $]? The commented markers seem to hint at the existence of something like this. I did this by hand for now. I think in the beginning I will need to restart mmj2 quite a bit to experiment with $c/$f/$v for some syntax I am thinking of using. By importing only till the internally marked "end of set.mm" mmj2 starts quite responsively.

To split it into sections, use the metamath program:

MM> read set.mm
MM> write source set.mm /split

To create the combined version again, just

MM> read set.mm
MM> write source set.mm

and the subsection files will be deleted, or more accurately renamed with a ~1 ending.

For a detailed description of how this works, see the 21-Dec-2017 entry in
http://us.metamath.org/mpeuni/mmnotes.txt

Norm

[Norman Megill]

On Sunday, February 10, 2019 at 4:28:45 PM UTC-5, David A. Wheeler wrote:

On February 10, 2019 2:39:33 PM EST, Haitao Zhang wrote:

>2) Is there a specification of the compression/decompression scheme?
>mmverify.py's was very helpful in helping me understand how the proof
>stack
>works but its decompression code is not easy to understand.

Yes, the metamath book expressly explains it. We are about to release an update to that book, nothing substantive changed about its spec, but there are a few minor clarifications that might be helpful.  I think you will see an announcement in a day or two (Norm?)

The updated book, with many improvements by David, is available at http://us2.metamath.org:88/index.html#book.  See the announcement in the 6-Feb-2019 entry at http://us2.metamath.org:88/mpeuni/mmrecent.html

The book is now maintained on GitHub:  https://github.com/metamath/metamath-book

The compressed proof format is explained in Appendix B, p. 169.

Norm

[Haitao Zhang]

Thanks for the pointer. Now I understand that it is the order of mandatory hypotheses that matters to the decompression of proofs. I still don't quite understand how the Z tag works but I get the idea of avoiding repeated subproofs. It is not critical to my understanding of what kind of editing of a file could destroy the compressed proofs. If I need to fully understand it I will probably consult with some verifier source code.

Thanks for pointing out the /split usage as well. I am sure it will come handy.

Haitao

[Mario Carneiro]

Compressed proofs depend on the order of the arguments in the paren list at the beginning, the order of $e hypotheses to the theorem, and the order of $f hypotheses in use (which are usually fixed for a database like set.mm). For theorems referenced, the theorems must have the expected conclusion and hypotheses, and the $e and $f hypotheses to these theorems must also not be reordered. Other than that, changes will not break compressed proofs. Theorems are not referenced by any global counter, but by name (so renaming theorems can also break compressed proofs as with normal proofs), so you can insert theorems anywhere without breaking proofs. You can remove unused proofs without breaking anything (or if they are used, you will only break the theorems that *directly* reference the deleted theorem). You can reorder theorems, provided that any users of a theorem come after the theorem definition (forward references are not allowed). You can change scopes however you like, as long as the $e and $d hypotheses get to the right places. $e names are not used, they can be renamed at will - only the order of $e hypotheses matters. Adding and removing $c $v $f is fine as long as you don't reorder the $f's and don't remove something in use.

--

[Haitao Zhang]

Thanks for the great explanation!

I also ran into trouble with mmj2 on:

"A-LA-0404 DefineWorkVarType error on RunParm or call parameter. Value of Work Variable Prefix = &C is the same on two different Work Var Types: class and cat"

which I was able to fix by sheepishly following RunParmsPeanoInfix.txt and putting the following line in my RunParms:

DefineWorkVarType,cat,&CAT,200

I think I will get the hang of finding workarounds on some of the rough spots.

[Norman Megill]

The only proof format defined by the official Metamath spec (Sec. 4.1 of the Metamath book) is the "normal" format consisting of an RPN list of labels.  Support for "compressed" format (Appendix B) is theoretically optional for a program to be considered a Metamath proof verifier, but it is strongly encouraged because of the significant size and speed savings for compressed proofs.

The metamath program supports some additional unofficial formats to assist database editing and maintenance.  It can work with 3 basic formats, "normal", "explicit", and "compressed", each in "unpacked" and "packed" form, and a database can have a mixture of formats.  The packed format places "local labels" on certain steps so that those steps can be referenced later in the proof without repeating their subproofs.  Except for unpacked normal and packed compressed, these are not recognized by any other program to my knowledge.

With compressed format (the format we usually use in our databases), you can't change the order of the theorem's $e or mandatory $f hypotheses without corrupting the proof.  OTOH unlike the other formats, you can change the name (label) of a $e or $f statement since it isn't referenced by name anywhere.

With the normal format, you can change the order of the $e and $f hypotheses of a theorem without affecting its proof, provided the theorem isn't referenced by a later proof.

With the explicit format, you can change the order of $e and $f statements of a theorem provided all proofs referencing the theorem are saved in the explicit format.

Each of these 3 formats can exist in 2 forms, packed and not packed.  The packed format places "local labels" on certain steps so that those steps can be referenced later in the proof without repeating their subproofs.

The packed compressed proof is a step by step translation of the packed normal format.  While it isn't normally done, it is possible to display or store a compressed proof in non-packed format with the trick shown below.

Below are examples of the 3 formats in unpacked and packed forms.  Use "save" instead of "show" if you want to store the proof in that format, which will be saved to disk when you do "write source".



MM> show proof id1 /normal
Proof of "id1":
---------Clip out the proof below this line to put it in the source file:
    wph wph wph wi wi wph wph wi wph wph ax-1 wph wph wph wi wph wi wi wph wph
    wph wi wi wph wph wi wi wph wph wph wi ax-1 wph wph wph wi wph ax-2 ax-mp
    ax-mp $.
---------The proof of "id1" (154 bytes) ends above this line.


MM> show proof id1 /normal /packed
Proof of "id1":
---------Clip out the proof below this line to put it in the source file:
    wph wph wph 1:wi 2:wi 1 wph wph ax-1 wph 1 wph wi wi 2 1 wi wph 1 ax-1 wph
    1 wph ax-2 ax-mp ax-mp $.
---------The proof of "id1" (97 bytes) ends above this line.


MM> show proof id1 /explicit
Proof of "id1":
---------Clip out the proof below this line to put it in the source file:
    wph=wph wph=wph wps=wph wps=wi wph=wi wph=wph wps=wph wps=wi wph=wph
    wps=wph min=ax-1 wph=wph wph=wph wps=wph wph=wi wps=wph wps=wi wph=wi
    wph=wph wph=wph wps=wph wps=wi wph=wi wph=wph wps=wph wps=wi wps=wi wph=wph
    wph=wph wps=wph wps=wi min=ax-1 wph=wph wph=wph wps=wph wps=wi wch=wph
    maj=ax-2 maj=ax-mp id1=ax-mp $.
---------The proof of "id1" (314 bytes) ends above this line.


MM> show proof id1 /explicit /packed
Proof of "id1":
---------Clip out the proof below this line to put it in the source file:
    wph=wph wph=wph wps=wph 1:wps=wi 2:wph=wi wps=1 wph=wph wps=wph min=ax-1
    wph=wph wph=1 wps=wph wps=wi wph=wi wph=2 wps=1 wps=wi wph=wph wps=1
    min=ax-1 wph=wph wps=1 wch=wph maj=ax-2 maj=ax-mp id1=ax-mp $.
---------The proof of "id1" (201 bytes) ends above this line.


(Note trick to get an unpacked compressed proof.)
MM> save proof id1 /normal
The proof of "id1" has been reformatted and saved internally.
Remember to use WRITE SOURCE to save changes permanently.
MM> show proof id1 /compressed /fast
Proof of "id1":
---------Clip out the proof below this line to put it in the source file:
    ( wi ax-1 ax-2 ax-mp ) AAABBAABAACAAABABBAAABBAABBAAABCAAABADEE $.
---------The proof of "id1" (63 bytes) ends above this line.


(Note that Z indicates a new local label on the immediately preceding step; compare to packed normal proof above)
MM> show proof id1 /compressed
Proof of "id1":
---------Clip out the proof below this line to put it in the source file:
    ( wi ax-1 ax-2 ax-mp ) AAABZBZFAACAFABBGFBAFCAFADEE $.
---------The proof of "id1" (51 bytes) ends above this line.

Norm

[Haitao Zhang]

This is great! I know I will come back to this thread to reference the insights provided here from time to time.

I think I finally grokked how the compression worked. I didn't take much notice of the list of labels in () before the compressed string. Taking the hints from here and re-reading the Appendix B it dawned on me that the decompressed integers (those greater than the number of mandatory hypotheses) are referring to the labels in the list. And Z is actually an operator to add a (unnamed) proof step to the label list. Very clever!

On Monday, February 11, 2019 at 7:29:59 AM UTC-8, Norman Megill wrote:

The only proof format defined by the official Metamath spec (pp. 100-103 of the Metamath book) is the "normal" format consisting of an RPN list of labels.  Support for "compressed" format (Appendix B) is theoretically optional for a program to be considered a Metamath proof verifier, but it is strongly encouraged because of the significant size and speed savings for compressed proofs.

[Haitao Zhang]

I am confused about how implication can be proved in Metamath. I am used to the intros tactic. What is the corresponding procedure here?

Haitao

[David A. Wheeler]

On Tue, 12 Feb 2019 20:18:43 -0800 (PST), Haitao Zhang <zht...@gmail.com> wrote:
> I am confused about how implication can be proved in Metamath. I am used to
> the intros tactic. What is the corresponding procedure here?

Others can answer this better than I can, but I'll take a shot.

First, if you're creating new proofs, I personally
recommend using mmj2 over metamath.exe itself.
mmj2 makes it much easier to create proofs forwards & backwards;
the proof assistant in metamath "wants" to go backwards (you can go the other
ways but it's trickier).

By using the term "tactic" that implies that you want to go backwards from a goal.
The simple answer is that *any* theorem or axiom that produces the goal
can be used as a way to get there.

I'll assume you're using set.mm. One way to get an implication is con4i,
which produces (𝜓 → 𝜑) but requires that you first prove (¬ 𝜑 → ¬ 𝜓).
So working backwards, if you want to prove (𝜓 → 𝜑) and you justify with with con4i,
you must now prove (¬ 𝜑 → ¬ 𝜓).

Metamath tools currently don't have anything that is exactly like the "tactic languages"
of Coq & the HOL family. In those systems, you provide steps that are not
really the proof, but programming steps that help the computer rediscover
the proof. In Metamath, instead of recording a program that can be run to try to
rediscover the proof, Metamath records the actual proof found & the actual steps used.
So instead of running a generic tactic like "intros" you specify the exact transformation.
Since Metamath emphasizes such a general substitution rule,
you end up creating a number of very general patterns that can be reused.
Some tools (like mmj2) have some built-in logic that's like "tactics" sortof (not really).
Also: mmj2 can *find* the justification for you if given the before & after
and there's already a matching justification in the database.

These are very different approaches & I'm not sure I'm explaining it well,
but hopefully that's a start.

--- David A. Wheeler

[Haitao Zhang]

Thanks David. I am using mmj2. Suppose I want to prove implication |- ( ph -> ps ), should I first create some named natural deduction form $e |- ph $. $p |- ps $. (which I know how to prove)? What do I then use to get the implication?

I read this from the webpage but I don't see how I can get the implication form:

Once you have an assertion in deduction form, you can easily convert it to inference form or closed form:

• To prove some assertion Ti in inference form, given assertion Td in deduction form, there is a simple mechanical process you can use. First take each Ti hypothesis and insert a T. ->prefix ("true implies") using a1i. You can then use the existing assertion Td to prove the resulting conclusion with a T. -> prefix. Finally, you can remove that prefix using trud, resulting in the conclusion you wanted to prove.
• To prove some assertion T in closed form, given assertion Td in deduction form, there is another simple mechanical process you can use. First, select an expression that is the conjunction (...∧...) of all of the consequents of every hypothesis of Td. Next, prove that this expression implies each of the separate hypotheses of Td in turn by eliminating conjuncts (there are a variety of proven assertions to do this, including simpl, simpr, 3simpa, 3simpb, 3simpc, simp1, simp2, and simp3). If the expression has nested conjunctions, inner conjuncts can be broken out by chaining the above theorems with syl. (There are actually many theorems (labeled simp* such as simp333) that break out inner conjuncts in one step, but rather than learning them you can just use the chaining we just described to prove them, and then let the metamath.exe command "minimize_with" figure out the right ones needed to collapse them.) As your final step, you can then apply the already-proven assertion Td (which is in deduction form), proving assertion T in closed form.

--
You received this message because you are subscribed to a topic in the Google Groups "Metamath" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/metamath/7uJBdCd9tbc/unsubscribe.
To unsubscribe from this group and all its topics, send an email to metamath+u...@googlegroups.com.

[Haitao Zhang]

It appears what I wanted could not be done in general and I will accept that. I believe I finally understand what the prescribed procedure means to convert from deduction form to closed form. The closed form is obtained by the substitution of the common antecedent by the conjunction of all hypotheses.  This is what is meant by "As your final step, you can then apply the already-proven assertion Td (which is in deduction form), proving assertion T in closed form." which I didn't quite understand earlier.

Thanks for bearing with me.

[Jens-Wolfhard Schicke-Uffmann]

On Wed, Feb 13, 2019 at 12:02:59AM -0500, David A. Wheeler wrote:
> On Tue, 12 Feb 2019 20:18:43 -0800 (PST), Haitao Zhang <zht...@gmail.com> wrote:
> > I am confused about how implication can be proved in Metamath. I am used to
> > the intros tactic. What is the corresponding procedure here?

> Metamath tools currently don't have anything that is exactly like the "tactic languages"
> of Coq & the HOL family. In those systems, you provide steps that are not
> really the proof, but programming steps that help the computer rediscover
> the proof.

This is not entirely accurate. I used
https://github.com/Drahflow/Igor
for creating the huge program covering proofs I once posted on the list
(that project is currently paused, not for lack of progress but for
other more economically useful things going on)

While this tools is clearly not as user-friendly as mmj2 is
(and I just notice I never got around writing documentation :( )
a session could go like this:

% prove lem-strimm

0) |- ( ( X step Y /\ ( ( X reg ; 1 5 ) = Z /\ ( ( X mem ( Z + 0 ) ) = 0
/\ ( ( X mem ( Z + 1 ) ) = ( ; 1 6 x. R ) /\ ( ( X mem ( Z + 2 ) ) = ( ;
; 1 2 8 + Q ) /\ ( ( X mem ( Z + 3 ) ) = ; ; 2 2 9 /\ ( R e. NN0 /\ ( R
<_ ; 1 4 /\ ( Q e. NN0 /\ ( Q <_ ; 1 4 /\ ( ( X reg Q ) mod 4 ) = 0 ) )
) ) ) ) ) ) ) ) -> ( ( Y mem32 ( X reg Q ) ) = ( X reg R ) /\ ( ( Y reg
; 1 5 ) = ( Z + 4 ) /\ ( A. q ( q <_ ; 1 4 -> ( Y reg q ) = ( X reg q )
) /\ A. m e. cpu-mem ( ( m < ( X reg Q ) \/ ( ( X reg Q ) + 3 ) < m ) ->
( Y mem m ) = ( X mem m ) ) ) ) ) )

% autoall
% antedisp

* X step Y
* ( X reg ; 1 5 ) = Z
* ( X mem ( Z + 0 ) ) = 0
* ( X mem ( Z + 1 ) ) = ( ; 1 6 x. R )
* ( X mem ( Z + 2 ) ) = ( ; ; 1 2 8 + Q )
* ( X mem ( Z + 3 ) ) = ; ; 2 2 9
* R e. NN0
* R <_ ; 1 4
* Q e. NN0
* Q <_ ; 1 4
* ( ( X reg Q ) mod 4 ) = 0
-------------------------------------------------
( ( Y mem32 ( X reg Q ) ) = ( X reg R ) /\ ( ( Y reg ; 1 5 ) = ( Z + 4
) /\ ( A. q ( q <_ ; 1 4 -> ( Y reg q ) = ( X reg q ) ) /\ A. m e.
cpu-mem ( ( m < ( X reg Q ) \/ ( ( X reg Q ) + 3 ) < m ) -> ( Y mem m
) = ( X mem m ) ) ) ) )

% conclude ( ( Y mem ( ( X reg Q ) + 0 ) ) = ( uint8 ` ( X reg R ) ) /\ (
( Y mem ( ( X reg Q ) + 1 ) ) = ( uint8 ` ( |_ ` ( ( X reg R ) / ; ; 2 5
6 ) ) ) /\ ( ( Y mem ( ( X reg Q ) + 2 ) ) = ( uint8 ` ( |_ ` ( ( X reg
R ) / ; ; ; ; 6 5 5 3 6 ) ) ) /\ ( ( Y mem ( ( X reg Q ) + 3 ) ) = (
uint8 ` ( |_ ` ( ( X reg R ) / ; ; ; ; ; ; ; 1 6 7 7 7 2 1 6 ) ) ) /\ (
( Y reg ; 1 5 ) = ( Z + 4 ) /\ ( A. q ( q <_ ; 1 4 -> ( Y reg q ) = ( X
reg q ) ) /\ A. m e. cpu-mem ( ( m < ( X reg Q ) \/ ( ( X reg Q ) + 3 )
< m ) -> ( Y mem m ) = ( X mem m ) ) ) ) ) ) ) )

* ( ( Y mem ( ( X reg Q ) + 0 ) ) = ( uint8 ` ( X reg R ) ) /\ ( ( Y mem
( ( X reg Q ) + 1 ) ) = ( uint8 ` ( |_ ` ( ( X reg R ) / ; ; 2 5 6 ) )
) /\ ( ( Y mem ( ( X reg Q ) + 2 ) ) = ( uint8 ` ( |_ ` ( ( X reg R )
/ ; ; ; ; 6 5 5 3 6 ) ) ) /\ ( ( Y mem ( ( X reg Q ) + 3 ) ) = ( uint8
` ( |_ ` ( ( X reg R ) / ; ; ; ; ; ; ; 1 6 7 7 7 2 1 6 ) ) ) /\ ( ( Y
reg ; 1 5 ) = ( Z + 4 ) /\ ( A. q ( q <_ ; 1 4 -> ( Y reg q ) = ( X
reg q ) ) /\ A. m e. cpu-mem ( ( m < ( X reg Q ) \/ ( ( X reg Q ) + 3
) < m ) -> ( Y mem m ) = ( X mem m ) ) ) ) ) ) ) )
* X step Y
* ( X reg ; 1 5 ) = Z
* ( X mem ( Z + 0 ) ) = 0
* ( X mem ( Z + 1 ) ) = ( ; 1 6 x. R )
* ( X mem ( Z + 2 ) ) = ( ; ; 1 2 8 + Q )
* ( X mem ( Z + 3 ) ) = ; ; 2 2 9
* R e. NN0
* R <_ ; 1 4
* Q e. NN0
* Q <_ ; 1 4
* ( ( X reg Q ) mod 4 ) = 0
-------------------------------------------------
( ( Y mem32 ( X reg Q ) ) = ( X reg R ) /\ ( ( Y reg ; 1 5 ) = ( Z + 4
) /\ ( A. q ( q <_ ; 1 4 -> ( Y reg q ) = ( X reg q ) ) /\ A. m e.
cpu-mem ( ( m < ( X reg Q ) \/ ( ( X reg Q ) + 3 ) < m ) -> ( Y mem m
) = ( X mem m ) ) ) ) )

% normalize:ante

* ( Y mem ( ( X reg Q ) + 0 ) ) = ( uint8 ` ( X reg R ) )
* ( Y mem ( ( X reg Q ) + 1 ) ) = ( uint8 ` ( |_ ` ( ( X reg R ) / ; ; 2 5 6 ) ) )
* ( Y mem ( ( X reg Q ) + 2 ) ) = ( uint8 ` ( |_ ` ( ( X reg R ) / ; ; ; ; 6 5 5 3 6 ) ) )
* ( Y mem ( ( X reg Q ) + 3 ) ) = ( uint8 ` ( |_ ` ( ( X reg R ) / ; ; ; ; ; ; ; 1 6 7 7 7 2 1 6 ) ) )
* ( Y reg ; 1 5 ) = ( Z + 4 )
* A. q ( q <_ ; 1 4 -> ( Y reg q ) = ( X reg q ) )
* A. m e. cpu-mem ( ( m < ( X reg Q ) \/ ( ( X reg Q ) + 3 ) < m ) -> ( Y mem m ) = ( X mem m ) )
* X step Y
* ( X reg ; 1 5 ) = Z
* ( X mem ( Z + 0 ) ) = 0
* ( X mem ( Z + 1 ) ) = ( ; 1 6 x. R )
* ( X mem ( Z + 2 ) ) = ( ; ; 1 2 8 + Q )
* ( X mem ( Z + 3 ) ) = ; ; 2 2 9
* R e. NN0
* R <_ ; 1 4
* Q e. NN0
* Q <_ ; 1 4
* ( ( X reg Q ) mod 4 ) = 0
-------------------------------------------------
( ( Y mem32 ( X reg Q ) ) = ( X reg R ) /\ ( ( Y reg ; 1 5 ) = ( Z + 4
) /\ ( A. q ( q <_ ; 1 4 -> ( Y reg q ) = ( X reg q ) ) /\ A. m e.
cpu-mem ( ( m < ( X reg Q ) \/ ( ( X reg Q ) + 3 ) < m ) -> ( Y mem m
) = ( X mem m ) ) ) ) )

% rewrite ( Y mem32 ( X reg Q ) ) = ( ( ( ( ( Y mem ( ( X reg Q ) + 3 ) )
x. ; ; ; ; ; ; ; 1 6 7 7 7 2 1 6 ) + ( ( Y mem ( ( X reg Q ) + 2 ) ) x.
; ; ; ; 6 5 5 3 6 ) ) + ( ( Y mem ( ( X reg Q ) + 1 ) ) x. ; ; 2 5 6 ) )
+ ( Y mem ( ( X reg Q ) + 0 ) ) )
% use df-mem32

* ( Y mem ( ( X reg Q ) + 0 ) ) = ( uint8 ` ( X reg R ) )
* ( Y mem ( ( X reg Q ) + 1 ) ) = ( uint8 ` ( |_ ` ( ( X reg R ) / ; ; 2 5 6 ) ) )
* ( Y mem ( ( X reg Q ) + 2 ) ) = ( uint8 ` ( |_ ` ( ( X reg R ) / ; ; ; ; 6 5 5 3 6 ) ) )
* ( Y mem ( ( X reg Q ) + 3 ) ) = ( uint8 ` ( |_ ` ( ( X reg R ) / ; ; ; ; ; ; ; 1 6 7 7 7 2 1 6 ) ) )
* ( Y reg ; 1 5 ) = ( Z + 4 )
* A. q ( q <_ ; 1 4 -> ( Y reg q ) = ( X reg q ) )
* A. m e. cpu-mem ( ( m < ( X reg Q ) \/ ( ( X reg Q ) + 3 ) < m ) -> ( Y mem m ) = ( X mem m ) )
* X step Y
* ( X reg ; 1 5 ) = Z
* ( X mem ( Z + 0 ) ) = 0
* ( X mem ( Z + 1 ) ) = ( ; 1 6 x. R )
* ( X mem ( Z + 2 ) ) = ( ; ; 1 2 8 + Q )
* ( X mem ( Z + 3 ) ) = ; ; 2 2 9
* R e. NN0
* R <_ ; 1 4
* Q e. NN0
* Q <_ ; 1 4
* ( ( X reg Q ) mod 4 ) = 0
-------------------------------------------------
( ( ( ( ( ( Y mem ( ( X reg Q ) + 3 ) ) x. ; ; ; ; ; ; ; 1 6 7 7 7 2 1
6 ) + ( ( Y mem ( ( X reg Q ) + 2 ) ) x. ; ; ; ; 6 5 5 3 6 ) ) + ( ( Y
mem ( ( X reg Q ) + 1 ) ) x. ; ; 2 5 6 ) ) + ( Y mem ( ( X reg Q ) + 0
) ) ) = ( X reg R ) /\ ( ( Y reg ; 1 5 ) = ( Z + 4 ) /\ ( A. q ( q <_
; 1 4 -> ( Y reg q ) = ( X reg q ) ) /\ A. m e. cpu-mem ( ( m < ( X
reg Q ) \/ ( ( X reg Q ) + 3 ) < m ) -> ( Y mem m ) = ( X mem m ) ) )
) )

% rewrite ( Y mem ( ( X reg Q ) + 0 ) ) = ( uint8 ` ( X reg R ) )
% rewrite ( Y mem ( ( X reg Q ) + 1 ) ) = ( uint8 ` ( |_ ` ( ( X reg R ) /
; ; 2 5 6 ) ) )
% rewrite ( Y mem ( ( X reg Q ) + 2 ) ) = ( uint8 ` ( |_ ` ( ( X reg R ) /
; ; ; ; 6 5 5 3 6 ) ) )
% rewrite ( Y mem ( ( X reg Q ) + 3 ) ) = ( uint8 ` ( |_ ` ( ( X reg R ) /
; ; ; ; ; ; ; 1 6 7 7 7 2 1 6 ) ) )

% normalize

* ( uint8 ` ( X reg R ) ) = ( uint8 ` ( X reg R ) )
* ( uint8 ` ( |_ ` ( ( X reg R ) / ; ; 2 5 6 ) ) ) = ( uint8 ` ( |_ ` ( ( X reg R ) / ; ; 2 5 6 ) ) )
* ( uint8 ` ( |_ ` ( ( X reg R ) / ; ; ; ; 6 5 5 3 6 ) ) ) = ( uint8 ` ( |_ ` ( ( X reg R ) / ; ; ; ; 6 5 5 3 6 ) ) )
* ( uint8 ` ( |_ ` ( ( X reg R ) / ; ; ; ; ; ; ; 1 6 7 7 7 2 1 6 ) ) ) = ( uint8 ` ( |_ ` ( ( X reg R ) / ; ; ; ; ; ; ; 1 6 7 7 7 2 1 6 ) ) )
* ( Y reg ; 1 5 ) = ( Z + 4 )
* A. q ( q <_ ; 1 4 -> ( Y reg q ) = ( X reg q ) )
* A. m e. cpu-mem ( ( m < ( X reg Q ) \/ ( ( X reg Q ) + 3 ) < m ) -> ( Y mem m ) = ( X mem m ) )
* X step Y
* ( X reg ; 1 5 ) = Z
* ( X mem ( Z + 0 ) ) = 0
* ( X mem ( Z + 1 ) ) = ( ; 1 6 x. R )
* ( X mem ( Z + 2 ) ) = ( ; ; 1 2 8 + Q )
* ( X mem ( Z + 3 ) ) = ; ; 2 2 9
* R e. NN0
* R <_ ; 1 4
* Q e. NN0
* Q <_ ; 1 4
* ( ( X reg Q ) mod 4 ) = 0
-------------------------------------------------
( ( ( ( ( uint8 ` ( |_ ` ( ( X reg R ) / ; ; ; ; ; ; ; 1 6 7 7 7 2 1 6
) ) ) x. ; ; ; ; ; ; ; 1 6 7 7 7 2 1 6 ) + ( ( uint8 ` ( |_ ` ( ( X
reg R ) / ; ; ; ; 6 5 5 3 6 ) ) ) x. ; ; ; ; 6 5 5 3 6 ) ) + ( ( uint8
` ( |_ ` ( ( X reg R ) / ; ; 2 5 6 ) ) ) x. ; ; 2 5 6 ) ) + ( uint8 `
( X reg R ) ) ) = ( X reg R )

% drop everything matching Z
% drop everything matching q
% drop everything matching m

% conclude X e. armstates
% with only X step Y
% drop X step Y

% drop everything matching uint8

* X e. armstates
* R e. NN0
* R <_ ; 1 4
* Q e. NN0
* Q <_ ; 1 4
* ( ( X reg Q ) mod 4 ) = 0
-------------------------------------------------
( ( ( ( ( uint8 ` ( |_ ` ( ( X reg R ) / ; ; ; ; ; ; ; 1 6 7 7 7 2 1 6
) ) ) x. ; ; ; ; ; ; ; 1 6 7 7 7 2 1 6 ) + ( ( uint8 ` ( |_ ` ( ( X
reg R ) / ; ; ; ; 6 5 5 3 6 ) ) ) x. ; ; ; ; 6 5 5 3 6 ) ) + ( ( uint8
` ( |_ ` ( ( X reg R ) / ; ; 2 5 6 ) ) ) x. ; ; 2 5 6 ) ) + ( uint8 `
( X reg R ) ) ) = ( X reg R )

... and so on until finally ...

% export:disj
$d X n $. $d R n $.

% export:compressed
( co cdc carmreg wa c6 c1 cfv wceq caddc c5 c2 cv c7 cmem wbr cuint8 c4
cdiv cfl c3 cle wcel cc0 cmul cn0 wi clt cmo wral wo ccpumem wal c9
cstep vn c8 carmstates id anim2i cmem32 oveq1d syl simpl adantl eqeq1d
anbi1d a1i fveq2d adantl4 jca imbi12d mpbird mpcom oveq12d mpd anbi2d
oveq2d adantl2 animpass mpancom arm_strimm df-mem32 adantl3 armstep1
arm_reg32 lem-uint32-uint8 expcom rgen arm_regnn0 ax-17 breq1d eqeq12d
rcla4 anbi2d4 imbi2d expcom2 expcom4 animpass4 ) EDAJHZUJPHUAHZDBJHZUCNZ
OZEXFMPHUAHZXHRQILIZUEHZUFNZUCNZOZEXFRPHUAHZXHLQIQIUGILIZUEHZUFNZUCNZOZE
<...snip...>
KYSUVHUULUVGXHUVHVEVLVMXBVSVTXCXDWFWFXEWG $.

It's definitely not as generic as Isabelle/HOL, but I think quite a
notch more abstract than the tools we traditionally use for metamath.


Regards,
Drahflow