HomePage RecentChanges

mmj2MoreDummyVarSpecs

The first "hilims" example shows unification (and proof construction) with work variables still in the proof.

Note that "hilims" variables are almost all "dummy" variables, but that some of the work variables got resolved into "dummy" variables during unification -- leaving a mixture of dummy variables and work variables.

The second "hilims" example shows the new mmj2 "work variable to dummy variable" conversion algorithm, which replaces any remaining work variables with dummy variables.

As you can determine by comparing the second example with the original "hilims" proof -- step 10 for example – in some cases where "x" is already in the proof step, mmj2 substitutes a different dummy variable, such as "w".

The reason for this is that although a "dummy" should be freely substitutable with another dummy in most cases popping up in mmj2 now, there is the theoretical possibility that substituting "x" into a formula that already contains "x" could result in a "hard" Distinct Variables Requirement error ($d error).

So to be "safe" mmj2 picks an unused dummy variable. This leads to a different issue which is not particularly serious, which is that additional $d statements may be needed on the theorem being proved. Thus, the users will be encouraged to use the "Generate Replacements" or "Generate Differences" RunParm?/Edit Option for Dj Vars editing.

Primarily this is an "issue" when re-processing existing proofs, and is almost a non-issue for new authorship. Still, the new mmj2 algorithm is less parsimonous with dummy variables than, say, Megill would be. Where Megill might require only x, y and z, mmj2 might need x, y, z, u, v and w. (It is very hard to write code that is as smart as Megill!)

If you have any suggestions, comments or complaints, speak up ASAP before I release this code into the wild!

Thanks!

P.S. Something I discovered during testing is that after converting any remaining work variables to dummy variables, the code must redo the Distinct Variable Restriction edits for affected derivation proof steps. Which is not hard, just a tedious gotcha (already coded…)

P.P.S. The proof of "hilims" looks much better with TMFF formatting option 4 - Align Var, Depth 4 -- than the default, Align Column, Depth 3. As a general rule long formulas containing the ".< x , y .>" point/coordinate syntax item look better with option 4 – that is because TMFF gives no weight to a point/coordinate as a single item but treats it the same as any other syntax form involving 2 operands.


hilims after unification with some work vars

    $( <MM> <PROOF_ASST> THEOREM=hilims  LOC_AFTER=?
     
    * The metric space induced by Hilbert space.
     
    h1::hilims.1       |-   D
                          = {
                            <.
                            <. x
                            ,  y
                            >.
                            ,  z
                            >.
                            |  (  ( x e. H~ /\ y e. H~ )
                               /\ z = ( normh ` ( x -h y ) ) ) }
    2::df-3an          |- (   (  &S1 e. H~
                              /\ &S2 e. H~
                              /\   &S5
                                 = ( normh
                                   ` ( &S1 +h ( -u 1 .h &S2 ) ) ) )
                          <-> (  ( &S1 e. H~ /\ &S2 e. H~ )
                              /\   &S5
                                 = ( normh
                                   ` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) )
    3:2:oprabbii       |-   {
                            <.
                            <. &S1
                            ,  &S2
                            >.
                            ,  &S5
                            >.
                            |  (  &S1 e. H~
                               /\ &S2 e. H~
                               /\   &S5
                                  = ( normh
                                    ` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) }
                          = {
                            <.
                            <. &S1
                            ,  &S2
                            >.
                            ,  &S5
                            >.
                            |  (  ( &S1 e. H~ /\ &S2 e. H~ )
                               /\   &S5
                                  = ( normh
                                    ` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) }
    4::fvex            |-    ( normh
                             ` ( &S1 +h ( -u 1 .h &S2 ) ) )
                          e. V
    5::eqid            |-   {
                            <.
                            <. &S1
                            ,  &S2
                            >.
                            ,  &S5
                            >.
                            |  (  ( &S1 e. H~ /\ &S2 e. H~ )
                               /\   &S5
                                  = ( normh
                                    ` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) }
                          = {
                            <.
                            <. &S1
                            ,  &S2
                            >.
                            ,  &S5
                            >.
                            |  (  ( &S1 e. H~ /\ &S2 e. H~ )
                               /\   &S5
                                  = ( normh
                                    ` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) }
    6:4,5:fnoprab2     |-    {
                             <.
                             <. &S1
                             ,  &S2
                             >.
                             ,  &S5
                             >.
                             |  (  ( &S1 e. H~ /\ &S2 e. H~ )
                                /\   &S5
                                   = ( normh
                                     ` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) }
                          Fn ( H~ X. H~ )
    7::fvex            |- ( normh ` ( x -h y ) ) e. V
    8::eqid            |-   {
                            <.
                            <. x
                            ,  y
                            >.
                            ,  z
                            >.
                            |  (  ( x e. H~ /\ y e. H~ )
                               /\ z = ( normh ` ( x -h y ) ) ) }
                          = {
                            <.
                            <. x
                            ,  y
                            >.
                            ,  z
                            >.
                            |  (  ( x e. H~ /\ y e. H~ )
                               /\ z = ( normh ` ( x -h y ) ) ) }
    9:7,8:fnoprab2     |-    {
                             <.
                             <. x
                             ,  y
                             >.
                             ,  z
                             >.
                             |  (  ( x e. H~ /\ y e. H~ )
                                /\ z = ( normh ` ( x -h y ) ) ) }
                          Fn ( H~ X. H~ )
    10::eqfnoprval     |- (  (     {
                                   <.
                                   <. &S1
                                   ,  &S2
                                   >.
                                   ,  &S5
                                   >.
                                   |  (  ( &S1 e. H~ /\ &S2 e. H~ )
                                      /\   &S5
                                         = ( normh
                                           ` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) }
                                Fn ( H~ X. H~ )
                             /\    {
                                   <.
                                   <. x
                                   ,  y
                                   >.
                                   ,  z
                                   >.
                                   |  (  ( x e. H~ /\ y e. H~ )
                                      /\ z = ( normh ` ( x -h y ) ) ) }
                                Fn ( H~ X. H~ ) )
                          -> (     {
                                   <.
                                   <. &S1
                                   ,  &S2
                                   >.
                                   ,  &S5
                                   >.
                                   |  (  ( &S1 e. H~ /\ &S2 e. H~ )
                                      /\   &S5
                                         = ( normh
                                           ` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) }
                                 = {
                                   <.
                                   <. x
                                   ,  y
                                   >.
                                   ,  z
                                   >.
                                   |  (  ( x e. H~ /\ y e. H~ )
                                      /\ z = ( normh ` ( x -h y ) ) ) }
                             <-> (  ( H~ X. H~ ) = ( H~ X. H~ )
                                 /\ A. &S18
                                    e. H~
                                       A. &S19
                                       e. H~
                                            ( &S18
                                              {
                                              <.
                                              <. &S1
                                              ,  &S2
                                              >.
                                              ,  &S5
                                              >.
                                              |  (  ( &S1 e. H~ /\ &S2 e. H~ )
                                                 /\   &S5
                                                    = ( normh
                                                      ` ( &S1 +h ( -u 1 .h &S2 ) )
                                                      ) ) }
                                              &S19 )
                                          = ( &S18
                                              {
                                              <.
                                              <. x
                                              ,  y
                                              >.
                                              ,  z
                                              >.
                                              |  (  ( x e. H~ /\ y e. H~ )
                                                 /\ z = ( normh ` ( x -h y ) ) ) }
                                              &S19 ) ) ) )
    11:6,9,10:mp2an    |- (     {
                                <.
                                <. &S1
                                ,  &S2
                                >.
                                ,  &S5
                                >.
                                |  (  ( &S1 e. H~ /\ &S2 e. H~ )
                                   /\   &S5
                                      = ( normh
                                        ` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) }
                              = {
                                <.
                                <. x
                                ,  y
                                >.
                                ,  z
                                >.
                                |  (  ( x e. H~ /\ y e. H~ )
                                   /\ z = ( normh ` ( x -h y ) ) ) }
                          <-> (  ( H~ X. H~ ) = ( H~ X. H~ )
                              /\ A. &S18
                                 e. H~
                                    A. &S19
                                    e. H~
                                         ( &S18
                                           {
                                           <.
                                           <. &S1
                                           ,  &S2
                                           >.
                                           ,  &S5
                                           >.
                                           |  (  ( &S1 e. H~ /\ &S2 e. H~ )
                                              /\   &S5
                                                 = ( normh
                                                   ` ( &S1 +h ( -u 1 .h &S2 ) ) ) )
                                           }
                                           &S19 )
                                       = ( &S18
                                           {
                                           <.
                                           <. x
                                           ,  y
                                           >.
                                           ,  z
                                           >.
                                           |  (  ( x e. H~ /\ y e. H~ )
                                              /\ z = ( normh ` ( x -h y ) ) ) }
                                           &S19 ) ) )
    12::eqid           |- ( H~ X. H~ ) = ( H~ X. H~ )
    13::hvsubvalt      |- (  ( &S18 e. H~ /\ &S19 e. H~ )
                          ->   ( &S18 -h &S19 )
                             = ( &S18 +h ( -u 1 .h &S19 ) ) )
    14:13:eqcomd       |- (  ( &S18 e. H~ /\ &S19 e. H~ )
                          ->   ( &S18 +h ( -u 1 .h &S19 ) )
                             = ( &S18 -h &S19 ) )
    15:14:fveq2d       |- (  ( &S18 e. H~ /\ &S19 e. H~ )
                          ->   ( normh
                               ` ( &S18 +h ( -u 1 .h &S19 ) ) )
                             = ( normh ` ( &S18 -h &S19 ) ) )
    16::fvex           |-    ( normh
                             ` ( &S18 +h ( -u 1 .h &S19 ) ) )
                          e. V
    17::opreq1         |- (  &S1 = &S18
                          ->   ( &S1 +h ( -u 1 .h &S2 ) )
                             = ( &S18 +h ( -u 1 .h &S2 ) ) )
    18:17:fveq2d       |- (  &S1 = &S18
                          ->   ( normh
                               ` ( &S1 +h ( -u 1 .h &S2 ) ) )
                             = ( normh
                               ` ( &S18 +h ( -u 1 .h &S2 ) ) ) )
    19::opreq2         |- (  &S2 = &S19
                          -> ( -u 1 .h &S2 ) = ( -u 1 .h &S19 ) )
    20:19:opreq2d      |- (  &S2 = &S19
                          ->   ( &S18 +h ( -u 1 .h &S2 ) )
                             = ( &S18 +h ( -u 1 .h &S19 ) ) )
    21:20:fveq2d       |- (  &S2 = &S19
                          ->   ( normh
                               ` ( &S18 +h ( -u 1 .h &S2 ) ) )
                             = ( normh
                               ` ( &S18 +h ( -u 1 .h &S19 ) ) ) )
    22::eqid           |-   {
                            <.
                            <. &S1
                            ,  &S2
                            >.
                            ,  &S5
                            >.
                            |  (  ( &S1 e. H~ /\ &S2 e. H~ )
                               /\   &S5
                                  = ( normh
                                    ` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) }
                          = {
                            <.
                            <. &S1
                            ,  &S2
                            >.
                            ,  &S5
                            >.
                            |  (  ( &S1 e. H~ /\ &S2 e. H~ )
                               /\   &S5
                                  = ( normh
                                    ` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) }
    23:16,18,21,22:oprabval2 
                       |- (  ( &S18 e. H~ /\ &S19 e. H~ )
                          ->   ( &S18
                                 {
                                 <.
                                 <. &S1
                                 ,  &S2
                                 >.
                                 ,  &S5
                                 >.
                                 |  (  ( &S1 e. H~ /\ &S2 e. H~ )
                                    /\   &S5
                                       = ( normh
                                         ` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) }
                                 &S19 )
                             = ( normh
                               ` ( &S18 +h ( -u 1 .h &S19 ) ) ) )
    24::eqid           |-   {
                            <.
                            <. x
                            ,  y
                            >.
                            ,  z
                            >.
                            |  (  ( x e. H~ /\ y e. H~ )
                               /\ z = ( normh ` ( x -h y ) ) ) }
                          = {
                            <.
                            <. x
                            ,  y
                            >.
                            ,  z
                            >.
                            |  (  ( x e. H~ /\ y e. H~ )
                               /\ z = ( normh ` ( x -h y ) ) ) }
    25:24:hilmsdval    |- (  ( &S18 e. H~ /\ &S19 e. H~ )
                          ->   ( &S18
                                 {
                                 <.
                                 <. x
                                 ,  y
                                 >.
                                 ,  z
                                 >.
                                 |  (  ( x e. H~ /\ y e. H~ )
                                    /\ z = ( normh ` ( x -h y ) ) ) }
                                 &S19 )
                             = ( normh ` ( &S18 -h &S19 ) ) )
    26:15,23,25:3eqtr4d 
                       |- (  ( &S18 e. H~ /\ &S19 e. H~ )
                          ->   ( &S18
                                 {
                                 <.
                                 <. &S1
                                 ,  &S2
                                 >.
                                 ,  &S5
                                 >.
                                 |  (  ( &S1 e. H~ /\ &S2 e. H~ )
                                    /\   &S5
                                       = ( normh
                                         ` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) }
                                 &S19 )
                             = ( &S18
                                 {
                                 <.
                                 <. x
                                 ,  y
                                 >.
                                 ,  z
                                 >.
                                 |  (  ( x e. H~ /\ y e. H~ )
                                    /\ z = ( normh ` ( x -h y ) ) ) }
                                 &S19 ) )
    27:26:rgen2        |- A. &S18
                          e. H~
                             A. &S19
                             e. H~
                                  ( &S18
                                    {
                                    <.
                                    <. &S1
                                    ,  &S2
                                    >.
                                    ,  &S5
                                    >.
                                    |  (  ( &S1 e. H~ /\ &S2 e. H~ )
                                       /\   &S5
                                          = ( normh
                                            ` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) }
                                    &S19 )
                                = ( &S18
                                    {
                                    <.
                                    <. x
                                    ,  y
                                    >.
                                    ,  z
                                    >.
                                    |  (  ( x e. H~ /\ y e. H~ )
                                       /\ z = ( normh ` ( x -h y ) ) ) }
                                    &S19 )
    28:11,12,27:mpbir2an 
                       |-   {
                            <.
                            <. &S1
                            ,  &S2
                            >.
                            ,  &S5
                            >.
                            |  (  ( &S1 e. H~ /\ &S2 e. H~ )
                               /\   &S5
                                  = ( normh
                                    ` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) }
                          = {
                            <.
                            <. x
                            ,  y
                            >.
                            ,  z
                            >.
                            |  (  ( x e. H~ /\ y e. H~ )
                               /\ z = ( normh ` ( x -h y ) ) ) }
    29:3,28:eqtr       |-   {
                            <.
                            <. &S1
                            ,  &S2
                            >.
                            ,  &S5
                            >.
                            |  (  &S1 e. H~
                               /\ &S2 e. H~
                               /\   &S5
                                  = ( normh
                                    ` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) }
                          = {
                            <.
                            <. x
                            ,  y
                            >.
                            ,  z
                            >.
                            |  (  ( x e. H~ /\ y e. H~ )
                               /\ z = ( normh ` ( x -h y ) ) ) }
    30:29:opeq2i       |-   <. H~
                            ,  {
                               <.
                               <. &S1
                               ,  &S2
                               >.
                               ,  &S5
                               >.
                               |  (  &S1 e. H~
                                  /\ &S2 e. H~
                                  /\   &S5
                                     = ( normh
                                       ` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) } >.
                          = <. H~
                            ,  {
                               <.
                               <. x
                               ,  y
                               >.
                               ,  z
                               >.
                               |  (  ( x e. H~ /\ y e. H~ )
                                  /\ z = ( normh ` ( x -h y ) ) ) } >.
    31::hilncv         |- <. <. +h , .h >. , normh >. e. NrmCVec
    32::opex           |- <. +h , .h >. e. V
    33:32:op1st        |-   ( 1st ` <. <. +h , .h >. , normh >. )
                          = <. +h , .h >.
    34:33:eqcomi       |-   <. +h , .h >.
                          = ( 1st ` <. <. +h , .h >. , normh >. )
    35::hilabl         |- +h e. Abel
    36:35:elisseti     |- +h e. V
    37:36:op1st        |- ( 1st ` <. +h , .h >. ) = +h
    38:37:eqcomi       |- +h = ( 1st ` <. +h , .h >. )
    39::hilabl         |- +h e. Abel
    40:39:elisseti     |- +h e. V
    41::hvmulex        |- .h e. V
    42:40,41:op2nd     |- ( 2nd ` <. +h , .h >. ) = .h
    43:42:eqcomi       |- .h = ( 2nd ` <. +h , .h >. )
    44::opex           |- <. +h , .h >. e. V
    45::df-hnorm       |-   normh
                          = {
                            <. &S3
                            ,  &S4
                            >.
                            |  (  &S3 e. H~
                               /\ &S4 = ( sqr ` ( &S3 .ih &S3 ) ) ) }
    46::ax-hilex       |- H~ e. V
    47:46:funopabex2   |-    {
                             <. &S3
                             ,  &S4
                             >.
                             |  (  &S3 e. H~
                                /\ &S4 = ( sqr ` ( &S3 .ih &S3 ) ) ) }
                          e. V
    48:45,47:eqeltr    |- normh e. V
    49:44,48:op2nd     |-   ( 2nd ` <. <. +h , .h >. , normh >. )
                          = normh
    50:49:eqcomi       |-   normh
                          = ( 2nd ` <. <. +h , .h >. , normh >. )
    51::hilabl         |- +h e. Abel
    52::ablgrp         |- ( +h e. Abel -> +h e. Grp )
    53:51,52:ax-mp     |- +h e. Grp
    54::ax-hfvadd      |- +h : ( H~ X. H~ ) --> H~
    55:53,54:grprn     |- H~ = ran +h
    56:34,38,43,50,55:imsval 
                       |- (  <. <. +h , .h >. , normh >. e. NrmCVec
                          ->   ( IndMet ` <. <. +h , .h >. , normh >. )
                             = <. H~
                               ,  {
                                  <.
                                  <. &S1
                                  ,  &S2
                                  >.
                                  ,  &S5
                                  >.
                                  |  (  &S1 e. H~
                                     /\ &S2 e. H~
                                     /\   &S5
                                        = ( normh
                                          ` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) } >. )
    57:31,56:ax-mp     |-   ( IndMet ` <. <. +h , .h >. , normh >. )
                          = <. H~
                            ,  {
                               <.
                               <. &S1
                               ,  &S2
                               >.
                               ,  &S5
                               >.
                               |  (  &S1 e. H~
                                  /\ &S2 e. H~
                                  /\   &S5
                                     = ( normh
                                       ` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) } >.
    58:1:opeq2i        |-   <. H~ , D >.
                          = <. H~
                            ,  {
                               <.
                               <. x
                               ,  y
                               >.
                               ,  z
                               >.
                               |  (  ( x e. H~ /\ y e. H~ )
                                  /\ z = ( normh ` ( x -h y ) ) ) } >.
    qed:30,57,58:3eqtr4 
                       |-   ( IndMet ` <. <. +h , .h >. , normh >. )
                          = <. H~ , D >.
     
    $=  chil &S1 cv chil wcel &S2 cv chil wcel &S5 cv &S1 cv c1 cneg &S2 
        cv csm co cva co cno cfv wceq w3a &S1 &S2 &S5 copab2 cop chil vx cv
        chil wcel vy cv chil wcel wa vz cv vx cv vy cv cmv co cno cfv 
        wceq wa vx vy vz copab2 cop cva csm cop cno cop cims cfv chil cD cop 
        &S1 cv chil wcel &S2 cv chil wcel &S5 cv &S1 cv c1 cneg &S2 cv csm 
        co cva co cno cfv wceq w3a &S1 &S2 &S5 copab2 vx cv chil wcel vy cv
        chil wcel wa vz cv vx cv vy cv cmv co cno cfv wceq wa vx vy vz 
        copab2 chil &S1 cv chil wcel &S2 cv chil wcel &S5 cv &S1 cv c1 cneg &S2
        cv csm co cva co cno cfv wceq w3a &S1 &S2 &S5 copab2 &S1 cv chil 
        wcel &S2 cv chil wcel wa &S5 cv &S1 cv c1 cneg &S2 cv csm co cva co 
        cno cfv wceq wa &S1 &S2 &S5 copab2 vx cv chil wcel vy cv chil wcel 
        wa vz cv vx cv vy cv cmv co cno cfv wceq wa vx vy vz copab2 &S1 cv 
        chil wcel &S2 cv chil wcel &S5 cv &S1 cv c1 cneg &S2 cv csm co cva co
        cno cfv wceq w3a &S1 cv chil wcel &S2 cv chil wcel wa &S5 cv &S1 
        cv c1 cneg &S2 cv csm co cva co cno cfv wceq wa &S1 &S2 &S5 &S1 cv 
        chil wcel &S2 cv chil wcel &S5 cv &S1 cv c1 cneg &S2 cv csm co cva co
        cno cfv wceq df-3an oprabbii &S1 cv chil wcel &S2 cv chil wcel wa
        &S5 cv &S1 cv c1 cneg &S2 cv csm co cva co cno cfv wceq wa &S1 
        &S2 &S5 copab2 vx cv chil wcel vy cv chil wcel wa vz cv vx cv vy cv 
        cmv co cno cfv wceq wa vx vy vz copab2 wceq chil chil cxp chil chil 
        cxp wceq &S18 cv &S19 cv &S1 cv chil wcel &S2 cv chil wcel wa &S5 cv
        &S1 cv c1 cneg &S2 cv csm co cva co cno cfv wceq wa &S1 &S2 &S5 
        copab2 co &S18 cv &S19 cv vx cv chil wcel vy cv chil wcel wa vz cv vx 
        cv vy cv cmv co cno cfv wceq wa vx vy vz copab2 co wceq &S19 chil 
        wral &S18 chil wral &S1 cv chil wcel &S2 cv chil wcel wa &S5 cv &S1 
        cv c1 cneg &S2 cv csm co cva co cno cfv wceq wa &S1 &S2 &S5 copab2 
        chil chil cxp wfn vx cv chil wcel vy cv chil wcel wa vz cv vx cv vy 
        cv cmv co cno cfv wceq wa vx vy vz copab2 chil chil cxp wfn &S1 cv 
        chil wcel &S2 cv chil wcel wa &S5 cv &S1 cv c1 cneg &S2 cv csm co cva
        co cno cfv wceq wa &S1 &S2 &S5 copab2 vx cv chil wcel vy cv chil 
        wcel wa vz cv vx cv vy cv cmv co cno cfv wceq wa vx vy vz copab2 wceq
        chil chil cxp chil chil cxp wceq &S18 cv &S19 cv &S1 cv chil wcel
        &S2 cv chil wcel wa &S5 cv &S1 cv c1 cneg &S2 cv csm co cva co 
        cno cfv wceq wa &S1 &S2 &S5 copab2 co &S18 cv &S19 cv vx cv chil 
        wcel vy cv chil wcel wa vz cv vx cv vy cv cmv co cno cfv wceq wa vx 
        vy vz copab2 co wceq &S19 chil wral &S18 chil wral wa wb &S1 &S2 
        &S5 chil chil &S1 cv c1 cneg &S2 cv csm co cva co cno cfv &S1 cv 
        chil wcel &S2 cv chil wcel wa &S5 cv &S1 cv c1 cneg &S2 cv csm co cva
        co cno cfv wceq wa &S1 &S2 &S5 copab2 &S1 cv c1 cneg &S2 cv csm 
        co cva co cno fvex &S1 cv chil wcel &S2 cv chil wcel wa &S5 cv &S1 
        cv c1 cneg &S2 cv csm co cva co cno cfv wceq wa &S1 &S2 &S5 copab2 
        eqid fnoprab2 vx vy vz chil chil vx cv vy cv cmv co cno cfv vx cv 
        chil wcel vy cv chil wcel wa vz cv vx cv vy cv cmv co cno cfv wceq wa
        vx vy vz copab2 vx cv vy cv cmv co cno fvex vx cv chil wcel vy cv
        chil wcel wa vz cv vx cv vy cv cmv co cno cfv wceq wa vx vy vz 
        copab2 eqid fnoprab2 &S18 &S19 chil chil chil chil &S1 cv chil wcel &S2
        cv chil wcel wa &S5 cv &S1 cv c1 cneg &S2 cv csm co cva co cno 
        cfv wceq wa &S1 &S2 &S5 copab2 vx cv chil wcel vy cv chil wcel wa vz
        cv vx cv vy cv cmv co cno cfv wceq wa vx vy vz copab2 eqfnoprval 
        mp2an chil chil cxp eqid &S18 cv &S19 cv &S1 cv chil wcel &S2 cv chil 
        wcel wa &S5 cv &S1 cv c1 cneg &S2 cv csm co cva co cno cfv wceq wa 
        &S1 &S2 &S5 copab2 co &S18 cv &S19 cv vx cv chil wcel vy cv chil 
        wcel wa vz cv vx cv vy cv cmv co cno cfv wceq wa vx vy vz copab2 co 
        wceq &S18 &S19 chil &S18 cv chil wcel &S19 cv chil wcel wa &S18 cv c1
        cneg &S19 cv csm co cva co cno cfv &S18 cv &S19 cv cmv co cno cfv
        &S18 cv &S19 cv &S1 cv chil wcel &S2 cv chil wcel wa &S5 cv &S1 
        cv c1 cneg &S2 cv csm co cva co cno cfv wceq wa &S1 &S2 &S5 copab2 
        co &S18 cv &S19 cv vx cv chil wcel vy cv chil wcel wa vz cv vx cv 
        vy cv cmv co cno cfv wceq wa vx vy vz copab2 co &S18 cv chil wcel 
        &S19 cv chil wcel wa &S18 cv c1 cneg &S19 cv csm co cva co &S18 cv 
        &S19 cv cmv co cno &S18 cv chil wcel &S19 cv chil wcel wa &S18 cv 
        &S19 cv cmv co &S18 cv c1 cneg &S19 cv csm co cva co &S18 cv &S19 cv 
        hvsubvalt eqcomd fveq2d &S1 &S2 &S5 &S18 cv &S19 cv chil chil &S1 cv c1 
        cneg &S2 cv csm co cva co cno cfv &S18 cv c1 cneg &S19 cv csm co cva 
        co cno cfv &S1 cv chil wcel &S2 cv chil wcel wa &S5 cv &S1 cv c1 
        cneg &S2 cv csm co cva co cno cfv wceq wa &S1 &S2 &S5 copab2 &S18 cv 
        c1 cneg &S2 cv csm co cva co cno cfv &S18 cv c1 cneg &S19 cv csm co
        cva co cno fvex &S1 cv &S18 cv wceq &S1 cv c1 cneg &S2 cv csm co 
        cva co &S18 cv c1 cneg &S2 cv csm co cva co cno &S1 cv &S18 cv c1 
        cneg &S2 cv csm co cva opreq1 fveq2d &S2 cv &S19 cv wceq &S18 cv c1 
        cneg &S2 cv csm co cva co &S18 cv c1 cneg &S19 cv csm co cva co cno 
        &S2 cv &S19 cv wceq c1 cneg &S2 cv csm co c1 cneg &S19 cv csm co 
        &S18 cv cva &S2 cv &S19 cv c1 cneg csm opreq2 opreq2d fveq2d &S1 cv 
        chil wcel &S2 cv chil wcel wa &S5 cv &S1 cv c1 cneg &S2 cv csm co cva
        co cno cfv wceq wa &S1 &S2 &S5 copab2 eqid oprabval2 vx vy vz 
        &S18 cv &S19 cv vx cv chil wcel vy cv chil wcel wa vz cv vx cv vy cv 
        cmv co cno cfv wceq wa vx vy vz copab2 vx cv chil wcel vy cv chil 
        wcel wa vz cv vx cv vy cv cmv co cno cfv wceq wa vx vy vz copab2 eqid
        hilmsdval 3eqtr4d rgen2 mpbir2an eqtr opeq2i cva csm cop cno cop 
        cncv wcel cva csm cop cno cop cims cfv chil &S1 cv chil wcel &S2 cv 
        chil wcel &S5 cv &S1 cv c1 cneg &S2 cv csm co cva co cno cfv wceq w3a
        &S1 &S2 &S5 copab2 cop wceq hilncv &S1 &S2 &S5 csm cva csm cop 
        cno cop cva cno cva csm cop chil cva csm cop cno cop c1st cfv cva 
        csm cop cva csm cop cno cva csm opex op1st eqcomi cva csm cop c1st 
        cfv cva cva csm cva cabl hilabl elisseti op1st eqcomi cva csm cop 
        c2nd cfv csm cva csm cva cabl hilabl elisseti hvmulex op2nd eqcomi 
        cva csm cop cno cop c2nd cfv cno cva csm cop cno cva csm opex cno 
        &S3 cv chil wcel &S4 cv &S3 cv &S3 cv csp co csqr cfv wceq wa &S3 
        &S4 copab cvv &S3 &S4 df-hnorm &S3 &S4 chil &S3 cv &S3 cv csp co 
        csqr cfv ax-hilex funopabex2 eqeltr op2nd eqcomi cva chil cva cabl 
        wcel cva cgr wcel hilabl cva ablgrp ax-mp ax-hfvadd grprn imsval 
        ax-mp cD vx cv chil wcel vy cv chil wcel wa vz cv vx cv vy cv cmv co 
        cno cfv wceq wa vx vy vz copab2 chil hilims.1 opeq2i 3eqtr4 $. 
    $)
     

hilims after unification with dummies replacing work vars

    $( <MM> <PROOF_ASST> THEOREM=hilims  LOC_AFTER=?
     
    * The metric space induced by Hilbert space.
    $d x y z u v w f g
     
    h1::hilims.1       |-   D
                          = {
                            <.
                            <. x
                            ,  y
                            >.
                            ,  z
                            >.
                            |  (  ( x e. H~ /\ y e. H~ )
                               /\ z = ( normh ` ( x -h y ) ) ) }
    2::df-3an          |- (   (  w e. H~
                              /\ v e. H~
                              /\   u
                                 = ( normh
                                   ` ( w +h ( -u 1 .h v ) ) ) )
                          <-> (  ( w e. H~ /\ v e. H~ )
                              /\   u
                                 = ( normh
                                   ` ( w +h ( -u 1 .h v ) ) ) ) )
    3:2:oprabbii       |-   {
                            <.
                            <. w
                            ,  v
                            >.
                            ,  u
                            >.
                            |  (  w e. H~
                               /\ v e. H~
                               /\   u
                                  = ( normh
                                    ` ( w +h ( -u 1 .h v ) ) ) ) }
                          = {
                            <.
                            <. w
                            ,  v
                            >.
                            ,  u
                            >.
                            |  (  ( w e. H~ /\ v e. H~ )
                               /\   u
                                  = ( normh
                                    ` ( w +h ( -u 1 .h v ) ) ) ) }
    4::fvex            |-    ( normh
                             ` ( w +h ( -u 1 .h v ) ) )
                          e. V
    5::eqid            |-   {
                            <.
                            <. w
                            ,  v
                            >.
                            ,  u
                            >.
                            |  (  ( w e. H~ /\ v e. H~ )
                               /\   u
                                  = ( normh
                                    ` ( w +h ( -u 1 .h v ) ) ) ) }
                          = {
                            <.
                            <. w
                            ,  v
                            >.
                            ,  u
                            >.
                            |  (  ( w e. H~ /\ v e. H~ )
                               /\   u
                                  = ( normh
                                    ` ( w +h ( -u 1 .h v ) ) ) ) }
    6:4,5:fnoprab2     |-    {
                             <.
                             <. w
                             ,  v
                             >.
                             ,  u
                             >.
                             |  (  ( w e. H~ /\ v e. H~ )
                                /\   u
                                   = ( normh
                                     ` ( w +h ( -u 1 .h v ) ) ) ) }
                          Fn ( H~ X. H~ )
    7::fvex            |- ( normh ` ( x -h y ) ) e. V
    8::eqid            |-   {
                            <.
                            <. x
                            ,  y
                            >.
                            ,  z
                            >.
                            |  (  ( x e. H~ /\ y e. H~ )
                               /\ z = ( normh ` ( x -h y ) ) ) }
                          = {
                            <.
                            <. x
                            ,  y
                            >.
                            ,  z
                            >.
                            |  (  ( x e. H~ /\ y e. H~ )
                               /\ z = ( normh ` ( x -h y ) ) ) }
    9:7,8:fnoprab2     |-    {
                             <.
                             <. x
                             ,  y
                             >.
                             ,  z
                             >.
                             |  (  ( x e. H~ /\ y e. H~ )
                                /\ z = ( normh ` ( x -h y ) ) ) }
                          Fn ( H~ X. H~ )
    10::eqfnoprval     |- (  (     {
                                   <.
                                   <. w
                                   ,  v
                                   >.
                                   ,  u
                                   >.
                                   |  (  ( w e. H~ /\ v e. H~ )
                                      /\   u
                                         = ( normh
                                           ` ( w +h ( -u 1 .h v ) ) ) ) }
                                Fn ( H~ X. H~ )
                             /\    {
                                   <.
                                   <. x
                                   ,  y
                                   >.
                                   ,  z
                                   >.
                                   |  (  ( x e. H~ /\ y e. H~ )
                                      /\ z = ( normh ` ( x -h y ) ) ) }
                                Fn ( H~ X. H~ ) )
                          -> (     {
                                   <.
                                   <. w
                                   ,  v
                                   >.
                                   ,  u
                                   >.
                                   |  (  ( w e. H~ /\ v e. H~ )
                                      /\   u
                                         = ( normh
                                           ` ( w +h ( -u 1 .h v ) ) ) ) }
                                 = {
                                   <.
                                   <. x
                                   ,  y
                                   >.
                                   ,  z
                                   >.
                                   |  (  ( x e. H~ /\ y e. H~ )
                                      /\ z = ( normh ` ( x -h y ) ) ) }
                             <-> (  ( H~ X. H~ ) = ( H~ X. H~ )
                                 /\ A. f
                                    e. H~
                                       A. g
                                       e. H~
                                            ( f
                                              {
                                              <.
                                              <. w
                                              ,  v
                                              >.
                                              ,  u
                                              >.
                                              |  (  ( w e. H~ /\ v e. H~ )
                                                 /\   u
                                                    = ( normh
                                                      ` ( w +h ( -u 1 .h v ) ) ) )
                                              }
                                              g )
                                          = ( f
                                              {
                                              <.
                                              <. x
                                              ,  y
                                              >.
                                              ,  z
                                              >.
                                              |  (  ( x e. H~ /\ y e. H~ )
                                                 /\ z = ( normh ` ( x -h y ) ) ) }
                                              g ) ) ) )
    11:6,9,10:mp2an    |- (     {
                                <.
                                <. w
                                ,  v
                                >.
                                ,  u
                                >.
                                |  (  ( w e. H~ /\ v e. H~ )
                                   /\   u
                                      = ( normh
                                        ` ( w +h ( -u 1 .h v ) ) ) ) }
                              = {
                                <.
                                <. x
                                ,  y
                                >.
                                ,  z
                                >.
                                |  (  ( x e. H~ /\ y e. H~ )
                                   /\ z = ( normh ` ( x -h y ) ) ) }
                          <-> (  ( H~ X. H~ ) = ( H~ X. H~ )
                              /\ A. f
                                 e. H~
                                    A. g
                                    e. H~
                                         ( f
                                           {
                                           <.
                                           <. w
                                           ,  v
                                           >.
                                           ,  u
                                           >.
                                           |  (  ( w e. H~ /\ v e. H~ )
                                              /\   u
                                                 = ( normh
                                                   ` ( w +h ( -u 1 .h v ) ) ) ) }
                                           g )
                                       = ( f
                                           {
                                           <.
                                           <. x
                                           ,  y
                                           >.
                                           ,  z
                                           >.
                                           |  (  ( x e. H~ /\ y e. H~ )
                                              /\ z = ( normh ` ( x -h y ) ) ) }
                                           g ) ) )
    12::eqid           |- ( H~ X. H~ ) = ( H~ X. H~ )
    13::hvsubvalt      |- (  ( f e. H~ /\ g e. H~ )
                          ->   ( f -h g )
                             = ( f +h ( -u 1 .h g ) ) )
    14:13:eqcomd       |- (  ( f e. H~ /\ g e. H~ )
                          ->   ( f +h ( -u 1 .h g ) )
                             = ( f -h g ) )
    15:14:fveq2d       |- (  ( f e. H~ /\ g e. H~ )
                          ->   ( normh
                               ` ( f +h ( -u 1 .h g ) ) )
                             = ( normh ` ( f -h g ) ) )
    16::fvex           |-    ( normh
                             ` ( f +h ( -u 1 .h g ) ) )
                          e. V
    17::opreq1         |- (  w = f
                          ->   ( w +h ( -u 1 .h v ) )
                             = ( f +h ( -u 1 .h v ) ) )
    18:17:fveq2d       |- (  w = f
                          ->   ( normh
                               ` ( w +h ( -u 1 .h v ) ) )
                             = ( normh
                               ` ( f +h ( -u 1 .h v ) ) ) )
    19::opreq2         |- (  v = g
                          -> ( -u 1 .h v ) = ( -u 1 .h g ) )
    20:19:opreq2d      |- (  v = g
                          ->   ( f +h ( -u 1 .h v ) )
                             = ( f +h ( -u 1 .h g ) ) )
    21:20:fveq2d       |- (  v = g
                          ->   ( normh
                               ` ( f +h ( -u 1 .h v ) ) )
                             = ( normh
                               ` ( f +h ( -u 1 .h g ) ) ) )
    22::eqid           |-   {
                            <.
                            <. w
                            ,  v
                            >.
                            ,  u
                            >.
                            |  (  ( w e. H~ /\ v e. H~ )
                               /\   u
                                  = ( normh
                                    ` ( w +h ( -u 1 .h v ) ) ) ) }
                          = {
                            <.
                            <. w
                            ,  v
                            >.
                            ,  u
                            >.
                            |  (  ( w e. H~ /\ v e. H~ )
                               /\   u
                                  = ( normh
                                    ` ( w +h ( -u 1 .h v ) ) ) ) }
    23:16,18,21,22:oprabval2 
                       |- (  ( f e. H~ /\ g e. H~ )
                          ->   ( f
                                 {
                                 <.
                                 <. w
                                 ,  v
                                 >.
                                 ,  u
                                 >.
                                 |  (  ( w e. H~ /\ v e. H~ )
                                    /\   u
                                       = ( normh
                                         ` ( w +h ( -u 1 .h v ) ) ) ) }
                                 g )
                             = ( normh
                               ` ( f +h ( -u 1 .h g ) ) ) )
    24::eqid           |-   {
                            <.
                            <. x
                            ,  y
                            >.
                            ,  z
                            >.
                            |  (  ( x e. H~ /\ y e. H~ )
                               /\ z = ( normh ` ( x -h y ) ) ) }
                          = {
                            <.
                            <. x
                            ,  y
                            >.
                            ,  z
                            >.
                            |  (  ( x e. H~ /\ y e. H~ )
                               /\ z = ( normh ` ( x -h y ) ) ) }
    25:24:hilmsdval    |- (  ( f e. H~ /\ g e. H~ )
                          ->   ( f
                                 {
                                 <.
                                 <. x
                                 ,  y
                                 >.
                                 ,  z
                                 >.
                                 |  (  ( x e. H~ /\ y e. H~ )
                                    /\ z = ( normh ` ( x -h y ) ) ) }
                                 g )
                             = ( normh ` ( f -h g ) ) )
    26:15,23,25:3eqtr4d 
                       |- (  ( f e. H~ /\ g e. H~ )
                          ->   ( f
                                 {
                                 <.
                                 <. w
                                 ,  v
                                 >.
                                 ,  u
                                 >.
                                 |  (  ( w e. H~ /\ v e. H~ )
                                    /\   u
                                       = ( normh
                                         ` ( w +h ( -u 1 .h v ) ) ) ) }
                                 g )
                             = ( f
                                 {
                                 <.
                                 <. x
                                 ,  y
                                 >.
                                 ,  z
                                 >.
                                 |  (  ( x e. H~ /\ y e. H~ )
                                    /\ z = ( normh ` ( x -h y ) ) ) }
                                 g ) )
    27:26:rgen2        |- A. f
                          e. H~
                             A. g
                             e. H~
                                  ( f
                                    {
                                    <.
                                    <. w
                                    ,  v
                                    >.
                                    ,  u
                                    >.
                                    |  (  ( w e. H~ /\ v e. H~ )
                                       /\   u
                                          = ( normh
                                            ` ( w +h ( -u 1 .h v ) ) ) ) }
                                    g )
                                = ( f
                                    {
                                    <.
                                    <. x
                                    ,  y
                                    >.
                                    ,  z
                                    >.
                                    |  (  ( x e. H~ /\ y e. H~ )
                                       /\ z = ( normh ` ( x -h y ) ) ) }
                                    g )
    28:11,12,27:mpbir2an 
                       |-   {
                            <.
                            <. w
                            ,  v
                            >.
                            ,  u
                            >.
                            |  (  ( w e. H~ /\ v e. H~ )
                               /\   u
                                  = ( normh
                                    ` ( w +h ( -u 1 .h v ) ) ) ) }
                          = {
                            <.
                            <. x
                            ,  y
                            >.
                            ,  z
                            >.
                            |  (  ( x e. H~ /\ y e. H~ )
                               /\ z = ( normh ` ( x -h y ) ) ) }
    29:3,28:eqtr       |-   {
                            <.
                            <. w
                            ,  v
                            >.
                            ,  u
                            >.
                            |  (  w e. H~
                               /\ v e. H~
                               /\   u
                                  = ( normh
                                    ` ( w +h ( -u 1 .h v ) ) ) ) }
                          = {
                            <.
                            <. x
                            ,  y
                            >.
                            ,  z
                            >.
                            |  (  ( x e. H~ /\ y e. H~ )
                               /\ z = ( normh ` ( x -h y ) ) ) }
    30:29:opeq2i       |-   <. H~
                            ,  {
                               <.
                               <. w
                               ,  v
                               >.
                               ,  u
                               >.
                               |  (  w e. H~
                                  /\ v e. H~
                                  /\   u
                                     = ( normh
                                       ` ( w +h ( -u 1 .h v ) ) ) ) } >.
                          = <. H~
                            ,  {
                               <.
                               <. x
                               ,  y
                               >.
                               ,  z
                               >.
                               |  (  ( x e. H~ /\ y e. H~ )
                                  /\ z = ( normh ` ( x -h y ) ) ) } >.
    31::hilncv         |- <. <. +h , .h >. , normh >. e. NrmCVec
    32::opex           |- <. +h , .h >. e. V
    33:32:op1st        |-   ( 1st ` <. <. +h , .h >. , normh >. )
                          = <. +h , .h >.
    34:33:eqcomi       |-   <. +h , .h >.
                          = ( 1st ` <. <. +h , .h >. , normh >. )
    35::hilabl         |- +h e. Abel
    36:35:elisseti     |- +h e. V
    37:36:op1st        |- ( 1st ` <. +h , .h >. ) = +h
    38:37:eqcomi       |- +h = ( 1st ` <. +h , .h >. )
    39::hilabl         |- +h e. Abel
    40:39:elisseti     |- +h e. V
    41::hvmulex        |- .h e. V
    42:40,41:op2nd     |- ( 2nd ` <. +h , .h >. ) = .h
    43:42:eqcomi       |- .h = ( 2nd ` <. +h , .h >. )
    44::opex           |- <. +h , .h >. e. V
    45::df-hnorm       |-   normh
                          = {
                            <. w
                            ,  v
                            >.
                            |  (  w e. H~
                               /\ v = ( sqr ` ( w .ih w ) ) ) }
    46::ax-hilex       |- H~ e. V
    47:46:funopabex2   |-    {
                             <. w
                             ,  v
                             >.
                             |  (  w e. H~
                                /\ v = ( sqr ` ( w .ih w ) ) ) }
                          e. V
    48:45,47:eqeltr    |- normh e. V
    49:44,48:op2nd     |-   ( 2nd ` <. <. +h , .h >. , normh >. )
                          = normh
    50:49:eqcomi       |-   normh
                          = ( 2nd ` <. <. +h , .h >. , normh >. )
    51::hilabl         |- +h e. Abel
    52::ablgrp         |- ( +h e. Abel -> +h e. Grp )
    53:51,52:ax-mp     |- +h e. Grp
    54::ax-hfvadd      |- +h : ( H~ X. H~ ) --> H~
    55:53,54:grprn     |- H~ = ran +h
    56:34,38,43,50,55:imsval 
                       |- (  <. <. +h , .h >. , normh >. e. NrmCVec
                          ->   ( IndMet ` <. <. +h , .h >. , normh >. )
                             = <. H~
                               ,  {
                                  <.
                                  <. w
                                  ,  v
                                  >.
                                  ,  u
                                  >.
                                  |  (  w e. H~
                                     /\ v e. H~
                                     /\   u
                                        = ( normh
                                          ` ( w +h ( -u 1 .h v ) ) ) ) } >. )
    57:31,56:ax-mp     |-   ( IndMet ` <. <. +h , .h >. , normh >. )
                          = <. H~
                            ,  {
                               <.
                               <. w
                               ,  v
                               >.
                               ,  u
                               >.
                               |  (  w e. H~
                                  /\ v e. H~
                                  /\   u
                                     = ( normh
                                       ` ( w +h ( -u 1 .h v ) ) ) ) } >.
    58:1:opeq2i        |-   <. H~ , D >.
                          = <. H~
                            ,  {
                               <.
                               <. x
                               ,  y
                               >.
                               ,  z
                               >.
                               |  (  ( x e. H~ /\ y e. H~ )
                                  /\ z = ( normh ` ( x -h y ) ) ) } >.
    qed:30,57,58:3eqtr4 
                       |-   ( IndMet ` <. <. +h , .h >. , normh >. )
                          = <. H~ , D >.
     
    $=  chil vw cv chil wcel vv cv chil wcel vu cv vw cv c1 cneg vv cv 
        csm co cva co cno cfv wceq w3a vw vv vu copab2 cop chil vx cv chil 
        wcel vy cv chil wcel wa vz cv vx cv vy cv cmv co cno cfv wceq wa vx 
        vy vz copab2 cop cva csm cop cno cop cims cfv chil cD cop vw cv 
        chil wcel vv cv chil wcel vu cv vw cv c1 cneg vv cv csm co cva co cno
        cfv wceq w3a vw vv vu copab2 vx cv chil wcel vy cv chil wcel wa 
        vz cv vx cv vy cv cmv co cno cfv wceq wa vx vy vz copab2 chil vw cv
        chil wcel vv cv chil wcel vu cv vw cv c1 cneg vv cv csm co cva co
        cno cfv wceq w3a vw vv vu copab2 vw cv chil wcel vv cv chil wcel 
        wa vu cv vw cv c1 cneg vv cv csm co cva co cno cfv wceq wa vw vv vu
        copab2 vx cv chil wcel vy cv chil wcel wa vz cv vx cv vy cv cmv 
        co cno cfv wceq wa vx vy vz copab2 vw cv chil wcel vv cv chil wcel 
        vu cv vw cv c1 cneg vv cv csm co cva co cno cfv wceq w3a vw cv chil
        wcel vv cv chil wcel wa vu cv vw cv c1 cneg vv cv csm co cva co 
        cno cfv wceq wa vw vv vu vw cv chil wcel vv cv chil wcel vu cv vw cv
        c1 cneg vv cv csm co cva co cno cfv wceq df-3an oprabbii vw cv 
        chil wcel vv cv chil wcel wa vu cv vw cv c1 cneg vv cv csm co cva co 
        cno cfv wceq wa vw vv vu copab2 vx cv chil wcel vy cv chil wcel wa 
        vz cv vx cv vy cv cmv co cno cfv wceq wa vx vy vz copab2 wceq chil 
        chil cxp chil chil cxp wceq vf cv vg cv vw cv chil wcel vv cv chil 
        wcel wa vu cv vw cv c1 cneg vv cv csm co cva co cno cfv wceq wa vw vv
        vu copab2 co vf cv vg cv vx cv chil wcel vy cv chil wcel wa vz cv
        vx cv vy cv cmv co cno cfv wceq wa vx vy vz copab2 co wceq vg 
        chil wral vf chil wral vw cv chil wcel vv cv chil wcel wa vu cv vw cv
        c1 cneg vv cv csm co cva co cno cfv wceq wa vw vv vu copab2 chil 
        chil cxp wfn vx cv chil wcel vy cv chil wcel wa vz cv vx cv vy cv cmv
        co cno cfv wceq wa vx vy vz copab2 chil chil cxp wfn vw cv chil 
        wcel vv cv chil wcel wa vu cv vw cv c1 cneg vv cv csm co cva co cno 
        cfv wceq wa vw vv vu copab2 vx cv chil wcel vy cv chil wcel wa vz cv
        vx cv vy cv cmv co cno cfv wceq wa vx vy vz copab2 wceq chil chil
        cxp chil chil cxp wceq vf cv vg cv vw cv chil wcel vv cv chil 
        wcel wa vu cv vw cv c1 cneg vv cv csm co cva co cno cfv wceq wa vw vv
        vu copab2 co vf cv vg cv vx cv chil wcel vy cv chil wcel wa vz cv
        vx cv vy cv cmv co cno cfv wceq wa vx vy vz copab2 co wceq vg 
        chil wral vf chil wral wa wb vw vv vu chil chil vw cv c1 cneg vv cv 
        csm co cva co cno cfv vw cv chil wcel vv cv chil wcel wa vu cv vw cv
        c1 cneg vv cv csm co cva co cno cfv wceq wa vw vv vu copab2 vw cv
        c1 cneg vv cv csm co cva co cno fvex vw cv chil wcel vv cv chil 
        wcel wa vu cv vw cv c1 cneg vv cv csm co cva co cno cfv wceq wa vw vv
        vu copab2 eqid fnoprab2 vx vy vz chil chil vx cv vy cv cmv co cno
        cfv vx cv chil wcel vy cv chil wcel wa vz cv vx cv vy cv cmv co 
        cno cfv wceq wa vx vy vz copab2 vx cv vy cv cmv co cno fvex vx cv 
        chil wcel vy cv chil wcel wa vz cv vx cv vy cv cmv co cno cfv wceq wa
        vx vy vz copab2 eqid fnoprab2 vf vg chil chil chil chil vw cv 
        chil wcel vv cv chil wcel wa vu cv vw cv c1 cneg vv cv csm co cva co 
        cno cfv wceq wa vw vv vu copab2 vx cv chil wcel vy cv chil wcel wa 
        vz cv vx cv vy cv cmv co cno cfv wceq wa vx vy vz copab2 eqfnoprval
        mp2an chil chil cxp eqid vf cv vg cv vw cv chil wcel vv cv chil 
        wcel wa vu cv vw cv c1 cneg vv cv csm co cva co cno cfv wceq wa vw vv
        vu copab2 co vf cv vg cv vx cv chil wcel vy cv chil wcel wa vz cv
        vx cv vy cv cmv co cno cfv wceq wa vx vy vz copab2 co wceq vf vg 
        chil vf cv chil wcel vg cv chil wcel wa vf cv c1 cneg vg cv csm co 
        cva co cno cfv vf cv vg cv cmv co cno cfv vf cv vg cv vw cv chil 
        wcel vv cv chil wcel wa vu cv vw cv c1 cneg vv cv csm co cva co cno 
        cfv wceq wa vw vv vu copab2 co vf cv vg cv vx cv chil wcel vy cv 
        chil wcel wa vz cv vx cv vy cv cmv co cno cfv wceq wa vx vy vz copab2
        co vf cv chil wcel vg cv chil wcel wa vf cv c1 cneg vg cv csm co 
        cva co vf cv vg cv cmv co cno vf cv chil wcel vg cv chil wcel wa vf 
        cv vg cv cmv co vf cv c1 cneg vg cv csm co cva co vf cv vg cv 
        hvsubvalt eqcomd fveq2d vw vv vu vf cv vg cv chil chil vw cv c1 cneg vv cv
        csm co cva co cno cfv vf cv c1 cneg vg cv csm co cva co cno cfv 
        vw cv chil wcel vv cv chil wcel wa vu cv vw cv c1 cneg vv cv csm co
        cva co cno cfv wceq wa vw vv vu copab2 vf cv c1 cneg vv cv csm co
        cva co cno cfv vf cv c1 cneg vg cv csm co cva co cno fvex vw cv 
        vf cv wceq vw cv c1 cneg vv cv csm co cva co vf cv c1 cneg vv cv 
        csm co cva co cno vw cv vf cv c1 cneg vv cv csm co cva opreq1 fveq2d
        vv cv vg cv wceq vf cv c1 cneg vv cv csm co cva co vf cv c1 cneg 
        vg cv csm co cva co cno vv cv vg cv wceq c1 cneg vv cv csm co c1 
        cneg vg cv csm co vf cv cva vv cv vg cv c1 cneg csm opreq2 opreq2d 
        fveq2d vw cv chil wcel vv cv chil wcel wa vu cv vw cv c1 cneg vv cv csm
        co cva co cno cfv wceq wa vw vv vu copab2 eqid oprabval2 vx vy vz
        vf cv vg cv vx cv chil wcel vy cv chil wcel wa vz cv vx cv vy cv 
        cmv co cno cfv wceq wa vx vy vz copab2 vx cv chil wcel vy cv chil 
        wcel wa vz cv vx cv vy cv cmv co cno cfv wceq wa vx vy vz copab2 eqid
        hilmsdval 3eqtr4d rgen2 mpbir2an eqtr opeq2i cva csm cop cno cop 
        cncv wcel cva csm cop cno cop cims cfv chil vw cv chil wcel vv cv 
        chil wcel vu cv vw cv c1 cneg vv cv csm co cva co cno cfv wceq w3a vw
        vv vu copab2 cop wceq hilncv vw vv vu csm cva csm cop cno cop cva
        cno cva csm cop chil cva csm cop cno cop c1st cfv cva csm cop cva
        csm cop cno cva csm opex op1st eqcomi cva csm cop c1st cfv cva 
        cva csm cva cabl hilabl elisseti op1st eqcomi cva csm cop c2nd cfv 
        csm cva csm cva cabl hilabl elisseti hvmulex op2nd eqcomi cva csm 
        cop cno cop c2nd cfv cno cva csm cop cno cva csm opex cno vw cv chil
        wcel vv cv vw cv vw cv csp co csqr cfv wceq wa vw vv copab cvv vw
        vv df-hnorm vw vv chil vw cv vw cv csp co csqr cfv ax-hilex 
        funopabex2 eqeltr op2nd eqcomi cva chil cva cabl wcel cva cgr wcel hilabl 
        cva ablgrp ax-mp ax-hfvadd grprn imsval ax-mp cD vx cv chil wcel vy 
        cv chil wcel wa vz cv vx cv vy cv cmv co cno cfv wceq wa vx vy vz 
        copab2 chil hilims.1 opeq2i 3eqtr4 $. 
    $)