Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk010Compact001Part058.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfsi2 (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCsi A) (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.synCsik (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCxpk Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synCvv)) (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.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 A))))))))

Checked nominal proof certificate identified upstream as g_dfsi2.

Equations

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

Certificates from NominalWPPReplayChunk010Compact001Part059.

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

Checked nominal proof certificate identified upstream as g_siexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSiex (A : SemanticCore.Class) (hyp_siex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsi A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_siex.

Equations

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