Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk010Compact001Part048.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDf1st2 : Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synC1st (Compiler.CompactSourceSyntax.synCuni1 (Compiler.CompactSourceSyntax.synCuni1 (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCxpk (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCvv) Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synCcnvk (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCsik (Compiler.CompactSourceSyntax.synCsik Compiler.CompactSourceSyntax.synCssetk))) (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCcomk Compiler.CompactSourceSyntax.synCssetk (Compiler.CompactSourceSyntax.synCsik (Compiler.CompactSourceSyntax.synCcnvk (Compiler.CompactSourceSyntax.synCimagek (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCimagek (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCins3k Compiler.CompactSourceSyntax.synCssetk) (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))) (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCins3k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCsik (Compiler.CompactSourceSyntax.synCsik Compiler.CompactSourceSyntax.synCssetk))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))) (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCnnc Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synCin Compiler.CompactSourceSyntax.synCidk (Compiler.CompactSourceSyntax.synCxpk (Compiler.CompactSourceSyntax.synCcompl Compiler.CompactSourceSyntax.synCnnc) Compiler.CompactSourceSyntax.synCvv)))))))) (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk) (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCsik (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk) (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCcomk (Compiler.CompactSourceSyntax.synCcnvk (Compiler.CompactSourceSyntax.synCimagek (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCimagek (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCins3k Compiler.CompactSourceSyntax.synCssetk) (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))) (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCins3k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCsik (Compiler.CompactSourceSyntax.synCsik Compiler.CompactSourceSyntax.synCssetk))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))) (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCnnc Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synCin Compiler.CompactSourceSyntax.synCidk (Compiler.CompactSourceSyntax.synCxpk (Compiler.CompactSourceSyntax.synCcompl Compiler.CompactSourceSyntax.synCnnc) Compiler.CompactSourceSyntax.synCvv))))) Compiler.CompactSourceSyntax.synCssetk) (Compiler.CompactSourceSyntax.synCxpk (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)) Compiler.CompactSourceSyntax.synCvv)))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))))))) (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCins3k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCcomk Compiler.CompactSourceSyntax.synCssetk (Compiler.CompactSourceSyntax.synCsik (Compiler.CompactSourceSyntax.synCcnvk (Compiler.CompactSourceSyntax.synCimagek (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCimagek (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCins3k Compiler.CompactSourceSyntax.synCssetk) (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))) (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCins3k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCsik (Compiler.CompactSourceSyntax.synCsik Compiler.CompactSourceSyntax.synCssetk))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))) (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCnnc Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synCin Compiler.CompactSourceSyntax.synCidk (Compiler.CompactSourceSyntax.synCxpk (Compiler.CompactSourceSyntax.synCcompl Compiler.CompactSourceSyntax.synCnnc) Compiler.CompactSourceSyntax.synCvv))))))))) (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCsik (Compiler.CompactSourceSyntax.synCsik (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk) (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCsik (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk) (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCcomk (Compiler.CompactSourceSyntax.synCcnvk (Compiler.CompactSourceSyntax.synCimagek (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCimagek (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCins3k Compiler.CompactSourceSyntax.synCssetk) (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))) (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCsymdif (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCins2k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCins2k (Compiler.CompactSourceSyntax.synCins3k Compiler.CompactSourceSyntax.synCssetk)) (Compiler.CompactSourceSyntax.synCins3k (Compiler.CompactSourceSyntax.synCsik (Compiler.CompactSourceSyntax.synCsik Compiler.CompactSourceSyntax.synCssetk))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))) (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCnnc Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synCin Compiler.CompactSourceSyntax.synCidk (Compiler.CompactSourceSyntax.synCxpk (Compiler.CompactSourceSyntax.synCcompl Compiler.CompactSourceSyntax.synCnnc) Compiler.CompactSourceSyntax.synCvv))))) Compiler.CompactSourceSyntax.synCssetk) (Compiler.CompactSourceSyntax.synCxpk (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)) Compiler.CompactSourceSyntax.synCvv)))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c)))))) (Compiler.CompactSourceSyntax.synCpw1 Compiler.CompactSourceSyntax.synC1c))))))

Checked nominal proof certificate identified upstream as g_df1st2.

Equations

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

Certificates from NominalWPPReplayChunk010Compact001Part049.

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

Checked nominal proof certificate identified upstream as g_n_1stex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElswap (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCswap) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv y) (SemanticCore.Class.cv x)))))))

Checked nominal proof certificate identified upstream as g_elswap.

Equations

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