def tr.split_go

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:934

import Base
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M

934def 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}:
935  match xs:
936    case Nil{}:
937      {==}
938    case Con{+y0, +r0}:
939      match r0:
940        case Nil{}:
941          {==}
942        case Con{+y1, +r1}:
943          match r1:
944            case Nil{}:
945              {==}
946            case Con{+y2, +r2}:
947              match r2:
948                case Nil{}:
949                  {==}
950                case Con{+y3, +r3}:
951                  match r3:
952                    case Nil{}:
953                      {==}
954                    case Con{+y4, +r4}:
955                      match r4:
956                        case Nil{}:
957                          {==}
958                        case Con{+y5, +r5}:
959                          match r5:
960                            case Nil{}:
961                              {==}
962                            case Con{+y6, +r6}:
963                              match r6:
964                                case Nil{}:
965                                  {==}
966                                case Con{+y7, +r7}:
967                                  match r7:
968                                    case Nil{}:
969                                      {==}
970                                    case Con{+y8, +r8}:
971                                      match r8:
972                                        case Nil{}:
973                                          {==}
974                                        case Con{+y9, +r9}:
975                                          match r9:
976                                            case Nil{}:
977                                              {==}
978                                            case Con{+y10, +r10}:
979                                              match r10:
980                                                case Nil{}:
981                                                  {==}
982                                                case Con{+y11, +r11}:
983                                                  match r11:
984                                                    case Nil{}:
985                                                      {==}
986                                                    case Con{+y12, +r12}:
987                                                      match r12:
988                                                        case Nil{}:
989                                                          {==}
990                                                        case Con{+y13, +r13}:
991                                                          match r13:
992                                                            case Nil{}:
993                                                              {==}
994                                                            case Con{+y14, +r14}:
995                                                              match r14:
996                                                                case Nil{}:
997                                                                  {==}
998                                                                case Con{+y15, +t}:
999                                                                  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)))