Apply df_trls__df_trlson__df_pths__df_spths__df_pthson__df_spthson__df_clwlks__df_crcts__df_cycls__df_wwlks__df_wwlksn__df_wwlksnon__df_wspthsn__df_wspthsnon__df_clwwlk__df_clwwlkn__df_clwwlknOLD__df_clwwlknon with wceq cclwwlknold (cmpt2 (λ x0 x1 . cn) (λ x0 x1 . cvv) (λ x0 x1 . crab (λ x2 . wceq (cfv (cv x2) chash) (cv x0)) (λ x2 . cfv (cv x1) cclwwlk))).

Assume H0: wceq ctrls (cmpt (λ x0 . cvv) (λ x0 . copab (λ x1 x2 . wa (wbr (cv x1) (cv x2) (cfv (cv x0) cwlks)) (wfun (ccnv (cv x1)))))).

Assume H1: wceq ctrlson (cmpt (λ x0 . cvv) (λ x0 . cmpt2 (λ x1 x2 . cfv (cv x0) cvtx) (λ x1 x2 . cfv (cv x0) cvtx) (λ x1 x2 . copab (λ x3 x4 . wa (wbr (cv x3) (cv x4) (co (cv x1) (cv x2) (cfv (cv x0) cwlkson))) (wbr (cv x3) (cv x4) (cfv (cv x0) ctrls)))))).

Assume H2: wceq cpths (cmpt (λ x0 . cvv) (λ x0 . copab (λ x1 x2 . w3a (wbr (cv x1) (cv x2) (cfv (cv x0) ctrls)) (wfun (ccnv (cres (cv x2) (co c1 (cfv (cv x1) chash) cfzo)))) (wceq (cin (cima (cv x2) (cpr cc0 (cfv (cv x1) chash))) (cima (cv x2) (co c1 (cfv (cv x1) chash) cfzo))) c0)))).

Assume H3: wceq cspths (cmpt (λ x0 . cvv) (λ x0 . copab (λ x1 x2 . wa (wbr (cv x1) (cv x2) (cfv (cv x0) ctrls)) (wfun (ccnv (cv x2)))))).

Assume H4: wceq cpthson (cmpt (λ x0 . cvv) (λ x0 . cmpt2 (λ x1 x2 . cfv (cv x0) cvtx) (λ x1 x2 . cfv (cv x0) cvtx) (λ x1 x2 . copab (λ x3 x4 . wa (wbr (cv x3) (cv x4) (co (cv x1) (cv x2) (cfv (cv x0) ctrlson))) (wbr (cv x3) (cv x4) (cfv (cv x0) cpths)))))).

Assume H5: wceq cspthson (cmpt (λ x0 . cvv) (λ x0 . cmpt2 (λ x1 x2 . cfv (cv x0) cvtx) (λ x1 x2 . cfv (cv x0) cvtx) (λ x1 x2 . copab (λ x3 x4 . wa (wbr (cv x3) (cv x4) (co (cv x1) (cv x2) (cfv (cv x0) ctrlson))) (wbr (cv x3) (cv x4) (cfv (cv x0) ...)))))).

...

■

Proofgold Proof