Proofgold Asset

Known 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 : ∀ x0 : ο . (wceq chash (cun (ccom (cres (crdg (cmpt (λ x1 . cvv) (λ x1 . co (cv x1) c1 caddc)) cc0) com) ccrd) (cxp (cdif cvv cfn) (csn cpnf))) ⟶ (∀ x1 : ι → ο . wceq (cword x1) (cab (λ x2 . wrex (λ x3 . wf (co cc0 (cv x3) cfzo) x1 (cv x2)) (λ x3 . cn0)))) ⟶ wceq clsw (cmpt (λ x1 . cvv) (λ x1 . cfv (co (cfv (cv x1) chash) c1 cmin) (cv x1))) ⟶ wceq cconcat (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cmpt (λ x3 . co cc0 (co (cfv (cv x1) chash) (cfv (cv x2) chash) caddc) cfzo) (λ x3 . cif (wcel (cv x3) (co cc0 (cfv (cv x1) chash) cfzo)) (cfv (cv x3) (cv x1)) (cfv (co (cv x3) (cfv (cv x1) chash) cmin) (cv x2))))) ⟶ (∀ x1 : ι → ο . wceq (cs1 x1) (csn (cop cc0 (cfv x1 cid)))) ⟶ wceq csubstr (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cxp cz cz) (λ x1 x2 . cif (wss (co (cfv (cv x2) c1st) (cfv (cv x2) c2nd) cfzo) (cdm (cv x1))) (cmpt (λ x3 . co cc0 (co (cfv (cv x2) c2nd) (cfv (cv x2) c1st) cmin) cfzo) (λ x3 . cfv (co (cv x3) (cfv (cv x2) c1st) caddc) (cv x1))) c0)) ⟶ wceq csplice (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . co (co (co (cv x1) (cop cc0 (cfv (cfv (cv x2) c1st) c1st)) csubstr) (cfv (cv x2) c2nd) cconcat) (co (cv x1) (cop (cfv (cfv (cv x2) c1st) c2nd) (cfv (cv x1) chash)) csubstr) cconcat)) ⟶ wceq creverse (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . co cc0 (cfv (cv x1) chash) cfzo) (λ x2 . cfv (co (co (cfv (cv x1) chash) c1 cmin) (cv x2) cmin) (cv x1)))) ⟶ wceq creps (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cn0) (λ x1 x2 . cmpt (λ x3 . co cc0 (cv x2) cfzo) (λ x3 . cv x1))) ⟶ wceq ccsh (cmpt2 (λ x1 x2 . cab (λ x3 . wrex (λ x4 . wfn (cv x3) (co cc0 (cv x4) cfzo)) (λ x4 . cn0))) (λ x1 x2 . cz) (λ x1 x2 . cif (wceq (cv x1) c0) c0 (co (co (cv x1) (cop (co (cv x2) (cfv (cv x1) chash) cmo) (cfv (cv x1) chash)) csubstr) (co (cv x1) (cop cc0 (co (cv x2) (cfv (cv x1) chash) cmo)) csubstr) cconcat))) ⟶ (∀ x1 x2 : ι → ο . wceq (cs2 x1 x2) (co (cs1 x1) (cs1 x2) cconcat)) ⟶ (∀ x1 x2 x3 : ι → ο . wceq (cs3 x1 x2 x3) (co (cs2 x1 x2) (cs1 x3) cconcat)) ⟶ (∀ x1 x2 x3 x4 : ι → ο . wceq (cs4 x1 x2 x3 x4) (co (cs3 x1 x2 x3) (cs1 x4) cconcat)) ⟶ (∀ x1 x2 x3 x4 x5 : ι → ο . wceq (cs5 x1 x2 x3 x4 x5) (co (cs4 x1 x2 x3 x4) (cs1 x5) cconcat)) ⟶ (∀ x1 x2 x3 x4 x5 x6 : ι → ο . wceq (cs6 x1 x2 x3 x4 x5 x6) (co (cs5 x1 x2 x3 x4 x5) (cs1 x6) cconcat)) ⟶ (∀ x1 x2 x3 x4 x5 x6 x7 : ι → ο . wceq (cs7 x1 x2 x3 x4 x5 x6 x7) (co (cs6 x1 x2 x3 x4 x5 x6) (cs1 x7) cconcat)) ⟶ (∀ x1 x2 x3 x4 x5 x6 x7 x8 : ι → ο . wceq (cs8 x1 x2 x3 x4 x5 x6 x7 x8) (co (cs7 x1 x2 x3 x4 x5 x6 x7) (cs1 x8) cconcat)) ⟶ wceq ctcl (cmpt (λ x1 . cvv) (λ x1 . cint (cab (λ x2 . wa (wss (cv x1) (cv x2)) (wss (ccom (cv x2) (cv x2)) (cv x2)))))) ⟶ x0) ⟶ x0
Theorem df_hash : wceq chash (cun (ccom (cres (crdg (cmpt (λ x0 . cvv) (λ x0 . co (cv x0) c1 caddc)) cc0) com) ccrd) (cxp (cdif cvv cfn) (csn cpnf))) (proof)
Theorem df_word : ∀ x0 : ι → ο . wceq (cword x0) (cab (λ x1 . wrex (λ x2 . wf (co cc0 (cv x2) cfzo) x0 (cv x1)) (λ x2 . cn0))) (proof)
Theorem df_lsw : wceq clsw (cmpt (λ x0 . cvv) (λ x0 . cfv (co (cfv (cv x0) chash) c1 cmin) (cv x0))) (proof)
Theorem df_concat : 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))))) (proof)
Theorem df_s1 : ∀ x0 : ι → ο . wceq (cs1 x0) (csn (cop cc0 (cfv x0 cid))) (proof)
Theorem df_substr : 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)) (proof)
Theorem df_splice : 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)) (proof)
Theorem df_reverse : wceq creverse (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . co cc0 (cfv (cv x0) chash) cfzo) (λ x1 . cfv (co (co (cfv (cv x0) chash) c1 cmin) (cv x1) cmin) (cv x0)))) (proof)
Theorem df_reps : wceq creps (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cn0) (λ x0 x1 . cmpt (λ x2 . co cc0 (cv x1) cfzo) (λ x2 . cv x0))) (proof)
Theorem df_csh : wceq ccsh (cmpt2 (λ x0 x1 . cab (λ x2 . wrex (λ x3 . wfn (cv x2) (co cc0 (cv x3) cfzo)) (λ x3 . cn0))) (λ x0 x1 . cz) (λ x0 x1 . cif (wceq (cv x0) c0) c0 (co (co (cv x0) (cop (co (cv x1) (cfv (cv x0) chash) cmo) (cfv (cv x0) chash)) csubstr) (co (cv x0) (cop cc0 (co (cv x1) (cfv (cv x0) chash) cmo)) csubstr) cconcat))) (proof)
Theorem df_s2 : ∀ x0 x1 : ι → ο . wceq (cs2 x0 x1) (co (cs1 x0) (cs1 x1) cconcat) (proof)
Theorem df_s3 : ∀ x0 x1 x2 : ι → ο . wceq (cs3 x0 x1 x2) (co (cs2 x0 x1) (cs1 x2) cconcat) (proof)
Theorem df_s4 : ∀ x0 x1 x2 x3 : ι → ο . wceq (cs4 x0 x1 x2 x3) (co (cs3 x0 x1 x2) (cs1 x3) cconcat) (proof)
Theorem df_s5 : ∀ x0 x1 x2 x3 x4 : ι → ο . wceq (cs5 x0 x1 x2 x3 x4) (co (cs4 x0 x1 x2 x3) (cs1 x4) cconcat) (proof)
Theorem df_s6 : ∀ x0 x1 x2 x3 x4 x5 : ι → ο . wceq (cs6 x0 x1 x2 x3 x4 x5) (co (cs5 x0 x1 x2 x3 x4) (cs1 x5) cconcat) (proof)
Theorem df_s7 : ∀ x0 x1 x2 x3 x4 x5 x6 : ι → ο . wceq (cs7 x0 x1 x2 x3 x4 x5 x6) (co (cs6 x0 x1 x2 x3 x4 x5) (cs1 x6) cconcat) (proof)
Theorem df_s8 : ∀ x0 x1 x2 x3 x4 x5 x6 x7 : ι → ο . wceq (cs8 x0 x1 x2 x3 x4 x5 x6 x7) (co (cs7 x0 x1 x2 x3 x4 x5 x6) (cs1 x7) cconcat) (proof)
Theorem df_trcl : wceq ctcl (cmpt (λ x0 . cvv) (λ x0 . cint (cab (λ x1 . wa (wss (cv x0) (cv x1)) (wss (ccom (cv x1) (cv x1)) (cv x1)))))) (proof)