Skip to content

Commit

Permalink
functionhood -> functionality and whitespace elimination
Browse files Browse the repository at this point in the history
  • Loading branch information
@sctfn
sctfn committed Oct 16, 2024
1 parent d7d91c4 commit 3821b6a
Showing 1 changed file with 35 additions and 59 deletions.
94 changes: 35 additions & 59 deletions set.mm
View file
Original file line number Diff line number Diff line change
Expand Up @@ -79688,24 +79688,18 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and

${
$d A f g w x y z $. $d f G g w x y z $. $d R f g w x y z $.
frrlem1.1 $e |- B = { f |
E. x ( f Fn x /\
( x C_ A /\
A. y e. x Pred ( R , A , y ) C_ x ) /\
A. y e. x ( f ` y ) =
( y G ( f |` Pred ( R , A , y ) ) )
) } $.
frrlem1.1 $e |- B = { f | E. x ( f Fn x /\
( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\
A. y e. x ( f ` y ) =
( y G ( f |` Pred ( R , A , y ) ) ) ) } $.
$( Lemma for well-founded recursion. The final item we are interested in
is the union of acceptable functions ` B ` . This lemma just changes
bound variables for later use. (Contributed by Paul Chapman,
21-Apr-2012.) $)
frrlem1 $p |- B = { g |
E. z ( g Fn z /\
( z C_ A /\
A. w e. z Pred ( R , A , w ) C_ z ) /\
A. w e. z ( g ` w ) =
( w G ( g |` Pred ( R , A , w ) ) )
) } $=
frrlem1 $p |- B = { g | E. z ( g Fn z /\
( z C_ A /\ A. w e. z Pred ( R , A , w ) C_ z ) /\
A. w e. z ( g ` w ) =
( w G ( g |` Pred ( R , A , w ) ) ) ) } $=
( cv wfn wss wral cfv cres co wceq w3a cpred wa wex cab weq reseq1 oveq2d
fneq1 fveq1 eqeq12d ralbidv 3anbi13d fneq2 sseq1 sseq2 raleqbi1dv predeq3
exbidv sseq1d cbvralvw bitrdi anbi12d raleq fveq2 reseq2d oveq12d cbvexvw
Expand Down Expand Up @@ -79738,13 +79732,10 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and
$d A a f g $. $d A a h x y $. $d B a $. $d f h x y $. $d G a f g $.
$d G h $. $d G g x y $. $d R a f g $. $d R h x y $. $d A a f g b c $.
$d h x y b c $. $d G b c $. $d R b c $.
frrlem4.1 $e |- B = { f |
E. x ( f Fn x /\
( x C_ A /\
A. y e. x Pred ( R , A , y ) C_ x ) /\
A. y e. x ( f ` y ) =
( y G ( f |` Pred ( R , A , y ) ) )
) } $.
frrlem4.1 $e |- B = { f | E. x ( f Fn x /\
( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\
A. y e. x ( f ` y ) =
( y G ( f |` Pred ( R , A , y ) ) ) ) } $.
$( Lemma for well-founded recursion. Properties of the restriction of an
acceptable function to the domain of another acceptable function.
(Contributed by Paul Chapman, 21-Apr-2012.) $)
Expand Down Expand Up @@ -79779,13 +79770,10 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and

${
$d A f g x y $. $d G f g x y $. $d R f g x y $. $d B g $.
frrlem5.1 $e |- B = { f |
E. x ( f Fn x /\
( x C_ A /\
A. y e. x Pred ( R , A , y ) C_ x ) /\
A. y e. x ( f ` y ) =
( y G ( f |` Pred ( R , A , y ) ) )
) } $.
frrlem5.1 $e |- B = { f | E. x ( f Fn x /\
( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\
A. y e. x ( f ` y ) =
( y G ( f |` Pred ( R , A , y ) ) ) ) } $.
frrlem5.2 $e |- F = frecs ( R , A , G ) $.
$( Lemma for well-founded recursion. State the well-founded recursion
generator in terms of the acceptable functions. (Contributed by Scott
Expand Down Expand Up @@ -79830,13 +79818,10 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and
${
$d A f x y z $. $d G f x y z $. $d R f x y z $. $d B g h z $.
$d F x u v z $. $d ph f z $. $d F f $. $d ph g h x u v $.
frrlem9.1 $e |- B = { f |
E. x ( f Fn x /\
( x C_ A /\
A. y e. x Pred ( R , A , y ) C_ x ) /\
A. y e. x ( f ` y ) =
( y G ( f |` Pred ( R , A , y ) ) )
) } $.
frrlem9.1 $e |- B = { f | E. x ( f Fn x /\
( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\
A. y e. x ( f ` y ) =
( y G ( f |` Pred ( R , A , y ) ) ) ) } $.
frrlem9.2 $e |- F = frecs ( R , A , G ) $.
frrlem9.3 $e |- ( ( ph /\ ( g e. B /\ h e. B ) ) ->
( ( x g u /\ x h v ) -> u = v ) ) $.
Expand Down Expand Up @@ -79878,13 +79863,10 @@ currently used conventions for such cases (see ~ cbvmpox , ~ ovmpox and
${
$d A f x y z $. $d G f x y z $. $d R f x y z $. $d B g h z $.
$d F x u v z $. $d ph f z $. $d F f $. $d ph g h x u v $.
frrlem11.1 $e |- B = { f |
E. x ( f Fn x /\
( x C_ A /\
A. y e. x Pred ( R , A , y ) C_ x ) /\
A. y e. x ( f ` y ) =
( y G ( f |` Pred ( R , A , y ) ) )
) } $.
frrlem11.1 $e |- B = { f | E. x ( f Fn x /\
( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\
A. y e. x ( f ` y ) =
( y G ( f |` Pred ( R , A , y ) ) ) ) } $.
frrlem11.2 $e |- F = frecs ( R , A , G ) $.
frrlem11.3 $e |- ( ( ph /\ ( g e. B /\ h e. B ) ) ->
( ( x g u /\ x h v ) -> u = v ) ) $.
Expand Down Expand Up @@ -80013,13 +79995,10 @@ C Fn ( ( S i^i dom F ) u. { z } ) ) $=
$}

${
fprlem.1 $e |- B = { f |
E. x ( f Fn x /\
( x C_ A /\
A. y e. x Pred ( R , A , y ) C_ x ) /\
A. y e. x ( f ` y ) =
( y G ( f |` Pred ( R , A , y ) ) )
) } $.
fprlem.1 $e |- B = { f | E. x ( f Fn x /\
( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\
A. y e. x ( f ` y ) =
( y G ( f |` Pred ( R , A , y ) ) ) ) } $.
fprlem.2 $e |- F = frecs ( R , A , G ) $.

$d A a f x y g h u v $. $d R a f x y g h u v $. $d G a f x y g h u v $.
Expand Down Expand Up @@ -80071,7 +80050,7 @@ C Fn ( ( S i^i dom F ) u. { z } ) ) $=
$d A x y z u v a b c f g h $. $d G x y z u v a b c f g h $.
fprr.1 $e |- F = frecs ( R , A , G ) $.
$( Law of well-founded recursion over a partial order, part one. Establish
the functionhood and domain of the recursive function generator. Note
the functionality and domain of the recursive function generator. Note
that by requiring a partial order we can avoid using the axiom of
infinity. (Contributed by Scott Fenton, 11-Sep-2023.) $)
fpr1 $p |- ( ( R Fr A /\ R Po A /\ R Se A ) -> F Fn A ) $=
Expand Down Expand Up @@ -529674,13 +529653,10 @@ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta ) $=
$}

${
frrlem15.1 $e |- B = { f |
E. x ( f Fn x /\
( x C_ A /\
A. y e. x Pred ( R , A , y ) C_ x ) /\
A. y e. x ( f ` y ) =
( y G ( f |` Pred ( R , A , y ) ) )
) } $.
frrlem15.1 $e |- B = { f | E. x ( f Fn x /\
( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\
A. y e. x ( f ` y ) =
( y G ( f |` Pred ( R , A , y ) ) ) ) } $.
frrlem15.2 $e |- F = frecs ( R , A , G ) $.

$d A a f x y g h u v $. $d R a f x y g h u v $. $d G a f x y g h u v $.
Expand Down Expand Up @@ -533715,7 +533691,7 @@ property of surreals and will be used (via surreal cuts) to prove many

${
$d a b x y z $.
$( Functionhood statement for the surreal cut operator. (Contributed by
$( Functionality statement for the surreal cut operator. (Contributed by
Scott Fenton, 15-Dec-2021.) $)
scutf $p |- |s : <<s --> No $=
( va vb vx vy vz csslt csur cscut wf wfn wceq csn cima cbday wbr mpbir2an
Expand Down Expand Up @@ -536132,7 +536108,7 @@ property of surreals and will be used (via surreal cuts) to prove many

${
$d F x y z $.
$( Another potential definition of functionhood. Based on statements in
$( Another potential definition of functionality. Based on statements in
~ http://people.math.gatech.edu/~~belinfan/research/autoreas/otter/sum/fs/ .
(Contributed by Scott Fenton, 30-Aug-2017.) $)
dffun10 $p |- ( Fun F <-> F C_ ( _I o. ( _V \ ( ( _V \ _I ) o. F ) ) ) ) $=
Expand Down

0 comments on commit 3821b6a

Please sign in to comment.