lfnauxnth - ../examples/peano.mm1

Step	Hyp	Ref	Expression
1		anl	a2 = i /\ a3 = k -> a2 = i
2	1	lteq1d	a2 = i /\ a3 = k -> (a2 < n <-> i < n)
3		anr	a2 = i /\ a3 = k -> a3 = k
4	3	lfnauxeq2d	a2 = i /\ a3 = k -> lfnaux F a3 n = lfnaux F k n
5	1, 4	ntheqd	a2 = i /\ a3 = k -> nth a2 (lfnaux F a3 n) = nth i (lfnaux F k n)
6	3, 1	addeqd	a2 = i /\ a3 = k -> a3 + a2 = k + i
7	6	appeq2d	a2 = i /\ a3 = k -> F @ (a3 + a2) = F @ (k + i)
8	7	suceqd	a2 = i /\ a3 = k -> suc (F @ (a3 + a2)) = suc (F @ (k + i))
9	5, 8	eqeqd	a2 = i /\ a3 = k -> (nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2)) <-> nth i (lfnaux F k n) = suc (F @ (k + i)))
10	2, 9	imeqd	a2 = i /\ a3 = k -> (a2 < n -> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2)) <-> i < n -> nth i (lfnaux F k n) = suc (F @ (k + i)))
11	10	bi1d	a2 = i /\ a3 = k -> (a2 < n -> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2))) -> i < n -> nth i (lfnaux F k n) = suc (F @ (k + i))
12	11	ealde	a2 = i -> A. a3 (a2 < n -> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2))) -> i < n -> nth i (lfnaux F k n) = suc (F @ (k + i))
13	12	ealie	A. a2 A. a3 (a2 < n -> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2))) -> i < n -> nth i (lfnaux F k n) = suc (F @ (k + i))
14		eqidd	_1 = n -> a2 = a2
15		id	_1 = n -> _1 = n
16	14, 15	lteqd	_1 = n -> (a2 < _1 <-> a2 < n)
17		eqsidd	_1 = n -> F == F
18		eqidd	_1 = n -> a3 = a3
19	17, 18, 15	lfnauxeqd	_1 = n -> lfnaux F a3 _1 = lfnaux F a3 n
20	14, 19	ntheqd	_1 = n -> nth a2 (lfnaux F a3 _1) = nth a2 (lfnaux F a3 n)
21		eqidd	_1 = n -> suc (F @ (a3 + a2)) = suc (F @ (a3 + a2))
22	20, 21	eqeqd	_1 = n -> (nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2)) <-> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2)))
23	16, 22	imeqd	_1 = n -> (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2)) <-> a2 < n -> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2)))
24	23	aleqd	_1 = n -> (A. a3 (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2))) <-> A. a3 (a2 < n -> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2))))
25	24	aleqd	_1 = n -> (A. a2 A. a3 (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2))) <-> A. a2 A. a3 (a2 < n -> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2))))
26		eqidd	_1 = 0 -> a2 = a2
27		id	_1 = 0 -> _1 = 0
28	26, 27	lteqd	_1 = 0 -> (a2 < _1 <-> a2 < 0)
29		eqsidd	_1 = 0 -> F == F
30		eqidd	_1 = 0 -> a3 = a3
31	29, 30, 27	lfnauxeqd	_1 = 0 -> lfnaux F a3 _1 = lfnaux F a3 0
32	26, 31	ntheqd	_1 = 0 -> nth a2 (lfnaux F a3 _1) = nth a2 (lfnaux F a3 0)
33		eqidd	_1 = 0 -> suc (F @ (a3 + a2)) = suc (F @ (a3 + a2))
34	32, 33	eqeqd	_1 = 0 -> (nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2)) <-> nth a2 (lfnaux F a3 0) = suc (F @ (a3 + a2)))
35	28, 34	imeqd	_1 = 0 -> (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2)) <-> a2 < 0 -> nth a2 (lfnaux F a3 0) = suc (F @ (a3 + a2)))
36	35	aleqd	_1 = 0 -> (A. a3 (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2))) <-> A. a3 (a2 < 0 -> nth a2 (lfnaux F a3 0) = suc (F @ (a3 + a2))))
37	36	aleqd	_1 = 0 -> (A. a2 A. a3 (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2))) <-> A. a2 A. a3 (a2 < 0 -> nth a2 (lfnaux F a3 0) = suc (F @ (a3 + a2))))
38		eqidd	_1 = a1 -> a2 = a2
39		id	_1 = a1 -> _1 = a1
40	38, 39	lteqd	_1 = a1 -> (a2 < _1 <-> a2 < a1)
41		eqsidd	_1 = a1 -> F == F
42		eqidd	_1 = a1 -> a3 = a3
43	41, 42, 39	lfnauxeqd	_1 = a1 -> lfnaux F a3 _1 = lfnaux F a3 a1
44	38, 43	ntheqd	_1 = a1 -> nth a2 (lfnaux F a3 _1) = nth a2 (lfnaux F a3 a1)
45		eqidd	_1 = a1 -> suc (F @ (a3 + a2)) = suc (F @ (a3 + a2))
46	44, 45	eqeqd	_1 = a1 -> (nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2)) <-> nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2)))
47	40, 46	imeqd	_1 = a1 -> (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2)) <-> a2 < a1 -> nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2)))
48	47	aleqd	_1 = a1 -> (A. a3 (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2))) <-> A. a3 (a2 < a1 -> nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2))))
49	48	aleqd	_1 = a1 -> (A. a2 A. a3 (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2))) <-> A. a2 A. a3 (a2 < a1 -> nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2))))
50		eqidd	_1 = suc a1 -> a2 = a2
51		id	_1 = suc a1 -> _1 = suc a1
52	50, 51	lteqd	_1 = suc a1 -> (a2 < _1 <-> a2 < suc a1)
53		eqsidd	_1 = suc a1 -> F == F
54		eqidd	_1 = suc a1 -> a3 = a3
55	53, 54, 51	lfnauxeqd	_1 = suc a1 -> lfnaux F a3 _1 = lfnaux F a3 (suc a1)
56	50, 55	ntheqd	_1 = suc a1 -> nth a2 (lfnaux F a3 _1) = nth a2 (lfnaux F a3 (suc a1))
57		eqidd	_1 = suc a1 -> suc (F @ (a3 + a2)) = suc (F @ (a3 + a2))
58	56, 57	eqeqd	_1 = suc a1 -> (nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2)) <-> nth a2 (lfnaux F a3 (suc a1)) = suc (F @ (a3 + a2)))
59	52, 58	imeqd	_1 = suc a1 -> (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2)) <-> a2 < suc a1 -> nth a2 (lfnaux F a3 (suc a1)) = suc (F @ (a3 + a2)))
60	59	aleqd	_1 = suc a1 -> (A. a3 (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2))) <-> A. a3 (a2 < suc a1 -> nth a2 (lfnaux F a3 (suc a1)) = suc (F @ (a3 + a2))))
61	60	aleqd	_1 = suc a1 -> (A. a2 A. a3 (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2))) <-> A. a2 A. a3 (a2 < suc a1 -> nth a2 (lfnaux F a3 (suc a1)) = suc (F @ (a3 + a2))))
62		absurd	~a2 < 0 -> a2 < 0 -> nth a2 (lfnaux F a3 0) = suc (F @ (a3 + a2))
63		lt02	~a2 < 0
64	62, 63	ax_mp	a2 < 0 -> nth a2 (lfnaux F a3 0) = suc (F @ (a3 + a2))
65	64	ax_gen	A. a3 (a2 < 0 -> nth a2 (lfnaux F a3 0) = suc (F @ (a3 + a2)))
66	65	ax_gen	A. a2 A. a3 (a2 < 0 -> nth a2 (lfnaux F a3 0) = suc (F @ (a3 + a2)))
67		anl	a2 = a4 /\ a3 = a5 -> a2 = a4
68	67	lteq1d	a2 = a4 /\ a3 = a5 -> (a2 < a1 <-> a4 < a1)
69		anr	a2 = a4 /\ a3 = a5 -> a3 = a5
70	69	lfnauxeq2d	a2 = a4 /\ a3 = a5 -> lfnaux F a3 a1 = lfnaux F a5 a1
71	67, 70	ntheqd	a2 = a4 /\ a3 = a5 -> nth a2 (lfnaux F a3 a1) = nth a4 (lfnaux F a5 a1)
72	69, 67	addeqd	a2 = a4 /\ a3 = a5 -> a3 + a2 = a5 + a4
73	72	appeq2d	a2 = a4 /\ a3 = a5 -> F @ (a3 + a2) = F @ (a5 + a4)
74	73	suceqd	a2 = a4 /\ a3 = a5 -> suc (F @ (a3 + a2)) = suc (F @ (a5 + a4))
75	71, 74	eqeqd	a2 = a4 /\ a3 = a5 -> (nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2)) <-> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4)))
76	68, 75	imeqd	a2 = a4 /\ a3 = a5 -> (a2 < a1 -> nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2)) <-> a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4)))
77	76	cbvald	a2 = a4 -> (A. a3 (a2 < a1 -> nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2))) <-> A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))))
78	77	cbval	A. a2 A. a3 (a2 < a1 -> nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2))) <-> A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4)))
79		ntheq2	lfnaux F a3 (suc a1) = F @ a3 : lfnaux F (suc a3) a1 -> nth a2 (lfnaux F a3 (suc a1)) = nth a2 (F @ a3 : lfnaux F (suc a3) a1)
80		lfnauxS	lfnaux F a3 (suc a1) = F @ a3 : lfnaux F (suc a3) a1
81	79, 80	ax_mp	nth a2 (lfnaux F a3 (suc a1)) = nth a2 (F @ a3 : lfnaux F (suc a3) a1)
82		nthZ	nth 0 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ a3)
83		anr	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = 0 -> a2 = 0
84	83	ntheq1d	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = 0 -> nth a2 (F @ a3 : lfnaux F (suc a3) a1) = nth 0 (F @ a3 : lfnaux F (suc a3) a1)
85	82, 84	syl6eq	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = 0 -> nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ a3)
86		add02	a3 + 0 = a3
87	83	addeq2d	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = 0 -> a3 + a2 = a3 + 0
88	86, 87	syl6eq	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = 0 -> a3 + a2 = a3
89	88	appeq2d	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = 0 -> F @ (a3 + a2) = F @ a3
90	89	suceqd	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = 0 -> suc (F @ (a3 + a2)) = suc (F @ a3)
91	85, 90	eqtr4d	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = 0 -> nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))
92	91	exp	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 -> a2 = 0 -> nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))
93		exsuc	a2 != 0 <-> E. a4 a2 = suc a4
94	93	conv ne	~a2 = 0 <-> E. a4 a2 = suc a4
95		nfal1	F/ a4 A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4)))
96		nfv	F/ a4 a2 < suc a1
97	95, 96	nfan	F/ a4 A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1
98		nfv	F/ a4 nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))
99		anr	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> a2 = suc a4
100	99	ntheq1d	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> nth a2 (F @ a3 : lfnaux F (suc a3) a1) = nth (suc a4) (F @ a3 : lfnaux F (suc a3) a1)
101		nthS	nth (suc a4) (F @ a3 : lfnaux F (suc a3) a1) = nth a4 (lfnaux F (suc a3) a1)
102		ltsuc	a4 < a1 <-> suc a4 < suc a1
103	99	lteq1d	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> (a2 < suc a1 <-> suc a4 < suc a1)
104		anlr	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> a2 < suc a1
105	103, 104	mpbid	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> suc a4 < suc a1
106	102, 105	sylibr	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> a4 < a1
107		eal	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) -> A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4)))
108	107	anwll	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4)))
109		lfnauxeq2	a5 = suc a3 -> lfnaux F a5 a1 = lfnaux F (suc a3) a1
110	109	ntheq2d	a5 = suc a3 -> nth a4 (lfnaux F a5 a1) = nth a4 (lfnaux F (suc a3) a1)
111		addeq1	a5 = suc a3 -> a5 + a4 = suc a3 + a4
112	111	appeq2d	a5 = suc a3 -> F @ (a5 + a4) = F @ (suc a3 + a4)
113	112	suceqd	a5 = suc a3 -> suc (F @ (a5 + a4)) = suc (F @ (suc a3 + a4))
114	110, 113	eqeqd	a5 = suc a3 -> (nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4)) <-> nth a4 (lfnaux F (suc a3) a1) = suc (F @ (suc a3 + a4)))
115	114	imeq2d	a5 = suc a3 -> (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4)) <-> a4 < a1 -> nth a4 (lfnaux F (suc a3) a1) = suc (F @ (suc a3 + a4)))
116	115	eale	A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) -> a4 < a1 -> nth a4 (lfnaux F (suc a3) a1) = suc (F @ (suc a3 + a4))
117	108, 116	rsyl	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> a4 < a1 -> nth a4 (lfnaux F (suc a3) a1) = suc (F @ (suc a3 + a4))
118	106, 117	mpd	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> nth a4 (lfnaux F (suc a3) a1) = suc (F @ (suc a3 + a4))
119		addSass	suc a3 + a4 = a3 + suc a4
120	99	addeq2d	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> a3 + a2 = a3 + suc a4
121	119, 120	syl6eqr	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> a3 + a2 = suc a3 + a4
122	121	appeq2d	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> F @ (a3 + a2) = F @ (suc a3 + a4)
123	122	suceqd	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> suc (F @ (a3 + a2)) = suc (F @ (suc a3 + a4))
124	118, 123	eqtr4d	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> nth a4 (lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))
125	101, 124	syl5eq	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> nth (suc a4) (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))
126	100, 125	eqtrd	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))
127	126	exp	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 -> a2 = suc a4 -> nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))
128	97, 98, 127	eexdh	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 -> E. a4 a2 = suc a4 -> nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))
129	94, 128	syl5bi	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 -> ~a2 = 0 -> nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))
130	92, 129	casesd	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 -> nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))
131	81, 130	syl5eq	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 -> nth a2 (lfnaux F a3 (suc a1)) = suc (F @ (a3 + a2))
132	131	ialda	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) -> A. a3 (a2 < suc a1 -> nth a2 (lfnaux F a3 (suc a1)) = suc (F @ (a3 + a2)))
133	132	iald	A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) -> A. a2 A. a3 (a2 < suc a1 -> nth a2 (lfnaux F a3 (suc a1)) = suc (F @ (a3 + a2)))
134	78, 133	sylbi	A. a2 A. a3 (a2 < a1 -> nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2))) -> A. a2 A. a3 (a2 < suc a1 -> nth a2 (lfnaux F a3 (suc a1)) = suc (F @ (a3 + a2)))
135	25, 37, 49, 61, 66, 134	ind	A. a2 A. a3 (a2 < n -> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2)))
136	13, 135	ax_mp	i < n -> nth i (lfnaux F k n) = suc (F @ (k + i))

1

a2 = i /\ a3 = k -> a2 = i

2

1

lteq1d

a2 = i /\ a3 = k -> (a2 < n <-> i < n)

3

anr

a2 = i /\ a3 = k -> a3 = k

4

3

lfnauxeq2d

a2 = i /\ a3 = k -> lfnaux F a3 n = lfnaux F k n

5

1, 4

ntheqd

a2 = i /\ a3 = k -> nth a2 (lfnaux F a3 n) = nth i (lfnaux F k n)

6

3, 1

addeqd

a2 = i /\ a3 = k -> a3 + a2 = k + i

7

6

appeq2d

a2 = i /\ a3 = k -> F @ (a3 + a2) = F @ (k + i)

8

7

suceqd

a2 = i /\ a3 = k -> suc (F @ (a3 + a2)) = suc (F @ (k + i))

9

5, 8

eqeqd

a2 = i /\ a3 = k -> (nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2)) <-> nth i (lfnaux F k n) = suc (F @ (k + i)))

10

2, 9

imeqd

a2 = i /\ a3 = k -> (a2 < n -> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2)) <-> i < n -> nth i (lfnaux F k n) = suc (F @ (k + i)))

11

10

bi1d

a2 = i /\ a3 = k -> (a2 < n -> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2))) -> i < n -> nth i (lfnaux F k n) = suc (F @ (k + i))

12

11

ealde

a2 = i -> A. a3 (a2 < n -> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2))) -> i < n -> nth i (lfnaux F k n) = suc (F @ (k + i))

13

12

ealie

A. a2 A. a3 (a2 < n -> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2))) -> i < n -> nth i (lfnaux F k n) = suc (F @ (k + i))

14

eqidd

_1 = n -> a2 = a2

15

id

_1 = n -> _1 = n

16

14, 15

lteqd

_1 = n -> (a2 < _1 <-> a2 < n)

17

eqsidd

_1 = n -> F == F

18

eqidd

_1 = n -> a3 = a3

19

17, 18, 15

lfnauxeqd

_1 = n -> lfnaux F a3 _1 = lfnaux F a3 n

20

14, 19

ntheqd

_1 = n -> nth a2 (lfnaux F a3 _1) = nth a2 (lfnaux F a3 n)

21

eqidd

_1 = n -> suc (F @ (a3 + a2)) = suc (F @ (a3 + a2))

22

20, 21

eqeqd

_1 = n -> (nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2)) <-> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2)))

23

16, 22

imeqd

_1 = n -> (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2)) <-> a2 < n -> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2)))

24

23

aleqd

_1 = n -> (A. a3 (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2))) <-> A. a3 (a2 < n -> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2))))

25

24

aleqd

_1 = n -> (A. a2 A. a3 (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2))) <-> A. a2 A. a3 (a2 < n -> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2))))

26

eqidd

_1 = 0 -> a2 = a2

27

id

_1 = 0 -> _1 = 0

28

26, 27

lteqd

_1 = 0 -> (a2 < _1 <-> a2 < 0)

29

eqsidd

_1 = 0 -> F == F

30

eqidd

_1 = 0 -> a3 = a3

31

29, 30, 27

lfnauxeqd

_1 = 0 -> lfnaux F a3 _1 = lfnaux F a3 0

32

26, 31

ntheqd

_1 = 0 -> nth a2 (lfnaux F a3 _1) = nth a2 (lfnaux F a3 0)

33

eqidd

_1 = 0 -> suc (F @ (a3 + a2)) = suc (F @ (a3 + a2))

34

32, 33

eqeqd

_1 = 0 -> (nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2)) <-> nth a2 (lfnaux F a3 0) = suc (F @ (a3 + a2)))

35

28, 34

imeqd

_1 = 0 -> (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2)) <-> a2 < 0 -> nth a2 (lfnaux F a3 0) = suc (F @ (a3 + a2)))

36

35

aleqd

_1 = 0 -> (A. a3 (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2))) <-> A. a3 (a2 < 0 -> nth a2 (lfnaux F a3 0) = suc (F @ (a3 + a2))))

37

36

aleqd

_1 = 0 -> (A. a2 A. a3 (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2))) <-> A. a2 A. a3 (a2 < 0 -> nth a2 (lfnaux F a3 0) = suc (F @ (a3 + a2))))

38

eqidd

_1 = a1 -> a2 = a2

39

id

_1 = a1 -> _1 = a1

40

38, 39

lteqd

_1 = a1 -> (a2 < _1 <-> a2 < a1)

41

eqsidd

_1 = a1 -> F == F

42

eqidd

_1 = a1 -> a3 = a3

43

41, 42, 39

lfnauxeqd

_1 = a1 -> lfnaux F a3 _1 = lfnaux F a3 a1

44

38, 43

ntheqd

_1 = a1 -> nth a2 (lfnaux F a3 _1) = nth a2 (lfnaux F a3 a1)

45

eqidd

_1 = a1 -> suc (F @ (a3 + a2)) = suc (F @ (a3 + a2))

46

44, 45

eqeqd

_1 = a1 -> (nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2)) <-> nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2)))

47

40, 46

imeqd

_1 = a1 -> (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2)) <-> a2 < a1 -> nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2)))

48

47

aleqd

_1 = a1 -> (A. a3 (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2))) <-> A. a3 (a2 < a1 -> nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2))))

49

48

aleqd

_1 = a1 -> (A. a2 A. a3 (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2))) <-> A. a2 A. a3 (a2 < a1 -> nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2))))

50

eqidd

_1 = suc a1 -> a2 = a2

51

id

_1 = suc a1 -> _1 = suc a1

52

50, 51

lteqd

_1 = suc a1 -> (a2 < _1 <-> a2 < suc a1)

53

eqsidd

_1 = suc a1 -> F == F

54

eqidd

_1 = suc a1 -> a3 = a3

55

53, 54, 51

lfnauxeqd

_1 = suc a1 -> lfnaux F a3 _1 = lfnaux F a3 (suc a1)

56

50, 55

ntheqd

_1 = suc a1 -> nth a2 (lfnaux F a3 _1) = nth a2 (lfnaux F a3 (suc a1))

57

eqidd

_1 = suc a1 -> suc (F @ (a3 + a2)) = suc (F @ (a3 + a2))

58

56, 57

eqeqd

_1 = suc a1 -> (nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2)) <-> nth a2 (lfnaux F a3 (suc a1)) = suc (F @ (a3 + a2)))

59

52, 58

imeqd

_1 = suc a1 -> (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2)) <-> a2 < suc a1 -> nth a2 (lfnaux F a3 (suc a1)) = suc (F @ (a3 + a2)))

60

59

aleqd

_1 = suc a1 -> (A. a3 (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2))) <-> A. a3 (a2 < suc a1 -> nth a2 (lfnaux F a3 (suc a1)) = suc (F @ (a3 + a2))))

61

60

aleqd

_1 = suc a1 ->
  (A. a2 A. a3 (a2 < _1 -> nth a2 (lfnaux F a3 _1) = suc (F @ (a3 + a2))) <-> A. a2 A. a3 (a2 < suc a1 -> nth a2 (lfnaux F a3 (suc a1)) = suc (F @ (a3 + a2))))

62

absurd

~a2 < 0 -> a2 < 0 -> nth a2 (lfnaux F a3 0) = suc (F @ (a3 + a2))

63

lt02

~a2 < 0

64

62, 63

ax_mp

a2 < 0 -> nth a2 (lfnaux F a3 0) = suc (F @ (a3 + a2))

65

64

ax_gen

A. a3 (a2 < 0 -> nth a2 (lfnaux F a3 0) = suc (F @ (a3 + a2)))

66

65

ax_gen

A. a2 A. a3 (a2 < 0 -> nth a2 (lfnaux F a3 0) = suc (F @ (a3 + a2)))

67

anl

a2 = a4 /\ a3 = a5 -> a2 = a4

68

67

lteq1d

a2 = a4 /\ a3 = a5 -> (a2 < a1 <-> a4 < a1)

69

anr

a2 = a4 /\ a3 = a5 -> a3 = a5

70

69

lfnauxeq2d

a2 = a4 /\ a3 = a5 -> lfnaux F a3 a1 = lfnaux F a5 a1

71

67, 70

ntheqd

a2 = a4 /\ a3 = a5 -> nth a2 (lfnaux F a3 a1) = nth a4 (lfnaux F a5 a1)

72

69, 67

addeqd

a2 = a4 /\ a3 = a5 -> a3 + a2 = a5 + a4

73

72

appeq2d

a2 = a4 /\ a3 = a5 -> F @ (a3 + a2) = F @ (a5 + a4)

74

73

suceqd

a2 = a4 /\ a3 = a5 -> suc (F @ (a3 + a2)) = suc (F @ (a5 + a4))

75

71, 74

eqeqd

a2 = a4 /\ a3 = a5 -> (nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2)) <-> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4)))

76

68, 75

imeqd

a2 = a4 /\ a3 = a5 -> (a2 < a1 -> nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2)) <-> a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4)))

77

76

cbvald

a2 = a4 -> (A. a3 (a2 < a1 -> nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2))) <-> A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))))

78

77

cbval

A. a2 A. a3 (a2 < a1 -> nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2))) <-> A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4)))

79

ntheq2

lfnaux F a3 (suc a1) = F @ a3 : lfnaux F (suc a3) a1 -> nth a2 (lfnaux F a3 (suc a1)) = nth a2 (F @ a3 : lfnaux F (suc a3) a1)

80

lfnauxS

lfnaux F a3 (suc a1) = F @ a3 : lfnaux F (suc a3) a1

81

79, 80

ax_mp

nth a2 (lfnaux F a3 (suc a1)) = nth a2 (F @ a3 : lfnaux F (suc a3) a1)

82

nthZ

nth 0 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ a3)

83

anr

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = 0 -> a2 = 0

84

83

ntheq1d

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = 0 ->
  nth a2 (F @ a3 : lfnaux F (suc a3) a1) = nth 0 (F @ a3 : lfnaux F (suc a3) a1)

85

82, 84

syl6eq

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = 0 -> nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ a3)

86

add02

a3 + 0 = a3

87

83

addeq2d

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = 0 -> a3 + a2 = a3 + 0

88

86, 87

syl6eq

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = 0 -> a3 + a2 = a3

89

88

appeq2d

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = 0 -> F @ (a3 + a2) = F @ a3

90

89

suceqd

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = 0 -> suc (F @ (a3 + a2)) = suc (F @ a3)

91

85, 90

eqtr4d

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = 0 -> nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))

92

91

exp

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 -> a2 = 0 -> nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))

93

exsuc

a2 != 0 <-> E. a4 a2 = suc a4

95

nfal1

F/ a4 A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4)))

96

nfv

F/ a4 a2 < suc a1

97

95, 96

nfan

F/ a4 A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1

98

nfv

F/ a4 nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))

99

anr

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> a2 = suc a4

100

99

ntheq1d

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 ->
  nth a2 (F @ a3 : lfnaux F (suc a3) a1) = nth (suc a4) (F @ a3 : lfnaux F (suc a3) a1)

101

nthS

nth (suc a4) (F @ a3 : lfnaux F (suc a3) a1) = nth a4 (lfnaux F (suc a3) a1)

102

ltsuc

a4 < a1 <-> suc a4 < suc a1

103

99

lteq1d

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> (a2 < suc a1 <-> suc a4 < suc a1)

104

anlr

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> a2 < suc a1

105

103, 104

mpbid

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> suc a4 < suc a1

106

102, 105

sylibr

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> a4 < a1

107

eal

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) -> A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4)))

108

107

anwll

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 ->
  A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4)))

109

lfnauxeq2

a5 = suc a3 -> lfnaux F a5 a1 = lfnaux F (suc a3) a1

110

109

ntheq2d

a5 = suc a3 -> nth a4 (lfnaux F a5 a1) = nth a4 (lfnaux F (suc a3) a1)

111

addeq1

a5 = suc a3 -> a5 + a4 = suc a3 + a4

112

111

appeq2d

a5 = suc a3 -> F @ (a5 + a4) = F @ (suc a3 + a4)

113

112

suceqd

a5 = suc a3 -> suc (F @ (a5 + a4)) = suc (F @ (suc a3 + a4))

114

110, 113

eqeqd

a5 = suc a3 -> (nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4)) <-> nth a4 (lfnaux F (suc a3) a1) = suc (F @ (suc a3 + a4)))

115

114

imeq2d

a5 = suc a3 -> (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4)) <-> a4 < a1 -> nth a4 (lfnaux F (suc a3) a1) = suc (F @ (suc a3 + a4)))

116

115

eale

A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) -> a4 < a1 -> nth a4 (lfnaux F (suc a3) a1) = suc (F @ (suc a3 + a4))

117

108, 116

rsyl

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 ->
  a4 < a1 ->
  nth a4 (lfnaux F (suc a3) a1) = suc (F @ (suc a3 + a4))

118

106, 117

mpd

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> nth a4 (lfnaux F (suc a3) a1) = suc (F @ (suc a3 + a4))

119

addSass

suc a3 + a4 = a3 + suc a4

120

99

addeq2d

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> a3 + a2 = a3 + suc a4

121

119, 120

syl6eqr

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> a3 + a2 = suc a3 + a4

122

121

appeq2d

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> F @ (a3 + a2) = F @ (suc a3 + a4)

123

122

suceqd

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> suc (F @ (a3 + a2)) = suc (F @ (suc a3 + a4))

124

118, 123

eqtr4d

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 -> nth a4 (lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))

125

101, 124

syl5eq

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 ->
  nth (suc a4) (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))

126

100, 125

eqtrd

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 /\ a2 = suc a4 ->
  nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))

127

126

exp

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 ->
  a2 = suc a4 ->
  nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))

128

97, 98, 127

eexdh

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 ->
  E. a4 a2 = suc a4 ->
  nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))

129

94, 128

syl5bi

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 -> ~a2 = 0 -> nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))

130

92, 129

casesd

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 -> nth a2 (F @ a3 : lfnaux F (suc a3) a1) = suc (F @ (a3 + a2))

131

81, 130

syl5eq

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) /\ a2 < suc a1 -> nth a2 (lfnaux F a3 (suc a1)) = suc (F @ (a3 + a2))

132

131

ialda

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) -> A. a3 (a2 < suc a1 -> nth a2 (lfnaux F a3 (suc a1)) = suc (F @ (a3 + a2)))

133

132

iald

A. a4 A. a5 (a4 < a1 -> nth a4 (lfnaux F a5 a1) = suc (F @ (a5 + a4))) -> A. a2 A. a3 (a2 < suc a1 -> nth a2 (lfnaux F a3 (suc a1)) = suc (F @ (a3 + a2)))

134

78, 133

sylbi

A. a2 A. a3 (a2 < a1 -> nth a2 (lfnaux F a3 a1) = suc (F @ (a3 + a2))) -> A. a2 A. a3 (a2 < suc a1 -> nth a2 (lfnaux F a3 (suc a1)) = suc (F @ (a3 + a2)))

135

25, 37, 49, 61, 66, 134

ind

A. a2 A. a3 (a2 < n -> nth a2 (lfnaux F a3 n) = suc (F @ (a3 + a2)))

136

13, 135

ax_mp

i < n -> nth i (lfnaux F k n) = suc (F @ (k + i))

Theorem lfnauxnth ≪ | index | src | ≫

Axiom use