Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk015Compact001Part016.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFrecdomfv (F I N : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns) (SemanticCore.Wff.classMem I (Compiler.CompactSourceSyntax.synCdm F)) (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F I) N) (Compiler.CompactSourceSyntax.synCdm F)))

Checked nominal proof certificate identified upstream as g_frecdomfv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFuneqfix (A P Q : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (Compiler.CompactSourceSyntax.synWfun P) (Compiler.CompactSourceSyntax.synWfun Q) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCdm P)) (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCdm Q)))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCfix (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv P) Q))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv P A) (Compiler.CompactSourceSyntax.synCfv Q A))))

Checked nominal proof certificate identified upstream as g_funeqfix.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFrecteqex (F G I : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem G Compiler.CompactSourceSyntax.synCvv)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfrecteq F G I) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_frecteqex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSifnvalv (x : SemanticCore.Var) (A F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfn F A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCsi F) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv x)))))

Checked nominal proof certificate identified upstream as g_sifnvalv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTcfnfv (A : SemanticCore.Class) (hyp_tcfnfv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCtcfn (Compiler.CompactSourceSyntax.synCsn A)) (Compiler.CompactSourceSyntax.synCtc A))

Checked nominal proof certificate identified upstream as g_tcfnfv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFrecteqval (n : SemanticCore.Var) (F G I : SemanticCore.Class) (hyp_frecteqval_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_frecteqval_2 : Nominal.NPrf (SemanticCore.Wff.classMem I (Compiler.CompactSourceSyntax.synCdm F))) (hyp_frecteqval_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) (hyp_frecteqval_4 : Nominal.NPrf (SemanticCore.Wff.classMem G Compiler.CompactSourceSyntax.synCfuns)) (hyp_frecteqval_5 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCtc I) (Compiler.CompactSourceSyntax.synCdm G))) (hyp_frecteqval_6 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn G) (Compiler.CompactSourceSyntax.synCdm G))) : 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.synCfrecteq F G I)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F I) (SemanticCore.Class.cv n))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G (Compiler.CompactSourceSyntax.synCtc I)) (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv n))))))

Checked nominal proof certificate identified upstream as g_frecteqval.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFrecteqvalcl (B F G I : SemanticCore.Class) (hyp_frecteqvalcl_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_frecteqvalcl_2 : Nominal.NPrf (SemanticCore.Wff.classMem I (Compiler.CompactSourceSyntax.synCdm F))) (hyp_frecteqvalcl_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) (hyp_frecteqvalcl_4 : Nominal.NPrf (SemanticCore.Wff.classMem G Compiler.CompactSourceSyntax.synCfuns)) (hyp_frecteqvalcl_5 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCtc I) (Compiler.CompactSourceSyntax.synCdm G))) (hyp_frecteqvalcl_6 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn G) (Compiler.CompactSourceSyntax.synCdm G))) : Nominal.NPrf ((SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCnnc).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synCfrecteq F G I)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F I) B)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G (Compiler.CompactSourceSyntax.synCtc I)) (Compiler.CompactSourceSyntax.synCtc B)))))

Checked nominal proof certificate identified upstream as g_frecteqvalcl.

Equations

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

Certificates from NominalWPPReplayChunk015Compact001Part017.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFrectchom0 (x : SemanticCore.Var) (F G I N : SemanticCore.Class) (dv_F_x : x ∉ F.fv) (dv_G_x : x ∉ G.fv) (dv_I_x : x ∉ I.fv) (hyp_frectchom0_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_frectchom0_2 : Nominal.NPrf (SemanticCore.Wff.classMem I (Compiler.CompactSourceSyntax.synCdm F))) (hyp_frectchom0_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) (hyp_frectchom0_4 : Nominal.NPrf (SemanticCore.Wff.classMem G Compiler.CompactSourceSyntax.synCfuns)) (hyp_frectchom0_5 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCtc I) (Compiler.CompactSourceSyntax.synCdm G))) (hyp_frectchom0_6 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn G) (Compiler.CompactSourceSyntax.synCdm G))) (hyp_frectchom0_7 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral x (Compiler.CompactSourceSyntax.synCdm F) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synCfv G (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv x)))))) : Nominal.NPrf ((SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F I) N)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec G (Compiler.CompactSourceSyntax.synCtc I)) (Compiler.CompactSourceSyntax.synCtc N))))

Checked nominal proof certificate identified upstream as g_frectchom0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1pwexd (ph : SemanticCore.Wff) (A B : SemanticCore.Class) (g : SemanticCore.Var) (F : SemanticCore.Class) (dv_A_g : g ∉ A.fv) (_dv_B_g : g ∉ B.fv) (dv_F_g : g ∉ F.fv) (dv_g_ph : g ∉ ph.fv) (hyp_f1pwexd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv))) (hyp_f1pwexd_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWf1 F A B))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWex g (Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv g) (Compiler.CompactSourceSyntax.synCpw A) (Compiler.CompactSourceSyntax.synCpw B))))

Checked nominal proof certificate identified upstream as g_f1pwexd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1pwpwexd (ph : SemanticCore.Wff) (A B : SemanticCore.Class) (h : SemanticCore.Var) (F : SemanticCore.Class) (dv_A_h : h ∉ A.fv) (dv_B_h : h ∉ B.fv) (hyp_f1pwpwexd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv))) (hyp_f1pwpwexd_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWf1 F A B))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv h) (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw A)) (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw B)))))

Checked nominal proof certificate identified upstream as g_f1pwpwexd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gF1pw2exim (A B : SemanticCore.Class) (f h : SemanticCore.Var) (dv_A_f : f ∉ A.fv) (dv_A_h : h ∉ A.fv) (dv_B_f : f ∉ B.fv) (dv_B_h : h ∉ B.fv) (dv_f_h : f ≠ h) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWex f (Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv f) A B)).imp (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv h) (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw A)) (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw B)))))

Checked nominal proof certificate identified upstream as g_f1pw2exim.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNcpw2le (A B : SemanticCore.Class) (hyp_ncpw2le_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_ncpw2le_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCnc A) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCnc B)).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw A))) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw B)))))

Checked nominal proof certificate identified upstream as g_ncpw2le.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwnisobaseext (v u : SemanticCore.Var) (A D : SemanticCore.Class) (dv_u_v : u ≠ v) (hyp_hwnisobaseext_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss D A)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn D)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcn D))).imp ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso D) (SemanticCore.Class.cv v)).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A) (SemanticCore.Class.cv v))))

Checked nominal proof certificate identified upstream as g_hwnisobaseext.

Equations

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

Certificates from NominalWPPReplayChunk015Compact001Part018.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwnisobaseextcl (A B C D : SemanticCore.Class) (hyp_hwnisobaseextcl_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss D A)) : 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 D) C).imp (Compiler.CompactSourceSyntax.synWbr B (Compiler.CompactSourceSyntax.synChwniso A) C)))

Checked nominal proof certificate identified upstream as g_hwnisobaseextcl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwnisobasebicl (A B C D : SemanticCore.Class) (hyp_hwnisobasebicl_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss D A)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synChwcn D)) (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcn D))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr B (Compiler.CompactSourceSyntax.synChwniso A) C) (Compiler.CompactSourceSyntax.synWbr B (Compiler.CompactSourceSyntax.synChwniso D) C)))

Checked nominal proof certificate identified upstream as g_hwnisobasebicl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnqmap1basecompat (A D : SemanticCore.Class) (q p : SemanticCore.Var) (hyp_hnqmap1basecompat_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss D A)) (hyp_hnqmap1basecompat_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) (hyp_hnqmap1basecompat_3 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv p) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn D))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn D)))).imp ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 D) (SemanticCore.Class.cv p)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 D) (SemanticCore.Class.cv q))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 A) (SemanticCore.Class.cv p)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 A) (SemanticCore.Class.cv q)))))

Checked nominal proof certificate identified upstream as g_hnqmap1basecompat.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnqmap1basereflect (A D : SemanticCore.Class) (q p : SemanticCore.Var) (hyp_hnqmap1basereflect_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss D A)) (hyp_hnqmap1basereflect_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) (hyp_hnqmap1basereflect_3 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv p) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn D))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn D)))).imp ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 A) (SemanticCore.Class.cv p)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 A) (SemanticCore.Class.cv q))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 D) (SemanticCore.Class.cv p)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnqmap1 D) (SemanticCore.Class.cv q)))))

Checked nominal proof certificate identified upstream as g_hnqmap1basereflect.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnqincexg (A D : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChnqinc D A) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_hnqincexg.

Equations

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

Certificates from NominalWPPReplayChunk015Compact001Part019.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnqincfun (A D : SemanticCore.Class) (hyp_hnqincfun_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss D A)) (hyp_hnqincfun_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) (hyp_hnqincfun_3 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfun (Compiler.CompactSourceSyntax.synChnqinc D A))

Checked nominal proof certificate identified upstream as g_hnqincfun.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnqincdm (A D : SemanticCore.Class) (hyp_hnqincdm_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss D A)) (hyp_hnqincdm_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) (hyp_hnqincdm_3 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synChnqinc D A)) (Compiler.CompactSourceSyntax.synChnord D))

Checked nominal proof certificate identified upstream as g_hnqincdm.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnqincfn (A D : SemanticCore.Class) (hyp_hnqincfn_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss D A)) (hyp_hnqincfn_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) (hyp_hnqincfn_3 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synChnqinc D A) (Compiler.CompactSourceSyntax.synChnord D))

Checked nominal proof certificate identified upstream as g_hnqincfn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnqincf (A D : SemanticCore.Class) (hyp_hnqincf_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss D A)) (hyp_hnqincf_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) (hyp_hnqincf_3 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf (Compiler.CompactSourceSyntax.synChnqinc D A) (Compiler.CompactSourceSyntax.synChnord D) (Compiler.CompactSourceSyntax.synChnord A))

Checked nominal proof certificate identified upstream as g_hnqincf.

Equations

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

Certificates from NominalWPPReplayChunk015Compact001Part020.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnqincf1 (A D : SemanticCore.Class) (hyp_hnqincf1_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss D A)) (hyp_hnqincf1_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) (hyp_hnqincf1_3 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1 (Compiler.CompactSourceSyntax.synChnqinc D A) (Compiler.CompactSourceSyntax.synChnord D) (Compiler.CompactSourceSyntax.synChnord A))

Checked nominal proof certificate identified upstream as g_hnqincf1.

Equations

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