Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk015Compact001Part032.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppostcompfv (R F : SemanticCore.Class) (hyp_wpppostcompfv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) (hyp_wpppostcompfv_2 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwpppostcomp F) R) (Compiler.CompactSourceSyntax.synCcom F R))

Checked nominal proof certificate identified upstream as g_wpppostcompfv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppupperpreopfn (C : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCwppupperpreop C) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wppupperpreopfn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppimageswapfv (R : SemanticCore.Class) (hyp_wppimageswapfv_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCimage Compiler.CompactSourceSyntax.synCswap) R) (Compiler.CompactSourceSyntax.synCcnv R))

Checked nominal proof certificate identified upstream as g_wppimageswapfv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppupperpreopfv (C R : SemanticCore.Class) (hyp_wppupperpreopfv_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwppupperpreop C) R) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv R) (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCsn C))))

Checked nominal proof certificate identified upstream as g_wppupperpreopfv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppowlayerseqfun (C F : SemanticCore.Class) (hyp_wpppowlayerseqfun_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synCwpppowlayerseq F C))

Checked nominal proof certificate identified upstream as g_wpppowlayerseqfun.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpphitfamfv (C D F : SemanticCore.Class) (hyp_wpphitfamfv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwpphitfam F C) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn D))) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCwpppowlayerseq F C)) (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synCsset (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn D)))))

Checked nominal proof certificate identified upstream as g_wpphitfamfv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElwpphitfam (C D F : SemanticCore.Class) (q : SemanticCore.Var) (hyp_elwpphitfam_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) (hyp_elwpphitfam_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwpphitfam F C) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn D)))) (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwpppowlayerseq F C) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv q)))))

Checked nominal proof certificate identified upstream as g_elwpphitfam.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppredmemrelex (C F : SemanticCore.Class) (hyp_wpppredmemrelex_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCwpppredmemrel F C) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wpppredmemrelex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpphitmemrelex (C F : SemanticCore.Class) (hyp_wpppredmemrelex_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCwpphitmemrel F C) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wpphitmemrelex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppreachincbex (C F : SemanticCore.Class) (hyp_wppreachincbex_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCwppreachincb F C) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wppreachincbex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElwppreachincb (C F N : SemanticCore.Class) (_dv_C_F : Disjoint C.fv F.fv) (_dv_C_N : Disjoint C.fv N.fv) (_dv_F_N : Disjoint F.fv N.fv) : Nominal.NPrf ((SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem N (Compiler.CompactSourceSyntax.synCwppreachincb F C)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn N)) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCres (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCwpppredmemrel F C) (Compiler.CompactSourceSyntax.synCwpphitmemrel F C)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCdm F)))))).neg))

Checked nominal proof certificate identified upstream as g_elwppreachincb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppbrcofnv (A B R H : SemanticCore.Class) (_dv_A_R : Disjoint A.fv R.fv) (hyp_wppbrcofnv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn H Compiler.CompactSourceSyntax.synCvv)) (hyp_wppbrcofnv_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A (Compiler.CompactSourceSyntax.synCcom R H) B) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv H A) R B))

Checked nominal proof certificate identified upstream as g_wppbrcofnv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppredfamfn (C F : SemanticCore.Class) (hyp_wpppredfamfn_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCwpppredfam F C) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wpppredfamfn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpphitfamfn (C F : SemanticCore.Class) (hyp_wpppredfamfn_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCwpphitfam F C) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wpphitfamfn.

Equations

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

Certificates from NominalWPPReplayChunk015Compact001Part033.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppreachincbrng (C F N : SemanticCore.Class) (d : SemanticCore.Var) (dv_C_d : d ∉ C.fv) (dv_F_d : d ∉ F.fv) (dv_N_d : d ∉ N.fv) (hyp_wppreachincbrng_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn N)) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCres (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCwpppredmemrel F C) (Compiler.CompactSourceSyntax.synCwpphitmemrel F C)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCdm F)))))).neg (Compiler.CompactSourceSyntax.synWral d (Compiler.CompactSourceSyntax.synCdm F) (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn N) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwpppredfam F C) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv d))))) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn N) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwpphitfam F C) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv d))))))))

Checked nominal proof certificate identified upstream as g_wppreachincbrng.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElwppreachincball (C F N : SemanticCore.Class) (d : SemanticCore.Var) (dv_C_F : Disjoint C.fv F.fv) (dv_C_N : Disjoint C.fv N.fv) (dv_C_d : d ∉ C.fv) (dv_F_N : Disjoint F.fv N.fv) (dv_F_d : d ∉ F.fv) (dv_N_d : d ∉ N.fv) (hyp_elwppreachincball_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem N (Compiler.CompactSourceSyntax.synCwppreachincb F C)) (Compiler.CompactSourceSyntax.synWral d (Compiler.CompactSourceSyntax.synCdm F) (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn N) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwpppredfam F C) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv d))))) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsn N) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwpphitfam F C) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv d)))))))))

Checked nominal proof certificate identified upstream as g_elwppreachincball.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppreachincblayers (C : SemanticCore.Class) (n : SemanticCore.Var) (F : SemanticCore.Class) (d : SemanticCore.Var) (dv_C_F : Disjoint C.fv F.fv) (dv_C_d : d ∉ C.fv) (dv_C_n : n ∉ C.fv) (dv_F_d : d ∉ F.fv) (dv_F_n : n ∉ F.fv) (dv_d_n : d ≠ n) (hyp_wppreachincblayers_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv n) Compiler.CompactSourceSyntax.synCnnc).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv n) (Compiler.CompactSourceSyntax.synCwppreachincb F C)) (Compiler.CompactSourceSyntax.synWral d (Compiler.CompactSourceSyntax.synCdm F) (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv d) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCimage (Compiler.CompactSourceSyntax.synCcnv F)) (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCsn C))) (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv n)))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv d) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwpppowlayerseq F C) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv n))))))))

Checked nominal proof certificate identified upstream as g_wppreachincblayers.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppowcorefn (F : SemanticCore.Class) (hyp_wpppowcorefn_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCwpppostcomp F) Compiler.CompactSourceSyntax.synCid) Compiler.CompactSourceSyntax.synCnnc)

Checked nominal proof certificate identified upstream as g_wpppowcorefn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppowcore0 (F : SemanticCore.Class) (hyp_wpppowcorefn_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCwpppostcomp F) Compiler.CompactSourceSyntax.synCid) Compiler.CompactSourceSyntax.synC0c) Compiler.CompactSourceSyntax.synCid)

Checked nominal proof certificate identified upstream as g_wpppowcore0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppowcoresuc (n : SemanticCore.Var) (F : SemanticCore.Class) (_dv_F_n : n ∉ F.fv) (hyp_wpppowcorefn_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv n) Compiler.CompactSourceSyntax.synCnnc).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCwpppostcomp F) Compiler.CompactSourceSyntax.synCid) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv n) Compiler.CompactSourceSyntax.synC1c)) (Compiler.CompactSourceSyntax.synCcom F (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCwpppostcomp F) Compiler.CompactSourceSyntax.synCid) (SemanticCore.Class.cv n)))))

Checked nominal proof certificate identified upstream as g_wpppowcoresuc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppowlayerseqfv (C : SemanticCore.Class) (n : SemanticCore.Var) (F : SemanticCore.Class) (_dv_C_F : Disjoint C.fv F.fv) (_dv_C_n : n ∉ C.fv) (_dv_F_n : n ∉ F.fv) (hyp_wpppowcorefn_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv n) Compiler.CompactSourceSyntax.synCnnc).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwpppowlayerseq F C) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv n))) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCwpppostcomp F) Compiler.CompactSourceSyntax.synCid) (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv n)))) (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCsn C)))))

Checked nominal proof certificate identified upstream as g_wpppowlayerseqfv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppimageatex (D : SemanticCore.Class) (_hyp_wppimageatex_1 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCwppimageat D) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wppimageatex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppimageatfn (D : SemanticCore.Class) (_hyp_wppimageatfn_1 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCwppimageat D) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wppimageatfn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppimageatfv (D R : SemanticCore.Class) (_hyp_wppimageatfv_1 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) (hyp_wppimageatfv_2 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwppimageat D) R) (Compiler.CompactSourceSyntax.synCima R (Compiler.CompactSourceSyntax.synCsn D)))

Checked nominal proof certificate identified upstream as g_wppimageatfv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppowateqex (D F : SemanticCore.Class) (hyp_wpppowateqex_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) (hyp_wpppowateqex_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCwpppowateq F D) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wpppowateqex.

Equations

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

Certificates from NominalWPPReplayChunk015Compact001Part034.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppowateqval (D : SemanticCore.Class) (n : SemanticCore.Var) (F : SemanticCore.Class) (hyp_wpppowateqval_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wpppowateqval_2 : Nominal.NPrf (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wpppowateqval_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv n) Compiler.CompactSourceSyntax.synCnnc).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv n) (Compiler.CompactSourceSyntax.synCwpppowateq F D)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCwpppostcomp F) Compiler.CompactSourceSyntax.synCid) (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv n))) (Compiler.CompactSourceSyntax.synCsn D)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F D) (SemanticCore.Class.cv n))))))

Checked nominal proof certificate identified upstream as g_wpppowateqval.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppowateqvalcl (B D F : SemanticCore.Class) (hyp_wpppowateqvalcl_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wpppowateqvalcl_2 : Nominal.NPrf (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wpppowateqvalcl_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) : Nominal.NPrf ((SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCnnc).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synCwpppowateq F D)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCwpppostcomp F) Compiler.CompactSourceSyntax.synCid) (Compiler.CompactSourceSyntax.synCtc B)) (Compiler.CompactSourceSyntax.synCsn D)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F D) B)))))

Checked nominal proof certificate identified upstream as g_wpppowateqvalcl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppowcoresuccl (B F : SemanticCore.Class) (hyp_wpppowcoresuccl_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCnnc).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCwpppostcomp F) Compiler.CompactSourceSyntax.synCid) (Compiler.CompactSourceSyntax.synCplc B Compiler.CompactSourceSyntax.synC1c)) (Compiler.CompactSourceSyntax.synCcom F (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCwpppostcomp F) Compiler.CompactSourceSyntax.synCid) B))))

Checked nominal proof certificate identified upstream as g_wpppowcoresuccl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppowateqall (D F N : SemanticCore.Class) (hyp_wpppowateqall_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wpppowateqall_2 : Nominal.NPrf (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wpppowateqall_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) : Nominal.NPrf ((SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc).imp (SemanticCore.Wff.classMem N (Compiler.CompactSourceSyntax.synCwpppowateq F D)))

Checked nominal proof certificate identified upstream as g_wpppowateqall.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppowatact (D F N : SemanticCore.Class) (hyp_wpppowatact_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wpppowatact_2 : Nominal.NPrf (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wpppowatact_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) : Nominal.NPrf ((SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCwpppostcomp F) Compiler.CompactSourceSyntax.synCid) (Compiler.CompactSourceSyntax.synCtc N)) (Compiler.CompactSourceSyntax.synCsn D)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F D) N))))

Checked nominal proof certificate identified upstream as g_wpppowatact.

Equations

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

Certificates from NominalWPPReplayChunk015Compact001Part035.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppreimaactsnd (ph : SemanticCore.Wff) (D R U O : SemanticCore.Class) (_hyp_wpppreimaactsnd_1 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) (hyp_wpppreimaactsnd_2 : Nominal.NPrf (SemanticCore.Wff.classMem O Compiler.CompactSourceSyntax.synCvv)) (hyp_wpppreimaactsnd_3 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima R (Compiler.CompactSourceSyntax.synCsn D)) (Compiler.CompactSourceSyntax.synCsn O)))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv R) U)) (SemanticCore.Wff.classMem O U)))

Checked nominal proof certificate identified upstream as g_wpppreimaactsnd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppowlayerorb (C D : SemanticCore.Class) (n : SemanticCore.Var) (F : SemanticCore.Class) (dv_C_F : Disjoint C.fv F.fv) (dv_C_n : n ∉ C.fv) (dv_F_n : n ∉ F.fv) (hyp_wpppowlayerorb_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wpppowlayerorb_2 : Nominal.NPrf (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wpppowlayerorb_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv n) Compiler.CompactSourceSyntax.synCnnc).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwpppowlayerseq F C) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv n)))) (Compiler.CompactSourceSyntax.synWbr C Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F D) (SemanticCore.Class.cv n)))))

Checked nominal proof certificate identified upstream as g_wpppowlayerorb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppprecompex (F : SemanticCore.Class) (_hyp_wppprecompex_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCwppprecomp F) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wppprecompex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppprecompfn (F : SemanticCore.Class) (hyp_wppprecompfn_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCwppprecomp F) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wppprecompfn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppprecompfv (R F : SemanticCore.Class) (hyp_wppprecompfv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) (hyp_wppprecompfv_2 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwppprecomp F) R) (Compiler.CompactSourceSyntax.synCcom R F))

Checked nominal proof certificate identified upstream as g_wppprecompfv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppowcommeqex (F : SemanticCore.Class) (hyp_wpppowcommeqex_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCwpppowcommeq F) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wpppowcommeqex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppowcommeqval (n : SemanticCore.Var) (F : SemanticCore.Class) (hyp_wpppowcommeqval_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv n) Compiler.CompactSourceSyntax.synCnnc).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv n) (Compiler.CompactSourceSyntax.synCwpppowcommeq F)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCwpppostcomp F) Compiler.CompactSourceSyntax.synCid) (SemanticCore.Class.cv n)) F) (Compiler.CompactSourceSyntax.synCcom F (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCwpppostcomp F) Compiler.CompactSourceSyntax.synCid) (SemanticCore.Class.cv n))))))

Checked nominal proof certificate identified upstream as g_wpppowcommeqval.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppowcommeqvalcl (B F : SemanticCore.Class) (hyp_wpppowcommeqvalcl_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCnnc).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synCwpppowcommeq F)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCwpppostcomp F) Compiler.CompactSourceSyntax.synCid) B) F) (Compiler.CompactSourceSyntax.synCcom F (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCwpppostcomp F) Compiler.CompactSourceSyntax.synCid) B)))))

Checked nominal proof certificate identified upstream as g_wpppowcommeqvalcl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppowcommall (F N : SemanticCore.Class) (hyp_wpppowcommall_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc).imp (SemanticCore.Wff.classMem N (Compiler.CompactSourceSyntax.synCwpppowcommeq F)))

Checked nominal proof certificate identified upstream as g_wpppowcommall.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppowcomm (B F : SemanticCore.Class) (hyp_wpppowcomm_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCnnc).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCwpppostcomp F) Compiler.CompactSourceSyntax.synCid) B) F) (Compiler.CompactSourceSyntax.synCcom F (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCwpppostcomp F) Compiler.CompactSourceSyntax.synCid) B))))

Checked nominal proof certificate identified upstream as g_wpppowcomm.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppowcorersuccl (B F : SemanticCore.Class) (hyp_wpppowcorersuccl_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCnnc).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCwpppostcomp F) Compiler.CompactSourceSyntax.synCid) (Compiler.CompactSourceSyntax.synCplc B Compiler.CompactSourceSyntax.synC1c)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCwpppostcomp F) Compiler.CompactSourceSyntax.synCid) B) F)))

Checked nominal proof certificate identified upstream as g_wpppowcorersuccl.

Equations

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

Certificates from NominalWPPReplayChunk015Compact001Part036.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppowlayerseqfvcl (B C F : SemanticCore.Class) (dv_C_F : Disjoint C.fv F.fv) (hyp_wpppowlayerseqfvcl_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCnnc).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwpppowlayerseq F C) (Compiler.CompactSourceSyntax.synCsn B)) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCwpppostcomp F) Compiler.CompactSourceSyntax.synCid) (Compiler.CompactSourceSyntax.synCtc B))) (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCsn C)))))

Checked nominal proof certificate identified upstream as g_wpppowlayerseqfvcl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpppowlayerseqsuc (C : SemanticCore.Class) (n : SemanticCore.Var) (F : SemanticCore.Class) (dv_C_F : Disjoint C.fv F.fv) (hyp_wpppowlayerseqsuc_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv n) Compiler.CompactSourceSyntax.synCnnc).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwpppowlayerseq F C) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv n) Compiler.CompactSourceSyntax.synC1c))) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv F) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwpppowlayerseq F C) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv n))))))

Checked nominal proof certificate identified upstream as g_wpppowlayerseqsuc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppreachincblayerscl (B C F : SemanticCore.Class) (d : SemanticCore.Var) (dv_B_d : d ∉ B.fv) (dv_C_F : Disjoint C.fv F.fv) (dv_C_d : d ∉ C.fv) (dv_F_d : d ∉ F.fv) (hyp_wppreachincblayerscl_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCnnc).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synCwppreachincb F C)) (Compiler.CompactSourceSyntax.synWral d (Compiler.CompactSourceSyntax.synCdm F) (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv d) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec (Compiler.CompactSourceSyntax.synCimage (Compiler.CompactSourceSyntax.synCcnv F)) (Compiler.CompactSourceSyntax.synCima Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCsn C))) (Compiler.CompactSourceSyntax.synCtc B))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv d) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwpppowlayerseq F C) (Compiler.CompactSourceSyntax.synCsn B)))))))

Checked nominal proof certificate identified upstream as g_wppreachincblayerscl.

Equations

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