Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk014Compact001Part041.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwnisodm (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synChwniso A)) (Compiler.CompactSourceSyntax.synChwcn A))

Checked nominal proof certificate identified upstream as g_hwnisodm.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwnisoclasseqb (v u : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv) (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 (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A)) (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synChwniso A))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwniso A) (SemanticCore.Class.cv v))))

Checked nominal proof certificate identified upstream as g_hwnisoclasseqb.

Equations

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

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

Checked nominal proof certificate identified upstream as g_hnordexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncardex (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChncard A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_hncardex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncardnc (A : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synChncard A) Compiler.CompactSourceSyntax.synCncs))

Checked nominal proof certificate identified upstream as g_hncardnc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncardtc (A : SemanticCore.Class) (hyp_hncardtc_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard A)) (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChnord A))))

Checked nominal proof certificate identified upstream as g_hncardtc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHncardtc2 (A : SemanticCore.Class) (hyp_hncardtc2_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synChncard A))) (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synChnord A)))))

Checked nominal proof certificate identified upstream as g_hncardtc2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwcnbase (u : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_u : u ∉ A.fv) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synChwcn A)).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)) A))

Checked nominal proof certificate identified upstream as g_hwcnbase.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElhwbases (u : SemanticCore.Var) (A D : SemanticCore.Class) (_dv_A_D : Disjoint A.fv D.fv) (dv_A_u : u ∉ A.fv) (dv_D_u : u ∉ D.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synChwbases A)) (Compiler.CompactSourceSyntax.synWrex u (Compiler.CompactSourceSyntax.synChwcn A) (SemanticCore.Wff.classEq D (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (SemanticCore.Class.cv u)))))

Checked nominal proof certificate identified upstream as g_elhwbases.

Equations

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

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

Checked nominal proof certificate identified upstream as g_hwcardsexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElhwcards (A K : SemanticCore.Class) (d : SemanticCore.Var) (_dv_A_K : Disjoint A.fv K.fv) (dv_A_d : d ∉ A.fv) (dv_K_d : d ∉ K.fv) (hyp_elhwcards_1 : Nominal.NPrf (SemanticCore.Wff.classMem K Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem K (Compiler.CompactSourceSyntax.synChwcards A)) (Compiler.CompactSourceSyntax.synWrex d (Compiler.CompactSourceSyntax.synChwbases A) (SemanticCore.Wff.classEq K (Compiler.CompactSourceSyntax.synCnc (SemanticCore.Class.cv d)))))

Checked nominal proof certificate identified upstream as g_elhwcards.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwcardssnc (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synChwcards A) Compiler.CompactSourceSyntax.synCncs)

Checked nominal proof certificate identified upstream as g_hwcardssnc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFrrd (ph : SemanticCore.Wff) (x y z : SemanticCore.Var) (B S : SemanticCore.Class) (dv_B_x : x ∉ B.fv) (_dv_B_y : y ∉ B.fv) (_dv_B_z : z ∉ B.fv) (dv_S_x : x ∉ S.fv) (dv_S_y : y ∉ S.fv) (dv_S_z : z ∉ S.fv) (dv_ph_x : x ∉ ph.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_frrd_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem S Compiler.CompactSourceSyntax.synCvv))) (hyp_frrd_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv))) (hyp_frrd_3 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss (SemanticCore.Class.cv x) B) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC0))).imp (Compiler.CompactSourceSyntax.synWrex z (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synWral y (SemanticCore.Class.cv x) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv y) S (SemanticCore.Class.cv z)).imp (SemanticCore.Wff.objEq y z)))))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCfound B))

Checked nominal proof certificate identified upstream as g_frrd.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part042.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwnisohwisocl (A B C : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)).imp ((Compiler.CompactSourceSyntax.synWbr B (Compiler.CompactSourceSyntax.synChwniso A) C).imp (Compiler.CompactSourceSyntax.synWbr B (Compiler.CompactSourceSyntax.synChwiso A) C)))

Checked nominal proof certificate identified upstream as g_hwnisohwisocl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwisowitnesscl (A B C : SemanticCore.Class) (h : SemanticCore.Var) (dv_A_h : h ∉ A.fv) (dv_B_h : h ∉ B.fv) (dv_C_h : h ∉ C.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)).imp ((Compiler.CompactSourceSyntax.synWbr B (Compiler.CompactSourceSyntax.synChwiso A) C).imp (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv h) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st B) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st C) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd B) (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd C)))))

Checked nominal proof certificate identified upstream as g_hwisowitnesscl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOpfvscl (B C : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC1st (Compiler.CompactSourceSyntax.synCop B C)) B) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv Compiler.CompactSourceSyntax.synC2nd (Compiler.CompactSourceSyntax.synCop B C)) C)))

Checked nominal proof certificate identified upstream as g_opfvscl.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part043.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWerestr (ph : SemanticCore.Wff) (A B R : SemanticCore.Class) (_dv_A_R : Disjoint A.fv R.fv) (hyp_werestr_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A))) (hyp_werestr_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss B A))) (hyp_werestr_3 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp B B)) Compiler.CompactSourceSyntax.synCwe B))

Checked nominal proof certificate identified upstream as g_werestr.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part044.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWerestrndv (ph : SemanticCore.Wff) (B D S : SemanticCore.Class) (hyp_werestrndv_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe D))) (hyp_werestrndv_2 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWss B D))) (hyp_werestrndv_3 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCin S (Compiler.CompactSourceSyntax.synCxp B B)) Compiler.CompactSourceSyntax.synCwe B))

Checked nominal proof certificate identified upstream as g_werestrndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWestrseg (x : SemanticCore.Var) (D R : SemanticCore.Class) (dv_D_R : Disjoint D.fv R.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) D)).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))))) Compiler.CompactSourceSyntax.synCwe (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))))))

Checked nominal proof certificate identified upstream as g_westrseg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWestrsegndv (x : SemanticCore.Var) (D S : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe D) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) D)).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCin S (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))))) Compiler.CompactSourceSyntax.synCwe (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))))))

Checked nominal proof certificate identified upstream as g_westrsegndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gStrictsegnel (x : SemanticCore.Var) (D R : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))))).neg

Checked nominal proof certificate identified upstream as g_strictsegnel.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part045.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElstrictseg (x y : SemanticCore.Var) (D R : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) D) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv y) R (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv y) (SemanticCore.Class.cv x)))))

Checked nominal proof certificate identified upstream as g_elstrictseg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gStrictsegdown (x y z : SemanticCore.Var) (D R : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) D)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv z) D)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv z) R (SemanticCore.Class.cv y))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv z) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))))))

Checked nominal proof certificate identified upstream as g_strictsegdown.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part046.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gStrictsegnoiso (x : SemanticCore.Var) (D R H : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) D)) (SemanticCore.Wff.classMem H Compiler.CompactSourceSyntax.synCvv)).imp (Compiler.CompactSourceSyntax.synWiso H R (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))))) D (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))))).neg)

Checked nominal proof certificate identified upstream as g_strictsegnoiso.

Equations

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