Blamka.cols_correct: def of bend-collections-laws-crypto@1.0.0.0 Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/blamka.bend as Blamka Lines 93-111 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/blamka.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/blamka.bend&start_line=93&end_line=111 import Base import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend as T import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend as A import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/blamka.bend as I import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/blamka.bend as S # 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}))))))))) Uses (10): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/blamka.bend&name=p_correct https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/blamka.bend&name=P https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/blamka.bend&name=cols https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/blamka.bend&name=cols https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/blamka.bend&name=p https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/blamka.bend&name=untr https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend&name=Block https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend&name=State