Search for blocks/addresses/...

Proofgold Proof

pf
Apply df_ppi__df_mu__df_sgm__df_dchr__df_lgs__df_itv__df_lng__df_trkgc__df_trkgb__df_trkgcb__df_trkge__df_trkgld__df_trkg__df_cgrg__df_ismt__df_leg__df_hlg__df_mir with wceq ccgrg (cmpt (λ x0 . cvv) (λ x0 . copab (λ x1 x2 . wa (wa (wcel (cv x1) (co (cfv (cv x0) cbs) cr cpm)) (wcel (cv x2) (co (cfv (cv x0) cbs) cr cpm))) (wa (wceq (cdm (cv x1)) (cdm (cv x2))) (wral (λ x3 . wral (λ x4 . wceq (co (cfv (cv x3) (cv x1)) (cfv (cv x4) (cv x1)) (cfv (cv x0) cds)) (co (cfv (cv x3) (cv x2)) (cfv (cv x4) (cv x2)) (cfv (cv x0) cds))) (λ x4 . cdm (cv x1))) (λ x3 . cdm (cv x1))))))).
Assume H0: wceq cppi (cmpt (λ x0 . cr) (λ x0 . cfv (cin (co cc0 (cv x0) cicc) cprime) chash)).
Assume H1: wceq cmu (cmpt (λ x0 . cn) (λ x0 . cif (wrex (λ x1 . wbr (co (cv x1) c2 cexp) (cv x0) cdvds) (λ x1 . cprime)) cc0 (co (cneg c1) (cfv (crab (λ x1 . wbr (cv x1) (cv x0) cdvds) (λ x1 . cprime)) chash) cexp))).
Assume H2: wceq csgm (cmpt2 (λ x0 x1 . cc) (λ x0 x1 . cn) (λ x0 x1 . csu (crab (λ x2 . wbr (cv x2) (cv x1) cdvds) (λ x2 . cn)) (λ x2 . co (cv x2) (cv x0) ccxp))).
Assume H3: wceq cdchr (cmpt (λ x0 . cn) (λ x0 . csb (cfv (cv x0) czn) (λ x1 . csb (crab (λ x2 . wss (cxp (cdif (cfv (cv x1) cbs) (cfv (cv x1) cui)) (csn cc0)) (cv x2)) (λ x2 . co (cfv (cv x1) cmgp) (cfv ccnfld cmgp) cmhm)) (λ x2 . cpr (cop (cfv cnx cbs) (cv x2)) (cop (cfv cnx cplusg) (cres (cof cmul) (cxp (cv x2) (cv x2)))))))).
Assume H4: wceq clgs (cmpt2 (λ x0 x1 . cz) (λ x0 x1 . cz) (λ x0 x1 . cif (wceq (cv x1) cc0) (cif (wceq (co (cv x0) c2 cexp) c1) c1 cc0) (co (cif (wa (wbr (cv x1) ... ...) ...) ... ...) ... ...))).
...