PROOF.fe_cuts: def of bend-osdev-apparmor@0.1.0.0
Import: import bend-osdev-apparmor@0.1.0.0/PROOF.bend as PROOF
Lines 230-238 of bend-osdev-apparmor@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&start_line=230&end_line=238

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

def 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}:
  match s:
    case Nil{}:
      fe_ef(r, G.AaGCuts.all(G.AaGSeq.len(r), Nil{}))
    case Con{h, t}:
      %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}
      %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}
      %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}
      b.or_false_r(G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})))

Uses (18):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=b.or_false_r
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=fe_any
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=fe_app
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=fe_ef
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=fe_gr
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGCuts.all
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGCuts.append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGCuts.empty_first
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGCuts.grow
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGSeq.fits_any
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGSeq.len
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/glob.bend&name=AaGTok