Apply df_hash__df_word__df_lsw__df_concat__df_s1__df_substr__df_splice__df_reverse__df_reps__df_csh__df_s2__df_s3__df_s4__df_s5__df_s6__df_s7__df_s8__df_trcl with wceq creps (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cn0) (λ x0 x1 . cmpt (λ x2 . co cc0 (cv x1) cfzo) (λ x2 . cv x0))).

Assume H0: wceq chash (cun (ccom (cres (crdg (cmpt (λ x0 . cvv) (λ x0 . co (cv x0) c1 caddc)) cc0) com) ccrd) (cxp (cdif cvv cfn) (csn cpnf))).

Assume H1: ∀ x0 : ι → ο . wceq (cword x0) (cab (λ x1 . wrex (λ x2 . wf (co cc0 (cv x2) cfzo) x0 (cv x1)) (λ x2 . cn0))).

Assume H2: wceq clsw (cmpt (λ x0 . cvv) (λ x0 . cfv (co (cfv (cv x0) chash) c1 cmin) (cv x0))).

Assume H3: wceq cconcat (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cmpt (λ x2 . co cc0 (co (cfv (cv x0) chash) (cfv (cv x1) chash) caddc) cfzo) (λ x2 . cif (wcel (cv x2) (co cc0 (cfv (cv x0) chash) cfzo)) (cfv (cv x2) (cv x0)) (cfv (co (cv x2) (cfv (cv x0) chash) cmin) (cv x1))))).

Assume H4: ∀ x0 : ι → ο . wceq (cs1 x0) (csn (cop cc0 (cfv x0 cid))).

Assume H5: wceq csubstr (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cxp cz cz) (λ x0 x1 . cif (wss (co (cfv (cv x1) c1st) (cfv (cv x1) c2nd) cfzo) (cdm (cv x0))) (cmpt (λ x2 . co cc0 (co (cfv (cv x1) c2nd) (cfv (cv x1) c1st) cmin) cfzo) (λ x2 . cfv (co (cv x2) (cfv (cv x1) c1st) caddc) (cv x0))) c0)).

Assume H6: wceq csplice (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . co (co (co (cv x0) (cop cc0 (cfv (cfv (cv x1) c1st) c1st)) csubstr) (cfv (cv x1) c2nd) cconcat) (co (cv x0) (cop (cfv (cfv (cv x1) c1st) c2nd) (cfv (cv x0) chash)) csubstr) cconcat)).

Assume H7: wceq creverse (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . co cc0 (cfv (cv x0) ...) ...) ...)).

...

■

Proofgold Proof