def tr.split_go

bend-osdev-mode-core@0.1.0.0 · PROOF.bend:534

import Base
import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M

534def tr.split_go(+xs: List<&2, U32>, +acc: List<&2, M.CmBlock>) -> {M.cm.split.go(xs, acc) == tr.split_fin(acc, M.cm.split(xs)) : M.CmSplit}:
535  match xs:
536    case Nil{}:
537      {==}
538    case Con{+y0, +r0}:
539      match r0:
540        case Nil{}:
541          {==}
542        case Con{+y1, +r1}:
543          match r1:
544            case Nil{}:
545              {==}
546            case Con{+y2, +r2}:
547              match r2:
548                case Nil{}:
549                  {==}
550                case Con{+y3, +r3}:
551                  match r3:
552                    case Nil{}:
553                      {==}
554                    case Con{+y4, +r4}:
555                      match r4:
556                        case Nil{}:
557                          {==}
558                        case Con{+y5, +r5}:
559                          match r5:
560                            case Nil{}:
561                              {==}
562                            case Con{+y6, +r6}:
563                              match r6:
564                                case Nil{}:
565                                  {==}
566                                case Con{+y7, +r7}:
567                                  match r7:
568                                    case Nil{}:
569                                      {==}
570                                    case Con{+y8, +r8}:
571                                      match r8:
572                                        case Nil{}:
573                                          {==}
574                                        case Con{+y9, +r9}:
575                                          match r9:
576                                            case Nil{}:
577                                              {==}
578                                            case Con{+y10, +r10}:
579                                              match r10:
580                                                case Nil{}:
581                                                  {==}
582                                                case Con{+y11, +r11}:
583                                                  match r11:
584                                                    case Nil{}:
585                                                      {==}
586                                                    case Con{+y12, +r12}:
587                                                      match r12:
588                                                        case Nil{}:
589                                                          {==}
590                                                        case Con{+y13, +r13}:
591                                                          match r13:
592                                                            case Nil{}:
593                                                              {==}
594                                                            case Con{+y14, +r14}:
595                                                              match r14:
596                                                                case Nil{}:
597                                                                  {==}
598                                                                case Con{+y15, +t}:
599                                                                  Equal.trans(M.CmSplit, M.cm.split.go(t, Con{M.cm.block16(y0, y1, y2, y3, y4, y5, y6, y7, y8, y9, y10, y11, y12, y13, y14, y15), acc}), tr.split_fin(Con{M.cm.block16(y0, y1, y2, y3, y4, y5, y6, y7, y8, y9, y10, y11, y12, y13, y14, y15), acc}, M.cm.split(t)), tr.split_fin(acc, M.cm.split.cons(M.cm.block16(y0, y1, y2, y3, y4, y5, y6, y7, y8, y9, y10, y11, y12, y13, y14, y15), M.cm.split(t))), tr.split_go(t, Con{M.cm.block16(y0, y1, y2, y3, y4, y5, y6, y7, y8, y9, y10, y11, y12, y13, y14, y15), acc}), tr.split_fin_cons(M.cm.block16(y0, y1, y2, y3, y4, y5, y6, y7, y8, y9, y10, y11, y12, y13, y14, y15), acc, M.cm.split(t)))