# Generated by tools/generators/argon2_gen.py; do not edit by hand.
import Base
import ../../../src/crypto/blake/blake2b/types.bend as T
import ../../../src/crypto/argon2/types.bend as A
import ../../../src/crypto/argon2/blamka.bend as I
import ../../../spec/crypto/argon2/blamka.bend as S
import ./gb.bend as GB

# The compression function of the implementation equals G of the
# specification for every two blocks: P step by step (each step one GB,
# gb.bend), then P on the rows and on the columns, then the XORs.
# Every function the proofs apply to symbolic arguments matches its
# argument first, so the checker keeps such calls folded.

def step0_correct(+v: T.State) -> {I.step0(v) == S.GBi(v, 0n, 4n, 8n, 12n) : T.State}:
  match v:
    case T.V{x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15}:
      Equal.cong(T.Quad, T.State, q => I.put0(q, x1,x2,x3,x5,x6,x7,x9,x10,x11,x13,x14,x15), I.gb(x0, x4, x8, x12), S.GB(x0, x4, x8, x12), GB.gb_correct(x0, x4, x8, x12))

def step1_correct(+v: T.State) -> {I.step1(v) == S.GBi(v, 1n, 5n, 9n, 13n) : T.State}:
  match v:
    case T.V{x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15}:
      Equal.cong(T.Quad, T.State, q => I.put1(q, x0,x2,x3,x4,x6,x7,x8,x10,x11,x12,x14,x15), I.gb(x1, x5, x9, x13), S.GB(x1, x5, x9, x13), GB.gb_correct(x1, x5, x9, x13))

def step2_correct(+v: T.State) -> {I.step2(v) == S.GBi(v, 2n, 6n, 10n, 14n) : T.State}:
  match v:
    case T.V{x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15}:
      Equal.cong(T.Quad, T.State, q => I.put2(q, x0,x1,x3,x4,x5,x7,x8,x9,x11,x12,x13,x15), I.gb(x2, x6, x10, x14), S.GB(x2, x6, x10, x14), GB.gb_correct(x2, x6, x10, x14))

def step3_correct(+v: T.State) -> {I.step3(v) == S.GBi(v, 3n, 7n, 11n, 15n) : T.State}:
  match v:
    case T.V{x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15}:
      Equal.cong(T.Quad, T.State, q => I.put3(q, x0,x1,x2,x4,x5,x6,x8,x9,x10,x12,x13,x14), I.gb(x3, x7, x11, x15), S.GB(x3, x7, x11, x15), GB.gb_correct(x3, x7, x11, x15))

def step4_correct(+v: T.State) -> {I.step4(v) == S.GBi(v, 0n, 5n, 10n, 15n) : T.State}:
  match v:
    case T.V{x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15}:
      Equal.cong(T.Quad, T.State, q => I.put4(q, x1,x2,x3,x4,x6,x7,x8,x9,x11,x12,x13,x14), I.gb(x0, x5, x10, x15), S.GB(x0, x5, x10, x15), GB.gb_correct(x0, x5, x10, x15))

def step5_correct(+v: T.State) -> {I.step5(v) == S.GBi(v, 1n, 6n, 11n, 12n) : T.State}:
  match v:
    case T.V{x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15}:
      Equal.cong(T.Quad, T.State, q => I.put5(q, x0,x2,x3,x4,x5,x7,x8,x9,x10,x13,x14,x15), I.gb(x1, x6, x11, x12), S.GB(x1, x6, x11, x12), GB.gb_correct(x1, x6, x11, x12))

def step6_correct(+v: T.State) -> {I.step6(v) == S.GBi(v, 2n, 7n, 8n, 13n) : T.State}:
  match v:
    case T.V{x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15}:
      Equal.cong(T.Quad, T.State, q => I.put6(q, x0,x1,x3,x4,x5,x6,x9,x10,x11,x12,x14,x15), I.gb(x2, x7, x8, x13), S.GB(x2, x7, x8, x13), GB.gb_correct(x2, x7, x8, x13))

def step7_correct(+v: T.State) -> {I.step7(v) == S.GBi(v, 3n, 4n, 9n, 14n) : T.State}:
  match v:
    case T.V{x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15}:
      Equal.cong(T.Quad, T.State, q => I.put7(q, x0,x1,x2,x5,x6,x7,x8,x10,x11,x12,x13,x15), I.gb(x3, x4, x9, x14), S.GB(x3, x4, x9, x14), GB.gb_correct(x3, x4, x9, x14))

# P, one GB at a time.
def p_correct(+v: T.State) -> {I.p(v) == S.P(v) : T.State}:
  Equal.trans(T.State, I.step7(I.step6(I.step5(I.step4(I.step3(I.step2(I.step1(I.step0(v)))))))), I.step7(I.step6(I.step5(I.step4(I.step3(I.step2(I.step1(S.GBi(v, 0n, 4n, 8n, 12n)))))))), S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n), 1n, 6n, 11n, 12n), 2n, 7n, 8n, 13n), 3n, 4n, 9n, 14n),
    Equal.cong(T.State, T.State, z => I.step7(I.step6(I.step5(I.step4(I.step3(I.step2(I.step1(z))))))), I.step0(v), S.GBi(v, 0n, 4n, 8n, 12n), step0_correct(v)),
    Equal.trans(T.State, I.step7(I.step6(I.step5(I.step4(I.step3(I.step2(I.step1(S.GBi(v, 0n, 4n, 8n, 12n)))))))), I.step7(I.step6(I.step5(I.step4(I.step3(I.step2(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n))))))), S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n), 1n, 6n, 11n, 12n), 2n, 7n, 8n, 13n), 3n, 4n, 9n, 14n),
    Equal.cong(T.State, T.State, z => I.step7(I.step6(I.step5(I.step4(I.step3(I.step2(z)))))), I.step1(S.GBi(v, 0n, 4n, 8n, 12n)), S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), step1_correct(S.GBi(v, 0n, 4n, 8n, 12n))),
    Equal.trans(T.State, I.step7(I.step6(I.step5(I.step4(I.step3(I.step2(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n))))))), I.step7(I.step6(I.step5(I.step4(I.step3(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n)))))), S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n), 1n, 6n, 11n, 12n), 2n, 7n, 8n, 13n), 3n, 4n, 9n, 14n),
    Equal.cong(T.State, T.State, z => I.step7(I.step6(I.step5(I.step4(I.step3(z))))), I.step2(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n)), S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), step2_correct(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n))),
    Equal.trans(T.State, I.step7(I.step6(I.step5(I.step4(I.step3(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n)))))), I.step7(I.step6(I.step5(I.step4(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n))))), S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n), 1n, 6n, 11n, 12n), 2n, 7n, 8n, 13n), 3n, 4n, 9n, 14n),
    Equal.cong(T.State, T.State, z => I.step7(I.step6(I.step5(I.step4(z)))), I.step3(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n)), S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), step3_correct(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n))),
    Equal.trans(T.State, I.step7(I.step6(I.step5(I.step4(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n))))), I.step7(I.step6(I.step5(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n)))), S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n), 1n, 6n, 11n, 12n), 2n, 7n, 8n, 13n), 3n, 4n, 9n, 14n),
    Equal.cong(T.State, T.State, z => I.step7(I.step6(I.step5(z))), I.step4(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n)), S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n), step4_correct(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n))),
    Equal.trans(T.State, I.step7(I.step6(I.step5(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n)))), I.step7(I.step6(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n), 1n, 6n, 11n, 12n))), S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n), 1n, 6n, 11n, 12n), 2n, 7n, 8n, 13n), 3n, 4n, 9n, 14n),
    Equal.cong(T.State, T.State, z => I.step7(I.step6(z)), I.step5(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n)), S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n), 1n, 6n, 11n, 12n), step5_correct(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n))),
    Equal.trans(T.State, I.step7(I.step6(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n), 1n, 6n, 11n, 12n))), I.step7(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n), 1n, 6n, 11n, 12n), 2n, 7n, 8n, 13n)), S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n), 1n, 6n, 11n, 12n), 2n, 7n, 8n, 13n), 3n, 4n, 9n, 14n),
    Equal.cong(T.State, T.State, z => I.step7(z), I.step6(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n), 1n, 6n, 11n, 12n)), S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n), 1n, 6n, 11n, 12n), 2n, 7n, 8n, 13n), step6_correct(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n), 1n, 6n, 11n, 12n))),
    step7_correct(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(S.GBi(v, 0n, 4n, 8n, 12n), 1n, 5n, 9n, 13n), 2n, 6n, 10n, 14n), 3n, 7n, 11n, 15n), 0n, 5n, 10n, 15n), 1n, 6n, 11n, 12n), 2n, 7n, 8n, 13n)))))))))

# P on the rows: the rows are the specification's gathered lanes.
def rows_correct(+b: A.Block) -> {I.rows(b) == S.rows(b) : A.Block}:
  match b:
    case A.B{T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15},T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31},T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47},T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63},T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79},T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95},T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111},T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127}}:
      Equal.trans(A.Block, A.B{I.p(T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15}),I.p(T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31}),I.p(T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47}),I.p(T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63}),I.p(T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79}),I.p(T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95}),I.p(T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111}),I.p(T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127})}, A.B{S.P(T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15}),I.p(T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31}),I.p(T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47}),I.p(T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63}),I.p(T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79}),I.p(T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95}),I.p(T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111}),I.p(T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127})}, A.B{S.P(T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15}),S.P(T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31}),S.P(T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47}),S.P(T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63}),S.P(T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79}),S.P(T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95}),S.P(T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111}),S.P(T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127})},
        Equal.cong(T.State, A.Block, z => A.B{z,I.p(T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31}),I.p(T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47}),I.p(T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63}),I.p(T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79}),I.p(T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95}),I.p(T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111}),I.p(T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127})}, I.p(T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15}), S.P(T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15}), p_correct(T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15})),
        Equal.trans(A.Block, A.B{S.P(T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15}),I.p(T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31}),I.p(T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47}),I.p(T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63}),I.p(T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79}),I.p(T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95}),I.p(T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111}),I.p(T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127})}, A.B{S.P(T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15}),S.P(T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31}),I.p(T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47}),I.p(T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63}),I.p(T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79}),I.p(T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95}),I.p(T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111}),I.p(T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127})}, A.B{S.P(T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15}),S.P(T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31}),S.P(T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47}),S.P(T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63}),S.P(T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79}),S.P(T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95}),S.P(T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111}),S.P(T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127})},
        Equal.cong(T.State, A.Block, z => A.B{S.P(T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15}),z,I.p(T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47}),I.p(T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63}),I.p(T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79}),I.p(T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95}),I.p(T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111}),I.p(T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127})}, I.p(T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31}), S.P(T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31}), p_correct(T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31})),
        Equal.trans(A.Block, A.B{S.P(T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15}),S.P(T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31}),I.p(T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47}),I.p(T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63}),I.p(T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79}),I.p(T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95}),I.p(T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111}),I.p(T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127})}, A.B{S.P(T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15}),S.P(T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31}),S.P(T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47}),I.p(T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63}),I.p(T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79}),I.p(T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95}),I.p(T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111}),I.p(T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127})}, A.B{S.P(T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15}),S.P(T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31}),S.P(T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47}),S.P(T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63}),S.P(T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79}),S.P(T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95}),S.P(T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111}),S.P(T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127})},
        Equal.cong(T.State, A.Block, z => A.B{S.P(T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15}),S.P(T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31}),z,I.p(T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63}),I.p(T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79}),I.p(T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95}),I.p(T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111}),I.p(T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127})}, I.p(T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47}), S.P(T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47}), p_correct(T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47})),
        Equal.trans(A.Block, A.B{S.P(T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15}),S.P(T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31}),S.P(T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47}),I.p(T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63}),I.p(T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79}),I.p(T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95}),I.p(T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111}),I.p(T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127})}, A.B{S.P(T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15}),S.P(T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31}),S.P(T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47}),S.P(T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63}),I.p(T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79}),I.p(T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95}),I.p(T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111}),I.p(T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127})}, A.B{S.P(T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15}),S.P(T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31}),S.P(T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47}),S.P(T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63}),S.P(T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79}),S.P(T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95}),S.P(T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111}),S.P(T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127})},
        Equal.cong(T.State, A.Block, z => A.B{S.P(T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15}),S.P(T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31}),S.P(T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47}),z,I.p(T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79}),I.p(T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95}),I.p(T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111}),I.p(T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127})}, I.p(T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63}), S.P(T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63}), p_correct(T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63})),
        Equal.trans(A.Block, A.B{S.P(T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15}),S.P(T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31}),S.P(T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47}),S.P(T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63}),I.p(T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79}),I.p(T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95}),I.p(T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111}),I.p(T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127})}, A.B{S.P(T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15}),S.P(T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31}),S.P(T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47}),S.P(T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63}),S.P(T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79}),I.p(T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95}),I.p(T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111}),I.p(T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127})}, A.B{S.P(T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15}),S.P(T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31}),S.P(T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47}),S.P(T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63}),S.P(T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79}),S.P(T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95}),S.P(T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111}),S.P(T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127})},
        Equal.cong(T.State, A.Block, z => A.B{S.P(T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15}),S.P(T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31}),S.P(T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47}),S.P(T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63}),z,I.p(T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95}),I.p(T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111}),I.p(T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127})}, I.p(T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79}), S.P(T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79}), p_correct(T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79})),
        Equal.trans(A.Block, A.B{S.P(T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15}),S.P(T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31}),S.P(T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47}),S.P(T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63}),S.P(T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79}),I.p(T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95}),I.p(T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111}),I.p(T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127})}, A.B{S.P(T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15}),S.P(T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31}),S.P(T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47}),S.P(T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63}),S.P(T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79}),S.P(T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95}),I.p(T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111}),I.p(T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127})}, A.B{S.P(T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15}),S.P(T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31}),S.P(T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47}),S.P(T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63}),S.P(T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79}),S.P(T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95}),S.P(T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111}),S.P(T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127})},
        Equal.cong(T.State, A.Block, z => A.B{S.P(T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15}),S.P(T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31}),S.P(T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47}),S.P(T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63}),S.P(T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79}),z,I.p(T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111}),I.p(T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127})}, I.p(T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95}), S.P(T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95}), p_correct(T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95})),
        Equal.trans(A.Block, A.B{S.P(T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15}),S.P(T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31}),S.P(T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47}),S.P(T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63}),S.P(T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79}),S.P(T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95}),I.p(T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111}),I.p(T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127})}, A.B{S.P(T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15}),S.P(T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31}),S.P(T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47}),S.P(T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63}),S.P(T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79}),S.P(T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95}),S.P(T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111}),I.p(T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127})}, A.B{S.P(T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15}),S.P(T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31}),S.P(T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47}),S.P(T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63}),S.P(T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79}),S.P(T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95}),S.P(T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111}),S.P(T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127})},
        Equal.cong(T.State, A.Block, z => A.B{S.P(T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15}),S.P(T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31}),S.P(T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47}),S.P(T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63}),S.P(T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79}),S.P(T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95}),z,I.p(T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127})}, I.p(T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111}), S.P(T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111}), p_correct(T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111})),
        Equal.cong(T.State, A.Block, z => A.B{S.P(T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15}),S.P(T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31}),S.P(T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47}),S.P(T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63}),S.P(T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79}),S.P(T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95}),S.P(T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111}),z}, I.p(T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127}), S.P(T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127}), p_correct(T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127})))))))))

# P on the columns: column i of the specification is lanes 2i, 2i+1, 2i+16, ...
def cols_correct(+b: A.Block) -> {I.cols(b) == S.cols(b) : A.Block}:
  match b:
    case A.B{T.V{l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15},T.V{l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31},T.V{l32,l33,l34,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47},T.V{l48,l49,l50,l51,l52,l53,l54,l55,l56,l57,l58,l59,l60,l61,l62,l63},T.V{l64,l65,l66,l67,l68,l69,l70,l71,l72,l73,l74,l75,l76,l77,l78,l79},T.V{l80,l81,l82,l83,l84,l85,l86,l87,l88,l89,l90,l91,l92,l93,l94,l95},T.V{l96,l97,l98,l99,l100,l101,l102,l103,l104,l105,l106,l107,l108,l109,l110,l111},T.V{l112,l113,l114,l115,l116,l117,l118,l119,l120,l121,l122,l123,l124,l125,l126,l127}}:
      Equal.trans(A.Block, I.untr(I.p(T.V{l0,l1,l16,l17,l32,l33,l48,l49,l64,l65,l80,l81,l96,l97,l112,l113}),I.p(T.V{l2,l3,l18,l19,l34,l35,l50,l51,l66,l67,l82,l83,l98,l99,l114,l115}),I.p(T.V{l4,l5,l20,l21,l36,l37,l52,l53,l68,l69,l84,l85,l100,l101,l116,l117}),I.p(T.V{l6,l7,l22,l23,l38,l39,l54,l55,l70,l71,l86,l87,l102,l103,l118,l119}),I.p(T.V{l8,l9,l24,l25,l40,l41,l56,l57,l72,l73,l88,l89,l104,l105,l120,l121}),I.p(T.V{l10,l11,l26,l27,l42,l43,l58,l59,l74,l75,l90,l91,l106,l107,l122,l123}),I.p(T.V{l12,l13,l28,l29,l44,l45,l60,l61,l76,l77,l92,l93,l108,l109,l124,l125}),I.p(T.V{l14,l15,l30,l31,l46,l47,l62,l63,l78,l79,l94,l95,l110,l111,l126,l127})), I.untr(S.P(T.V{l0,l1,l16,l17,l32,l33,l48,l49,l64,l65,l80,l81,l96,l97,l112,l113}),I.p(T.V{l2,l3,l18,l19,l34,l35,l50,l51,l66,l67,l82,l83,l98,l99,l114,l115}),I.p(T.V{l4,l5,l20,l21,l36,l37,l52,l53,l68,l69,l84,l85,l100,l101,l116,l117}),I.p(T.V{l6,l7,l22,l23,l38,l39,l54,l55,l70,l71,l86,l87,l102,l103,l118,l119}),I.p(T.V{l8,l9,l24,l25,l40,l41,l56,l57,l72,l73,l88,l89,l104,l105,l120,l121}),I.p(T.V{l10,l11,l26,l27,l42,l43,l58,l59,l74,l75,l90,l91,l106,l107,l122,l123}),I.p(T.V{l12,l13,l28,l29,l44,l45,l60,l61,l76,l77,l92,l93,l108,l109,l124,l125}),I.p(T.V{l14,l15,l30,l31,l46,l47,l62,l63,l78,l79,l94,l95,l110,l111,l126,l127})), I.untr(S.P(T.V{l0,l1,l16,l17,l32,l33,l48,l49,l64,l65,l80,l81,l96,l97,l112,l113}),S.P(T.V{l2,l3,l18,l19,l34,l35,l50,l51,l66,l67,l82,l83,l98,l99,l114,l115}),S.P(T.V{l4,l5,l20,l21,l36,l37,l52,l53,l68,l69,l84,l85,l100,l101,l116,l117}),S.P(T.V{l6,l7,l22,l23,l38,l39,l54,l55,l70,l71,l86,l87,l102,l103,l118,l119}),S.P(T.V{l8,l9,l24,l25,l40,l41,l56,l57,l72,l73,l88,l89,l104,l105,l120,l121}),S.P(T.V{l10,l11,l26,l27,l42,l43,l58,l59,l74,l75,l90,l91,l106,l107,l122,l123}),S.P(T.V{l12,l13,l28,l29,l44,l45,l60,l61,l76,l77,l92,l93,l108,l109,l124,l125}),S.P(T.V{l14,l15,l30,l31,l46,l47,l62,l63,l78,l79,l94,l95,l110,l111,l126,l127})),
        Equal.cong(T.State, A.Block, z => I.untr(z,I.p(T.V{l2,l3,l18,l19,l34,l35,l50,l51,l66,l67,l82,l83,l98,l99,l114,l115}),I.p(T.V{l4,l5,l20,l21,l36,l37,l52,l53,l68,l69,l84,l85,l100,l101,l116,l117}),I.p(T.V{l6,l7,l22,l23,l38,l39,l54,l55,l70,l71,l86,l87,l102,l103,l118,l119}),I.p(T.V{l8,l9,l24,l25,l40,l41,l56,l57,l72,l73,l88,l89,l104,l105,l120,l121}),I.p(T.V{l10,l11,l26,l27,l42,l43,l58,l59,l74,l75,l90,l91,l106,l107,l122,l123}),I.p(T.V{l12,l13,l28,l29,l44,l45,l60,l61,l76,l77,l92,l93,l108,l109,l124,l125}),I.p(T.V{l14,l15,l30,l31,l46,l47,l62,l63,l78,l79,l94,l95,l110,l111,l126,l127})), I.p(T.V{l0,l1,l16,l17,l32,l33,l48,l49,l64,l65,l80,l81,l96,l97,l112,l113}), S.P(T.V{l0,l1,l16,l17,l32,l33,l48,l49,l64,l65,l80,l81,l96,l97,l112,l113}), p_correct(T.V{l0,l1,l16,l17,l32,l33,l48,l49,l64,l65,l80,l81,l96,l97,l112,l113})),
        Equal.trans(A.Block, I.untr(S.P(T.V{l0,l1,l16,l17,l32,l33,l48,l49,l64,l65,l80,l81,l96,l97,l112,l113}),I.p(T.V{l2,l3,l18,l19,l34,l35,l50,l51,l66,l67,l82,l83,l98,l99,l114,l115}),I.p(T.V{l4,l5,l20,l21,l36,l37,l52,l53,l68,l69,l84,l85,l100,l101,l116,l117}),I.p(T.V{l6,l7,l22,l23,l38,l39,l54,l55,l70,l71,l86,l87,l102,l103,l118,l119}),I.p(T.V{l8,l9,l24,l25,l40,l41,l56,l57,l72,l73,l88,l89,l104,l105,l120,l121}),I.p(T.V{l10,l11,l26,l27,l42,l43,l58,l59,l74,l75,l90,l91,l106,l107,l122,l123}),I.p(T.V{l12,l13,l28,l29,l44,l45,l60,l61,l76,l77,l92,l93,l108,l109,l124,l125}),I.p(T.V{l14,l15,l30,l31,l46,l47,l62,l63,l78,l79,l94,l95,l110,l111,l126,l127})), I.untr(S.P(T.V{l0,l1,l16,l17,l32,l33,l48,l49,l64,l65,l80,l81,l96,l97,l112,l113}),S.P(T.V{l2,l3,l18,l19,l34,l35,l50,l51,l66,l67,l82,l83,l98,l99,l114,l115}),I.p(T.V{l4,l5,l20,l21,l36,l37,l52,l53,l68,l69,l84,l85,l100,l101,l116,l117}),I.p(T.V{l6,l7,l22,l23,l38,l39,l54,l55,l70,l71,l86,l87,l102,l103,l118,l119}),I.p(T.V{l8,l9,l24,l25,l40,l41,l56,l57,l72,l73,l88,l89,l104,l105,l120,l121}),I.p(T.V{l10,l11,l26,l27,l42,l43,l58,l59,l74,l75,l90,l91,l106,l107,l122,l123}),I.p(T.V{l12,l13,l28,l29,l44,l45,l60,l61,l76,l77,l92,l93,l108,l109,l124,l125}),I.p(T.V{l14,l15,l30,l31,l46,l47,l62,l63,l78,l79,l94,l95,l110,l111,l126,l127})), I.untr(S.P(T.V{l0,l1,l16,l17,l32,l33,l48,l49,l64,l65,l80,l81,l96,l97,l112,l113}),S.P(T.V{l2,l3,l18,l19,l34,l35,l50,l51,l66,l67,l82,l83,l98,l99,l114,l115}),S.P(T.V{l4,l5,l20,l21,l36,l37,l52,l53,l68,l69,l84,l85,l100,l101,l116,l117}),S.P(T.V{l6,l7,l22,l23,l38,l39,l54,l55,l70,l71,l86,l87,l102,l103,l118,l119}),S.P(T.V{l8,l9,l24,l25,l40,l41,l56,l57,l72,l73,l88,l89,l104,l105,l120,l121}),S.P(T.V{l10,l11,l26,l27,l42,l43,l58,l59,l74,l75,l90,l91,l106,l107,l122,l123}),S.P(T.V{l12,l13,l28,l29,l44,l45,l60,l61,l76,l77,l92,l93,l108,l109,l124,l125}),S.P(T.V{l14,l15,l30,l31,l46,l47,l62,l63,l78,l79,l94,l95,l110,l111,l126,l127})),
        Equal.cong(T.State, A.Block, z => I.untr(S.P(T.V{l0,l1,l16,l17,l32,l33,l48,l49,l64,l65,l80,l81,l96,l97,l112,l113}),z,I.p(T.V{l4,l5,l20,l21,l36,l37,l52,l53,l68,l69,l84,l85,l100,l101,l116,l117}),I.p(T.V{l6,l7,l22,l23,l38,l39,l54,l55,l70,l71,l86,l87,l102,l103,l118,l119}),I.p(T.V{l8,l9,l24,l25,l40,l41,l56,l57,l72,l73,l88,l89,l104,l105,l120,l121}),I.p(T.V{l10,l11,l26,l27,l42,l43,l58,l59,l74,l75,l90,l91,l106,l107,l122,l123}),I.p(T.V{l12,l13,l28,l29,l44,l45,l60,l61,l76,l77,l92,l93,l108,l109,l124,l125}),I.p(T.V{l14,l15,l30,l31,l46,l47,l62,l63,l78,l79,l94,l95,l110,l111,l126,l127})), I.p(T.V{l2,l3,l18,l19,l34,l35,l50,l51,l66,l67,l82,l83,l98,l99,l114,l115}), S.P(T.V{l2,l3,l18,l19,l34,l35,l50,l51,l66,l67,l82,l83,l98,l99,l114,l115}), p_correct(T.V{l2,l3,l18,l19,l34,l35,l50,l51,l66,l67,l82,l83,l98,l99,l114,l115})),
        Equal.trans(A.Block, I.untr(S.P(T.V{l0,l1,l16,l17,l32,l33,l48,l49,l64,l65,l80,l81,l96,l97,l112,l113}),S.P(T.V{l2,l3,l18,l19,l34,l35,l50,l51,l66,l67,l82,l83,l98,l99,l114,l115}),I.p(T.V{l4,l5,l20,l21,l36,l37,l52,l53,l68,l69,l84,l85,l100,l101,l116,l117}),I.p(T.V{l6,l7,l22,l23,l38,l39,l54,l55,l70,l71,l86,l87,l102,l103,l118,l119}),I.p(T.V{l8,l9,l24,l25,l40,l41,l56,l57,l72,l73,l88,l89,l104,l105,l120,l121}),I.p(T.V{l10,l11,l26,l27,l42,l43,l58,l59,l74,l75,l90,l91,l106,l107,l122,l123}),I.p(T.V{l12,l13,l28,l29,l44,l45,l60,l61,l76,l77,l92,l93,l108,l109,l124,l125}),I.p(T.V{l14,l15,l30,l31,l46,l47,l62,l63,l78,l79,l94,l95,l110,l111,l126,l127})), I.untr(S.P(T.V{l0,l1,l16,l17,l32,l33,l48,l49,l64,l65,l80,l81,l96,l97,l112,l113}),S.P(T.V{l2,l3,l18,l19,l34,l35,l50,l51,l66,l67,l82,l83,l98,l99,l114,l115}),S.P(T.V{l4,l5,l20,l21,l36,l37,l52,l53,l68,l69,l84,l85,l100,l101,l116,l117}),I.p(T.V{l6,l7,l22,l23,l38,l39,l54,l55,l70,l71,l86,l87,l102,l103,l118,l119}),I.p(T.V{l8,l9,l24,l25,l40,l41,l56,l57,l72,l73,l88,l89,l104,l105,l120,l121}),I.p(T.V{l10,l11,l26,l27,l42,l43,l58,l59,l74,l75,l90,l91,l106,l107,l122,l123}),I.p(T.V{l12,l13,l28,l29,l44,l45,l60,l61,l76,l77,l92,l93,l108,l109,l124,l125}),I.p(T.V{l14,l15,l30,l31,l46,l47,l62,l63,l78,l79,l94,l95,l110,l111,l126,l127})), I.untr(S.P(T.V{l0,l1,l16,l17,l32,l33,l48,l49,l64,l65,l80,l81,l96,l97,l112,l113}),S.P(T.V{l2,l3,l18,l19,l34,l35,l50,l51,l66,l67,l82,l83,l98,l99,l114,l115}),S.P(T.V{l4,l5,l20,l21,l36,l37,l52,l53,l68,l69,l84,l85,l100,l101,l116,l117}),S.P(T.V{l6,l7,l22,l23,l38,l39,l54,l55,l70,l71,l86,l87,l102,l103,l118,l119}),S.P(T.V{l8,l9,l24,l25,l40,l41,l56,l57,l72,l73,l88,l89,l104,l105,l120,l121}),S.P(T.V{l10,l11,l26,l27,l42,l43,l58,l59,l74,l75,l90,l91,l106,l107,l122,l123}),S.P(T.V{l12,l13,l28,l29,l44,l45,l60,l61,l76,l77,l92,l93,l108,l109,l124,l125}),S.P(T.V{l14,l15,l30,l31,l46,l47,l62,l63,l78,l79,l94,l95,l110,l111,l126,l127})),
        Equal.cong(T.State, A.Block, z => I.untr(S.P(T.V{l0,l1,l16,l17,l32,l33,l48,l49,l64,l65,l80,l81,l96,l97,l112,l113}),S.P(T.V{l2,l3,l18,l19,l34,l35,l50,l51,l66,l67,l82,l83,l98,l99,l114,l115}),z,I.p(T.V{l6,l7,l22,l23,l38,l39,l54,l55,l70,l71,l86,l87,l102,l103,l118,l119}),I.p(T.V{l8,l9,l24,l25,l40,l41,l56,l57,l72,l73,l88,l89,l104,l105,l120,l121}),I.p(T.V{l10,l11,l26,l27,l42,l43,l58,l59,l74,l75,l90,l91,l106,l107,l122,l123}),I.p(T.V{l12,l13,l28,l29,l44,l45,l60,l61,l76,l77,l92,l93,l108,l109,l124,l125}),I.p(T.V{l14,l15,l30,l31,l46,l47,l62,l63,l78,l79,l94,l95,l110,l111,l126,l127})), I.p(T.V{l4,l5,l20,l21,l36,l37,l52,l53,l68,l69,l84,l85,l100,l101,l116,l117}), S.P(T.V{l4,l5,l20,l21,l36,l37,l52,l53,l68,l69,l84,l85,l100,l101,l116,l117}), p_correct(T.V{l4,l5,l20,l21,l36,l37,l52,l53,l68,l69,l84,l85,l100,l101,l116,l117})),
        Equal.trans(A.Block, I.untr(S.P(T.V{l0,l1,l16,l17,l32,l33,l48,l49,l64,l65,l80,l81,l96,l97,l112,l113}),S.P(T.V{l2,l3,l18,l19,l34,l35,l50,l51,l66,l67,l82,l83,l98,l99,l114,l115}),S.P(T.V{l4,l5,l20,l21,l36,l37,l52,l53,l68,l69,l84,l85,l100,l101,l116,l117}),I.p(T.V{l6,l7,l22,l23,l38,l39,l54,l55,l70,l71,l86,l87,l102,l103,l118,l119}),I.p(T.V{l8,l9,l24,l25,l40,l41,l56,l57,l72,l73,l88,l89,l104,l105,l120,l121}),I.p(T.V{l10,l11,l26,l27,l42,l43,l58,l59,l74,l75,l90,l91,l106,l107,l122,l123}),I.p(T.V{l12,l13,l28,l29,l44,l45,l60,l61,l76,l77,l92,l93,l108,l109,l124,l125}),I.p(T.V{l14,l15,l30,l31,l46,l47,l62,l63,l78,l79,l94,l95,l110,l111,l126,l127})), I.untr(S.P(T.V{l0,l1,l16,l17,l32,l33,l48,l49,l64,l65,l80,l81,l96,l97,l112,l113}),S.P(T.V{l2,l3,l18,l19,l34,l35,l50,l51,l66,l67,l82,l83,l98,l99,l114,l115}),S.P(T.V{l4,l5,l20,l21,l36,l37,l52,l53,l68,l69,l84,l85,l100,l101,l116,l117}),S.P(T.V{l6,l7,l22,l23,l38,l39,l54,l55,l70,l71,l86,l87,l102,l103,l118,l119}),I.p(T.V{l8,l9,l24,l25,l40,l41,l56,l57,l72,l73,l88,l89,l104,l105,l120,l121}),I.p(T.V{l10,l11,l26,l27,l42,l43,l58,l59,l74,l75,l90,l91,l106,l107,l122,l123}),I.p(T.V{l12,l13,l28,l29,l44,l45,l60,l61,l76,l77,l92,l93,l108,l109,l124,l125}),I.p(T.V{l14,l15,l30,l31,l46,l47,l62,l63,l78,l79,l94,l95,l110,l111,l126,l127})), I.untr(S.P(T.V{l0,l1,l16,l17,l32,l33,l48,l49,l64,l65,l80,l81,l96,l97,l112,l113}),S.P(T.V{l2,l3,l18,l19,l34,l35,l50,l51,l66,l67,l82,l83,l98,l99,l114,l115}),S.P(T.V{l4,l5,l20,l21,l36,l37,l52,l53,l68,l69,l84,l85,l100,l101,l116,l117}),S.P(T.V{l6,l7,l22,l23,l38,l39,l54,l55,l70,l71,l86,l87,l102,l103,l118,l119}),S.P(T.V{l8,l9,l24,l25,l40,l41,l56,l57,l72,l73,l88,l89,l104,l105,l120,l121}),S.P(T.V{l10,l11,l26,l27,l42,l43,l58,l59,l74,l75,l90,l91,l106,l107,l122,l123}),S.P(T.V{l12,l13,l28,l29,l44,l45,l60,l61,l76,l77,l92,l93,l108,l109,l124,l125}),S.P(T.V{l14,l15,l30,l31,l46,l47,l62,l63,l78,l79,l94,l95,l110,l111,l126,l127})),
        Equal.cong(T.State, A.Block, z => I.untr(S.P(T.V{l0,l1,l16,l17,l32,l33,l48,l49,l64,l65,l80,l81,l96,l97,l112,l113}),S.P(T.V{l2,l3,l18,l19,l34,l35,l50,l51,l66,l67,l82,l83,l98,l99,l114,l115}),S.P(T.V{l4,l5,l20,l21,l36,l37,l52,l53,l68,l69,l84,l85,l100,l101,l116,l117}),z,I.p(T.V{l8,l9,l24,l25,l40,l41,l56,l57,l72,l73,l88,l89,l104,l105,l120,l121}),I.p(T.V{l10,l11,l26,l27,l42,l43,l58,l59,l74,l75,l90,l91,l106,l107,l122,l123}),I.p(T.V{l12,l13,l28,l29,l44,l45,l60,l61,l76,l77,l92,l93,l108,l109,l124,l125}),I.p(T.V{l14,l15,l30,l31,l46,l47,l62,l63,l78,l79,l94,l95,l110,l111,l126,l127})), I.p(T.V{l6,l7,l22,l23,l38,l39,l54,l55,l70,l71,l86,l87,l102,l103,l118,l119}), S.P(T.V{l6,l7,l22,l23,l38,l39,l54,l55,l70,l71,l86,l87,l102,l103,l118,l119}), p_correct(T.V{l6,l7,l22,l23,l38,l39,l54,l55,l70,l71,l86,l87,l102,l103,l118,l119})),
        Equal.trans(A.Block, I.untr(S.P(T.V{l0,l1,l16,l17,l32,l33,l48,l49,l64,l65,l80,l81,l96,l97,l112,l113}),S.P(T.V{l2,l3,l18,l19,l34,l35,l50,l51,l66,l67,l82,l83,l98,l99,l114,l115}),S.P(T.V{l4,l5,l20,l21,l36,l37,l52,l53,l68,l69,l84,l85,l100,l101,l116,l117}),S.P(T.V{l6,l7,l22,l23,l38,l39,l54,l55,l70,l71,l86,l87,l102,l103,l118,l119}),I.p(T.V{l8,l9,l24,l25,l40,l41,l56,l57,l72,l73,l88,l89,l104,l105,l120,l121}),I.p(T.V{l10,l11,l26,l27,l42,l43,l58,l59,l74,l75,l90,l91,l106,l107,l122,l123}),I.p(T.V{l12,l13,l28,l29,l44,l45,l60,l61,l76,l77,l92,l93,l108,l109,l124,l125}),I.p(T.V{l14,l15,l30,l31,l46,l47,l62,l63,l78,l79,l94,l95,l110,l111,l126,l127})), I.untr(S.P(T.V{l0,l1,l16,l17,l32,l33,l48,l49,l64,l65,l80,l81,l96,l97,l112,l113}),S.P(T.V{l2,l3,l18,l19,l34,l35,l50,l51,l66,l67,l82,l83,l98,l99,l114,l115}),S.P(T.V{l4,l5,l20,l21,l36,l37,l52,l53,l68,l69,l84,l85,l100,l101,l116,l117}),S.P(T.V{l6,l7,l22,l23,l38,l39,l54,l55,l70,l71,l86,l87,l102,l103,l118,l119}),S.P(T.V{l8,l9,l24,l25,l40,l41,l56,l57,l72,l73,l88,l89,l104,l105,l120,l121}),I.p(T.V{l10,l11,l26,l27,l42,l43,l58,l59,l74,l75,l90,l91,l106,l107,l122,l123}),I.p(T.V{l12,l13,l28,l29,l44,l45,l60,l61,l76,l77,l92,l93,l108,l109,l124,l125}),I.p(T.V{l14,l15,l30,l31,l46,l47,l62,l63,l78,l79,l94,l95,l110,l111,l126,l127})), I.untr(S.P(T.V{l0,l1,l16,l17,l32,l33,l48,l49,l64,l65,l80,l81,l96,l97,l112,l113}),S.P(T.V{l2,l3,l18,l19,l34,l35,l50,l51,l66,l67,l82,l83,l98,l99,l114,l115}),S.P(T.V{l4,l5,l20,l21,l36,l37,l52,l53,l68,l69,l84,l85,l100,l101,l116,l117}),S.P(T.V{l6,l7,l22,l23,l38,l39,l54,l55,l70,l71,l86,l87,l102,l103,l118,l119}),S.P(T.V{l8,l9,l24,l25,l40,l41,l56,l57,l72,l73,l88,l89,l104,l105,l120,l121}),S.P(T.V{l10,l11,l26,l27,l42,l43,l58,l59,l74,l75,l90,l91,l106,l107,l122,l123}),S.P(T.V{l12,l13,l28,l29,l44,l45,l60,l61,l76,l77,l92,l93,l108,l109,l124,l125}),S.P(T.V{l14,l15,l30,l31,l46,l47,l62,l63,l78,l79,l94,l95,l110,l111,l126,l127})),
        Equal.cong(T.State, A.Block, z => I.untr(S.P(T.V{l0,l1,l16,l17,l32,l33,l48,l49,l64,l65,l80,l81,l96,l97,l112,l113}),S.P(T.V{l2,l3,l18,l19,l34,l35,l50,l51,l66,l67,l82,l83,l98,l99,l114,l115}),S.P(T.V{l4,l5,l20,l21,l36,l37,l52,l53,l68,l69,l84,l85,l100,l101,l116,l117}),S.P(T.V{l6,l7,l22,l23,l38,l39,l54,l55,l70,l71,l86,l87,l102,l103,l118,l119}),z,I.p(T.V{l10,l11,l26,l27,l42,l43,l58,l59,l74,l75,l90,l91,l106,l107,l122,l123}),I.p(T.V{l12,l13,l28,l29,l44,l45,l60,l61,l76,l77,l92,l93,l108,l109,l124,l125}),I.p(T.V{l14,l15,l30,l31,l46,l47,l62,l63,l78,l79,l94,l95,l110,l111,l126,l127})), I.p(T.V{l8,l9,l24,l25,l40,l41,l56,l57,l72,l73,l88,l89,l104,l105,l120,l121}), S.P(T.V{l8,l9,l24,l25,l40,l41,l56,l57,l72,l73,l88,l89,l104,l105,l120,l121}), p_correct(T.V{l8,l9,l24,l25,l40,l41,l56,l57,l72,l73,l88,l89,l104,l105,l120,l121})),
        Equal.trans(A.Block, I.untr(S.P(T.V{l0,l1,l16,l17,l32,l33,l48,l49,l64,l65,l80,l81,l96,l97,l112,l113}),S.P(T.V{l2,l3,l18,l19,l34,l35,l50,l51,l66,l67,l82,l83,l98,l99,l114,l115}),S.P(T.V{l4,l5,l20,l21,l36,l37,l52,l53,l68,l69,l84,l85,l100,l101,l116,l117}),S.P(T.V{l6,l7,l22,l23,l38,l39,l54,l55,l70,l71,l86,l87,l102,l103,l118,l119}),S.P(T.V{l8,l9,l24,l25,l40,l41,l56,l57,l72,l73,l88,l89,l104,l105,l120,l121}),I.p(T.V{l10,l11,l26,l27,l42,l43,l58,l59,l74,l75,l90,l91,l106,l107,l122,l123}),I.p(T.V{l12,l13,l28,l29,l44,l45,l60,l61,l76,l77,l92,l93,l108,l109,l124,l125}),I.p(T.V{l14,l15,l30,l31,l46,l47,l62,l63,l78,l79,l94,l95,l110,l111,l126,l127})), I.untr(S.P(T.V{l0,l1,l16,l17,l32,l33,l48,l49,l64,l65,l80,l81,l96,l97,l112,l113}),S.P(T.V{l2,l3,l18,l19,l34,l35,l50,l51,l66,l67,l82,l83,l98,l99,l114,l115}),S.P(T.V{l4,l5,l20,l21,l36,l37,l52,l53,l68,l69,l84,l85,l100,l101,l116,l117}),S.P(T.V{l6,l7,l22,l23,l38,l39,l54,l55,l70,l71,l86,l87,l102,l103,l118,l119}),S.P(T.V{l8,l9,l24,l25,l40,l41,l56,l57,l72,l73,l88,l89,l104,l105,l120,l121}),S.P(T.V{l10,l11,l26,l27,l42,l43,l58,l59,l74,l75,l90,l91,l106,l107,l122,l123}),I.p(T.V{l12,l13,l28,l29,l44,l45,l60,l61,l76,l77,l92,l93,l108,l109,l124,l125}),I.p(T.V{l14,l15,l30,l31,l46,l47,l62,l63,l78,l79,l94,l95,l110,l111,l126,l127})), I.untr(S.P(T.V{l0,l1,l16,l17,l32,l33,l48,l49,l64,l65,l80,l81,l96,l97,l112,l113}),S.P(T.V{l2,l3,l18,l19,l34,l35,l50,l51,l66,l67,l82,l83,l98,l99,l114,l115}),S.P(T.V{l4,l5,l20,l21,l36,l37,l52,l53,l68,l69,l84,l85,l100,l101,l116,l117}),S.P(T.V{l6,l7,l22,l23,l38,l39,l54,l55,l70,l71,l86,l87,l102,l103,l118,l119}),S.P(T.V{l8,l9,l24,l25,l40,l41,l56,l57,l72,l73,l88,l89,l104,l105,l120,l121}),S.P(T.V{l10,l11,l26,l27,l42,l43,l58,l59,l74,l75,l90,l91,l106,l107,l122,l123}),S.P(T.V{l12,l13,l28,l29,l44,l45,l60,l61,l76,l77,l92,l93,l108,l109,l124,l125}),S.P(T.V{l14,l15,l30,l31,l46,l47,l62,l63,l78,l79,l94,l95,l110,l111,l126,l127})),
        Equal.cong(T.State, A.Block, z => I.untr(S.P(T.V{l0,l1,l16,l17,l32,l33,l48,l49,l64,l65,l80,l81,l96,l97,l112,l113}),S.P(T.V{l2,l3,l18,l19,l34,l35,l50,l51,l66,l67,l82,l83,l98,l99,l114,l115}),S.P(T.V{l4,l5,l20,l21,l36,l37,l52,l53,l68,l69,l84,l85,l100,l101,l116,l117}),S.P(T.V{l6,l7,l22,l23,l38,l39,l54,l55,l70,l71,l86,l87,l102,l103,l118,l119}),S.P(T.V{l8,l9,l24,l25,l40,l41,l56,l57,l72,l73,l88,l89,l104,l105,l120,l121}),z,I.p(T.V{l12,l13,l28,l29,l44,l45,l60,l61,l76,l77,l92,l93,l108,l109,l124,l125}),I.p(T.V{l14,l15,l30,l31,l46,l47,l62,l63,l78,l79,l94,l95,l110,l111,l126,l127})), I.p(T.V{l10,l11,l26,l27,l42,l43,l58,l59,l74,l75,l90,l91,l106,l107,l122,l123}), S.P(T.V{l10,l11,l26,l27,l42,l43,l58,l59,l74,l75,l90,l91,l106,l107,l122,l123}), p_correct(T.V{l10,l11,l26,l27,l42,l43,l58,l59,l74,l75,l90,l91,l106,l107,l122,l123})),
        Equal.trans(A.Block, I.untr(S.P(T.V{l0,l1,l16,l17,l32,l33,l48,l49,l64,l65,l80,l81,l96,l97,l112,l113}),S.P(T.V{l2,l3,l18,l19,l34,l35,l50,l51,l66,l67,l82,l83,l98,l99,l114,l115}),S.P(T.V{l4,l5,l20,l21,l36,l37,l52,l53,l68,l69,l84,l85,l100,l101,l116,l117}),S.P(T.V{l6,l7,l22,l23,l38,l39,l54,l55,l70,l71,l86,l87,l102,l103,l118,l119}),S.P(T.V{l8,l9,l24,l25,l40,l41,l56,l57,l72,l73,l88,l89,l104,l105,l120,l121}),S.P(T.V{l10,l11,l26,l27,l42,l43,l58,l59,l74,l75,l90,l91,l106,l107,l122,l123}),I.p(T.V{l12,l13,l28,l29,l44,l45,l60,l61,l76,l77,l92,l93,l108,l109,l124,l125}),I.p(T.V{l14,l15,l30,l31,l46,l47,l62,l63,l78,l79,l94,l95,l110,l111,l126,l127})), I.untr(S.P(T.V{l0,l1,l16,l17,l32,l33,l48,l49,l64,l65,l80,l81,l96,l97,l112,l113}),S.P(T.V{l2,l3,l18,l19,l34,l35,l50,l51,l66,l67,l82,l83,l98,l99,l114,l115}),S.P(T.V{l4,l5,l20,l21,l36,l37,l52,l53,l68,l69,l84,l85,l100,l101,l116,l117}),S.P(T.V{l6,l7,l22,l23,l38,l39,l54,l55,l70,l71,l86,l87,l102,l103,l118,l119}),S.P(T.V{l8,l9,l24,l25,l40,l41,l56,l57,l72,l73,l88,l89,l104,l105,l120,l121}),S.P(T.V{l10,l11,l26,l27,l42,l43,l58,l59,l74,l75,l90,l91,l106,l107,l122,l123}),S.P(T.V{l12,l13,l28,l29,l44,l45,l60,l61,l76,l77,l92,l93,l108,l109,l124,l125}),I.p(T.V{l14,l15,l30,l31,l46,l47,l62,l63,l78,l79,l94,l95,l110,l111,l126,l127})), I.untr(S.P(T.V{l0,l1,l16,l17,l32,l33,l48,l49,l64,l65,l80,l81,l96,l97,l112,l113}),S.P(T.V{l2,l3,l18,l19,l34,l35,l50,l51,l66,l67,l82,l83,l98,l99,l114,l115}),S.P(T.V{l4,l5,l20,l21,l36,l37,l52,l53,l68,l69,l84,l85,l100,l101,l116,l117}),S.P(T.V{l6,l7,l22,l23,l38,l39,l54,l55,l70,l71,l86,l87,l102,l103,l118,l119}),S.P(T.V{l8,l9,l24,l25,l40,l41,l56,l57,l72,l73,l88,l89,l104,l105,l120,l121}),S.P(T.V{l10,l11,l26,l27,l42,l43,l58,l59,l74,l75,l90,l91,l106,l107,l122,l123}),S.P(T.V{l12,l13,l28,l29,l44,l45,l60,l61,l76,l77,l92,l93,l108,l109,l124,l125}),S.P(T.V{l14,l15,l30,l31,l46,l47,l62,l63,l78,l79,l94,l95,l110,l111,l126,l127})),
        Equal.cong(T.State, A.Block, z => I.untr(S.P(T.V{l0,l1,l16,l17,l32,l33,l48,l49,l64,l65,l80,l81,l96,l97,l112,l113}),S.P(T.V{l2,l3,l18,l19,l34,l35,l50,l51,l66,l67,l82,l83,l98,l99,l114,l115}),S.P(T.V{l4,l5,l20,l21,l36,l37,l52,l53,l68,l69,l84,l85,l100,l101,l116,l117}),S.P(T.V{l6,l7,l22,l23,l38,l39,l54,l55,l70,l71,l86,l87,l102,l103,l118,l119}),S.P(T.V{l8,l9,l24,l25,l40,l41,l56,l57,l72,l73,l88,l89,l104,l105,l120,l121}),S.P(T.V{l10,l11,l26,l27,l42,l43,l58,l59,l74,l75,l90,l91,l106,l107,l122,l123}),z,I.p(T.V{l14,l15,l30,l31,l46,l47,l62,l63,l78,l79,l94,l95,l110,l111,l126,l127})), I.p(T.V{l12,l13,l28,l29,l44,l45,l60,l61,l76,l77,l92,l93,l108,l109,l124,l125}), S.P(T.V{l12,l13,l28,l29,l44,l45,l60,l61,l76,l77,l92,l93,l108,l109,l124,l125}), p_correct(T.V{l12,l13,l28,l29,l44,l45,l60,l61,l76,l77,l92,l93,l108,l109,l124,l125})),
        Equal.cong(T.State, A.Block, z => I.untr(S.P(T.V{l0,l1,l16,l17,l32,l33,l48,l49,l64,l65,l80,l81,l96,l97,l112,l113}),S.P(T.V{l2,l3,l18,l19,l34,l35,l50,l51,l66,l67,l82,l83,l98,l99,l114,l115}),S.P(T.V{l4,l5,l20,l21,l36,l37,l52,l53,l68,l69,l84,l85,l100,l101,l116,l117}),S.P(T.V{l6,l7,l22,l23,l38,l39,l54,l55,l70,l71,l86,l87,l102,l103,l118,l119}),S.P(T.V{l8,l9,l24,l25,l40,l41,l56,l57,l72,l73,l88,l89,l104,l105,l120,l121}),S.P(T.V{l10,l11,l26,l27,l42,l43,l58,l59,l74,l75,l90,l91,l106,l107,l122,l123}),S.P(T.V{l12,l13,l28,l29,l44,l45,l60,l61,l76,l77,l92,l93,l108,l109,l124,l125}),z), I.p(T.V{l14,l15,l30,l31,l46,l47,l62,l63,l78,l79,l94,l95,l110,l111,l126,l127}), S.P(T.V{l14,l15,l30,l31,l46,l47,l62,l63,l78,l79,l94,l95,l110,l111,l126,l127}), p_correct(T.V{l14,l15,l30,l31,l46,l47,l62,l63,l78,l79,l94,l95,l110,l111,l126,l127})))))))))

# Two rows XORed, lane by lane.
def xs_correct(+s: T.State, +t: T.State) -> {I.xs(s, t) == S.xor_state(s, t) : T.State}:
  match s t:
    case T.V{T.W{a0,b0},T.W{a1,b1},T.W{a2,b2},T.W{a3,b3},T.W{a4,b4},T.W{a5,b5},T.W{a6,b6},T.W{a7,b7},T.W{a8,b8},T.W{a9,b9},T.W{a10,b10},T.W{a11,b11},T.W{a12,b12},T.W{a13,b13},T.W{a14,b14},T.W{a15,b15}} T.V{T.W{c0,d0},T.W{c1,d1},T.W{c2,d2},T.W{c3,d3},T.W{c4,d4},T.W{c5,d5},T.W{c6,d6},T.W{c7,d7},T.W{c8,d8},T.W{c9,d9},T.W{c10,d10},T.W{c11,d11},T.W{c12,d12},T.W{c13,d13},T.W{c14,d14},T.W{c15,d15}}:
      {==}

# X XOR Y, row by row.
def xor_correct(+x: A.Block, +y: A.Block) -> {I.xor(x, y) == S.xor(x, y) : A.Block}:
  match x y:
    case A.B{+x0,+x1,+x2,+x3,+x4,+x5,+x6,+x7} A.B{+y0,+y1,+y2,+y3,+y4,+y5,+y6,+y7}:
      %Equal.sym(T.State, I.xs(x0, y0), S.xor_state(x0, y0), xs_correct(x0, y0)) : {A.B{_, I.xs(x1, y1), I.xs(x2, y2), I.xs(x3, y3), I.xs(x4, y4), I.xs(x5, y5), I.xs(x6, y6), I.xs(x7, y7)} == S.xor(A.B{x0,x1,x2,x3,x4,x5,x6,x7}, A.B{y0,y1,y2,y3,y4,y5,y6,y7}) : A.Block}
      %Equal.sym(T.State, I.xs(x1, y1), S.xor_state(x1, y1), xs_correct(x1, y1)) : {A.B{S.xor_state(x0, y0), _, I.xs(x2, y2), I.xs(x3, y3), I.xs(x4, y4), I.xs(x5, y5), I.xs(x6, y6), I.xs(x7, y7)} == S.xor(A.B{x0,x1,x2,x3,x4,x5,x6,x7}, A.B{y0,y1,y2,y3,y4,y5,y6,y7}) : A.Block}
      %Equal.sym(T.State, I.xs(x2, y2), S.xor_state(x2, y2), xs_correct(x2, y2)) : {A.B{S.xor_state(x0, y0), S.xor_state(x1, y1), _, I.xs(x3, y3), I.xs(x4, y4), I.xs(x5, y5), I.xs(x6, y6), I.xs(x7, y7)} == S.xor(A.B{x0,x1,x2,x3,x4,x5,x6,x7}, A.B{y0,y1,y2,y3,y4,y5,y6,y7}) : A.Block}
      %Equal.sym(T.State, I.xs(x3, y3), S.xor_state(x3, y3), xs_correct(x3, y3)) : {A.B{S.xor_state(x0, y0), S.xor_state(x1, y1), S.xor_state(x2, y2), _, I.xs(x4, y4), I.xs(x5, y5), I.xs(x6, y6), I.xs(x7, y7)} == S.xor(A.B{x0,x1,x2,x3,x4,x5,x6,x7}, A.B{y0,y1,y2,y3,y4,y5,y6,y7}) : A.Block}
      %Equal.sym(T.State, I.xs(x4, y4), S.xor_state(x4, y4), xs_correct(x4, y4)) : {A.B{S.xor_state(x0, y0), S.xor_state(x1, y1), S.xor_state(x2, y2), S.xor_state(x3, y3), _, I.xs(x5, y5), I.xs(x6, y6), I.xs(x7, y7)} == S.xor(A.B{x0,x1,x2,x3,x4,x5,x6,x7}, A.B{y0,y1,y2,y3,y4,y5,y6,y7}) : A.Block}
      %Equal.sym(T.State, I.xs(x5, y5), S.xor_state(x5, y5), xs_correct(x5, y5)) : {A.B{S.xor_state(x0, y0), S.xor_state(x1, y1), S.xor_state(x2, y2), S.xor_state(x3, y3), S.xor_state(x4, y4), _, I.xs(x6, y6), I.xs(x7, y7)} == S.xor(A.B{x0,x1,x2,x3,x4,x5,x6,x7}, A.B{y0,y1,y2,y3,y4,y5,y6,y7}) : A.Block}
      %Equal.sym(T.State, I.xs(x6, y6), S.xor_state(x6, y6), xs_correct(x6, y6)) : {A.B{S.xor_state(x0, y0), S.xor_state(x1, y1), S.xor_state(x2, y2), S.xor_state(x3, y3), S.xor_state(x4, y4), S.xor_state(x5, y5), _, I.xs(x7, y7)} == S.xor(A.B{x0,x1,x2,x3,x4,x5,x6,x7}, A.B{y0,y1,y2,y3,y4,y5,y6,y7}) : A.Block}
      %Equal.sym(T.State, I.xs(x7, y7), S.xor_state(x7, y7), xs_correct(x7, y7)) : {A.B{S.xor_state(x0, y0), S.xor_state(x1, y1), S.xor_state(x2, y2), S.xor_state(x3, y3), S.xor_state(x4, y4), S.xor_state(x5, y5), S.xor_state(x6, y6), _} == S.xor(A.B{x0,x1,x2,x3,x4,x5,x6,x7}, A.B{y0,y1,y2,y3,y4,y5,y6,y7}) : A.Block}
      {==}

# G(X, Y): the compression function.
def compress_correct(+x: A.Block, +y: A.Block) -> {I.compress(x, y) == S.G(x, y) : A.Block}:
  Equal.trans(A.Block, I.xor(I.cols(I.rows(I.xor(x, y))), I.xor(x, y)), I.xor(I.cols(I.rows(S.xor(x, y))), S.xor(x, y)), S.xor(S.cols(S.rows(S.xor(x, y))), S.xor(x, y)),
    Equal.cong(A.Block, A.Block, +z => I.xor(I.cols(I.rows(z)), z), I.xor(x, y), S.xor(x, y), xor_correct(x, y)),
    Equal.trans(A.Block, I.xor(I.cols(I.rows(S.xor(x, y))), S.xor(x, y)), I.xor(I.cols(S.rows(S.xor(x, y))), S.xor(x, y)), S.xor(S.cols(S.rows(S.xor(x, y))), S.xor(x, y)),
      Equal.cong(A.Block, A.Block, z => I.xor(I.cols(z), S.xor(x, y)), I.rows(S.xor(x, y)), S.rows(S.xor(x, y)), rows_correct(S.xor(x, y))),
      Equal.trans(A.Block, I.xor(I.cols(S.rows(S.xor(x, y))), S.xor(x, y)), I.xor(S.cols(S.rows(S.xor(x, y))), S.xor(x, y)), S.xor(S.cols(S.rows(S.xor(x, y))), S.xor(x, y)),
        Equal.cong(A.Block, A.Block, z => I.xor(z, S.xor(x, y)), I.cols(S.rows(S.xor(x, y))), S.cols(S.rows(S.xor(x, y))), cols_correct(S.rows(S.xor(x, y)))),
        xor_correct(S.cols(S.rows(S.xor(x, y))), S.xor(x, y)))))

# Version 0x13 passes after the first: G(X, Y) XOR the old block.
def compress_xor_correct(+x: A.Block, +y: A.Block, +old: A.Block) -> {I.compress_xor(x, y, old) == S.xor(S.G(x, y), old) : A.Block}:
  Equal.trans(A.Block, I.xor(I.compress(x, y), old), I.xor(S.G(x, y), old), S.xor(S.G(x, y), old),
    Equal.cong(A.Block, A.Block, z => I.xor(z, old), I.compress(x, y), S.G(x, y), compress_correct(x, y)),
    xor_correct(S.G(x, y), old))

# The all-zero block.
def zero_correct() -> {I.zero() == S.zero() : A.Block}:
  {==}