Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-sseq Structured version   Unicode version

Definition df-sseq 29043
Description: Define a builder for sequences by strong recursion, i.e. by computing the value of the n-th element of the sequence from all preceding elements and not just the previous one. (Contributed by Thierry Arnoux, 21-Apr-2019.)
Assertion
Ref Expression
df-sseq  |- seqstr  =  ( m  e.  _V ,  f  e.  _V  |->  ( m  u.  ( lastS  o.  seq ( # `  m ) ( ( x  e. 
_V ,  y  e. 
_V  |->  ( x ++  <" ( f `  x
) "> )
) ,  ( NN0 
X.  { ( m ++ 
<" ( f `  m ) "> ) } ) ) ) ) )
Distinct variable group:    f, m, x, y

Detailed syntax breakdown of Definition df-sseq
StepHypRef Expression
1 csseq 29042 . 2  class seqstr
2 vm . . 3  setvar  m
3 vf . . 3  setvar  f
4 cvv 3087 . . 3  class  _V
52cv 1436 . . . 4  class  m
6 clsw 12644 . . . . 5  class lastS
7 vx . . . . . . 7  setvar  x
8 vy . . . . . . 7  setvar  y
97cv 1436 . . . . . . . 8  class  x
103cv 1436 . . . . . . . . . 10  class  f
119, 10cfv 5601 . . . . . . . . 9  class  ( f `
 x )
1211cs1 12646 . . . . . . . 8  class  <" (
f `  x ) ">
13 cconcat 12645 . . . . . . . 8  class ++
149, 12, 13co 6305 . . . . . . 7  class  ( x ++ 
<" ( f `  x ) "> )
157, 8, 4, 4, 14cmpt2 6307 . . . . . 6  class  ( x  e.  _V ,  y  e.  _V  |->  ( x ++ 
<" ( f `  x ) "> ) )
16 cn0 10869 . . . . . . 7  class  NN0
175, 10cfv 5601 . . . . . . . . . 10  class  ( f `
 m )
1817cs1 12646 . . . . . . . . 9  class  <" (
f `  m ) ">
195, 18, 13co 6305 . . . . . . . 8  class  ( m ++ 
<" ( f `  m ) "> )
2019csn 4002 . . . . . . 7  class  { ( m ++  <" ( f `
 m ) "> ) }
2116, 20cxp 4852 . . . . . 6  class  ( NN0 
X.  { ( m ++ 
<" ( f `  m ) "> ) } )
22 chash 12512 . . . . . . 7  class  #
235, 22cfv 5601 . . . . . 6  class  ( # `  m )
2415, 21, 23cseq 12210 . . . . 5  class  seq ( # `
 m ) ( ( x  e.  _V ,  y  e.  _V  |->  ( x ++  <" (
f `  x ) "> ) ) ,  ( NN0  X.  {
( m ++  <" (
f `  m ) "> ) } ) )
256, 24ccom 4858 . . . 4  class  ( lastS  o.  seq ( # `  m
) ( ( x  e.  _V ,  y  e.  _V  |->  ( x ++ 
<" ( f `  x ) "> ) ) ,  ( NN0  X.  { ( m ++  <" ( f `
 m ) "> ) } ) ) )
265, 25cun 3440 . . 3  class  ( m  u.  ( lastS  o.  seq ( # `  m ) ( ( x  e. 
_V ,  y  e. 
_V  |->  ( x ++  <" ( f `  x
) "> )
) ,  ( NN0 
X.  { ( m ++ 
<" ( f `  m ) "> ) } ) ) ) )
272, 3, 4, 4, 26cmpt2 6307 . 2  class  ( m  e.  _V ,  f  e.  _V  |->  ( m  u.  ( lastS  o.  seq ( # `  m ) ( ( x  e. 
_V ,  y  e. 
_V  |->  ( x ++  <" ( f `  x
) "> )
) ,  ( NN0 
X.  { ( m ++ 
<" ( f `  m ) "> ) } ) ) ) ) )
281, 27wceq 1437 1  wff seqstr  =  ( m  e.  _V ,  f  e.  _V  |->  ( m  u.  ( lastS  o.  seq ( # `  m ) ( ( x  e. 
_V ,  y  e. 
_V  |->  ( x ++  <" ( f `  x
) "> )
) ,  ( NN0 
X.  { ( m ++ 
<" ( f `  m ) "> ) } ) ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  sseqval  29047
  Copyright terms: Public domain W3C validator