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	Could not format assertion : No typesetting found for |- 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 ) ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cack	Could not format Ack : No typesetting found for class Ack with typecode class
1		cc0	$$class0$$
2		vf	$$setvarf$$
3		cvv	$$class\mathrm{V}$$
4		vj	$$setvarj$$
5		vn	$$setvarn$$
6		cn0	$$class{\mathbb{N}}_0$$
7		citco	Could not format IterComp : No typesetting found for class IterComp with typecode class
8	2	cv	$$setvarf$$
9	8 7	cfv	Could not format ( IterComp ` f ) : No typesetting found for class ( IterComp ` f ) with typecode class
10	5	cv	$$setvarn$$
11		caddc	$$class+$$
12		c1	$$class1$$
13	10 12 11	co	$$class\left(n+1\right)$$
14	13 9	cfv	Could not format ( ( IterComp ` f ) ` ( n + 1 ) ) : No typesetting found for class ( ( IterComp ` f ) ` ( n + 1 ) ) with typecode class
15	12 14	cfv	Could not format ( ( ( IterComp ` f ) ` ( n + 1 ) ) ` 1 ) : No typesetting found for class ( ( ( IterComp ` f ) ` ( n + 1 ) ) ` 1 ) with typecode class
16	5 6 15	cmpt	Could not format ( n e. NN0 |-> ( ( ( IterComp ` f ) ` ( n + 1 ) ) ` 1 ) ) : No typesetting found for class ( n e. NN0 |-> ( ( ( IterComp ` f ) ` ( n + 1 ) ) ` 1 ) ) with typecode class
17	2 4 3 3 16	cmpo	Could not format ( f e. _V , j e. _V |-> ( n e. NN0 |-> ( ( ( IterComp ` f ) ` ( n + 1 ) ) ` 1 ) ) ) : No typesetting found for class ( f e. _V , j e. _V |-> ( n e. NN0 |-> ( ( ( IterComp ` f ) ` ( n + 1 ) ) ` 1 ) ) ) with typecode class
18		vi	$$setvari$$
19	18	cv	$$setvari$$
20	19 1	wceq	$$wffi=0$$
21	5 6 13	cmpt	$$class\left(n\in {\mathbb{N}}_0⟼n+1\right)$$
22	20 21 19	cif	$$classif\left(i=0,\left(n\in {\mathbb{N}}_0⟼n+1\right),i\right)$$
23	18 6 22	cmpt	$$class\left(i\in {\mathbb{N}}_0⟼if\left(i=0,\left(n\in {\mathbb{N}}_0⟼n+1\right),i\right)\right)$$
24	17 23 1	cseq	Could not format 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 ) ) ) : No typesetting found for class 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 ) ) ) with typecode class
25	0 24	wceq	Could not format 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 ) ) ) : No typesetting found for wff 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 ) ) ) with typecode wff