Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Move 'monoid of endomorphisms' subsection from my mathbox to Main. #4249

Open
wants to merge 1 commit into
base: develop
Choose a base branch
from
Open

Move 'monoid of endomorphisms' subsection from my mathbox to Main. #4249

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions discouraged
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16168,6 +16168,9 @@ New usage of "funop" is discouraged (2 uses).
New usage of "funopg" is discouraged (0 uses).
New usage of "funopsn" is discouraged (2 uses).
New usage of "fvimacnvALT" is discouraged (0 uses).
New usage of "fvpr1OLD" is discouraged (0 uses).
New usage of "fvpr2OLD" is discouraged (0 uses).
New usage of "fvpr2gOLD" is discouraged (0 uses).
New usage of "fvprcALT" is discouraged (0 uses).
New usage of "gcdabsOLD" is discouraged (0 uses).
New usage of "gcdmultipleOLD" is discouraged (0 uses).
Expand Down Expand Up @@ -19792,6 +19795,9 @@ Proof modification of "funcrngcsetcALT" is discouraged (765 steps).
Proof modification of "fundcmpsurinjALT" is discouraged (221 steps).
Proof modification of "fvilbdRP" is discouraged (27 steps).
Proof modification of "fvimacnvALT" is discouraged (102 steps).
Proof modification of "fvpr1OLD" is discouraged (56 steps).
Proof modification of "fvpr2OLD" is discouraged (44 steps).
Proof modification of "fvpr2gOLD" is discouraged (75 steps).
Proof modification of "fvprcALT" is discouraged (26 steps).
Proof modification of "gcdabsOLD" is discouraged (170 steps).
Proof modification of "gcdmultipleOLD" is discouraged (348 steps).
Expand Down
220 changes: 122 additions & 98 deletions set.mm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -66040,7 +66040,7 @@ pairs as classes (in set.mm, the Kuratowski encoding). A more
$( Recover the original function from a point-added function. (Contributed
by Stefan O'Rear, 28-Feb-2015.) $)
fsnunres $p |- ( ( F Fn S /\ -. X e. S ) ->
( ( F u. { <. X , Y >. } ) |` S ) = F ) $=
( ( F u. { <. X , Y >. } ) |` S ) = F ) $=
( wfn wcel wn wa cres cop csn cun c0 fnresdm adantr ressnop0 adantl uneq12d
wceq resundir un0 eqcomi 3eqtr4g ) BAEZCAFGZHZBAIZCDJKZAIZLBMLZBUHLAIBUFUGB
UIMUDUGBSUEABNOUEUIMSUDCDAPQRBUHATUJBBUAUBUC $.
Expand All @@ -66056,12 +66056,46 @@ pairs as classes (in set.mm, the Kuratowski encoding). A more
AKLHZMAUGUJIJZULMZAUIUKUMULUFUKUMNZUHUFAOUOAPABQRSTUFAUGUAUHAUNNAUBUGABUCUD
UE $.

$( The value of a function with a domain of (at most) two elements.
(Contributed by Alexander van der Vekens, 3-Dec-2017.) $)
fvpr1g $p |- ( ( A e. V /\ C e. W /\ A =/= B )
-> ( { <. A , C >. , <. B , D >. } ` A ) = C ) $=
( wcel wne w3a cop cpr cfv csn wceq cun df-pr fveq1i necom fvunsn sylbi
syl5eq 3ad2ant3 fvsng 3adant3 eqtrd ) AEGZCFGZABHZIAACJZBDJZKZLZAUIMZLZCUHU
FULUNNUGUHULAUMUJMOZLZUNAUKUOUIUJPQUHBAHUPUNNABRUMBDASTUAUBUFUGUNCNUHACEFUC
UDUE $.

$( The value of a function with a domain of (at most) two elements.
(Contributed by Alexander van der Vekens, 3-Dec-2017.) (Proof shortened
by BJ, 26-Sep-2024.) $)
fvpr2g $p |- ( ( B e. V /\ D e. W /\ A =/= B )
-> ( { <. A , C >. , <. B , D >. } ` B ) = D ) $=
( wcel wne w3a cop cpr cfv prcom fveq1i wceq necom fvpr1g syl3an3b syl5eq )
BEGZDFGZABHZIBACJZBDJZKZLBUDUCKZLZDBUEUFUCUDMNUBTUABAHUGDOABPBADCEFQRS $.

$( Obsolete version of ~ fvpr2g as of 26-Sep-2024. (Contributed by Alexander
van der Vekens, 3-Dec-2017.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
fvpr2gOLD $p |- ( ( B e. V /\ D e. W /\ A =/= B )
-> ( { <. A , C >. , <. B , D >. } ` B ) = D ) $=
( wcel wne w3a cop cpr cfv csn wceq cun prcom df-pr eqtri fveq1i fvunsn
syl5eq 3ad2ant3 fvsng 3adant3 eqtrd ) BEGZDFGZABHZIBACJZBDJZKZLZBUJMZLZDUHU
FULUNNUGUHULBUMUIMOZLUNBUKUOUKUJUIKUOUIUJPUJUIQRSUMACBTUAUBUFUGUNDNUHBDEFUC
UDUE $.

${
fvpr1.1 $e |- A e. _V $.
fvpr1.2 $e |- C e. _V $.
$( The value of a function with a domain of two elements. (Contributed by
Jeff Madsen, 20-Jun-2010.) $)
Jeff Madsen, 20-Jun-2010.) (Proof shortened by BJ, 26-Sep-2024.) $)
fvpr1 $p |- ( A =/= B -> ( { <. A , C >. , <. B , D >. } ` A ) = C ) $=
( cvv wcel wne cop cpr cfv wceq fvpr1g mp3an12 ) AGHCGHABIAACJBDJKLCMEFAB
CDGGNO $.

$( Obsolete version of ~ fvpr1 as of 26-Sep-2024. (Contributed by Jeff
Madsen, 20-Jun-2010.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
fvpr1OLD $p |- ( A =/= B -> ( { <. A , C >. , <. B , D >. } ` A ) = C ) $=
( wne cop cpr cfv csn df-pr fveq1i wceq necom fvunsn sylbi syl5eq fvsn
cun eqtrdi ) ABGZAACHZBDHZIZJZAUCKZJZCUBUFAUGUDKTZJZUHAUEUIUCUDLMUBBAGUJU
HNABOUGBDAPQRACEFSUA $.
Expand All @@ -66071,30 +66105,19 @@ pairs as classes (in set.mm, the Kuratowski encoding). A more
fvpr2.1 $e |- B e. _V $.
fvpr2.2 $e |- D e. _V $.
$( The value of a function with a domain of two elements. (Contributed by
Jeff Madsen, 20-Jun-2010.) $)
Jeff Madsen, 20-Jun-2010.) (Proof shortened by BJ, 26-Sep-2024.) $)
fvpr2 $p |- ( A =/= B -> ( { <. A , C >. , <. B , D >. } ` B ) = D ) $=
( cvv wcel wne cop cpr cfv wceq fvpr2g mp3an12 ) BGHDGHABIBACJBDJKLDMEFAB
CDGGNO $.

$( Obsolete version of ~ fvpr2 as of 26-Sep-2024. (Contributed by Jeff
Madsen, 20-Jun-2010.) (Proof modification is discouraged.)
(New usage is discouraged.) $)
fvpr2OLD $p |- ( A =/= B -> ( { <. A , C >. , <. B , D >. } ` B ) = D ) $=
( wne cop cpr cfv prcom fveq1i wceq necom fvpr1 sylbi syl5eq ) ABGZBACHZB
DHZIZJBTSIZJZDBUAUBSTKLRBAGUCDMABNBADCEFOPQ $.
$}

$( The value of a function with a domain of (at most) two elements.
(Contributed by Alexander van der Vekens, 3-Dec-2017.) $)
fvpr1g $p |- ( ( A e. V /\ C e. W /\ A =/= B )
-> ( { <. A , C >. , <. B , D >. } ` A ) = C ) $=
( wcel wne w3a cop cpr cfv csn wceq cun df-pr fveq1i necom fvunsn sylbi
syl5eq 3ad2ant3 fvsng 3adant3 eqtrd ) AEGZCFGZABHZIAACJZBDJZKZLZAUIMZLZCUHU
FULUNNUGUHULAUMUJMOZLZUNAUKUOUIUJPQUHBAHUPUNNABRUMBDASTUAUBUFUGUNCNUHACEFUC
UDUE $.

$( The value of a function with a domain of (at most) two elements.
(Contributed by Alexander van der Vekens, 3-Dec-2017.) $)
fvpr2g $p |- ( ( B e. V /\ D e. W /\ A =/= B )
-> ( { <. A , C >. , <. B , D >. } ` B ) = D ) $=
( wcel wne w3a cop cpr cfv csn wceq cun prcom df-pr eqtri fveq1i fvunsn
syl5eq 3ad2ant3 fvsng 3adant3 eqtrd ) BEGZDFGZABHZIBACJZBDJZKZLZBUJMZLZDUHU
FULUNNUGUHULBUMUIMOZLUNBUKUOUKUJUIKUOUIUJPUJUIQRSUMACBTUAUBUFUGUNDNUHBDEFUC
UDUE $.

${
$d A x y $. $d B x y $. $d F x y $. $d R x y $.
fprb.1 $e |- A e. _V $.
Expand Down Expand Up @@ -70390,11 +70413,11 @@ result of an operator (deduction version). (Contributed by Paul
ovigg.1 $e |- ( ( x = A /\ y = B /\ z = C ) -> ( ph <-> ps ) ) $.
ovigg.4 $e |- E* z ph $.
ovigg.5 $e |- F = { <. <. x , y >. , z >. | ph } $.
$( The value of an operation class abstraction. Compare ~ ovig . The
condition ` ( x e. R /\ y e. S ) ` is been removed. (Contributed by FL,
$( The value of an operation class abstraction. Compared with ~ ovig , the
condition ` ( x e. R /\ y e. S ) ` is removed. (Contributed by FL,
24-Mar-2007.) (Revised by Mario Carneiro, 19-Dec-2013.) $)
ovigg $p |- ( ( A e. V /\ B e. W /\ C e. X ) ->
( ps -> ( A F B ) = C ) ) $=
ovigg $p |-
( ( A e. V /\ B e. W /\ C e. X ) -> ( ps -> ( A F B ) = C ) ) $=
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I find some of these reformattings a bit dubious. I'm very much not a fan of right alignment, and would prefer we used a consistent formatting style in the library.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I can revert that. I thought the rule of thumb was to break line at highest possible token (in the sense of "oldest in the syntax tree), and I would actually break these at $p if not for formatting problems arising from that choice.

Consistency is indeed paramount. Actually, I wouldn't mind having an automatic "dumb" line-wrap as for proofs and comments.

( wcel w3a cop wceq cfv coprab eloprabga df-ov fveq1i eqtri wfun funoprab
co wi funopfv ax-mp syl5eq syl6bir ) FJPGKPHLPQBFGRZHRACDEUAZPZFGIUHZHSAB
CDEFGHJKLMUBUPUQUNUOTZHUQUNITURFGIUCUNIUOOUDUEUOUFUPURHSUIACDENUGUNHUOUJU
Expand Down Expand Up @@ -221332,6 +221355,76 @@ proposition to be be proved (the first four hypotheses tell its values
$}


$(
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Monoid of endomorphisms
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
$)

$c End $.
$( Token for the monoid of endomorphisms. $)
cend $a class End $. $( Syntax for the monoid of endomorphisms. $)

${
$d c x $.
$( Define the monoid of endomorphisms on an object of a category.
(Contributed by BJ, 4-Apr-2024.) $)
df-end $a |- End = ( c e. Cat |-> ( x e. ( Base ` c ) |->
{ <. ( Base ` ndx ) , ( x ( Hom ` c ) x ) >. ,
<. ( +g ` ndx ) , ( <. x , x >. ( comp ` c ) x ) >. } ) ) $.
$}

${
$d C c x $. $d X c x $. $d ph c x $.
endval.c $e |- ( ph -> C e. Cat ) $.
endval.x $e |- ( ph -> X e. ( Base ` C ) ) $.
$( Value of the monoid of endomorphisms on an object of a category.
(Contributed by BJ, 5-Apr-2024.) $)
endval $p |- ( ph -> ( ( End ` C ) ` X ) =
{ <. ( Base ` ndx ) , ( X ( Hom ` C ) X ) >. ,
<. ( +g ` ndx ) , ( <. X , X >. ( comp ` C ) X ) >. } ) $=
( vx vc cnx cbs cfv cv chom co cop cco cpr cvv wceq fveq2 opeq2d cend a1i
cplusg cmpt ccat df-end oveqd preq12d mpteq12dv wcel fvex fvmptd3 oveq12d
mptex id opeq12d adantl prex fvmptd ) AFCHIJZFKZVABLJZMZNZHUCJZVAVANZVABO
JZMZNZPZUTCCVBMZNZVECCNZCVGMZNZPZBIJZBUAJQAGBFGKZIJZUTVAVAVRLJZMZNZVEVFVA
VROJZMZNZPZUDFVQVJUDZUEUAQFGUFVRBRZFVSWFVQVJVRBISWHWBVDWEVIWHWAVCUTWHVTVB
VAVAVRBLSUGTWHWDVHVEWHWCVGVFVAVRBOSUGTUHUIDWGQUJAFVQVJBIUKUNUBULVACRZVJVP
RAWIVDVLVIVOWIVCVKUTWIVACVACVBWIUOZWJUMTWIVHVNVEWIVFVMVACVGWIVACVACWJWJUP
WJUMTUHUQEVPQUJAVLVOURUBUS $.

$( Base set of the monoid of endomorphisms on an object of a category.
(Contributed by BJ, 5-Apr-2024.) $)
endbase $p |- ( ph ->
( Base ` ( ( End ` C ) ` X ) ) = ( X ( Hom ` C ) X ) ) $=
( cnx cbs cfv cend chom co cop cplusg cco cpr endval fveq1d c1 cvv fvexd
df-base 1nn strndxid wceq basendxnplusgndx fvex ovex fvpr1 mp1i 3eqtr3d
wne ) AFGHZCBIHZHZHULULCCBJHZKZLFMHZCCLCBNHKZLOZHZUNGHUPAULUNUSABCDEPQAUN
GRSACUMTUAUBUCULUQUKUTUPUDAUEULUQUPURFGUFCCUOUGUHUIUJ $.

$( Composition law of the monoid of endomorphisms on an object of a
category. (Contributed by BJ, 5-Apr-2024.) $)
endcomp $p |- ( ph ->
( +g ` ( ( End ` C ) ` X ) ) = ( <. X , X >. ( comp ` C ) X ) ) $=
( cnx cplusg cfv cend cbs chom co cop cco cpr endval fveq1d c2 cvv fvexd
df-plusg 2nn strndxid wceq basendxnplusgndx fvex ovex fvpr2 mp1i 3eqtr3d
wne ) AFGHZCBIHZHZHULFJHZCCBKHLZMULCCMZCBNHZLZMOZHZUNGHUSAULUNUTABCDEPQAU
NGRSACUMTUAUBUCUOULUKVAUSUDAUEUOULUPUSFGUFUQCURUGUHUIUJ $.

$d C x y z $. $d X x y z $. $d ph x y z $.
$( The monoid of endomorphisms on an object of a category is a monoid.
(Contributed by BJ, 5-Apr-2024.) $)
endmnd $p |- ( ph -> ( ( End ` C ) ` X ) e. Mnd ) $=
( vx vy vz cfv co cbs eqcomd cv wcel w3a eqid 3ad2ant1 simp3 adantr syl
chom cop cco cend ccid endbase cplusg endcomp ccat simp2 catcocl wa simpr
simp1 catass catidcl catlid catrid ismndd ) AFGHCCBUAIZJZCCUBCBUCIZJZCBUD
IIZCBUEIZIAVDKIVAABCDEUFLAVDUGIVCABCDEUHLAFMZVANZGMZVANZOBKIZBVBVHVFUTCCC
VJPZUTPZVBPZAVGBUINZVIDQAVGCVJNZVIEQZVPVPAVGVIRAVGVIUJUKAVGVIHMZVANZOZULZ
VJBVBVQVHUTVFCCCCVKVLVMAVNVSDSAVOVSESZWAWAVTVSVRAVSUMZVGVIVRRTVTVSVIWBVGV
IVRUJTWAVTVSVGWBVGVIVRUNTUOAVJBVEUTCVKVLVEPZDEUPAVGULZVJBVBVEVFUTCCVKVLWC
AVNVGDSZAVOVGESZVMWFAVGUMZUQWDVJBVBVEVFUTCCVKVLWCWEWFVMWFWGURUS $.
$}


$(
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Iterated sums in a monoid
Expand Down Expand Up @@ -441175,6 +441268,9 @@ orthogonal vectors (i.e. whose inner product is 0) is the sum of the
"<IMG SRC='_mnd.gif' WIDTH=28 HEIGHT=19 ALT=' Mnd' TITLE='Mnd'>";
althtmldef "Mnd" as "Mnd";
latexdef "Mnd" as "\mathrm{Mnd}";
htmldef "End" as "End ";
althtmldef "End" as "End ";
latexdef "End" as "\operatorname{End}";
htmldef "Grp" as
"<IMG SRC='_grp.gif' WIDTH=25 HEIGHT=19 ALT=' Grp' TITLE='Grp'>";
althtmldef "Grp" as "Grp";
Expand Down Expand Up @@ -445867,9 +445963,6 @@ orthogonal vectors (i.e. whose inner product is 0) is the sum of the
htmldef "RRVec" as "RR-Vec";
althtmldef "RRVec" as "&#8477;-Vec";
latexdef "RRVec" as "{\mathbb{R}-\mathrm{Vec}}";
htmldef "End" as "End ";
althtmldef "End" as "End ";
latexdef "End" as "\operatorname{End}";
/* End of BJ's mathbox */

/* Mathbox of Norm Megill */
Expand Down Expand Up @@ -524495,6 +524588,7 @@ Real and complex numbers (cont.)
ZURUSVAVBURUSJUOVBUQACVBUQAKBAUDLMNVDUSUTUOVBUSUTUMUNVBUSIUTRULBACOUEPUIQUL
UMUPVBUFZUNULASBSVEUMATBTABUGUHUJUK $.


$(
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Properties of real and complex numbers
Expand Down Expand Up @@ -553041,76 +553135,6 @@ coordinates of a barycenter of two points in one dimension (complex
GVCVFVDTVEUOVG $.
$}


$(
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Monoid of endomorphisms
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
$)

$c End $.
$( Token for the monoid of endomorphisms. $)
cend $a class End $. $( Syntax for the monoid of endomorphisms. $)

${
$d c x $.
$( The monoid of endomorphisms on an object of a category. (Contributed by
BJ, 4-Apr-2024.) $)
df-bj-end $a |- End = ( c e. Cat |-> ( x e. ( Base ` c ) |->
{ <. ( Base ` ndx ) , ( x ( Hom ` c ) x ) >. ,
<. ( +g ` ndx ) , ( <. x , x >. ( comp ` c ) x ) >. } ) ) $.
$}

${
$d C c x $. $d X c x $. $d ph c x $.
bj-endval.c $e |- ( ph -> C e. Cat ) $.
bj-endval.x $e |- ( ph -> X e. ( Base ` C ) ) $.
$( Value of the monoid of endomorphisms on an object of a category.
(Contributed by BJ, 5-Apr-2024.) $)
bj-endval $p |- ( ph -> ( ( End ` C ) ` X ) =
{ <. ( Base ` ndx ) , ( X ( Hom ` C ) X ) >. ,
<. ( +g ` ndx ) , ( <. X , X >. ( comp ` C ) X ) >. } ) $=
( vx vc cnx cbs cfv cv chom co cop cco cpr cvv wceq fveq2 opeq2d cend a1i
cplusg cmpt ccat df-bj-end preq12d mpteq12dv wcel fvex fvmptd3 id oveq12d
oveqd mptex opeq12d adantl prex fvmptd ) AFCHIJZFKZVABLJZMZNZHUCJZVAVANZV
ABOJZMZNZPZUTCCVBMZNZVECCNZCVGMZNZPZBIJZBUAJQAGBFGKZIJZUTVAVAVRLJZMZNZVEV
FVAVROJZMZNZPZUDFVQVJUDZUEUAQFGUFVRBRZFVSWFVQVJVRBISWHWBVDWEVIWHWAVCUTWHV
TVBVAVAVRBLSUNTWHWDVHVEWHWCVGVFVAVRBOSUNTUGUHDWGQUIAFVQVJBIUJUOUBUKVACRZV
JVPRAWIVDVLVIVOWIVCVKUTWIVACVACVBWIULZWJUMTWIVHVNVEWIVFVMVACVGWIVACVACWJW
JUPWJUMTUGUQEVPQUIAVLVOURUBUS $.

$( Base set of the monoid of endomorphisms on an object of a category.
(Contributed by BJ, 5-Apr-2024.) $)
bj-endbase $p |- ( ph ->
( Base ` ( ( End ` C ) ` X ) ) = ( X ( Hom ` C ) X ) ) $=
( cnx cbs cfv cend chom co cop cplusg cco cpr bj-endval fveq1d cvv fvexd
c1 df-base 1nn strndxid wne wceq basendxnplusgndx fvex ovex fvpr1 3eqtr3d
mp1i ) AFGHZCBIHZHZHULULCCBJHZKZLFMHZCCLCBNHKZLOZHZUNGHUPAULUNUSABCDEPQAU
NGTRACUMSUAUBUCULUQUDUTUPUEAUFULUQUPURFGUGCCUOUHUIUKUJ $.

$( Composition law of the monoid of endomorphisms on an object of a
category. (Contributed by BJ, 5-Apr-2024.) $)
bj-endcomp $p |- ( ph ->
( +g ` ( ( End ` C ) ` X ) ) = ( <. X , X >. ( comp ` C ) X ) ) $=
( cnx cplusg cfv cend cbs chom co cop cco cpr bj-endval fveq1d cvv fvexd
c2 df-plusg 2nn strndxid wne wceq basendxnplusgndx fvex ovex mp1i 3eqtr3d
fvpr2 ) AFGHZCBIHZHZHULFJHZCCBKHLZMULCCMZCBNHZLZMOZHZUNGHUSAULUNUTABCDEPQ
AUNGTRACUMSUAUBUCUOULUDVAUSUEAUFUOULUPUSFGUGUQCURUHUKUIUJ $.

$d C x y z $. $d X x y z $. $d ph x y z $.
$( The monoid of endomorphisms on an object of a category is a monoid.
(Contributed by BJ, 5-Apr-2024.) $)
bj-endmnd $p |- ( ph -> ( ( End ` C ) ` X ) e. Mnd ) $=
( vx vy vz cfv co cbs eqcomd cv wcel w3a eqid 3ad2ant1 simp3 adantr syl
chom cop cco cend ccid bj-endbase cplusg bj-endcomp ccat simp2 catcocl wa
simpr simp1 catass catidcl catlid catrid ismndd ) AFGHCCBUAIZJZCCUBCBUCIZ
JZCBUDIIZCBUEIZIAVDKIVAABCDEUFLAVDUGIVCABCDEUHLAFMZVANZGMZVANZOBKIZBVBVHV
FUTCCCVJPZUTPZVBPZAVGBUINZVIDQAVGCVJNZVIEQZVPVPAVGVIRAVGVIUJUKAVGVIHMZVAN
ZOZULZVJBVBVQVHUTVFCCCCVKVLVMAVNVSDSAVOVSESZWAWAVTVSVRAVSUMZVGVIVRRTVTVSV
IWBVGVIVRUJTWAVTVSVGWBVGVIVRUNTUOAVJBVEUTCVKVLVEPZDEUPAVGULZVJBVBVEVFUTCC
VKVLWCAVNVGDSZAVOVGESZVMWFAVGUMZUQWDVJBVBVEVFUTCCVKVLWCWEWFVMWFWGURUS $.
$}

$( (End of BJ's mathbox.) $)
$( End $[ set-mbox-bj.mm $] $)

Expand Down
Loading