def zb_ne0
lawful-words@0.1.0.0 · proof_zb.bend:1136
import lawful-words@0.1.0.0/proof_zb.bend as ProofZb
import Base
import lawful-words@0.1.0.0/defs.bend as D
import lawful-words@0.1.0.0/proof_nat.bend as N
1136def zb_ne0(+c0: Bool, +c1: Bool, +c2: Bool, +c3: Bool, +c4: Bool, +c5: Bool, +c6: Bool, +c7: Bool, +c8: Bool, +c9: Bool, +c10: Bool, +c11: Bool, +c12: Bool, +c13: Bool, +c14: Bool, +c15: Bool, +c16: Bool, +c17: Bool, +c18: Bool, +c19: Bool, +c20: Bool, +c21: Bool, +c22: Bool, +c23: Bool, +c24: Bool, +c25: Bool, +c26: Bool, +c27: Bool, +c28: Bool, +c29: Bool, +c30: Bool, +c31: Bool) ->
1137 {U32.is_ne(D.byte(U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, 0n), 0) == Bool.not(allz(8n, WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WNil{}}}}}}}}})) : Bool}:
1138 Equal.cong(Bool, Bool, t => Bool.not(t), Cmp.is_eq(Word.cmp(Nat.add(8n, 24n), Word.and(Nat.add(8n, 24n), app8(24n, WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WNil{}}}}}}}}}, app8(16n, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WNil{}}}}}}}}}, app8(8n, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WNil{}}}}}}}}}, app8(0n, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}, WNil{})))), app8(24n, ones8(), Word.zero(24n))), Word.zero(Nat.add(8n, 24n)))), allz(8n, WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WNil{}}}}}}}}}),
1139 Equal.trans(Bool, Cmp.is_eq(Word.cmp(Nat.add(8n, 24n), Word.and(Nat.add(8n, 24n), app8(24n, WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WNil{}}}}}}}}}, app8(16n, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WNil{}}}}}}}}}, app8(8n, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WNil{}}}}}}}}}, app8(0n, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}, WNil{})))), app8(24n, ones8(), Word.zero(24n))), Word.zero(Nat.add(8n, 24n)))), allz(Nat.add(8n, 24n), Word.and(Nat.add(8n, 24n), app8(24n, WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WNil{}}}}}}}}}, app8(16n, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WNil{}}}}}}}}}, app8(8n, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WNil{}}}}}}}}}, app8(0n, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}, WNil{})))), app8(24n, ones8(), Word.zero(24n)))), allz(8n, WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WNil{}}}}}}}}}),
1140 allz_cmp(Nat.add(8n, 24n), Word.and(Nat.add(8n, 24n), app8(24n, WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WNil{}}}}}}}}}, app8(16n, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WNil{}}}}}}}}}, app8(8n, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WNil{}}}}}}}}}, app8(0n, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}, WNil{})))), app8(24n, ones8(), Word.zero(24n)))),
1141 Equal.trans(Bool, allz(Nat.add(8n, 24n), Word.and(Nat.add(8n, 24n), app8(24n, WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WNil{}}}}}}}}}, app8(16n, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WNil{}}}}}}}}}, app8(8n, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WNil{}}}}}}}}}, app8(0n, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}, WNil{})))), app8(24n, ones8(), Word.zero(24n)))), Bool.and(allz(8n, WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WNil{}}}}}}}}}), allz(24n, Word.and(24n, app8(16n, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WNil{}}}}}}}}}, app8(8n, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WNil{}}}}}}}}}, app8(0n, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}, WNil{}))), Word.zero(24n)))), allz(8n, WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WNil{}}}}}}}}}),
1142 allz_mask(24n, WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WNil{}}}}}}}}}, app8(16n, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WNil{}}}}}}}}}, app8(8n, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WNil{}}}}}}}}}, app8(0n, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}, WNil{})))),
1143 %Equal.sym(Bool, allz(24n, Word.and(24n, app8(16n, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WNil{}}}}}}}}}, app8(8n, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WNil{}}}}}}}}}, app8(0n, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}, WNil{}))), Word.zero(24n))), True{}, allz_andz(24n, app8(16n, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WNil{}}}}}}}}}, app8(8n, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WNil{}}}}}}}}}, app8(0n, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}, WNil{}))))) : {Bool.and(allz(8n, WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WNil{}}}}}}}}}), _) == allz(8n, WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WNil{}}}}}}}}}) : Bool}
1144 N.and_true_r_id(allz(8n, WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WNil{}}}}}}}}})))))