Metamath Proof Explorer

Definition df-ack

Description: Define the Ackermann function (recursively). (Contributed by Thierry Arnoux, 28-Apr-2024) (Revised by AV, 2-May-2024)

Ref Expression
Assertion df-ack 
|- Ack = seq 0 ( ( f e. _V , j e. _V |-> ( n e. NN0 |-> ( ( ( IterComp ` f ) ` ( n + 1 ) ) ` 1 ) ) ) , ( i e. NN0 |-> if ( i = 0 , ( n e. NN0 |-> ( n + 1 ) ) , i ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cack 
 |-  Ack
1 cc0 
 |-  0
2 vf 
 |-  f
3 cvv 
 |-  _V
4 vj 
 |-  j
5 vn 
 |-  n
6 cn0 
 |-  NN0
7 citco 
 |-  IterComp
8 2 cv 
 |-  f
9 8 7 cfv 
 |-  ( IterComp ` f )
10 5 cv 
 |-  n
11 caddc 
 |-  +
12 c1 
 |-  1
13 10 12 11 co 
 |-  ( n + 1 )
14 13 9 cfv 
 |-  ( ( IterComp ` f ) ` ( n + 1 ) )
15 12 14 cfv 
 |-  ( ( ( IterComp ` f ) ` ( n + 1 ) ) ` 1 )
16 5 6 15 cmpt 
 |-  ( n e. NN0 |-> ( ( ( IterComp ` f ) ` ( n + 1 ) ) ` 1 ) )
17 2 4 3 3 16 cmpo 
 |-  ( f e. _V , j e. _V |-> ( n e. NN0 |-> ( ( ( IterComp ` f ) ` ( n + 1 ) ) ` 1 ) ) )
18 vi 
 |-  i
19 18 cv 
 |-  i
20 19 1 wceq 
 |-  i = 0
21 5 6 13 cmpt 
 |-  ( n e. NN0 |-> ( n + 1 ) )
22 20 21 19 cif 
 |-  if ( i = 0 , ( n e. NN0 |-> ( n + 1 ) ) , i )
23 18 6 22 cmpt 
 |-  ( i e. NN0 |-> if ( i = 0 , ( n e. NN0 |-> ( n + 1 ) ) , i ) )
24 17 23 1 cseq 
 |-  seq 0 ( ( f e. _V , j e. _V |-> ( n e. NN0 |-> ( ( ( IterComp ` f ) ` ( n + 1 ) ) ` 1 ) ) ) , ( i e. NN0 |-> if ( i = 0 , ( n e. NN0 |-> ( n + 1 ) ) , i ) ) )
25 0 24 wceq 
 |-  Ack = seq 0 ( ( f e. _V , j e. _V |-> ( n e. NN0 |-> ( ( ( IterComp ` f ) ` ( n + 1 ) ) ` 1 ) ) ) , ( i e. NN0 |-> if ( i = 0 , ( n e. NN0 |-> ( n + 1 ) ) , i ) ) )