Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk017Compact001Part074.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnsicodemap2valclndv (v : SemanticCore.Var) (A : SemanticCore.Class) (_dv_A_v : v ∉ A.fv) (_hyp_hnsicodemap2valclndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwcn A)).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsicodemap (Compiler.CompactSourceSyntax.synCpw1 A)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsicodemap A) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv v))))) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv v)))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv v)))))) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsicodemap (Compiler.CompactSourceSyntax.synCpw1 A)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsicodemap A) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv v))))) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 A))))))

Checked nominal proof certificate identified upstream as g_hnsicodemap2valclndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part075.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodepw12repdndv (v u : SemanticCore.Var) (A : SemanticCore.Class) (_dv_A_u : u ∉ A.fv) (dv_A_v : v ∉ A.fv) (dv_u_v : u ≠ v) (hyp_hncodepw12repdndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 A)))).imp (Compiler.CompactSourceSyntax.synWrex v (Compiler.CompactSourceSyntax.synChwcn A) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 A))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsicodemap (Compiler.CompactSourceSyntax.synCpw1 A)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsicodemap A) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv v))))))))

Checked nominal proof certificate identified upstream as g_hncodepw12repdndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part076.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodecmpquotbrproxyimpndv (v u : SemanticCore.Var) (A : SemanticCore.Class) (r : SemanticCore.Var) (dv_A_r : r ∉ A.fv) (_dv_A_u : u ∉ A.fv) (_dv_A_v : v ∉ A.fv) (hyp_hncodecmpquotbrproxyimpndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synChncodecmpset A)) (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 (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A)) (Compiler.CompactSourceSyntax.synClnqord (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synChwcn A)) (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwniso A))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChncodecmpset A) (SemanticCore.Class.cv v))))

Checked nominal proof certificate identified upstream as g_hncodecmpquotbrproxyimpndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodecmpquotbrproxyimpclndv (A B C : SemanticCore.Class) (r : SemanticCore.Var) (dv_A_r : r ∉ A.fv) (hyp_hncodecmpquotbrproxyimpclndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synChncodecmpset A)) (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 (Compiler.CompactSourceSyntax.synCec B (Compiler.CompactSourceSyntax.synChwniso A)) (Compiler.CompactSourceSyntax.synClnqord (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synChwcn A)) (Compiler.CompactSourceSyntax.synCec C (Compiler.CompactSourceSyntax.synChwniso A))) (Compiler.CompactSourceSyntax.synWbr B (Compiler.CompactSourceSyntax.synChncodecmpset A) C)))

Checked nominal proof certificate identified upstream as g_hncodecmpquotbrproxyimpclndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncodecmpquotstrictbrproxyimpclndv (A B C : SemanticCore.Class) (r : SemanticCore.Var) (dv_A_r : r ∉ A.fv) (hyp_hncodecmpquotstrictbrproxyimpclndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synChncodecmpset A)) (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 (Compiler.CompactSourceSyntax.synCec B (Compiler.CompactSourceSyntax.synChwniso A)) (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synClnqord (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synChwcn A)) Compiler.CompactSourceSyntax.synCid) (Compiler.CompactSourceSyntax.synCec C (Compiler.CompactSourceSyntax.synChwniso A))) (Compiler.CompactSourceSyntax.synWbr B (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synChncodecmpset A) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChncodecmpset A))) C)))

Checked nominal proof certificate identified upstream as g_hncodecmpquotstrictbrproxyimpclndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutrelambfnnoarndv (A D R : SemanticCore.Class) (hyp_hnwcutrelambfnnoarndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss D A)) (hyp_hnwcutrelambfnnoarndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf (Compiler.CompactSourceSyntax.synChnwcutrel R D) (Compiler.CompactSourceSyntax.synCpw1 D) (Compiler.CompactSourceSyntax.synChwcn A))

Checked nominal proof certificate identified upstream as g_hnwcutrelambfnnoarndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutambfactorvalnoarndv (A D R : SemanticCore.Class) (q : SemanticCore.Var) (_dv_D_q : q ∉ D.fv) (_dv_R_q : q ∉ R.fv) (hyp_hnwcutambfactorvalnoarndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss D A)) (hyp_hnwcutambfactorvalnoarndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (hyp_hnwcutambfactorvalnoarndv_3 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 A) (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChnwcutrel R D))) (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synChnwcutcode R D (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q)))) (Compiler.CompactSourceSyntax.synChwniso A))))

Checked nominal proof certificate identified upstream as g_hnwcutambfactorvalnoarndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutambfactorvalcodendv (A B : SemanticCore.Class) (q : SemanticCore.Var) (dv_B_q : q ∉ B.fv) (hyp_hnwcutambfactorvalcodendv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_hnwcutambfactorvalcodendv_2 : Nominal.NPrf (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synChwcn A))) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd B)))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 A) (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChnwcutrel (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st B) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd B)))) (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synChnwcutcode (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st B) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd B) (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q)))) (Compiler.CompactSourceSyntax.synChwniso A))))

Checked nominal proof certificate identified upstream as g_hnwcutambfactorvalcodendv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcuttxpeq1dndv (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_hnwcuttxpeq1dndv_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtxp A C) (Compiler.CompactSourceSyntax.synCtxp B C)))

Checked nominal proof certificate identified upstream as g_hnwcuttxpeq1dndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutimageeqdndv (ph : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_hnwcutimageeqdndv_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCimage A) (Compiler.CompactSourceSyntax.synCimage B)))

Checked nominal proof certificate identified upstream as g_hnwcutimageeqdndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part077.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutreleq12dndv (ph : SemanticCore.Wff) (D R S E : SemanticCore.Class) (hyp_hnwcutreleq12dndv_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq R S))) (hyp_hnwcutreleq12dndv_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq D E))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synChnwcutrel R D) (Compiler.CompactSourceSyntax.synChnwcutrel S E)))

Checked nominal proof certificate identified upstream as g_hnwcutreleq12dndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutcodeeq12clndv (C D R S E : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv).imp ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq R S) (SemanticCore.Wff.classEq D E)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synChnwcutcode R D C) (Compiler.CompactSourceSyntax.synChnwcutcode S E C))))

Checked nominal proof certificate identified upstream as g_hnwcutcodeeq12clndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutambfactorvalimpclndv (A B : SemanticCore.Class) (q : SemanticCore.Var) (dv_A_q : q ∉ A.fv) (dv_B_q : q ∉ B.fv) (hyp_hnwcutambfactorvalimpclndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synChwcn A)).imp ((SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd B)))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 A) (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChnwcutrel (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st B) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd B)))) (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synChnwcutcode (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st B) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd B) (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q)))) (Compiler.CompactSourceSyntax.synChwniso A)))))

Checked nominal proof certificate identified upstream as g_hnwcutambfactorvalimpclndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutambfactorvalimpndv (u : SemanticCore.Var) (A : SemanticCore.Class) (q : SemanticCore.Var) (dv_A_q : q ∉ A.fv) (_dv_A_u : u ∉ A.fv) (dv_q_u : q ≠ u) (hyp_hnwcutambfactorvalimpndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)).imp ((SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 A) (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChnwcutrel (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synChnwcutcode (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q)))) (Compiler.CompactSourceSyntax.synChwniso A)))))

Checked nominal proof certificate identified upstream as g_hnwcutambfactorvalimpndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part078.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutambordbrproxyimpndv (u : SemanticCore.Var) (A : SemanticCore.Class) (r q p : SemanticCore.Var) (dv_A_p : p ∉ A.fv) (dv_A_q : q ∉ A.fv) (dv_A_r : r ∉ A.fv) (dv_A_u : u ∉ A.fv) (_dv_p_q : p ≠ q) (_dv_p_r : p ≠ r) (dv_p_u : p ≠ u) (_dv_q_r : q ≠ r) (dv_q_u : q ≠ u) (_dv_r_u : r ≠ u) (hyp_hnwcutambordbrproxyimpndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synChncodecmpset A)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv p) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv p) (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)))) (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 A) (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChnwcutrel (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv p)) (Compiler.CompactSourceSyntax.synClnqord (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synChwcn A)) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 A) (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChnwcutrel (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (SemanticCore.Class.cv q)))))

Checked nominal proof certificate identified upstream as g_hnwcutambordbrproxyimpndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutambfactorfnnoarndv (A D R : SemanticCore.Class) (hyp_hnwcutambfactorfnnoarndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss D A)) (hyp_hnwcutambfactorfnnoarndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (hyp_hnwcutambfactorfnnoarndv_3 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 A) (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChnwcutrel R D))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)) (Compiler.CompactSourceSyntax.synChnord A))

Checked nominal proof certificate identified upstream as g_hnwcutambfactorfnnoarndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutclassinjambnoarndv (A B C D R : SemanticCore.Class) (hyp_hnwcutclassinjambnoarndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss D A)) (hyp_hnwcutclassinjambnoarndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (hyp_hnwcutclassinjambnoarndv_3 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem B D) (SemanticCore.Wff.classMem C D)).imp ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synChnwcutcode R D B) (Compiler.CompactSourceSyntax.synChwniso A)) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synChnwcutcode R D C) (Compiler.CompactSourceSyntax.synChwniso A))).imp (SemanticCore.Wff.classEq B C)))

Checked nominal proof certificate identified upstream as g_hnwcutclassinjambnoarndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part079.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutambfactorf1noarndv (A D R : SemanticCore.Class) (hyp_hnwcutambfactorf1noarndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss D A)) (hyp_hnwcutambfactorf1noarndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (hyp_hnwcutambfactorf1noarndv_3 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1 (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 A) (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChnwcutrel R D))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)) (Compiler.CompactSourceSyntax.synChnord A))

Checked nominal proof certificate identified upstream as g_hnwcutambfactorf1noarndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutambfactorf1codendv (A B : SemanticCore.Class) (hyp_hnwcutambfactorf1codendv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_hnwcutambfactorf1codendv_2 : Nominal.NPrf (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synChwcn A))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWf1 (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 A) (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChnwcutrel (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st B) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd B)))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd B))) (Compiler.CompactSourceSyntax.synChnord A))

Checked nominal proof certificate identified upstream as g_hnwcutambfactorf1codendv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutambfactorf1impclndv (A B : SemanticCore.Class) (hyp_hnwcutambfactorf1impclndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synChwcn A)).imp (Compiler.CompactSourceSyntax.synWf1 (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 A) (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChnwcutrel (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st B) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd B)))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd B))) (Compiler.CompactSourceSyntax.synChnord A)))

Checked nominal proof certificate identified upstream as g_hnwcutambfactorf1impclndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutambfactorf1impndv (u : SemanticCore.Var) (A : SemanticCore.Class) (_dv_A_u : u ∉ A.fv) (hyp_hnwcutambfactorf1impndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)).imp (Compiler.CompactSourceSyntax.synWf1 (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqmap1 A) (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChnwcutrel (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synChnord A)))

Checked nominal proof certificate identified upstream as g_hnwcutambfactorf1impndv.

Equations

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