Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk017Compact001Part001.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSifrreflectndv (D R : SemanticCore.Class) (hyp_sifrreflectndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_sifrreflectndv_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.synCfound D))

Checked nominal proof certificate identified upstream as g_sifrreflectndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSiwereflectndv (D R : SemanticCore.Class) (hyp_siwereflectndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_siwereflectndv_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.synCwe D))

Checked nominal proof certificate identified upstream as g_siwereflectndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHndownbrclndv (x y : SemanticCore.Var) (S : SemanticCore.Class) (a b : SemanticCore.Var) (dv_S_x : x ∉ S.fv) (dv_S_y : y ∉ S.fv) (dv_a_x : a ≠ x) (dv_a_y : a ≠ y) (dv_b_x : b ≠ x) (dv_b_y : b ≠ 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)) S (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y)))) (SemanticCore.Class.cv b)) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv a)) S (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv b))))

Checked nominal proof certificate identified upstream as g_hndownbrclndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part002.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHndownexclndv (x y : SemanticCore.Var) (S : SemanticCore.Class) (dv_S_x : x ∉ S.fv) (dv_S_y : y ∉ S.fv) (dv_x_y : x ≠ y) (hyp_hndownexclndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem S Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopab x y (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)) S (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y)))) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_hndownexclndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSidownrecoverclndv (x y : SemanticCore.Var) (D S : SemanticCore.Class) (_dv_D_x : x ∉ D.fv) (_dv_D_y : y ∉ D.fv) (dv_S_x : x ∉ S.fv) (dv_S_y : y ∉ S.fv) (dv_x_y : x ≠ y) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss S (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCpw1 D) (Compiler.CompactSourceSyntax.synCpw1 D))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synCopab x y (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)) S (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y))))) S))

Checked nominal proof certificate identified upstream as g_sidownrecoverclndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part003.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSidownsuppclndv (x y : SemanticCore.Var) (D S : SemanticCore.Class) (_dv_D_x : x ∉ D.fv) (_dv_D_y : y ∉ D.fv) (dv_S_x : x ∉ S.fv) (dv_S_y : y ∉ S.fv) (dv_x_y : x ≠ y) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss S (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCpw1 D) (Compiler.CompactSourceSyntax.synCpw1 D))).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCopab x y (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)) S (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y)))) (Compiler.CompactSourceSyntax.synCxp D D)))

Checked nominal proof certificate identified upstream as g_sidownsuppclndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPw1subunissclndv (A S : SemanticCore.Class) (hyp_pw1subunissclndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem S Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss S (Compiler.CompactSourceSyntax.synCpw1 A)).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCuni S) A))

Checked nominal proof certificate identified upstream as g_pw1subunissclndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsireversecodememndv (x y u : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_u : u ∉ A.fv) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_u_x : u ≠ x) (dv_u_y : u ≠ y) (dv_x_y : x ≠ y) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCpw1 A))).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCopab x y (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y)))) (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synChwcn A)))

Checked nominal proof certificate identified upstream as g_hnsireversecodememndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsireversecodeidndv (x y u : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_u : u ∉ A.fv) (_dv_A_x : x ∉ A.fv) (_dv_A_y : y ∉ A.fv) (dv_u_x : u ≠ x) (dv_u_y : u ≠ y) (dv_x_y : x ≠ y) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCpw1 A))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synCopab x y (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))))

Checked nominal proof certificate identified upstream as g_hnsireversecodeidndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part004.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSieqdndv (ph : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_sieqdndv_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCsi A) (Compiler.CompactSourceSyntax.synCsi B)))

Checked nominal proof certificate identified upstream as g_sieqdndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsicodemapvalclndv (A Q : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem Q (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChwcn A))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsicodemap A) Q) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (Compiler.CompactSourceSyntax.synCuni Q))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (Compiler.CompactSourceSyntax.synCuni Q))))))

Checked nominal proof certificate identified upstream as g_hnsicodemapvalclndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsicodemapfondv (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfo (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_hnsicodemapfondv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSiinjndv (ph : SemanticCore.Wff) (R S : SemanticCore.Class) (hyp_siinjndv_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCsi R) (Compiler.CompactSourceSyntax.synCsi S)))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq R S))

Checked nominal proof certificate identified upstream as g_siinjndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwcnpairclndv (A B : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synChwcn A)).imp (SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st B) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd B))))

Checked nominal proof certificate identified upstream as g_hwcnpairclndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part005.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsicodemapf1ndv (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1 (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_hnsicodemapf1ndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsicodemapf1ondv (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1o (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_hnsicodemapf1ondv.

Equations

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

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

Checked nominal proof certificate identified upstream as g_hnsiquomapexgndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsiquomapfnndv (A : SemanticCore.Class) (hyp_hnsiquomapfnndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synChnsiquomap A) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChnord A)))

Checked nominal proof certificate identified upstream as g_hnsiquomapfnndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsiquomapvalndv (A : SemanticCore.Class) (q : SemanticCore.Var) (dv_A_q : q ∉ A.fv) (hyp_hnsiquomapvalndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChnord A))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsiquomap A) (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synChnsicodemap A) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q))))))

Checked nominal proof certificate identified upstream as g_hnsiquomapvalndv.

Equations

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