def len_rcat

bendtorch@1.3.0.0 · PROOF.bend:165

import Base
import bendtorch@1.3.0.0/main.bend as T
import bend-ml-nat-lemmas@0.1.2.0/main.bend as NL

165# xs reversed onto acc has the length of both
166def len_rcat(+xs: List<&2, F32>, +acc: List<&2, F32>) -> {List.length(&2, F32, T.rcat(xs, acc)) == Nat.add(List.length(&2, F32, xs), List.length(&2, F32, acc)) : Nat}:
167  match xs:
168    case Nil{}:
169      {==}
170    case Con{+x, +t}:
171      Equal.trans(Nat, List.length(&2, F32, T.rcat(t, x <> acc)), Nat.add(List.length(&2, F32, t), 1n+List.length(&2, F32, acc)), 1n+Nat.add(List.length(&2, F32, t), List.length(&2, F32, acc)), len_rcat(t, x <> acc), Equal.sym(Nat, 1n+Nat.add(List.length(&2, F32, t), List.length(&2, F32, acc)), Nat.add(List.length(&2, F32, t), 1n+List.length(&2, F32, acc)), NL.add_succ(List.length(&2, F32, t), List.length(&2, F32, acc))))