More theorems on terminal categories (#5066)

* [add] eufunc; [propose] euendfunc

* [minimize]

* [add] euendfunc2

* [shorten]

* [split] precoffunc

* [add] basresprsfo

* [add] unfinished df-termc description

* [propose] termcnex

* [minimize]

* [add] posnex, prsnex, termcnex

* [minimize] discsntermlem

* [shorten] termc2

* [propose] dftermc3; [fix] descriptions

* [prove] dftermc3

* [minimize]

* [add] diag1f1o

* [minimize]

* [add] diag2f1

* [revise] fnsnbt, termcfuncval; [add] diag2f1o

* [move] fnsnbt to main as fnsnbg; [shorten] fnsnb; [fix] format

* [add] diagcic

* [minimize]

* [revise] precofval3

* [move] slotresfo fonex

* [temp] remove unfinished part

* [fix] description for termc2

* [add] revision reason

* [bugfix] incorrect merge conflict resolve...

* [remove] duplicate revise in description

---------

Co-authored-by: Wolf Lammen <[email protected]>

Author: zwang123

changes-set.txt

@@ -93,6 +93,9 @@ make a github issue.)
 DONE:
 Date      Old       New         Notes
 27-Oct-25 cringmul32d crng32d   moved from TA's mathbox to main set.mm
+21-Oct-25 fnsnbt    fnsnbg      Moved from SN's mathbox to main set.mm and
+                                _V to V and renamed to match other sn theorems
+                                such as xpsng
 19-Oct-25 ralin     [same]      moved from PM's mathbox to main set.mm
 17-Oct-25 decexp2   ---         deleted - unused
 16-Oct-25 ringdid   [same]      Moved from TA's mathbox to main set.mm

discouraged

@@ -16807,6 +16807,7 @@ New usage of "flddivrng" is discouraged (2 uses).
 New usage of "fldhmsubcALTV" is discouraged (0 uses).
 New usage of "fldidomOLD" is discouraged (0 uses).
 New usage of "fnexALT" is discouraged (0 uses).
+New usage of "fnsnbOLD" is discouraged (0 uses).
 New usage of "fodomfiOLD" is discouraged (0 uses).
 New usage of "fodomfibOLD" is discouraged (0 uses).
 New usage of "footexALT" is discouraged (0 uses).
@@ -20653,6 +20654,7 @@ Proof modification of "findcard3OLD" is discouraged (488 steps).
 Proof modification of "fineqvacALT" is discouraged (40 steps).
 Proof modification of "fldidomOLD" is discouraged (34 steps).
 Proof modification of "fnexALT" is discouraged (111 steps).
+Proof modification of "fnsnbOLD" is discouraged (110 steps).
 Proof modification of "fodomfiOLD" is discouraged (388 steps).
 Proof modification of "fodomfibOLD" is discouraged (183 steps).
 Proof modification of "footexALT" is discouraged (2161 steps).