Documentation

LeanPool.NFWeakPartition.Certificates.NominalWPPReplayChunk015Compact001Block001

Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk015Compact001Part001.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gKqfinantinn (A B : SemanticCore.Class) :

Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCnnc)).imp ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr A (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) B) (Compiler.CompactSourceSyntax.synWbr B (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) A)).imp (SemanticCore.Wff.classEq A B)))

Checked nominal proof certificate identified upstream as g_kqfinantinn.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNntctfin (N : SemanticCore.Class) :

Nominal.NPrf ((SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc N) (Compiler.CompactSourceSyntax.synCtfin N)))

Checked nominal proof certificate identified upstream as g_nntctfin.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTc6lecan (M N : SemanticCore.Class) (hyp_tc6lecb_1 : Nominal.NPrf (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCncs)) (hyp_tc6lecb_2 : Nominal.NPrf (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCncs)) :

Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc M)))))) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc N))))))).imp (Compiler.CompactSourceSyntax.synWbr M Compiler.CompactSourceSyntax.synClec N))

Checked nominal proof certificate identified upstream as g_tc6lecan.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTc2nc (A : SemanticCore.Class) (hyp_tc2nc_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) :

Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCnc A))) (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 A))))

Checked nominal proof certificate identified upstream as g_tc2nc.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gResiidima (A B : SemanticCore.Class) :

Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCres Compiler.CompactSourceSyntax.synCid A) B) (Compiler.CompactSourceSyntax.synCin A B))

Checked nominal proof certificate identified upstream as g_resiidima.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwsegfnex (D R : SemanticCore.Class) (hyp_hnwsegfnex_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) :

Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChnwsegfn R D) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_hnwsegfnex.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcodefnex (D R : SemanticCore.Class) (hyp_hnwcodefnex_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) :

Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChnwcodefn R) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_hnwcodefnex.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutfnex (D R : SemanticCore.Class) (hyp_hnwcutfnex_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) :

Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChnwcutfn R D) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_hnwcutfnex.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvimagecl (B F : SemanticCore.Class) (hyp_fvimagecl_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) (hyp_fvimagecl_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) :

Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCimage F) B) (Compiler.CompactSourceSyntax.synCima F B))

Checked nominal proof certificate identified upstream as g_fvimagecl.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFncovv (F G : SemanticCore.Class) (hyp_fncovv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn F Compiler.CompactSourceSyntax.synCvv)) (hyp_fncovv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn G Compiler.CompactSourceSyntax.synCvv)) :

Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCcom F G) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_fncovv.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFvtxpvv (A F G : SemanticCore.Class) (hyp_fvtxpvv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn F Compiler.CompactSourceSyntax.synCvv)) (hyp_fvtxpvv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn G Compiler.CompactSourceSyntax.synCvv)) (hyp_fvtxpvv_3 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) :

Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCtxp F G) A) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCfv F A) (Compiler.CompactSourceSyntax.synCfv G A)))

Checked nominal proof certificate identified upstream as g_fvtxpvv.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwsegfnfn (D R : SemanticCore.Class) (hyp_hnwsegfnfn_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) :

Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synChnwsegfn R D) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_hnwsegfnfn.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcodefnfn (D R : SemanticCore.Class) (hyp_hnwcodefnfn_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) :

Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synChnwcodefn R) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_hnwcodefnfn.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutfnfn (D R : SemanticCore.Class) (hyp_hnwcutfnfn_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) :

Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synChnwcutfn R D) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_hnwcutfnfn.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwsegfnval (B D R : SemanticCore.Class) (hyp_hnwsegfnval_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_hnwsegfnval_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) (hyp_hnwsegfnval_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) :

Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnwsegfn R D) B) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) B)))

Checked nominal proof certificate identified upstream as g_hnwsegfnval.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcodefnval (B R : SemanticCore.Class) (hyp_hnwcodefnval_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_hnwcodefnval_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) :

Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnwcodefn R) B) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp B B)) B))

Checked nominal proof certificate identified upstream as g_hnwcodefnval.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutfnvalg (B D R : SemanticCore.Class) (hyp_hnwcutfnvalg_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_hnwcutfnvalg_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) (hyp_hnwcutfnvalg_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) :

Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnwcutfn R D) B) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) B)) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) B)))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) B))))

Checked nominal proof certificate identified upstream as g_hnwcutfnvalg.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutfnvalcl (B D R : SemanticCore.Class) (hyp_hnwcutfnvalcl_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (_hyp_hnwcutfnvalcl_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) :

Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnwcutfn R D) (Compiler.CompactSourceSyntax.synCsn B)) (Compiler.CompactSourceSyntax.synChnwcutcode R D B))

Checked nominal proof certificate identified upstream as g_hnwcutfnvalcl.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutrelex (D R : SemanticCore.Class) (hyp_hnwcutrelex_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) :

Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChnwcutrel R D) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_hnwcutrelex.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutrelfn (D R : SemanticCore.Class) (hyp_hnwcutrelfn_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) :

Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synChnwcutrel R D) (Compiler.CompactSourceSyntax.synCpw1 D))

Checked nominal proof certificate identified upstream as g_hnwcutrelfn.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwpw1argcl (D : SemanticCore.Class) (q : SemanticCore.Var) :

Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCpw1 D)).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q)) D) (SemanticCore.Wff.classEq (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q))))))

Checked nominal proof certificate identified upstream as g_hnwpw1argcl.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutrelval (D R : SemanticCore.Class) (q : SemanticCore.Var) (hyp_hnwcutrelval_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) :

Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCpw1 D)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnwcutrel R D) (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synChnwcutcode R D (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q)))))

Checked nominal proof certificate identified upstream as g_hnwcutrelval.

Equations

One or more equations did not get rendered due to their size.

Instances For

Certificates from NominalWPPReplayChunk015Compact001Part002.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutrelf (D R : SemanticCore.Class) (dv_D_R : Disjoint D.fv R.fv) (hyp_hnwcutrelf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) :

Nominal.NPrf (Compiler.CompactSourceSyntax.synWf (Compiler.CompactSourceSyntax.synChnwcutrel R D) (Compiler.CompactSourceSyntax.synCpw1 D) (Compiler.CompactSourceSyntax.synChwcn D))

Checked nominal proof certificate identified upstream as g_hnwcutrelf.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSifmap (A B F : SemanticCore.Class) :

Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf F A B).imp (Compiler.CompactSourceSyntax.synWf (Compiler.CompactSourceSyntax.synCsi F) (Compiler.CompactSourceSyntax.synCpw1 A) (Compiler.CompactSourceSyntax.synCpw1 B)))

Checked nominal proof certificate identified upstream as g_sifmap.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSifvaldv (A B F : SemanticCore.Class) (c : SemanticCore.Var) (_dv_A_c : c ∉ A.fv) (_dv_B_c : c ∉ B.fv) (_dv_F_c : c ∉ F.fv) (hyp_sifvaldv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf F A B)) :

Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv c) A).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCsi F) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv c))) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv c)))))

Checked nominal proof certificate identified upstream as g_sifvaldv.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSifvald (A B C F : SemanticCore.Class) (hyp_sifvald_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf F A B)) :

Nominal.NPrf ((SemanticCore.Wff.classMem C A).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCsi F) (Compiler.CompactSourceSyntax.synCsn C)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv F C))))

Checked nominal proof certificate identified upstream as g_sifvald.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnqmap1valcl (A B : SemanticCore.Class) (hyp_hnqmap1valcl_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) :

Nominal.NPrf ((SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synChwcn A)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 A) (Compiler.CompactSourceSyntax.synCsn B)) (Compiler.CompactSourceSyntax.synCec B (Compiler.CompactSourceSyntax.synChwniso A))))

Checked nominal proof certificate identified upstream as g_hnqmap1valcl.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gQmapcompvald (ph : SemanticCore.Wff) (A B G X : SemanticCore.Class) (p : SemanticCore.Var) (hyp_qmapcompvald_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_qmapcompvald_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf G X (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn A)))) (hyp_qmapcompvald_3 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv p) X))) (hyp_qmapcompvald_4 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv G (SemanticCore.Class.cv p)) (Compiler.CompactSourceSyntax.synCsn B)))) (hyp_qmapcompvald_5 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synChwcn A)))) :

Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 A) G) (SemanticCore.Class.cv p)) (Compiler.CompactSourceSyntax.synCec B (Compiler.CompactSourceSyntax.synChwniso A))))

Checked nominal proof certificate identified upstream as g_qmapcompvald.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutsirelf (D R : SemanticCore.Class) (dv_D_R : Disjoint D.fv R.fv) (hyp_hnwcutsirelf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) :

Nominal.NPrf (Compiler.CompactSourceSyntax.synWf (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChnwcutrel R D)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn D)))

Checked nominal proof certificate identified upstream as g_hnwcutsirelf.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutsirelex (D R : SemanticCore.Class) (hyp_hnwcutsirelex_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) :

Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChnwcutrel R D)) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_hnwcutsirelex.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutfactorf (D R : SemanticCore.Class) (dv_D_R : Disjoint D.fv R.fv) (hyp_hnwcutfactorf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) :

Nominal.NPrf (Compiler.CompactSourceSyntax.synWf (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 D) (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChnwcutrel R D))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)) (Compiler.CompactSourceSyntax.synChnord D))

Checked nominal proof certificate identified upstream as g_hnwcutfactorf.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutrelvalcld (B D R : SemanticCore.Class) (hyp_hnwcutrelvalcld_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) :

Nominal.NPrf ((SemanticCore.Wff.classMem B D).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnwcutrel R D) (Compiler.CompactSourceSyntax.synCsn B)) (Compiler.CompactSourceSyntax.synChnwcutcode R D B)))

Checked nominal proof certificate identified upstream as g_hnwcutrelvalcld.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutsirelval (D R : SemanticCore.Class) (q : SemanticCore.Var) (dv_D_R : Disjoint D.fv R.fv) (hyp_hnwcutsirelval_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) :

Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChnwcutrel R D)) (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synChnwcutcode R D (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q)))))))

Checked nominal proof certificate identified upstream as g_hnwcutsirelval.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutfactorval (D R : SemanticCore.Class) (q : SemanticCore.Var) (dv_D_R : Disjoint D.fv R.fv) (hyp_hnwcutfactorval_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) :

Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 D) (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChnwcutrel R D))) (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synChnwcutcode R D (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q)))) (Compiler.CompactSourceSyntax.synChwniso D))))

Checked nominal proof certificate identified upstream as g_hnwcutfactorval.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutmapfactor (D R : SemanticCore.Class) (dv_D_R : Disjoint D.fv R.fv) (hyp_hnwcutmapfactor_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) :

Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synChnwcutmap R D) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 D) (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChnwcutrel R D))))

Checked nominal proof certificate identified upstream as g_hnwcutmapfactor.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutmapex (D R : SemanticCore.Class) (dv_D_R : Disjoint D.fv R.fv) (hyp_hnwcutmapex_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) :

Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChnwcutmap R D) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_hnwcutmapex.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutmapcardle (D R : SemanticCore.Class) (dv_D_R : Disjoint D.fv R.fv) (hyp_hnwcutmapcardle_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) :

Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D))) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synChncard D))

Checked nominal proof certificate identified upstream as g_hnwcutmapcardle.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutmaptc2le (D R : SemanticCore.Class) (dv_D_R : Disjoint D.fv R.fv) (hyp_hnwcutmaptc2le_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) :

Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCnc D))) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synChncard D))

Checked nominal proof certificate identified upstream as g_hnwcutmaptc2le.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwcnssbase (A D : SemanticCore.Class) (hyp_hwcnssbase_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss D A)) :

Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synChwcn D) (Compiler.CompactSourceSyntax.synChwcn A))

Checked nominal proof certificate identified upstream as g_hwcnssbase.

Equations

One or more equations did not get rendered due to their size.

Instances For

Certificates from NominalWPPReplayChunk015Compact001Part003.

Checked nominal proof certificate identified upstream as g_hwnisobaserestr.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwnisobaserestrcl (A B C D : SemanticCore.Class) :

Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synChwcn D)) (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcn D))).imp ((Compiler.CompactSourceSyntax.synWbr B (Compiler.CompactSourceSyntax.synChwniso A) C).imp (Compiler.CompactSourceSyntax.synWbr B (Compiler.CompactSourceSyntax.synChwniso D) C)))

Checked nominal proof certificate identified upstream as g_hwnisobaserestrcl.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrlnqrelg (x y : SemanticCore.Var) (C D R V W : SemanticCore.Class) (dv_C_x : x ∉ C.fv) (_dv_C_y : y ∉ C.fv) (dv_D_x : x ∉ D.fv) (dv_D_y : y ∉ D.fv) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) (dv_x_y : x ≠ y) :

Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem C V) (SemanticCore.Wff.classMem D W)).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr C (Compiler.CompactSourceSyntax.synClnqrel R) D) (Compiler.CompactSourceSyntax.synWrex x C (Compiler.CompactSourceSyntax.synWrex y D (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) R (SemanticCore.Class.cv y))))))

Checked nominal proof certificate identified upstream as g_brlnqrelg.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEllnkerec (u : SemanticCore.Var) (R X : SemanticCore.Class) :

Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synCec X (Compiler.CompactSourceSyntax.synClnker R))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr X R (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) R X)))

Checked nominal proof certificate identified upstream as g_ellnkerec.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEllnkerecg (B C R : SemanticCore.Class) :

Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synCec C (Compiler.CompactSourceSyntax.synClnker R))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr C R B) (Compiler.CompactSourceSyntax.synWbr B R C)))

Checked nominal proof certificate identified upstream as g_ellnkerecg.

Equations

One or more equations did not get rendered due to their size.

Instances For

Certificates from NominalWPPReplayChunk015Compact001Part004.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnqrelreps (v u : SemanticCore.Var) (C R X Y : SemanticCore.Class) (dv_C_u : u ∉ C.fv) (dv_C_v : v ∉ C.fv) (dv_R_u : u ∉ R.fv) (dv_R_v : v ∉ R.fv) (dv_X_u : u ∉ X.fv) (dv_X_v : v ∉ X.fv) (dv_Y_u : u ∉ Y.fv) (dv_Y_v : v ∉ Y.fv) (dv_u_v : u ≠ v) :

Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCref C) (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCtrans C)) (Compiler.CompactSourceSyntax.synWss R (Compiler.CompactSourceSyntax.synCxp C C))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem X C) (SemanticCore.Wff.classMem Y C))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWrex u (Compiler.CompactSourceSyntax.synCec X (Compiler.CompactSourceSyntax.synClnker R)) (Compiler.CompactSourceSyntax.synWrex v (Compiler.CompactSourceSyntax.synCec Y (Compiler.CompactSourceSyntax.synClnker R)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) R (SemanticCore.Class.cv v)))) (Compiler.CompactSourceSyntax.synWbr X R Y)))

Checked nominal proof certificate identified upstream as g_lnqrelreps.

Equations

One or more equations did not get rendered due to their size.

Instances For

Certificates from NominalWPPReplayChunk015Compact001Part005.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnkerexg (R : SemanticCore.Class) :

Nominal.NPrf ((SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synClnker R) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_lnkerexg.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrlnqrelkern (C R X Y : SemanticCore.Class) :

Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCref C) (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCtrans C)) (Compiler.CompactSourceSyntax.synWss R (Compiler.CompactSourceSyntax.synCxp C C))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem X C) (SemanticCore.Wff.classMem Y C)))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCec X (Compiler.CompactSourceSyntax.synClnker R)) (Compiler.CompactSourceSyntax.synClnqrel R) (Compiler.CompactSourceSyntax.synCec Y (Compiler.CompactSourceSyntax.synClnker R))) (Compiler.CompactSourceSyntax.synWbr X R Y)))

Checked nominal proof certificate identified upstream as g_brlnqrelkern.

Equations

One or more equations did not get rendered due to their size.

Instances For

Certificates from NominalWPPReplayChunk015Compact001Part006.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnqrelexg (R : SemanticCore.Class) :

Nominal.NPrf ((SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synClnqrel R) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_lnqrelexg.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnquoexg (C R : SemanticCore.Class) (_dv_C_R : Disjoint C.fv R.fv) :

Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synClnquo R C) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_lnquoexg.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnqordexg (C R : SemanticCore.Class) (_dv_C_R : Disjoint C.fv R.fv) :

Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synClnqord R C) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_lnqordexg.

Equations

One or more equations did not get rendered due to their size.

Instances For