lfnauxshift - examples/peano.mm1

Step	Hyp	Ref	Expression
1		anl	a2 = k1 /\ a3 = k2 -> a2 = k1
2	1	addeq1d	a2 = k1 /\ a3 = k2 -> a2 + i = k1 + i
3	2	appeq2d	a2 = k1 /\ a3 = k2 -> F1 @ (a2 + i) = F1 @ (k1 + i)
4		anr	a2 = k1 /\ a3 = k2 -> a3 = k2
5	4	addeq1d	a2 = k1 /\ a3 = k2 -> a3 + i = k2 + i
6	5	appeq2d	a2 = k1 /\ a3 = k2 -> F2 @ (a3 + i) = F2 @ (k2 + i)
7	3, 6	eqeqd	a2 = k1 /\ a3 = k2 -> (F1 @ (a2 + i) = F2 @ (a3 + i) <-> F1 @ (k1 + i) = F2 @ (k2 + i))
8	7	aleqd	a2 = k1 /\ a3 = k2 -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) <-> A. i F1 @ (k1 + i) = F2 @ (k2 + i))
9	1	lfnauxeq2d	a2 = k1 /\ a3 = k2 -> lfnaux F1 a2 n = lfnaux F1 k1 n
10	4	lfnauxeq2d	a2 = k1 /\ a3 = k2 -> lfnaux F2 a3 n = lfnaux F2 k2 n
11	9, 10	eqeqd	a2 = k1 /\ a3 = k2 -> (lfnaux F1 a2 n = lfnaux F2 a3 n <-> lfnaux F1 k1 n = lfnaux F2 k2 n)
12	8, 11	imeqd	a2 = k1 /\ a3 = k2 -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 n = lfnaux F2 a3 n <-> A. i F1 @ (k1 + i) = F2 @ (k2 + i) -> lfnaux F1 k1 n = lfnaux F2 k2 n)
13	12	bi1d	a2 = k1 /\ a3 = k2 -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 n = lfnaux F2 a3 n) -> A. i F1 @ (k1 + i) = F2 @ (k2 + i) -> lfnaux F1 k1 n = lfnaux F2 k2 n
14	13	ealde	a2 = k1 -> A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 n = lfnaux F2 a3 n) -> A. i F1 @ (k1 + i) = F2 @ (k2 + i) -> lfnaux F1 k1 n = lfnaux F2 k2 n
15	14	ealie	A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 n = lfnaux F2 a3 n) -> A. i F1 @ (k1 + i) = F2 @ (k2 + i) -> lfnaux F1 k1 n = lfnaux F2 k2 n
16		id	_1 = n -> _1 = n
17	16	lfnauxeq3d	_1 = n -> lfnaux F1 a2 _1 = lfnaux F1 a2 n
18	16	lfnauxeq3d	_1 = n -> lfnaux F2 a3 _1 = lfnaux F2 a3 n
19	17, 18	eqeqd	_1 = n -> (lfnaux F1 a2 _1 = lfnaux F2 a3 _1 <-> lfnaux F1 a2 n = lfnaux F2 a3 n)
20	19	imeq2d	_1 = n -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1 <-> A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 n = lfnaux F2 a3 n)
21	20	aleqd	_1 = n -> (A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1) <-> A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 n = lfnaux F2 a3 n))
22	21	aleqd	_1 = n -> (A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1) <-> A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 n = lfnaux F2 a3 n))
23		id	_1 = 0 -> _1 = 0
24	23	lfnauxeq3d	_1 = 0 -> lfnaux F1 a2 _1 = lfnaux F1 a2 0
25	23	lfnauxeq3d	_1 = 0 -> lfnaux F2 a3 _1 = lfnaux F2 a3 0
26	24, 25	eqeqd	_1 = 0 -> (lfnaux F1 a2 _1 = lfnaux F2 a3 _1 <-> lfnaux F1 a2 0 = lfnaux F2 a3 0)
27	26	imeq2d	_1 = 0 -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1 <-> A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 0 = lfnaux F2 a3 0)
28	27	aleqd	_1 = 0 -> (A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1) <-> A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 0 = lfnaux F2 a3 0))
29	28	aleqd	_1 = 0 -> (A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1) <-> A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 0 = lfnaux F2 a3 0))
30		id	_1 = a1 -> _1 = a1
31	30	lfnauxeq3d	_1 = a1 -> lfnaux F1 a2 _1 = lfnaux F1 a2 a1
32	30	lfnauxeq3d	_1 = a1 -> lfnaux F2 a3 _1 = lfnaux F2 a3 a1
33	31, 32	eqeqd	_1 = a1 -> (lfnaux F1 a2 _1 = lfnaux F2 a3 _1 <-> lfnaux F1 a2 a1 = lfnaux F2 a3 a1)
34	33	imeq2d	_1 = a1 -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1 <-> A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 a1 = lfnaux F2 a3 a1)
35	34	aleqd	_1 = a1 -> (A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1) <-> A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 a1 = lfnaux F2 a3 a1))
36	35	aleqd	_1 = a1 -> (A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1) <-> A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 a1 = lfnaux F2 a3 a1))
37		id	_1 = suc a1 -> _1 = suc a1
38	37	lfnauxeq3d	_1 = suc a1 -> lfnaux F1 a2 _1 = lfnaux F1 a2 (suc a1)
39	37	lfnauxeq3d	_1 = suc a1 -> lfnaux F2 a3 _1 = lfnaux F2 a3 (suc a1)
40	38, 39	eqeqd	_1 = suc a1 -> (lfnaux F1 a2 _1 = lfnaux F2 a3 _1 <-> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1))
41	40	imeq2d	_1 = suc a1 -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1 <-> A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1))
42	41	aleqd	_1 = suc a1 -> (A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1) <-> A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1)))
43	42	aleqd	_1 = suc a1 -> (A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1) <-> A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1)))
44		eqtr4	lfnaux F1 a2 0 = 0 -> lfnaux F2 a3 0 = 0 -> lfnaux F1 a2 0 = lfnaux F2 a3 0
45		lfnaux0	lfnaux F1 a2 0 = 0
46	44, 45	ax_mp	lfnaux F2 a3 0 = 0 -> lfnaux F1 a2 0 = lfnaux F2 a3 0
47		lfnaux0	lfnaux F2 a3 0 = 0
48	46, 47	ax_mp	lfnaux F1 a2 0 = lfnaux F2 a3 0
49	48	a1i	A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 0 = lfnaux F2 a3 0
50	49	ax_gen	A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 0 = lfnaux F2 a3 0)
51	50	ax_gen	A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 0 = lfnaux F2 a3 0)
52		anl	a2 = a4 /\ a3 = a5 -> a2 = a4
53	52	addeq1d	a2 = a4 /\ a3 = a5 -> a2 + i = a4 + i
54	53	appeq2d	a2 = a4 /\ a3 = a5 -> F1 @ (a2 + i) = F1 @ (a4 + i)
55		anr	a2 = a4 /\ a3 = a5 -> a3 = a5
56	55	addeq1d	a2 = a4 /\ a3 = a5 -> a3 + i = a5 + i
57	56	appeq2d	a2 = a4 /\ a3 = a5 -> F2 @ (a3 + i) = F2 @ (a5 + i)
58	54, 57	eqeqd	a2 = a4 /\ a3 = a5 -> (F1 @ (a2 + i) = F2 @ (a3 + i) <-> F1 @ (a4 + i) = F2 @ (a5 + i))
59	58	aleqd	a2 = a4 /\ a3 = a5 -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) <-> A. i F1 @ (a4 + i) = F2 @ (a5 + i))
60	52	lfnauxeq2d	a2 = a4 /\ a3 = a5 -> lfnaux F1 a2 a1 = lfnaux F1 a4 a1
61	55	lfnauxeq2d	a2 = a4 /\ a3 = a5 -> lfnaux F2 a3 a1 = lfnaux F2 a5 a1
62	60, 61	eqeqd	a2 = a4 /\ a3 = a5 -> (lfnaux F1 a2 a1 = lfnaux F2 a3 a1 <-> lfnaux F1 a4 a1 = lfnaux F2 a5 a1)
63	59, 62	imeqd	a2 = a4 /\ a3 = a5 -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 a1 = lfnaux F2 a3 a1 <-> A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1)
64	63	cbvald	a2 = a4 -> (A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 a1 = lfnaux F2 a3 a1) <-> A. a5 (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1))
65	64	cbval	A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 a1 = lfnaux F2 a3 a1) <-> A. a4 A. a5 (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1)
66		anl	a4 = suc a2 /\ a5 = suc a3 -> a4 = suc a2
67	66	addeq1d	a4 = suc a2 /\ a5 = suc a3 -> a4 + i = suc a2 + i
68	67	appeq2d	a4 = suc a2 /\ a5 = suc a3 -> F1 @ (a4 + i) = F1 @ (suc a2 + i)
69		anr	a4 = suc a2 /\ a5 = suc a3 -> a5 = suc a3
70	69	addeq1d	a4 = suc a2 /\ a5 = suc a3 -> a5 + i = suc a3 + i
71	70	appeq2d	a4 = suc a2 /\ a5 = suc a3 -> F2 @ (a5 + i) = F2 @ (suc a3 + i)
72	68, 71	eqeqd	a4 = suc a2 /\ a5 = suc a3 -> (F1 @ (a4 + i) = F2 @ (a5 + i) <-> F1 @ (suc a2 + i) = F2 @ (suc a3 + i))
73	72	aleqd	a4 = suc a2 /\ a5 = suc a3 -> (A. i F1 @ (a4 + i) = F2 @ (a5 + i) <-> A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i))
74	66	lfnauxeq2d	a4 = suc a2 /\ a5 = suc a3 -> lfnaux F1 a4 a1 = lfnaux F1 (suc a2) a1
75	69	lfnauxeq2d	a4 = suc a2 /\ a5 = suc a3 -> lfnaux F2 a5 a1 = lfnaux F2 (suc a3) a1
76	74, 75	eqeqd	a4 = suc a2 /\ a5 = suc a3 -> (lfnaux F1 a4 a1 = lfnaux F2 a5 a1 <-> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1)
77	73, 76	imeqd	a4 = suc a2 /\ a5 = suc a3 -> (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1 <-> A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i) -> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1)
78	77	bi1d	a4 = suc a2 /\ a5 = suc a3 -> (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1) -> A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i) -> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1
79	78	ealde	a4 = suc a2 -> A. a5 (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1) -> A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i) -> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1
80	79	ealie	A. a4 A. a5 (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1) -> A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i) -> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1
81		addeq2	i = a6 -> a2 + i = a2 + a6
82	81	appeq2d	i = a6 -> F1 @ (a2 + i) = F1 @ (a2 + a6)
83		addeq2	i = a6 -> a3 + i = a3 + a6
84	83	appeq2d	i = a6 -> F2 @ (a3 + i) = F2 @ (a3 + a6)
85	82, 84	eqeqd	i = a6 -> (F1 @ (a2 + i) = F2 @ (a3 + i) <-> F1 @ (a2 + a6) = F2 @ (a3 + a6))
86	85	cbval	A. i F1 @ (a2 + i) = F2 @ (a3 + i) <-> A. a6 F1 @ (a2 + a6) = F2 @ (a3 + a6)
87		eqeq	F1 @ (suc a2 + i) = F1 @ (a2 + suc i) -> F2 @ (suc a3 + i) = F2 @ (a3 + suc i) -> (F1 @ (suc a2 + i) = F2 @ (suc a3 + i) <-> F1 @ (a2 + suc i) = F2 @ (a3 + suc i))
88		appeq2	suc a2 + i = a2 + suc i -> F1 @ (suc a2 + i) = F1 @ (a2 + suc i)
89		addSass	suc a2 + i = a2 + suc i
90	88, 89	ax_mp	F1 @ (suc a2 + i) = F1 @ (a2 + suc i)
91	87, 90	ax_mp	F2 @ (suc a3 + i) = F2 @ (a3 + suc i) -> (F1 @ (suc a2 + i) = F2 @ (suc a3 + i) <-> F1 @ (a2 + suc i) = F2 @ (a3 + suc i))
92		appeq2	suc a3 + i = a3 + suc i -> F2 @ (suc a3 + i) = F2 @ (a3 + suc i)
93		addSass	suc a3 + i = a3 + suc i
94	92, 93	ax_mp	F2 @ (suc a3 + i) = F2 @ (a3 + suc i)
95	91, 94	ax_mp	F1 @ (suc a2 + i) = F2 @ (suc a3 + i) <-> F1 @ (a2 + suc i) = F2 @ (a3 + suc i)
96		addeq2	a6 = suc i -> a2 + a6 = a2 + suc i
97	96	appeq2d	a6 = suc i -> F1 @ (a2 + a6) = F1 @ (a2 + suc i)
98		addeq2	a6 = suc i -> a3 + a6 = a3 + suc i
99	98	appeq2d	a6 = suc i -> F2 @ (a3 + a6) = F2 @ (a3 + suc i)
100	97, 99	eqeqd	a6 = suc i -> (F1 @ (a2 + a6) = F2 @ (a3 + a6) <-> F1 @ (a2 + suc i) = F2 @ (a3 + suc i))
101	100	eale	A. a6 F1 @ (a2 + a6) = F2 @ (a3 + a6) -> F1 @ (a2 + suc i) = F2 @ (a3 + suc i)
102	95, 101	sylibr	A. a6 F1 @ (a2 + a6) = F2 @ (a3 + a6) -> F1 @ (suc a2 + i) = F2 @ (suc a3 + i)
103	102	iald	A. a6 F1 @ (a2 + a6) = F2 @ (a3 + a6) -> A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i)
104	86, 103	sylbi	A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i)
105	104	imim1i	(A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i) -> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1) -> A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1
106		lfnauxS	lfnaux F1 a2 (suc a1) = F1 @ a2 : lfnaux F1 (suc a2) a1
107		lfnauxS	lfnaux F2 a3 (suc a1) = F2 @ a3 : lfnaux F2 (suc a3) a1
108		add0	a2 + 0 = a2
109		addeq2	i = 0 -> a2 + i = a2 + 0
110	108, 109	syl6eq	i = 0 -> a2 + i = a2
111	110	appeq2d	i = 0 -> F1 @ (a2 + i) = F1 @ a2
112		add0	a3 + 0 = a3
113		addeq2	i = 0 -> a3 + i = a3 + 0
114	112, 113	syl6eq	i = 0 -> a3 + i = a3
115	114	appeq2d	i = 0 -> F2 @ (a3 + i) = F2 @ a3
116	111, 115	eqeqd	i = 0 -> (F1 @ (a2 + i) = F2 @ (a3 + i) <-> F1 @ a2 = F2 @ a3)
117	116	eale	A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> F1 @ a2 = F2 @ a3
118	117	anwl	A. i F1 @ (a2 + i) = F2 @ (a3 + i) /\ lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1 -> F1 @ a2 = F2 @ a3
119		anr	A. i F1 @ (a2 + i) = F2 @ (a3 + i) /\ lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1 -> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1
120	118, 119	conseqd	A. i F1 @ (a2 + i) = F2 @ (a3 + i) /\ lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1 -> F1 @ a2 : lfnaux F1 (suc a2) a1 = F2 @ a3 : lfnaux F2 (suc a3) a1
121	106, 107, 120	eqtr4g	A. i F1 @ (a2 + i) = F2 @ (a3 + i) /\ lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1 -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1)
122	121	exp	A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1 -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1)
123	122	a2i	(A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1) -> A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1)
124	105, 123	rsyl	(A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i) -> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1) -> A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1)
125	80, 124	rsyl	A. a4 A. a5 (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1) -> A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1)
126	125	iald	A. a4 A. a5 (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1) -> A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1))
127	126	iald	A. a4 A. a5 (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1) -> A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1))
128	65, 127	sylbi	A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 a1 = lfnaux F2 a3 a1) -> A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1))
129	22, 29, 36, 43, 51, 128	ind	A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 n = lfnaux F2 a3 n)
130	15, 129	ax_mp	A. i F1 @ (k1 + i) = F2 @ (k2 + i) -> lfnaux F1 k1 n = lfnaux F2 k2 n

1

a2 = k1 /\ a3 = k2 -> a2 = k1

2

1

addeq1d

a2 = k1 /\ a3 = k2 -> a2 + i = k1 + i

3

2

appeq2d

a2 = k1 /\ a3 = k2 -> F1 @ (a2 + i) = F1 @ (k1 + i)

4

anr

a2 = k1 /\ a3 = k2 -> a3 = k2

5

4

addeq1d

a2 = k1 /\ a3 = k2 -> a3 + i = k2 + i

6

5

appeq2d

a2 = k1 /\ a3 = k2 -> F2 @ (a3 + i) = F2 @ (k2 + i)

7

3, 6

eqeqd

a2 = k1 /\ a3 = k2 -> (F1 @ (a2 + i) = F2 @ (a3 + i) <-> F1 @ (k1 + i) = F2 @ (k2 + i))

8

7

aleqd

a2 = k1 /\ a3 = k2 -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) <-> A. i F1 @ (k1 + i) = F2 @ (k2 + i))

9

1

lfnauxeq2d

a2 = k1 /\ a3 = k2 -> lfnaux F1 a2 n = lfnaux F1 k1 n

10

4

lfnauxeq2d

a2 = k1 /\ a3 = k2 -> lfnaux F2 a3 n = lfnaux F2 k2 n

11

9, 10

eqeqd

a2 = k1 /\ a3 = k2 -> (lfnaux F1 a2 n = lfnaux F2 a3 n <-> lfnaux F1 k1 n = lfnaux F2 k2 n)

12

8, 11

imeqd

a2 = k1 /\ a3 = k2 ->
  (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 n = lfnaux F2 a3 n <-> A. i F1 @ (k1 + i) = F2 @ (k2 + i) -> lfnaux F1 k1 n = lfnaux F2 k2 n)

13

12

bi1d

a2 = k1 /\ a3 = k2 ->
  (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 n = lfnaux F2 a3 n) ->
  A. i F1 @ (k1 + i) = F2 @ (k2 + i) ->
  lfnaux F1 k1 n = lfnaux F2 k2 n

14

13

ealde

a2 = k1 ->
  A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 n = lfnaux F2 a3 n) ->
  A. i F1 @ (k1 + i) = F2 @ (k2 + i) ->
  lfnaux F1 k1 n = lfnaux F2 k2 n

15

14

ealie

A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 n = lfnaux F2 a3 n) -> A. i F1 @ (k1 + i) = F2 @ (k2 + i) -> lfnaux F1 k1 n = lfnaux F2 k2 n

16

id

_1 = n -> _1 = n

17

16

lfnauxeq3d

_1 = n -> lfnaux F1 a2 _1 = lfnaux F1 a2 n

18

16

lfnauxeq3d

_1 = n -> lfnaux F2 a3 _1 = lfnaux F2 a3 n

19

17, 18

eqeqd

_1 = n -> (lfnaux F1 a2 _1 = lfnaux F2 a3 _1 <-> lfnaux F1 a2 n = lfnaux F2 a3 n)

20

19

imeq2d

_1 = n -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1 <-> A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 n = lfnaux F2 a3 n)

21

20

aleqd

_1 = n ->
  (A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1) <->
    A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 n = lfnaux F2 a3 n))

22

21

aleqd

_1 = n ->
  (A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1) <->
    A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 n = lfnaux F2 a3 n))

23

id

_1 = 0 -> _1 = 0

24

23

lfnauxeq3d

_1 = 0 -> lfnaux F1 a2 _1 = lfnaux F1 a2 0

25

23

lfnauxeq3d

_1 = 0 -> lfnaux F2 a3 _1 = lfnaux F2 a3 0

26

24, 25

eqeqd

_1 = 0 -> (lfnaux F1 a2 _1 = lfnaux F2 a3 _1 <-> lfnaux F1 a2 0 = lfnaux F2 a3 0)

27

26

imeq2d

_1 = 0 -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1 <-> A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 0 = lfnaux F2 a3 0)

28

27

aleqd

_1 = 0 ->
  (A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1) <->
    A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 0 = lfnaux F2 a3 0))

29

28

aleqd

_1 = 0 ->
  (A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1) <->
    A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 0 = lfnaux F2 a3 0))

30

id

_1 = a1 -> _1 = a1

31

30

lfnauxeq3d

_1 = a1 -> lfnaux F1 a2 _1 = lfnaux F1 a2 a1

32

30

lfnauxeq3d

_1 = a1 -> lfnaux F2 a3 _1 = lfnaux F2 a3 a1

33

31, 32

eqeqd

_1 = a1 -> (lfnaux F1 a2 _1 = lfnaux F2 a3 _1 <-> lfnaux F1 a2 a1 = lfnaux F2 a3 a1)

34

33

imeq2d

_1 = a1 -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1 <-> A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 a1 = lfnaux F2 a3 a1)

35

34

aleqd

_1 = a1 ->
  (A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1) <->
    A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 a1 = lfnaux F2 a3 a1))

36

35

aleqd

_1 = a1 ->
  (A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1) <->
    A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 a1 = lfnaux F2 a3 a1))

37

id

_1 = suc a1 -> _1 = suc a1

38

37

lfnauxeq3d

_1 = suc a1 -> lfnaux F1 a2 _1 = lfnaux F1 a2 (suc a1)

39

37

lfnauxeq3d

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

40

38, 39

eqeqd

_1 = suc a1 -> (lfnaux F1 a2 _1 = lfnaux F2 a3 _1 <-> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1))

41

40

imeq2d

_1 = suc a1 ->
  (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1 <->
    A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1))

42

41

aleqd

_1 = suc a1 ->
  (A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1) <->
    A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1)))

43

42

aleqd

_1 = suc a1 ->
  (A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 _1 = lfnaux F2 a3 _1) <->
    A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1)))

44

eqtr4

lfnaux F1 a2 0 = 0 -> lfnaux F2 a3 0 = 0 -> lfnaux F1 a2 0 = lfnaux F2 a3 0

45

lfnaux0

lfnaux F1 a2 0 = 0

46

44, 45

ax_mp

lfnaux F2 a3 0 = 0 -> lfnaux F1 a2 0 = lfnaux F2 a3 0

47

lfnaux0

lfnaux F2 a3 0 = 0

48

46, 47

ax_mp

lfnaux F1 a2 0 = lfnaux F2 a3 0

49

48

a1i

A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 0 = lfnaux F2 a3 0

50

49

ax_gen

A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 0 = lfnaux F2 a3 0)

51

50

ax_gen

A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 0 = lfnaux F2 a3 0)

52

anl

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

53

52

addeq1d

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

54

53

appeq2d

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

55

anr

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

56

55

addeq1d

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

57

56

appeq2d

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

58

54, 57

eqeqd

a2 = a4 /\ a3 = a5 -> (F1 @ (a2 + i) = F2 @ (a3 + i) <-> F1 @ (a4 + i) = F2 @ (a5 + i))

59

58

aleqd

a2 = a4 /\ a3 = a5 -> (A. i F1 @ (a2 + i) = F2 @ (a3 + i) <-> A. i F1 @ (a4 + i) = F2 @ (a5 + i))

60

52

lfnauxeq2d

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

61

55

lfnauxeq2d

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

62

60, 61

eqeqd

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

63

59, 62

imeqd

a2 = a4 /\ a3 = a5 ->
  (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 a1 = lfnaux F2 a3 a1 <-> A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1)

64

63

cbvald

a2 = a4 ->
  (A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 a1 = lfnaux F2 a3 a1) <->
    A. a5 (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1))

65

64

cbval

A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 a1 = lfnaux F2 a3 a1) <->
  A. a4 A. a5 (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1)

66

anl

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

67

66

addeq1d

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

68

67

appeq2d

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

69

anr

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

70

69

addeq1d

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

71

70

appeq2d

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

72

68, 71

eqeqd

a4 = suc a2 /\ a5 = suc a3 -> (F1 @ (a4 + i) = F2 @ (a5 + i) <-> F1 @ (suc a2 + i) = F2 @ (suc a3 + i))

73

72

aleqd

a4 = suc a2 /\ a5 = suc a3 -> (A. i F1 @ (a4 + i) = F2 @ (a5 + i) <-> A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i))

74

66

lfnauxeq2d

a4 = suc a2 /\ a5 = suc a3 -> lfnaux F1 a4 a1 = lfnaux F1 (suc a2) a1

75

69

lfnauxeq2d

a4 = suc a2 /\ a5 = suc a3 -> lfnaux F2 a5 a1 = lfnaux F2 (suc a3) a1

76

74, 75

eqeqd

a4 = suc a2 /\ a5 = suc a3 -> (lfnaux F1 a4 a1 = lfnaux F2 a5 a1 <-> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1)

77

73, 76

imeqd

a4 = suc a2 /\ a5 = suc a3 ->
  (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1 <->
    A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i) -> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1)

78

77

bi1d

a4 = suc a2 /\ a5 = suc a3 ->
  (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1) ->
  A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i) ->
  lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1

79

78

ealde

a4 = suc a2 ->
  A. a5 (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1) ->
  A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i) ->
  lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1

80

79

ealie

A. a4 A. a5 (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1) ->
  A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i) ->
  lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1

81

addeq2

i = a6 -> a2 + i = a2 + a6

82

81

appeq2d

i = a6 -> F1 @ (a2 + i) = F1 @ (a2 + a6)

83

addeq2

i = a6 -> a3 + i = a3 + a6

84

83

appeq2d

i = a6 -> F2 @ (a3 + i) = F2 @ (a3 + a6)

85

82, 84

eqeqd

i = a6 -> (F1 @ (a2 + i) = F2 @ (a3 + i) <-> F1 @ (a2 + a6) = F2 @ (a3 + a6))

86

85

cbval

A. i F1 @ (a2 + i) = F2 @ (a3 + i) <-> A. a6 F1 @ (a2 + a6) = F2 @ (a3 + a6)

87

eqeq

F1 @ (suc a2 + i) = F1 @ (a2 + suc i) ->
  F2 @ (suc a3 + i) = F2 @ (a3 + suc i) ->
  (F1 @ (suc a2 + i) = F2 @ (suc a3 + i) <-> F1 @ (a2 + suc i) = F2 @ (a3 + suc i))

88

appeq2

suc a2 + i = a2 + suc i -> F1 @ (suc a2 + i) = F1 @ (a2 + suc i)

89

addSass

suc a2 + i = a2 + suc i

90

88, 89

ax_mp

F1 @ (suc a2 + i) = F1 @ (a2 + suc i)

91

87, 90

ax_mp

F2 @ (suc a3 + i) = F2 @ (a3 + suc i) -> (F1 @ (suc a2 + i) = F2 @ (suc a3 + i) <-> F1 @ (a2 + suc i) = F2 @ (a3 + suc i))

92

appeq2

suc a3 + i = a3 + suc i -> F2 @ (suc a3 + i) = F2 @ (a3 + suc i)

93

addSass

suc a3 + i = a3 + suc i

94

92, 93

ax_mp

F2 @ (suc a3 + i) = F2 @ (a3 + suc i)

95

91, 94

ax_mp

F1 @ (suc a2 + i) = F2 @ (suc a3 + i) <-> F1 @ (a2 + suc i) = F2 @ (a3 + suc i)

96

addeq2

a6 = suc i -> a2 + a6 = a2 + suc i

97

96

appeq2d

a6 = suc i -> F1 @ (a2 + a6) = F1 @ (a2 + suc i)

98

addeq2

a6 = suc i -> a3 + a6 = a3 + suc i

99

98

appeq2d

a6 = suc i -> F2 @ (a3 + a6) = F2 @ (a3 + suc i)

100

97, 99

eqeqd

a6 = suc i -> (F1 @ (a2 + a6) = F2 @ (a3 + a6) <-> F1 @ (a2 + suc i) = F2 @ (a3 + suc i))

101

100

eale

A. a6 F1 @ (a2 + a6) = F2 @ (a3 + a6) -> F1 @ (a2 + suc i) = F2 @ (a3 + suc i)

102

95, 101

sylibr

A. a6 F1 @ (a2 + a6) = F2 @ (a3 + a6) -> F1 @ (suc a2 + i) = F2 @ (suc a3 + i)

103

102

iald

A. a6 F1 @ (a2 + a6) = F2 @ (a3 + a6) -> A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i)

104

86, 103

sylbi

A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i)

105

104

imim1i

(A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i) -> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1) ->
  A. i F1 @ (a2 + i) = F2 @ (a3 + i) ->
  lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1

106

lfnauxS

lfnaux F1 a2 (suc a1) = F1 @ a2 : lfnaux F1 (suc a2) a1

107

lfnauxS

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

108

add0

a2 + 0 = a2

109

addeq2

i = 0 -> a2 + i = a2 + 0

110

108, 109

syl6eq

i = 0 -> a2 + i = a2

111

110

appeq2d

i = 0 -> F1 @ (a2 + i) = F1 @ a2

112

add0

a3 + 0 = a3

113

addeq2

i = 0 -> a3 + i = a3 + 0

114

112, 113

syl6eq

i = 0 -> a3 + i = a3

115

114

appeq2d

i = 0 -> F2 @ (a3 + i) = F2 @ a3

116

111, 115

eqeqd

i = 0 -> (F1 @ (a2 + i) = F2 @ (a3 + i) <-> F1 @ a2 = F2 @ a3)

117

116

eale

A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> F1 @ a2 = F2 @ a3

118

117

anwl

A. i F1 @ (a2 + i) = F2 @ (a3 + i) /\ lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1 -> F1 @ a2 = F2 @ a3

119

anr

A. i F1 @ (a2 + i) = F2 @ (a3 + i) /\ lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1 -> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1

120

118, 119

conseqd

A. i F1 @ (a2 + i) = F2 @ (a3 + i) /\ lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1 -> F1 @ a2 : lfnaux F1 (suc a2) a1 = F2 @ a3 : lfnaux F2 (suc a3) a1

121

106, 107, 120

eqtr4g

A. i F1 @ (a2 + i) = F2 @ (a3 + i) /\ lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1 -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1)

122

121

exp

A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1 -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1)

123

122

a2i

(A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1) ->
  A. i F1 @ (a2 + i) = F2 @ (a3 + i) ->
  lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1)

124

105, 123

rsyl

(A. i F1 @ (suc a2 + i) = F2 @ (suc a3 + i) -> lfnaux F1 (suc a2) a1 = lfnaux F2 (suc a3) a1) ->
  A. i F1 @ (a2 + i) = F2 @ (a3 + i) ->
  lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1)

125

80, 124

rsyl

A. a4 A. a5 (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1) ->
  A. i F1 @ (a2 + i) = F2 @ (a3 + i) ->
  lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1)

126

125

iald

A. a4 A. a5 (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1) ->
  A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1))

127

126

iald

A. a4 A. a5 (A. i F1 @ (a4 + i) = F2 @ (a5 + i) -> lfnaux F1 a4 a1 = lfnaux F2 a5 a1) ->
  A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1))

128

65, 127

sylbi

A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 a1 = lfnaux F2 a3 a1) ->
  A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 (suc a1) = lfnaux F2 a3 (suc a1))

129

22, 29, 36, 43, 51, 128

ind

A. a2 A. a3 (A. i F1 @ (a2 + i) = F2 @ (a3 + i) -> lfnaux F1 a2 n = lfnaux F2 a3 n)

130

15, 129

ax_mp

A. i F1 @ (k1 + i) = F2 @ (k2 + i) -> lfnaux F1 k1 n = lfnaux F2 k2 n

Theorem lfnauxshift ≪ | index | src | ≫

Axiom use