Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk017Compact001Part091.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbwpphwcncarrierinjndv (C : SemanticCore.Class) (k : SemanticCore.Var) (X : SemanticCore.Class) (dv_C_k : k ∉ C.fv) (dv_X_k : k ∉ X.fv) (hyp_cfbwpphwcncarrierinjndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCvv)) (hyp_cfbwpphwcncarrierinjndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCpw X)))) (hyp_cfbwpphwcncarrierinjndv_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synChncard (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCxpk X X) Compiler.CompactSourceSyntax.synCnnc)) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard X))))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWwpp.imp (Compiler.CompactSourceSyntax.synWex k (Compiler.CompactSourceSyntax.synWf1 (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd C)))) (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synChnord X))))))

Checked nominal proof certificate identified upstream as g_cfbwpphwcncarrierinjndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhnpw13genericraisedcodendv (C X : SemanticCore.Class) (_hyp_cfbhnpw13genericraisedcodendv_1 : Nominal.NPrf (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCvv)) (hyp_cfbhnpw13genericraisedcodendv_2 : Nominal.NPrf (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCpw X)))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsicodemap (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw X)))) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsicodemap (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw X))) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsicodemap (Compiler.CompactSourceSyntax.synCpw X)) (Compiler.CompactSourceSyntax.synCsn C)))))) (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw X)))))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsicodemap (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw X)))) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsicodemap (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw X))) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsicodemap (Compiler.CompactSourceSyntax.synCpw X)) (Compiler.CompactSourceSyntax.synCsn C))))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd C))))))

Checked nominal proof certificate identified upstream as g_cfbhnpw13genericraisedcodendv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part092.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhnpw13genericquotrepcohndv (C Q X : SemanticCore.Class) (hyp_cfbhnpw13genericquotrepcohndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCvv)) (hyp_cfbhnpw13genericquotrepcohndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCpw X)))) (hyp_cfbhnpw13genericquotrepcohndv_3 : Nominal.NPrf (SemanticCore.Wff.classMem Q (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCpw X))))))) (hyp_cfbhnpw13genericquotrepcohndv_4 : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni Q))) (Compiler.CompactSourceSyntax.synCec C (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCpw X))))) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnsiquomap (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw X)))) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChnsiquomap (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw X)))) (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChnsiquomap (Compiler.CompactSourceSyntax.synCpw X)))))) Q) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsicodemap (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw X)))) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsicodemap (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw X))) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synChnsicodemap (Compiler.CompactSourceSyntax.synCpw X)) (Compiler.CompactSourceSyntax.synCsn C)))))) (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw X)))))))

Checked nominal proof certificate identified upstream as g_cfbhnpw13genericquotrepcohndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part093.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhnpw13genericcodepointcoverndv (C Q X : SemanticCore.Class) (hyp_cfbhnpw13genericcodepointcoverndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCvv)) (hyp_cfbhnpw13genericcodepointcoverndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcn (Compiler.CompactSourceSyntax.synCpw X)))) (hyp_cfbhnpw13genericcodepointcoverndv_3 : Nominal.NPrf (SemanticCore.Wff.classMem Q (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCpw X))))))) (hyp_cfbhnpw13genericcodepointcoverndv_4 : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni Q))) (Compiler.CompactSourceSyntax.synCec C (Compiler.CompactSourceSyntax.synChwniso (Compiler.CompactSourceSyntax.synCpw X))))) (hyp_cfbhnpw13genericcodepointcoverndv_5 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synChncard (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCxpk X X) Compiler.CompactSourceSyntax.synCnnc)) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard X))))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWwpp.imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqinc (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw X)))) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw X)))) (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synChnord X))))) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnsiquomap (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw X)))) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChnsiquomap (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw X)))) (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChnsiquomap (Compiler.CompactSourceSyntax.synCpw X))))))) Q) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synChnqinc (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synChnord X))) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw X)))) (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synChnord X))))))))

Checked nominal proof certificate identified upstream as g_cfbhnpw13genericcodepointcoverndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part094.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbhnpw13pointcoverndv (X : SemanticCore.Class) (q : SemanticCore.Var) (hyp_cfbhnpw13pointcoverndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCvv)) (hyp_cfbhnpw13pointcoverndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synChncard (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCxpk X X) Compiler.CompactSourceSyntax.synCnnc)) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard X))))) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCpw X)))))).imp (Compiler.CompactSourceSyntax.synWwpp.imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqinc (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw X)))) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw X)))) (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synChnord X))))) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnsiquomap (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw X)))) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChnsiquomap (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw X)))) (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChnsiquomap (Compiler.CompactSourceSyntax.synCpw X))))))) (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synChnqinc (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synChnord X))) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw X)))) (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synChnord X)))))))))

Checked nominal proof certificate identified upstream as g_cfbhnpw13pointcoverndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part095.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbwppfixedblockhnqimagecoverndv (X : SemanticCore.Class) (hyp_cfbwppfixedblockhnqimagecoverndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCvv)) (hyp_cfbwppfixedblockhnqimagecoverndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synChncard (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCxpk X X) Compiler.CompactSourceSyntax.synCnnc)) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard X))))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWwpp.imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqinc (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw X)))) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw X)))) (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synChnord X))))) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnsiquomap (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw X)))) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChnsiquomap (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw X)))) (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChnsiquomap (Compiler.CompactSourceSyntax.synCpw X))))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCpw X)))))) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synChnqinc (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synChnord X))) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw X)))) (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synChnord X))))))))

Checked nominal proof certificate identified upstream as g_cfbwppfixedblockhnqimagecoverndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCfbwppfixedblockhnqgraphinjndv (X : SemanticCore.Class) (hyp_cfbwppfixedblockhnqgraphinjndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCvv)) (hyp_cfbwppfixedblockhnqgraphinjndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synChncard (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCxpk X X) Compiler.CompactSourceSyntax.synCnnc)) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard X))))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWwpp.imp (Compiler.CompactSourceSyntax.synWf1 (Compiler.CompactSourceSyntax.synCres (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synChnqinc (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synChnord X))) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw X)))) (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synChnord X)))))) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnqinc (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw X)))) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw X)))) (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synChnord X))))) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synChnsiquomap (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw X)))) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChnsiquomap (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw X)))) (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synCsi (Compiler.CompactSourceSyntax.synChnsiquomap (Compiler.CompactSourceSyntax.synCpw X)))))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCpw X)))))) (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCpw X))))) (Compiler.CompactSourceSyntax.synChnord (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synChnord X))))))

Checked nominal proof certificate identified upstream as g_cfbwppfixedblockhnqgraphinjndv.

Equations

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