def fe_cuts

bend-osdev-apparmor@0.1.0.0 · PROOF.bend:230

import Base
import bend-osdev-apparmor@0.1.0.0/glob.bend as G

230def fe_cuts(+r: List<&2, G.AaGTok>, +s: List<&2, U32>) -> {fe_any(r, G.AaGCuts.all(1n+G.AaGSeq.len(r), s)) == G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), s)) : Bool}:
231  match s:
232    case Nil{}:
233      fe_ef(r, G.AaGCuts.all(G.AaGSeq.len(r), Nil{}))
234    case Con{h, t}:
235      %Equal.sym(Bool, fe_any(r, G.AaGCuts.append(G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), Bool.or(fe_any(r, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), fe_any(r, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), fe_app(r, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : {_ == G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})) : Bool}
236      %Equal.sym(Bool, fe_any(r, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), fe_ef(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))) : {Bool.or(_, fe_any(r, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) == G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})) : Bool}
237      %Equal.sym(Bool, fe_any(r, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), False{}, fe_gr(r, h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))) : {Bool.or(G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), _) == G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})) : Bool}
238      b.or_false_r(G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})))