Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk016Compact001Part066.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsicodemapexgndv (A : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChnsicodemap A) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_hnsicodemapexgndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsicodemapvalndv (A : SemanticCore.Class) (q : SemanticCore.Var) (_dv_A_q : q ∉ A.fv) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn A))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsicodemap A) (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q)))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q)))))))

Checked nominal proof certificate identified upstream as g_hnsicodemapvalndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsicodemapfndv (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf (Compiler.CompactSourceSyntax.synChnsicodemap A) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn A)) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCpw1 A)))

Checked nominal proof certificate identified upstream as g_hnsicodemapfndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPw1typedbrndv (D R : SemanticCore.Class) (q p : SemanticCore.Var) (_dv_D_p : p ∉ D.fv) (_dv_D_q : q ∉ D.fv) (_dv_R_p : p ∉ R.fv) (_dv_R_q : q ∉ R.fv) (_dv_p_q : p ≠ q) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv p) (Compiler.CompactSourceSyntax.synCpw1 D)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCpw1 D))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv p) (Compiler.CompactSourceSyntax.synCsi R) (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)) R (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q)))))

Checked nominal proof certificate identified upstream as g_pw1typedbrndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPw1argclcl (D Q : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem Q (Compiler.CompactSourceSyntax.synCpw1 D)).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni Q) D) (SemanticCore.Wff.classEq Q (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni Q)))))

Checked nominal proof certificate identified upstream as g_pw1argclcl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPw1descentf1odv (x : SemanticCore.Var) (D : SemanticCore.Class) (g : SemanticCore.Var) (E : SemanticCore.Class) (dv_D_x : x ∉ D.fv) (dv_E_x : x ∉ E.fv) (dv_g_x : g ≠ x) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv g) (Compiler.CompactSourceSyntax.synCpw1 D) (Compiler.CompactSourceSyntax.synCpw1 E)).imp (Compiler.CompactSourceSyntax.synWf1o (Compiler.CompactSourceSyntax.synCmpt x D (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv g) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))))) D E))

Checked nominal proof certificate identified upstream as g_pw1descentf1odv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part067.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPw1typedbrcldv (D P Q R : SemanticCore.Class) (hyp_pw1typedbrcldv_1 : Nominal.NPrf (SemanticCore.Wff.classMem P Compiler.CompactSourceSyntax.synCvv)) (hyp_pw1typedbrcldv_2 : Nominal.NPrf (SemanticCore.Wff.classMem Q Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem P (Compiler.CompactSourceSyntax.synCpw1 D)) (SemanticCore.Wff.classMem Q (Compiler.CompactSourceSyntax.synCpw1 D))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr P (Compiler.CompactSourceSyntax.synCsi R) Q) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCuni P) R (Compiler.CompactSourceSyntax.synCuni Q))))

Checked nominal proof certificate identified upstream as g_pw1typedbrcldv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPw1descentisomdv (z : SemanticCore.Var) (D R S : SemanticCore.Class) (g : SemanticCore.Var) (E : SemanticCore.Class) (dv_D_z : z ∉ D.fv) (dv_E_z : z ∉ E.fv) (dv_g_z : g ≠ z) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv g) (Compiler.CompactSourceSyntax.synCsi R) (Compiler.CompactSourceSyntax.synCsi S) (Compiler.CompactSourceSyntax.synCpw1 D) (Compiler.CompactSourceSyntax.synCpw1 E)).imp (Compiler.CompactSourceSyntax.synWiso (Compiler.CompactSourceSyntax.synCmpt z D (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv g) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv z))))) R S D E))

Checked nominal proof certificate identified upstream as g_pw1descentisomdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSifvalimpclndv (C D E F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf F D E) (SemanticCore.Wff.classMem C D)).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_sifvalimpclndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPw1sif1omapndv (A B F : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1o F A B).imp (Compiler.CompactSourceSyntax.synWf1o (Compiler.CompactSourceSyntax.synCsi F) (Compiler.CompactSourceSyntax.synCpw1 A) (Compiler.CompactSourceSyntax.synCpw1 B)))

Checked nominal proof certificate identified upstream as g_pw1sif1omapndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part068.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPw1raiseisomdv (D R S : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv f) R S D E).imp (Compiler.CompactSourceSyntax.synWiso (Compiler.CompactSourceSyntax.synCsi (SemanticCore.Class.cv f)) (Compiler.CompactSourceSyntax.synCsi R) (Compiler.CompactSourceSyntax.synCsi S) (Compiler.CompactSourceSyntax.synCpw1 D) (Compiler.CompactSourceSyntax.synCpw1 E)))

Checked nominal proof certificate identified upstream as g_pw1raiseisomdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHndownbrndv (x y g a b : SemanticCore.Var) (dv_a_x : a ≠ x) (dv_a_y : a ≠ y) (dv_b_x : b ≠ x) (dv_b_y : b ≠ y) (dv_g_x : g ≠ x) (dv_g_y : g ≠ y) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv a) (Compiler.CompactSourceSyntax.synCopab x y (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)) (SemanticCore.Class.cv g) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y)))) (SemanticCore.Class.cv b)) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv a)) (SemanticCore.Class.cv g) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv b))))

Checked nominal proof certificate identified upstream as g_hndownbrndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHndownexndv (x y g : SemanticCore.Var) (dv_g_x : g ≠ x) (dv_g_y : g ≠ y) (dv_x_y : x ≠ y) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopab x y (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)) (SemanticCore.Class.cv g) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y)))) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_hndownexndv.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gHndownexndv x y g dv_g_x dv_g_y dv_x_y = NFChoice.DirectNominalPrf.WPPReplay.gEnpw1lem1 x y g ⋯ ⋯ ⋯

Certificates from NominalWPPReplayChunk016Compact001Part069.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHndownmpteqdv (x y z : SemanticCore.Var) (D : SemanticCore.Class) (g : SemanticCore.Var) (E : SemanticCore.Class) (_dv_D_x : x ∉ D.fv) (_dv_D_y : y ∉ D.fv) (dv_D_z : z ∉ D.fv) (_dv_E_x : x ∉ E.fv) (_dv_E_y : y ∉ E.fv) (dv_E_z : z ∉ E.fv) (dv_g_x : g ≠ x) (dv_g_y : g ≠ y) (dv_g_z : g ≠ z) (dv_x_y : x ≠ y) (_dv_x_z : x ≠ z) (_dv_y_z : y ≠ z) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWf1o (SemanticCore.Class.cv g) (Compiler.CompactSourceSyntax.synCpw1 D) (Compiler.CompactSourceSyntax.synCpw1 E)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCopab x y (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)) (SemanticCore.Class.cv g) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y)))) (Compiler.CompactSourceSyntax.synCmpt z D (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv g) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv z)))))))

Checked nominal proof certificate identified upstream as g_hndownmpteqdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPw1isoexequivndv (D R S : SemanticCore.Class) (f g : SemanticCore.Var) (E : SemanticCore.Class) (dv_D_f : f ∉ D.fv) (dv_D_g : g ∉ D.fv) (dv_E_f : f ∉ E.fv) (dv_E_g : g ∉ E.fv) (dv_R_f : f ∉ R.fv) (dv_R_g : g ∉ R.fv) (dv_S_f : f ∉ S.fv) (dv_S_g : g ∉ S.fv) (dv_f_g : f ≠ g) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWex f (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv f) R S D E)) (Compiler.CompactSourceSyntax.synWex g (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv g) (Compiler.CompactSourceSyntax.synCsi R) (Compiler.CompactSourceSyntax.synCsi S) (Compiler.CompactSourceSyntax.synCpw1 D) (Compiler.CompactSourceSyntax.synCpw1 E))))

Checked nominal proof certificate identified upstream as g_pw1isoexequivndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part070.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwnisodirectisobndv (v u : SemanticCore.Var) (A : SemanticCore.Class) (h : SemanticCore.Var) (dv_A_h : h ∉ A.fv) (dv_h_u : h ≠ u) (dv_h_v : h ≠ v) (dv_u_v : u ≠ v) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcn A))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A) (SemanticCore.Class.cv v)) (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv h) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv v)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v))))))

Checked nominal proof certificate identified upstream as g_hwnisodirectisobndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwnisodirectisobclndv (A B C : SemanticCore.Class) (h : SemanticCore.Var) (dv_A_h : h ∉ A.fv) (dv_B_h : h ∉ B.fv) (dv_C_h : h ∉ C.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synChwcn A)) (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcn A))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr B (Compiler.CompactSourceSyntax.synChwniso A) C) (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv h) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st B) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st C) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd B) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd C)))))

Checked nominal proof certificate identified upstream as g_hwnisodirectisobclndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part071.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsicodemapkernelndv (A : SemanticCore.Class) (r q : SemanticCore.Var) (dv_A_q : q ∉ A.fv) (dv_A_r : r ∉ A.fv) (dv_q_r : q ≠ r) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn A))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn A)))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChwniso A)) (SemanticCore.Class.cv r)) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsicodemap A) (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCpw1 A)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsicodemap A) (SemanticCore.Class.cv r)))))

Checked nominal proof certificate identified upstream as g_hnsicodemapkernelndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part072.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSiorreflectndv (D R : SemanticCore.Class) (hyp_siorreflectndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_siorreflectndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsi R) Compiler.CompactSourceSyntax.synCwe (Compiler.CompactSourceSyntax.synCpw1 D)).imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCstrict D))

Checked nominal proof certificate identified upstream as g_siorreflectndv.

Equations

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