Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk016Compact001Part048.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpphitnestndv (m n : SemanticCore.Var) (F H I L : SemanticCore.Class) (dv_F_m : m ∉ F.fv) (dv_F_n : n ∉ F.fv) (_dv_H_m : m ∉ H.fv) (dv_H_n : n ∉ H.fv) (dv_I_m : m ∉ I.fv) (dv_I_n : n ∉ I.fv) (_dv_L_m : m ∉ L.fv) (dv_L_n : n ∉ L.fv) (dv_m_n : m ≠ n) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (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))) (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem L Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem H Compiler.CompactSourceSyntax.synCncs) (Compiler.CompactSourceSyntax.synWbr L Compiler.CompactSourceSyntax.synClec H))) (Compiler.CompactSourceSyntax.synWral m Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F I) (SemanticCore.Class.cv m)) Compiler.CompactSourceSyntax.synCncs))).imp (Compiler.CompactSourceSyntax.synWral n Compiler.CompactSourceSyntax.synCnnc ((SemanticCore.Wff.classMem (SemanticCore.Class.cv n) (Compiler.CompactSourceSyntax.synCwpphit F I H)).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv n) (Compiler.CompactSourceSyntax.synCwpphit F I L)))))

Checked nominal proof certificate identified upstream as g_wpphitnestndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpphitstepptndv (F H I L N : SemanticCore.Class) (_dv_F_N : Disjoint F.fv N.fv) (_dv_I_N : Disjoint I.fv N.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (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)) ((Compiler.CompactSourceSyntax.synWbr L Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F I) N)).imp (Compiler.CompactSourceSyntax.synWbr H Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv F (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F I) N))))).imp ((SemanticCore.Wff.classMem N (Compiler.CompactSourceSyntax.synCwpphit F I L)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCplc N Compiler.CompactSourceSyntax.synC1c) (Compiler.CompactSourceSyntax.synCwpphit F I H))))

Checked nominal proof certificate identified upstream as g_wpphitstepptndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpphitstepndv (m n : SemanticCore.Var) (F H I L : SemanticCore.Class) (dv_F_m : m ∉ F.fv) (dv_F_n : n ∉ F.fv) (dv_H_m : m ∉ H.fv) (dv_H_n : n ∉ H.fv) (dv_I_m : m ∉ I.fv) (dv_I_n : n ∉ I.fv) (dv_L_m : m ∉ L.fv) (dv_L_n : n ∉ L.fv) (dv_m_n : m ≠ n) : 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))) (Compiler.CompactSourceSyntax.synWral m Compiler.CompactSourceSyntax.synCnnc ((Compiler.CompactSourceSyntax.synWbr L Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F I) (SemanticCore.Class.cv m))).imp (Compiler.CompactSourceSyntax.synWbr H Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv F (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F I) (SemanticCore.Class.cv m))))))).imp (Compiler.CompactSourceSyntax.synWral n Compiler.CompactSourceSyntax.synCnnc ((SemanticCore.Wff.classMem (SemanticCore.Class.cv n) (Compiler.CompactSourceSyntax.synCwpphit F I L)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv n) Compiler.CompactSourceSyntax.synC1c) (Compiler.CompactSourceSyntax.synCwpphit F I H)))))

Checked nominal proof certificate identified upstream as g_wpphitstepndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part049.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpphitminadjndv (k m n : SemanticCore.Var) (F H I L : SemanticCore.Class) (r q : SemanticCore.Var) (dv_F_k : k ∉ F.fv) (dv_F_m : m ∉ F.fv) (dv_F_n : n ∉ F.fv) (dv_F_q : q ∉ F.fv) (dv_F_r : r ∉ F.fv) (dv_H_k : k ∉ H.fv) (dv_H_m : m ∉ H.fv) (dv_H_n : n ∉ H.fv) (dv_H_q : q ∉ H.fv) (dv_H_r : r ∉ H.fv) (dv_I_k : k ∉ I.fv) (dv_I_m : m ∉ I.fv) (dv_I_n : n ∉ I.fv) (dv_I_q : q ∉ I.fv) (dv_I_r : r ∉ I.fv) (dv_L_k : k ∉ L.fv) (dv_L_m : m ∉ L.fv) (dv_L_n : n ∉ L.fv) (dv_L_q : q ∉ L.fv) (dv_L_r : r ∉ L.fv) (dv_k_m : k ≠ m) (dv_k_n : k ≠ n) (dv_m_n : m ≠ n) (dv_n_q : n ≠ q) (dv_n_r : n ≠ r) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv m) Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem (SemanticCore.Class.cv k) Compiler.CompactSourceSyntax.synCnnc)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv m) (Compiler.CompactSourceSyntax.synCwpphit F I H)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCwpphit F I L)))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWral n Compiler.CompactSourceSyntax.synCnnc ((SemanticCore.Wff.classMem (SemanticCore.Class.cv n) (Compiler.CompactSourceSyntax.synCwpphit F I H)).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv m) (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (SemanticCore.Class.cv n)))) (Compiler.CompactSourceSyntax.synWral n Compiler.CompactSourceSyntax.synCnnc ((SemanticCore.Wff.classMem (SemanticCore.Class.cv n) (Compiler.CompactSourceSyntax.synCwpphit F I L)).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (SemanticCore.Class.cv n)))))) (Compiler.CompactSourceSyntax.synWa (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))) (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem L Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem H Compiler.CompactSourceSyntax.synCncs) (Compiler.CompactSourceSyntax.synWbr L Compiler.CompactSourceSyntax.synClec H))) (Compiler.CompactSourceSyntax.synWral q Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F I) (SemanticCore.Class.cv q)) Compiler.CompactSourceSyntax.synCncs))) (Compiler.CompactSourceSyntax.synWral r Compiler.CompactSourceSyntax.synCnnc ((Compiler.CompactSourceSyntax.synWbr L Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F I) (SemanticCore.Class.cv r))).imp (Compiler.CompactSourceSyntax.synWbr H Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv F (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F I) (SemanticCore.Class.cv r))))))).imp (Compiler.CompactSourceSyntax.synWo (SemanticCore.Wff.classEq (SemanticCore.Class.cv m) (SemanticCore.Class.cv k)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv m) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv k) Compiler.CompactSourceSyntax.synC1c))))

Checked nominal proof certificate identified upstream as g_wpphitminadjndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcardt2fnexndv : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCwppcardt2fn Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_wppcardt2fnexndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcardt2fnmapndv : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf Compiler.CompactSourceSyntax.synCwppcardt2fn (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synCncs)) Compiler.CompactSourceSyntax.synCncs)

Checked nominal proof certificate identified upstream as g_wppcardt2fnmapndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcardt2fnvalsingndv (D : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCncs).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synCwppcardt2fn (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn D))) (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc D))))

Checked nominal proof certificate identified upstream as g_wppcardt2fnvalsingndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwgenvalclndv (B C : SemanticCore.Class) (hyp_hwgenvalclndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) (hyp_hwgenvalclndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synChwgen (Compiler.CompactSourceSyntax.synCop B C)) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCop C (Compiler.CompactSourceSyntax.synCdm B)) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom B C) (Compiler.CompactSourceSyntax.synCcnv B)) (Compiler.CompactSourceSyntax.synCrn B))))

Checked nominal proof certificate identified upstream as g_hwgenvalclndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnbaseresfnvalndv (u : SemanticCore.Var) (F : SemanticCore.Class) (hyp_hnbaseresfnvalndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) (hyp_hnbaseresfnvalndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnbaseresfn F) (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCres F (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))

Checked nominal proof certificate identified upstream as g_hnbaseresfnvalndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part050.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodetrnfnvalndv (u : SemanticCore.Var) (F : SemanticCore.Class) (hyp_hncodetrnfnvalndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) (hyp_hncodetrnfnvalndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChncodetrnfn F) (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCres F (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u))) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCres F (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCres F (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))))

Checked nominal proof certificate identified upstream as g_hncodetrnfnvalndv.

Equations

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