Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk017Compact001Part080.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutambfactorranbrimpndv (x z u : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_u : u ∉ A.fv) (dv_A_x : x ∉ A.fv) (dv_u_x : u ≠ x) (dv_x_z : x ≠ z) (hyp_hnwcutambfactorranbrimpndv_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.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv z) (Compiler.CompactSourceSyntax.synCrn (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.synWrex x (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) (SemanticCore.Wff.classEq (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)) (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synChwniso A)) (SemanticCore.Class.cv z)))))

Checked nominal proof certificate identified upstream as g_hnwcutambfactorranbrimpndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part081.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutambstrictsegranimpndv (u : SemanticCore.Var) (A : SemanticCore.Class) (r : SemanticCore.Var) (dv_A_r : r ∉ A.fv) (dv_A_u : u ∉ A.fv) (_dv_r_u : r ≠ u) (hyp_hnwcutstrictsegimp_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)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn (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.synCin (Compiler.CompactSourceSyntax.synChnord A) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synClnqord (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synChwcn A)) Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A)))))))

Checked nominal proof certificate identified upstream as g_hnwcutambstrictsegranimpndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part082.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutambstrictsegresisomralias0ndv (u : SemanticCore.Var) (A : SemanticCore.Class) (r : SemanticCore.Var) (dv_A_r : r ∉ A.fv) (dv_A_u : u ∉ A.fv) (dv_r_u : r ≠ u) (hyp_hnwcutambstrictsegresisomralias0ndv_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)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A))).imp (Compiler.CompactSourceSyntax.synWiso (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.synCsi (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synClnqord (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synChwcn A)) (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synChnord A) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synClnqord (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synChwcn A)) Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A))))) (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synChnord A) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synClnqord (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synChwcn A)) Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A))))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synChnord A) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synClnqord (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synChwcn A)) Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A)))))))

Checked nominal proof certificate identified upstream as g_hnwcutambstrictsegresisomralias0ndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHnwcutambstrictsegresisomraliasdndv (u : SemanticCore.Var) (A : SemanticCore.Class) (r : SemanticCore.Var) (dv_A_r : r ∉ A.fv) (dv_A_u : u ∉ A.fv) (dv_r_u : r ≠ u) (hyp_hnwcutambstrictsegresisomraliasdndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synChncodecmpset A)).imp ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)).imp (Compiler.CompactSourceSyntax.synWiso (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.synCsi (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synClnqord (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synChwcn A)) (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synChnord A) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synClnqord (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synChwcn A)) Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A))))) (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synChnord A) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synClnqord (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synChwcn A)) Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A))))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synChnord A) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synClnqord (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synChwcn A)) Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A))))))))

Checked nominal proof certificate identified upstream as g_hnwcutambstrictsegresisomraliasdndv.

Equations

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