def internal_all_reverse_go

bend-mathlib@0.8.1.0 · list.bend:1534

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

1534def internal_all_reverse_go(~a: Quant, ~A: Kind(a), ~f: A -> Bool, xs: List<a, A>, -acc: List<a, A>, c: Bool, e: {List.all(~a, ~A, ~f, acc) == c : Bool}) -> {List.all(~a, ~A, ~f, List.reverse.go(a, A, xs, acc)) == Bool.and(c, List.all(~a, ~A, ~f, xs)) : Bool}:
1535  match xs c:
1536    case Nil{} True{}:
1537      e
1538    case Nil{} False{}:
1539      e
1540    case h <> t True{}:
1541      +v = f(h)
1542      %internal_all_cons_test(~a, ~A, ~f, h, t, v, {==}) : {List.all(~a, ~A, ~f, List.reverse.go(a, A, t, h <> acc)) == _ : Bool}
1543      internal_all_reverse_go(~a, ~A, ~f, t, h <> acc, v, Equal.trans(Bool, List.all(~a, ~A, ~f, h <> acc), Bool.and(v, List.all(~a, ~A, ~f, acc)), v, Equal.sym(Bool, Bool.and(v, List.all(~a, ~A, ~f, acc)), List.all(~a, ~A, ~f, h <> acc), internal_all_cons_test(~a, ~A, ~f, h, acc, v, {==})), Equal.trans(Bool, Bool.and(v, List.all(~a, ~A, ~f, acc)), Bool.and(v, True{}), v, Equal.cong(Bool, Bool, k => Bool.and(v, k), List.all(~a, ~A, ~f, acc), True{}, e), MBool.and_true(v))))
1544    case h <> t False{}:
1545      +v = f(h)
1546      internal_all_reverse_go(~a, ~A, ~f, t, h <> acc, False{}, Equal.trans(Bool, List.all(~a, ~A, ~f, h <> acc), Bool.and(v, List.all(~a, ~A, ~f, acc)), False{}, Equal.sym(Bool, Bool.and(v, List.all(~a, ~A, ~f, acc)), List.all(~a, ~A, ~f, h <> acc), internal_all_cons_test(~a, ~A, ~f, h, acc, v, {==})), Equal.trans(Bool, Bool.and(v, List.all(~a, ~A, ~f, acc)), Bool.and(v, False{}), False{}, Equal.cong(Bool, Bool, k => Bool.and(v, k), List.all(~a, ~A, ~f, acc), False{}, e), MBool.and_false(v))))