PROOF.ap.trans: def of bend-osdev-aes@0.1.0.0
Import: import bend-osdev-aes@0.1.0.0/PROOF.bend as PROOF
Lines 1849-1859 of bend-osdev-aes@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&start_line=1849&end_line=1859

import Base
import bend-osdev-gf@0.1.1.0/gf.bend as G

def ap.trans(+t00: U32, +t01: U32, +t02: U32, +t03: U32, +t10: U32, +t11: U32, +t12: U32, +t13: U32, +t20: U32, +t21: U32, +t22: U32, +t23: U32, +t30: U32, +t31: U32, +t32: U32, +t33: U32) -> {G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t01), G.Gf8.add(t02, t03)), G.Gf8.add(G.Gf8.add(t10, t11), G.Gf8.add(t12, t13))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t20, t21), G.Gf8.add(t22, t23)), G.Gf8.add(G.Gf8.add(t30, t31), G.Gf8.add(t32, t33)))) == G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t20, t30)), G.Gf8.add(G.Gf8.add(t01, t11), G.Gf8.add(t21, t31))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t12), G.Gf8.add(t22, t32)), G.Gf8.add(G.Gf8.add(t03, t13), G.Gf8.add(t23, t33)))) : U32}:
  %Equal.sym(U32, G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t01), G.Gf8.add(t02, t03)), G.Gf8.add(G.Gf8.add(t10, t11), G.Gf8.add(t12, t13))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t01), G.Gf8.add(t10, t11)), G.Gf8.add(G.Gf8.add(t02, t03), G.Gf8.add(t12, t13))), ap.swap4(G.Gf8.add(t00, t01), G.Gf8.add(t02, t03), G.Gf8.add(t10, t11), G.Gf8.add(t12, t13))) : {G.Gf8.add(_, G.Gf8.add(G.Gf8.add(G.Gf8.add(t20, t21), G.Gf8.add(t22, t23)), G.Gf8.add(G.Gf8.add(t30, t31), G.Gf8.add(t32, t33)))) == G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t20, t30)), G.Gf8.add(G.Gf8.add(t01, t11), G.Gf8.add(t21, t31))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t12), G.Gf8.add(t22, t32)), G.Gf8.add(G.Gf8.add(t03, t13), G.Gf8.add(t23, t33)))) : U32}
  %Equal.sym(U32, G.Gf8.add(G.Gf8.add(G.Gf8.add(t20, t21), G.Gf8.add(t22, t23)), G.Gf8.add(G.Gf8.add(t30, t31), G.Gf8.add(t32, t33))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t20, t21), G.Gf8.add(t30, t31)), G.Gf8.add(G.Gf8.add(t22, t23), G.Gf8.add(t32, t33))), ap.swap4(G.Gf8.add(t20, t21), G.Gf8.add(t22, t23), G.Gf8.add(t30, t31), G.Gf8.add(t32, t33))) : {G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t01), G.Gf8.add(t10, t11)), G.Gf8.add(G.Gf8.add(t02, t03), G.Gf8.add(t12, t13))), _) == G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t20, t30)), G.Gf8.add(G.Gf8.add(t01, t11), G.Gf8.add(t21, t31))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t12), G.Gf8.add(t22, t32)), G.Gf8.add(G.Gf8.add(t03, t13), G.Gf8.add(t23, t33)))) : U32}
  %Equal.sym(U32, G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t01), G.Gf8.add(t10, t11)), G.Gf8.add(G.Gf8.add(t02, t03), G.Gf8.add(t12, t13))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t20, t21), G.Gf8.add(t30, t31)), G.Gf8.add(G.Gf8.add(t22, t23), G.Gf8.add(t32, t33)))), G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t01), G.Gf8.add(t10, t11)), G.Gf8.add(G.Gf8.add(t20, t21), G.Gf8.add(t30, t31))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t03), G.Gf8.add(t12, t13)), G.Gf8.add(G.Gf8.add(t22, t23), G.Gf8.add(t32, t33)))), ap.swap4(G.Gf8.add(G.Gf8.add(t00, t01), G.Gf8.add(t10, t11)), G.Gf8.add(G.Gf8.add(t02, t03), G.Gf8.add(t12, t13)), G.Gf8.add(G.Gf8.add(t20, t21), G.Gf8.add(t30, t31)), G.Gf8.add(G.Gf8.add(t22, t23), G.Gf8.add(t32, t33)))) : {_ == G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t20, t30)), G.Gf8.add(G.Gf8.add(t01, t11), G.Gf8.add(t21, t31))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t12), G.Gf8.add(t22, t32)), G.Gf8.add(G.Gf8.add(t03, t13), G.Gf8.add(t23, t33)))) : U32}
  %Equal.sym(U32, G.Gf8.add(G.Gf8.add(t00, t01), G.Gf8.add(t10, t11)), G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t01, t11)), ap.swap4(t00, t01, t10, t11)) : {G.Gf8.add(G.Gf8.add(_, G.Gf8.add(G.Gf8.add(t20, t21), G.Gf8.add(t30, t31))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t03), G.Gf8.add(t12, t13)), G.Gf8.add(G.Gf8.add(t22, t23), G.Gf8.add(t32, t33)))) == G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t20, t30)), G.Gf8.add(G.Gf8.add(t01, t11), G.Gf8.add(t21, t31))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t12), G.Gf8.add(t22, t32)), G.Gf8.add(G.Gf8.add(t03, t13), G.Gf8.add(t23, t33)))) : U32}
  %Equal.sym(U32, G.Gf8.add(G.Gf8.add(t20, t21), G.Gf8.add(t30, t31)), G.Gf8.add(G.Gf8.add(t20, t30), G.Gf8.add(t21, t31)), ap.swap4(t20, t21, t30, t31)) : {G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t01, t11)), _), G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t03), G.Gf8.add(t12, t13)), G.Gf8.add(G.Gf8.add(t22, t23), G.Gf8.add(t32, t33)))) == G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t20, t30)), G.Gf8.add(G.Gf8.add(t01, t11), G.Gf8.add(t21, t31))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t12), G.Gf8.add(t22, t32)), G.Gf8.add(G.Gf8.add(t03, t13), G.Gf8.add(t23, t33)))) : U32}
  %Equal.sym(U32, G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t01, t11)), G.Gf8.add(G.Gf8.add(t20, t30), G.Gf8.add(t21, t31))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t20, t30)), G.Gf8.add(G.Gf8.add(t01, t11), G.Gf8.add(t21, t31))), ap.swap4(G.Gf8.add(t00, t10), G.Gf8.add(t01, t11), G.Gf8.add(t20, t30), G.Gf8.add(t21, t31))) : {G.Gf8.add(_, G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t03), G.Gf8.add(t12, t13)), G.Gf8.add(G.Gf8.add(t22, t23), G.Gf8.add(t32, t33)))) == G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t20, t30)), G.Gf8.add(G.Gf8.add(t01, t11), G.Gf8.add(t21, t31))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t12), G.Gf8.add(t22, t32)), G.Gf8.add(G.Gf8.add(t03, t13), G.Gf8.add(t23, t33)))) : U32}
  %Equal.sym(U32, G.Gf8.add(G.Gf8.add(t02, t03), G.Gf8.add(t12, t13)), G.Gf8.add(G.Gf8.add(t02, t12), G.Gf8.add(t03, t13)), ap.swap4(t02, t03, t12, t13)) : {G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t20, t30)), G.Gf8.add(G.Gf8.add(t01, t11), G.Gf8.add(t21, t31))), G.Gf8.add(_, G.Gf8.add(G.Gf8.add(t22, t23), G.Gf8.add(t32, t33)))) == G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t20, t30)), G.Gf8.add(G.Gf8.add(t01, t11), G.Gf8.add(t21, t31))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t12), G.Gf8.add(t22, t32)), G.Gf8.add(G.Gf8.add(t03, t13), G.Gf8.add(t23, t33)))) : U32}
  %Equal.sym(U32, G.Gf8.add(G.Gf8.add(t22, t23), G.Gf8.add(t32, t33)), G.Gf8.add(G.Gf8.add(t22, t32), G.Gf8.add(t23, t33)), ap.swap4(t22, t23, t32, t33)) : {G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t20, t30)), G.Gf8.add(G.Gf8.add(t01, t11), G.Gf8.add(t21, t31))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t12), G.Gf8.add(t03, t13)), _)) == G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t20, t30)), G.Gf8.add(G.Gf8.add(t01, t11), G.Gf8.add(t21, t31))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t12), G.Gf8.add(t22, t32)), G.Gf8.add(G.Gf8.add(t03, t13), G.Gf8.add(t23, t33)))) : U32}
  %Equal.sym(U32, G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t12), G.Gf8.add(t03, t13)), G.Gf8.add(G.Gf8.add(t22, t32), G.Gf8.add(t23, t33))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t12), G.Gf8.add(t22, t32)), G.Gf8.add(G.Gf8.add(t03, t13), G.Gf8.add(t23, t33))), ap.swap4(G.Gf8.add(t02, t12), G.Gf8.add(t03, t13), G.Gf8.add(t22, t32), G.Gf8.add(t23, t33))) : {G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t20, t30)), G.Gf8.add(G.Gf8.add(t01, t11), G.Gf8.add(t21, t31))), _) == G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(t00, t10), G.Gf8.add(t20, t30)), G.Gf8.add(G.Gf8.add(t01, t11), G.Gf8.add(t21, t31))), G.Gf8.add(G.Gf8.add(G.Gf8.add(t02, t12), G.Gf8.add(t22, t32)), G.Gf8.add(G.Gf8.add(t03, t13), G.Gf8.add(t23, t33)))) : U32}
  {==}

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.swap4
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/gf.bend&name=Gf8.add