Welcome to Walnut v7.1.0! Type "help;" to see all available commands.
Starting Walnut session: Session/2026_05_16_17_28/

[Walnut]$ load verify_basic_recurrences.txt;
eval qma_rec "?msd_4 An (QMA[4*n]=QMA[n] & QMA[4*n+1]!=QMA[n] & QMA[4*n+2]=QMA[2*n] & QMA[4*n+3]!=QMA[2*n])";
Converted from brics:2 states - 5ms
____
TRUE
eval qma_balance "?msd_4 An ((QMA[2*n]=0 <=> QMA[2*n+1]=1) & (QMA[2*n]=1 <=> QMA[2*n+1]=0))";
____
TRUE
eval m1a_rec01 "?msd_4 An (M1A[4*n]=M1A[n] & M1A[4*n+1]!=M1A[n])";
____
TRUE
eval m1a_rec23 "?msd_4 An (((M1A[n]=0 => M1A[4*n+2]=M1A[2*n+1]) & (M1A[n]=1 => M1A[4*n+2]=M1A[2*n])) & M1A[4*n+3]!=M1A[4*n+2])";
____
TRUE
eval m1a_balance "?msd_4 An ((M1A[2*n]=0 <=> M1A[2*n+1]=1) & (M1A[2*n]=1 <=> M1A[2*n+1]=0))";
____
TRUE
eval m2a_rec01 "?msd_4 An (((M2A[n]=0 => M2A[4*n]=M2A[2*n]) & (M2A[n]=1 => M2A[4*n]=M2A[2*n+1])) & M2A[4*n+1]!=M2A[4*n])";
____
TRUE
eval m2a_rec23 "?msd_4 An (((M2A[n]=0 => M2A[4*n+2]=M2A[2*n+1]) & (M2A[n]=1 => M2A[4*n+2]=M2A[2*n])) & M2A[4*n+3]!=M2A[4*n+2])";
____
TRUE
eval m2a_balance "?msd_4 An ((M2A[2*n]=0 <=> M2A[2*n+1]=1) & (M2A[2*n]=1 <=> M2A[2*n+1]=0))";
____
TRUE

[Walnut]$ load verify_factor_complexity_QMA.txt;
reg pow2_4 msd_4 "0*(1|2)0*";
Set from brics:2 states - 3ms
def eqfac_qma "?msd_4 Ai (i<n) => QMA[x+i]=QMA[y+i]";
def firstfac_qma "?msd_4 Ai (i<x) => ~$eqfac_qma(n,i,x)";
def rs_qma "?msd_4 Ey ($eqfac_qma(n,x,y) & QMA[x+n]!=QMA[y+n])";
def crs_qma "?msd_4 $rs_qma(n,x) & $firstfac_qma(n,x)";
def rs2_qma "?msd_4 Eu,v (u!=v & $crs_qma(n,u) & $crs_qma(n,v) & Ax ($crs_qma(n,x) => (x=u|x=v)))";
def rs3_qma "?msd_4 Eu,v,w (u!=v & u!=w & v!=w & $crs_qma(n,u) & $crs_qma(n,v) & $crs_qma(n,w) & Ax ($crs_qma(n,x) => (x=u|x=v|x=w)))";
def rs4_qma "?msd_4 Eu,v,w,z (u!=v & u!=w & u!=z & v!=w & v!=z & w!=z & $crs_qma(n,u) & $crs_qma(n,v) & $crs_qma(n,w) & $crs_qma(n,z) & Ax ($crs_qma(n,x) => (x=u|x=v|x=w|x=z)))";
def qma_rs4_range "?msd_4 EP ($pow2_4(P) & P>=16 & P<n & n<2*P & 2*n<=3*P)";
def qma_rs3_range "?msd_4 EP ($pow2_4(P) & P>=16 & n<2*P & 2*n>3*P & 4*n<=7*P)";
def qma_rs2_range "?msd_4 EP ($pow2_4(P) & P>=16 & P<=n & n<2*P & (n=P | 4*n>7*P))";
eval qma_rs2_check "?msd_4 An (n>=16 => ($rs2_qma(n) <=> $qma_rs2_range(n)))";
____
TRUE
eval qma_rs3_check "?msd_4 An (n>=16 => ($rs3_qma(n) <=> $qma_rs3_range(n)))";
____
TRUE
eval qma_rs4_check "?msd_4 An (n>=16 => ($rs4_qma(n) <=> $qma_rs4_range(n)))";
____
TRUE

[Walnut]$ reg pow2_k0_4 msd_4 "0*(1(000)*|20(000)*)";
reg pow2_k1_4 msd_4 "0*(100(000)*|2(000)*)";
reg pow2_k2_4 msd_4 "0*(10(000)*|200(000)*)";
reg pow2_4 msd_4 "0*(1|2)0*";Set from brics:4 states - 12ms

[Walnut]$ Set from brics:4 states - 2ms

[Walnut]$ Set from brics:4 states - 2ms

[Walnut]$ 
Set from brics:2 states - 2ms

[Walnut]$ def eqfac_m2a "?msd_4 Ai (i<n) => M2A[x+i]=M2A[y+i]";

[Walnut]$ def firstfac_m2a "?msd_4 Ai (i<x) => ~$eqfac_m2a(n,i,x)";

[Walnut]$ def rs_m2a "?msd_4 Ey ($eqfac_m2a(n,x,y) & M2A[x+n]!=M2A[y+n])";

[Walnut]$ def crs_m2a "?msd_4 $rs_m2a(n,x) & $firstfac_m2a(n,x)";

[Walnut]$ def rs2_m2a "?msd_4 Eu,v (u!=v & $crs_m2a(n,u) & $crs_m2a(n,v) & Ax ($crs_m2a(n,x) => (x=u|x=v)))";

[Walnut]$ def m2a_rs4_range "?msd_4 EP (P>=8 & P<n & n<2*P & (($pow2_k0_4(P) & 4*n<=7*P) | ($pow2_k1_4(P) & 2*n<=3*P)))";
Converted from brics:2 states - 7ms

[Walnut]$ def m2a_rs2_range "?msd_4 n>=1 & ~$m2a_rs4_range(n)";

[Walnut]$ eval m2a_rs2_check "?msd_4 An (n>=8 => ($rs2_m2a(n) <=> $m2a_rs2_range(n)))";
____
TRUE

[Walnut]$ [strategy 5 CCLS]def rs4_m2a "?msd_4 Eu,v,w,z (u!=v & u!=w & u!=z & v!=w & v!=z & w!=z & $crs_m2a(n,u) & $crs_m2a(n,v) & $crs_m2a(n,w) & $crs_m2a(n,z) & Ax ($crs_m2a(n,x) => (x=u|x=v|x=w|x=z)))"::
computing u!=v
computed u!=v
u!=v:2 states - 12ms
 computing u!=w
 computed u!=w
 u!=w:2 states - 0ms
  computing u!=v&u!=w
   computing &:2 states - 2 states
    computing cross product:2 states - 2 states
    computed cross product:4 states - 5ms
    Minimizing: 4 states.
    Minimized:4 states - 1ms.
   computed &:4 states - 9ms
  computed u!=v&u!=w
  (u!=v&u!=w):4 states - 10ms
   computing u!=z
   computed u!=z
   u!=z:2 states - 0ms
    computing (u!=v&u!=w)&u!=z
     computing &:4 states - 2 states
      computing cross product:4 states - 2 states
      computed cross product:8 states - 2ms
      Minimizing: 8 states.
      Minimized:8 states - 2ms.
     computed &:8 states - 4ms
    computed (u!=v&u!=w)&u!=z
    ((u!=v&u!=w)&u!=z):8 states - 4ms
     computing v!=w
     computed v!=w
     v!=w:2 states - 1ms
      computing ((u!=v&u!=w)&u!=z)&v!=w
       computing &:8 states - 2 states
        computing cross product:8 states - 2 states
        computed cross product:10 states - 4ms
        Minimizing: 10 states.
        Minimized:10 states - 2ms.
       computed &:10 states - 6ms
      computed ((u!=v&u!=w)&u!=z)&v!=w
      (((u!=v&u!=w)&u!=z)&v!=w):10 states - 6ms
       computing v!=z
       computed v!=z
       v!=z:2 states - 0ms
        computing (((u!=v&u!=w)&u!=z)&v!=w)&v!=z
         computing &:10 states - 2 states
          computing cross product:10 states - 2 states
          computed cross product:13 states - 4ms
          Minimizing: 13 states.
          Minimized:13 states - 3ms.
         computed &:13 states - 7ms
        computed (((u!=v&u!=w)&u!=z)&v!=w)&v!=z
        ((((u!=v&u!=w)&u!=z)&v!=w)&v!=z):13 states - 7ms
         computing w!=z
         computed w!=z
         w!=z:2 states - 0ms
          computing ((((u!=v&u!=w)&u!=z)&v!=w)&v!=z)&w!=z
           computing &:13 states - 2 states
            computing cross product:13 states - 2 states
            computed cross product:15 states - 4ms
            Minimizing: 15 states.
            Minimized:15 states - 2ms.
           computed &:15 states - 7ms
          computed ((((u!=v&u!=w)&u!=z)&v!=w)&v!=z)&w!=z
          (((((u!=v&u!=w)&u!=z)&v!=w)&v!=z)&w!=z):15 states - 7ms
           computing crs_m2a(...)
            fixing leading zeros:28 states
             Determinizing [#0, strategy: SC]: 28 states
             Determinized: 28 states - 3ms
             Minimizing: 28 states.
             Minimized:28 states - 0ms.
            fixed leading zeros:28 states - 6ms
           computed crs_m2a(n,u))
           computing (((((u!=v&u!=w)&u!=z)&v!=w)&v!=z)&w!=z)&crs_m2a(n,u))
            computing &:15 states - 28 states
             computing cross product:15 states - 28 states
               Progress: Added 100 states - 237 states left in queue - 337 reachable states - 35ms
             computed cross product:420 states - 97ms
             Minimizing: 420 states.
             Minimized:420 states - 67ms.
            computed &:420 states - 164ms
           computed (((((u!=v&u!=w)&u!=z)&v!=w)&v!=z)&w!=z)&crs_m2a(n,u))
           ((((((u!=v&u!=w)&u!=z)&v!=w)&v!=z)&w!=z)&crs_m2a(n,u))):420 states - 164ms
            computing crs_m2a(...)
             fixing leading zeros:28 states
              Determinizing [#1, strategy: SC]: 28 states
              Determinized: 28 states - 0ms
              Minimizing: 28 states.
              Minimized:28 states - 1ms.
             fixed leading zeros:28 states - 1ms
            computed crs_m2a(n,v))
            computing ((((((u!=v&u!=w)&u!=z)&v!=w)&v!=z)&w!=z)&crs_m2a(n,u)))&crs_m2a(n,v))
             computing &:420 states - 28 states
              computing cross product:420 states - 28 states
                Progress: Added 100 states - 1646 states left in queue - 1746 reachable states - 18ms
                Progress: Added 1000 states - 1600 states left in queue - 2600 reachable states - 58ms
              computed cross product:3070 states - 155ms
              Minimizing: 3070 states.
              Minimized:274 states - 40ms.
             computed &:274 states - 195ms
            computed ((((((u!=v&u!=w)&u!=z)&v!=w)&v!=z)&w!=z)&crs_m2a(n,u)))&crs_m2a(n,v))
            (((((((u!=v&u!=w)&u!=z)&v!=w)&v!=z)&w!=z)&crs_m2a(n,u)))&crs_m2a(n,v))):274 states - 195ms
             computing crs_m2a(...)
              fixing leading zeros:28 states
               Determinizing [#2, strategy: SC]: 28 states
               Determinized: 28 states - 1ms
               Minimizing: 28 states.
               Minimized:28 states - 0ms.
              fixed leading zeros:28 states - 1ms
             computed crs_m2a(n,w))
             computing (((((((u!=v&u!=w)&u!=z)&v!=w)&v!=z)&w!=z)&crs_m2a(n,u)))&crs_m2a(n,v)))&crs_m2a(n,w))
              computing &:274 states - 28 states
               computing cross product:274 states - 28 states
                 Progress: Added 100 states - 758 states left in queue - 858 reachable states - 3ms
                 Progress: Added 1000 states - 153 states left in queue - 1153 reachable states - 7ms
               computed cross product:1154 states - 7ms
               Minimizing: 1154 states.
               Minimized:122 states - 3ms.
              computed &:122 states - 11ms
             computed (((((((u!=v&u!=w)&u!=z)&v!=w)&v!=z)&w!=z)&crs_m2a(n,u)))&crs_m2a(n,v)))&crs_m2a(n,w))
             ((((((((u!=v&u!=w)&u!=z)&v!=w)&v!=z)&w!=z)&crs_m2a(n,u)))&crs_m2a(n,v)))&crs_m2a(n,w))):122 states - 11ms
              computing crs_m2a(...)
               fixing leading zeros:28 states
                Determinizing [#3, strategy: SC]: 28 states
                Determinized: 28 states - 0ms
                Minimizing: 28 states.
                Minimized:28 states - 0ms.
               fixed leading zeros:28 states - 0ms
              computed crs_m2a(n,z))
              computing ((((((((u!=v&u!=w)&u!=z)&v!=w)&v!=z)&w!=z)&crs_m2a(n,u)))&crs_m2a(n,v)))&crs_m2a(n,w)))&crs_m2a(n,z))
               computing &:122 states - 28 states
                computing cross product:122 states - 28 states
                  Progress: Added 100 states - 188 states left in queue - 288 reachable states - 2ms
                computed cross product:315 states - 2ms
                Minimizing: 315 states.
                Minimized:47 states - 1ms.
               computed &:47 states - 3ms
              computed ((((((((u!=v&u!=w)&u!=z)&v!=w)&v!=z)&w!=z)&crs_m2a(n,u)))&crs_m2a(n,v)))&crs_m2a(n,w)))&crs_m2a(n,z))
              (((((((((u!=v&u!=w)&u!=z)&v!=w)&v!=z)&w!=z)&crs_m2a(n,u)))&crs_m2a(n,v)))&crs_m2a(n,w)))&crs_m2a(n,z))):47 states - 3ms
               computing crs_m2a(...)
                fixing leading zeros:28 states
                 Determinizing [#4, strategy: SC]: 28 states
                 Determinized: 28 states - 0ms
                 Minimizing: 28 states.
                 Minimized:28 states - 0ms.
                fixed leading zeros:28 states - 0ms
               computed crs_m2a(n,x))
               computing x=u
               computed x=u
               x=u:1 states - 0ms
                computing x=v
                computed x=v
                x=v:1 states - 0ms
                 computing x=u|x=v
                  computing |:1 states - 1 states
                   totalizing:1 states
                   totalized:2 states - 0ms
                   totalizing:1 states
                   totalized:2 states - 0ms
                   computing cross product:2 states - 2 states
                   computed cross product:4 states - 1ms
                   Minimizing: 4 states.
                   Minimized:3 states - 0ms.
                  computed |:3 states - 1ms
                 computed x=u|x=v
                 (x=u|x=v):3 states - 1ms
                  computing x=w
                  computed x=w
                  x=w:1 states - 0ms
                   computing (x=u|x=v)|x=w
                    computing |:3 states - 1 states
                     totalizing:3 states
                     totalized:4 states - 0ms
                     totalizing:1 states
                     totalized:2 states - 0ms
                     computing cross product:4 states - 2 states
                     computed cross product:8 states - 1ms
                     Minimizing: 8 states.
                     Minimized:7 states - 0ms.
                    computed |:7 states - 1ms
                   computed (x=u|x=v)|x=w
                   ((x=u|x=v)|x=w):7 states - 1ms
                    computing x=z
                    computed x=z
                    x=z:1 states - 0ms
                     computing ((x=u|x=v)|x=w)|x=z
                      computing |:7 states - 1 states
                       totalizing:7 states
                       totalized:8 states - 1ms
                       totalizing:1 states
                       totalized:2 states - 0ms
                       computing cross product:8 states - 2 states
                       computed cross product:16 states - 1ms
                       Minimizing: 16 states.
                       Minimized:15 states - 3ms.
                      computed |:15 states - 6ms
                     computed ((x=u|x=v)|x=w)|x=z
                     (((x=u|x=v)|x=w)|x=z):15 states - 6ms
                      computing crs_m2a(n,x))=>(((x=u|x=v)|x=w)|x=z)
                       computing =>:28 states - 15 states
                        totalizing:28 states
                        totalized:29 states - 0ms
                        totalizing:15 states
                        totalized:16 states - 2ms
                        computing cross product:29 states - 16 states
                          Progress: Added 100 states - 284 states left in queue - 384 reachable states - 25ms
                        computed cross product:464 states - 96ms
                        Minimizing: 464 states.
                        Minimized:449 states - 522ms.
                       computed =>:449 states - 802ms
                      computed crs_m2a(n,x))=>(((x=u|x=v)|x=w)|x=z)
                      (crs_m2a(n,x))=>(((x=u|x=v)|x=w)|x=z)):449 states - 803ms
                       computing quantifier A
                        computing ~:449 states
                         totalizing:449 states
                         totalized:449 states - 39ms
                          Minimizing: 449 states.
                          Minimized:448 states - 263ms.
                        computed ~:448 states - 381ms
                        quantifying:448 states
                          Determinizing [#5, strategy: CCLS]: 448 states
                          Calculating simulation relations; this can be resource-intensive
                          Simulation altered to 445 states
                          Found 10852 simulation relations
                            Progress: Explored 0 states - 1 states left in queue - 1 states added - 895ms
                            Progress: Explored 100 states - 757 states left in queue - 857 states added - 934ms
                            Progress: Explored 1000 states - 704 states left in queue - 1704 states added - 1070ms
                            Progress: Explored 10000 states - 263 states left in queue - 10263 states added - 2050ms
                            Progress: Periodic minimization: 10371 -> 3757 states added - 2399ms
                          Determinized: 10371 states - 3110ms
                          Minimizing: 10371 states.
                          Minimized:5805 states - 1684ms.
                        quantified:5805 states - 5093ms
                        fixing leading zeros:5805 states
                         Determinizing [#6, strategy: SC]: 5805 states
                           Progress: Added 100 states - 1586 states left in queue - 1686 reachable states - 66ms
                           Progress: Added 1000 states - 2209 states left in queue - 3209 reachable states - 206ms
                         Determinized: 6320 states - 893ms
                         Minimizing: 6320 states.
                         Minimized:1853 states - 782ms.
                        fixed leading zeros:1853 states - 1676ms
                        computing ~:1853 states
                         totalizing:1853 states
                         totalized:1853 states - 42ms
                          Minimizing: 1853 states.
                          Minimized:1852 states - 136ms.
                        computed ~:1852 states - 227ms
                       computed quantifier (A x (crs_m2a(n,x))=>(((x=u|x=v)|x=w)|x=z)))
                       (A x (crs_m2a(n,x))=>(((x=u|x=v)|x=w)|x=z))):1852 states - 7428ms
                        computing (((((((((u!=v&u!=w)&u!=z)&v!=w)&v!=z)&w!=z)&crs_m2a(n,u)))&crs_m2a(n,v)))&crs_m2a(n,w)))&crs_m2a(n,z)))&(A x (crs_m2a(n,x))=>(((x=u|x=v)|x=w)|x=z)))
                         computing &:47 states - 1852 states
                          computing cross product:47 states - 1852 states
                            Progress: Added 100 states - 95 states left in queue - 195 reachable states - 45ms
                          computed cross product:203 states - 46ms
                          Minimizing: 203 states.
                          Minimized:47 states - 0ms.
                         computed &:47 states - 46ms
                        computed (((((((((u!=v&u!=w)&u!=z)&v!=w)&v!=z)&w!=z)&crs_m2a(n,u)))&crs_m2a(n,v)))&crs_m2a(n,w)))&crs_m2a(n,z)))&(A x (crs_m2a(n,x))=>(((x=u|x=v)|x=w)|x=z)))
                        ((((((((((u!=v&u!=w)&u!=z)&v!=w)&v!=z)&w!=z)&crs_m2a(n,u)))&crs_m2a(n,v)))&crs_m2a(n,w)))&crs_m2a(n,z)))&(A x (crs_m2a(n,x))=>(((x=u|x=v)|x=w)|x=z)))):47 states - 46ms
                         computing quantifier E
                          quantifying:47 states
                            Determinizing [#7, strategy: SC]: 47 states
                            Determinized: 20 states - 0ms
                            Minimizing: 20 states.
                            Minimized:19 states - 0ms.
                          quantified:19 states - 1ms
                          fixing leading zeros:19 states
                           Determinizing [#8, strategy: SC]: 19 states
                           Determinized: 18 states - 0ms
                           Minimizing: 18 states.
                           Minimized:18 states - 0ms.
                          fixed leading zeros:18 states - 0ms
                         computed quantifier (E u , v , w , z ((((((((((u!=v&u!=w)&u!=z)&v!=w)&v!=z)&w!=z)&crs_m2a(n,u)))&crs_m2a(n,v)))&crs_m2a(n,w)))&crs_m2a(n,z)))&(A x (crs_m2a(n,x))=>(((x=u|x=v)|x=w)|x=z)))))
                         (E u , v , w , z ((((((((((u!=v&u!=w)&u!=z)&v!=w)&v!=z)&w!=z)&crs_m2a(n,u)))&crs_m2a(n,v)))&crs_m2a(n,w)))&crs_m2a(n,z)))&(A x (crs_m2a(n,x))=>(((x=u|x=v)|x=w)|x=z))))):18 states - 1ms
Total computation time: 8719ms.

If the CCL(S) or BRZ-CCL(S) algorithms are used in a result,
please cite the OTF paper by John Nicol and Markus Frohme.
The latest citation information is available at https://github.com/jn1z/OTF/blob/main/README.md


[Walnut]$ eval m2a_rs4_check "?msd_4 An (n>=8 => ($rs4_m2a(n) <=> $m2a_rs4_range(n)))";
Converted from brics:2 states - 6ms
____
TRUE
