def internal_any_reverse_go

bend-mathlib@0.8.1.0 · list.bend:1559

import Base
import bend-mathlib@0.8.1.0/bool.bend as MBool

1559def internal_any_reverse_go(~a: Quant, ~A: Kind(a), ~f: A -> Bool, xs: List<a, A>, -acc: List<a, A>, c: Bool, e: {List.any(~a, ~A, ~f, acc) == c : Bool}) -> {List.any(~a, ~A, ~f, List.reverse.go(a, A, xs, acc)) == Bool.or(c, List.any(~a, ~A, ~f, xs)) : Bool}:
1560  match xs c:
1561    case Nil{} True{}:
1562      e
1563    case Nil{} False{}:
1564      e
1565    case h <> t True{}:
1566      +v = f(h)
1567      internal_any_reverse_go(~a, ~A, ~f, t, h <> acc, True{}, Equal.trans(Bool, List.any(~a, ~A, ~f, h <> acc), Bool.or(v, List.any(~a, ~A, ~f, acc)), True{}, Equal.sym(Bool, Bool.or(v, List.any(~a, ~A, ~f, acc)), List.any(~a, ~A, ~f, h <> acc), internal_any_cons_test(~a, ~A, ~f, h, acc, v, {==})), Equal.trans(Bool, Bool.or(v, List.any(~a, ~A, ~f, acc)), Bool.or(v, True{}), True{}, Equal.cong(Bool, Bool, k => Bool.or(v, k), List.any(~a, ~A, ~f, acc), True{}, e), MBool.or_true(v))))
1568    case h <> t False{}:
1569      +v = f(h)
1570      %internal_any_cons_test(~a, ~A, ~f, h, t, v, {==}) : {List.any(~a, ~A, ~f, List.reverse.go(a, A, t, h <> acc)) == _ : Bool}
1571      internal_any_reverse_go(~a, ~A, ~f, t, h <> acc, v, Equal.trans(Bool, List.any(~a, ~A, ~f, h <> acc), Bool.or(v, List.any(~a, ~A, ~f, acc)), v, Equal.sym(Bool, Bool.or(v, List.any(~a, ~A, ~f, acc)), List.any(~a, ~A, ~f, h <> acc), internal_any_cons_test(~a, ~A, ~f, h, acc, v, {==})), Equal.trans(Bool, Bool.or(v, List.any(~a, ~A, ~f, acc)), Bool.or(v, False{}), v, Equal.cong(Bool, Bool, k => Bool.or(v, k), List.any(~a, ~A, ~f, acc), False{}, e), MBool.or_false(v))))