def aria_st

bend-osdev-legacy-ciphers@0.1.0.0 · PROOF.bend:8369

import Base
import bend-osdev-legacy-ciphers@0.1.0.0/aria.bend as A

8369def aria_st(s: A.LcAriaSt) -> {s == A.aria.of_block(A.aria.to_block(s)) : A.LcAriaSt}:
8370  match s:
8371    case A.LcAriaSt{WCon{b0_0, WCon{b0_1, WCon{b0_2, WCon{b0_3, WCon{b0_4, WCon{b0_5, WCon{b0_6, WCon{b0_7, WNil{}}}}}}}}}, WCon{b1_0, WCon{b1_1, WCon{b1_2, WCon{b1_3, WCon{b1_4, WCon{b1_5, WCon{b1_6, WCon{b1_7, WNil{}}}}}}}}}, WCon{b2_0, WCon{b2_1, WCon{b2_2, WCon{b2_3, WCon{b2_4, WCon{b2_5, WCon{b2_6, WCon{b2_7, WNil{}}}}}}}}}, WCon{b3_0, WCon{b3_1, WCon{b3_2, WCon{b3_3, WCon{b3_4, WCon{b3_5, WCon{b3_6, WCon{b3_7, WNil{}}}}}}}}}, WCon{b4_0, WCon{b4_1, WCon{b4_2, WCon{b4_3, WCon{b4_4, WCon{b4_5, WCon{b4_6, WCon{b4_7, WNil{}}}}}}}}}, WCon{b5_0, WCon{b5_1, WCon{b5_2, WCon{b5_3, WCon{b5_4, WCon{b5_5, WCon{b5_6, WCon{b5_7, WNil{}}}}}}}}}, WCon{b6_0, WCon{b6_1, WCon{b6_2, WCon{b6_3, WCon{b6_4, WCon{b6_5, WCon{b6_6, WCon{b6_7, WNil{}}}}}}}}}, WCon{b7_0, WCon{b7_1, WCon{b7_2, WCon{b7_3, WCon{b7_4, WCon{b7_5, WCon{b7_6, WCon{b7_7, WNil{}}}}}}}}}, WCon{b8_0, WCon{b8_1, WCon{b8_2, WCon{b8_3, WCon{b8_4, WCon{b8_5, WCon{b8_6, WCon{b8_7, WNil{}}}}}}}}}, WCon{b9_0, WCon{b9_1, WCon{b9_2, WCon{b9_3, WCon{b9_4, WCon{b9_5, WCon{b9_6, WCon{b9_7, WNil{}}}}}}}}}, WCon{b10_0, WCon{b10_1, WCon{b10_2, WCon{b10_3, WCon{b10_4, WCon{b10_5, WCon{b10_6, WCon{b10_7, WNil{}}}}}}}}}, WCon{b11_0, WCon{b11_1, WCon{b11_2, WCon{b11_3, WCon{b11_4, WCon{b11_5, WCon{b11_6, WCon{b11_7, WNil{}}}}}}}}}, WCon{b12_0, WCon{b12_1, WCon{b12_2, WCon{b12_3, WCon{b12_4, WCon{b12_5, WCon{b12_6, WCon{b12_7, WNil{}}}}}}}}}, WCon{b13_0, WCon{b13_1, WCon{b13_2, WCon{b13_3, WCon{b13_4, WCon{b13_5, WCon{b13_6, WCon{b13_7, WNil{}}}}}}}}}, WCon{b14_0, WCon{b14_1, WCon{b14_2, WCon{b14_3, WCon{b14_4, WCon{b14_5, WCon{b14_6, WCon{b14_7, WNil{}}}}}}}}}, WCon{b15_0, WCon{b15_1, WCon{b15_2, WCon{b15_3, WCon{b15_4, WCon{b15_5, WCon{b15_6, WCon{b15_7, WNil{}}}}}}}}}}:
8372      {==}