Theorem grecaux2eqd ≪ | index | src | ≫

theorem grecaux2eqd (_G: wff) (_z1 _z2: nat) (_K1 _K2 _F1 _F2: set)
  (_x1 _x2 _n1 _n2 _k1 _k2: nat):
  $ _G -> _z1 = _z2 $ >
  $ _G -> _K1 == _K2 $ >
  $ _G -> _F1 == _F2 $ >
  $ _G -> _x1 = _x2 $ >
  $ _G -> _n1 = _n2 $ >
  $ _G -> _k1 = _k2 $ >
  $ _G -> grecaux2 _z1 _K1 _F1 _x1 _n1 _k1 = grecaux2 _z2 _K2 _F2 _x2 _n2 _k2 $;


_G -> _z1 = _z2
_G -> _F1 == _F2
_G -> u = u
_G -> _K1 == _K2
_G -> _x1 = _x2
_G -> _k1 = _k2
_G -> suc u = suc u
_G -> _x1 - suc u = _x2 - suc u
_G -> grecaux1 _K1 _x1 _k1 (_x1 - suc u) = grecaux1 _K2 _x2 _k2 (_x2 - suc u)
_G -> i = i
_G -> grecaux1 _K1 _x1 _k1 (_x1 - suc u), i = grecaux1 _K2 _x2 _k2 (_x2 - suc u), i
_G -> u, grecaux1 _K1 _x1 _k1 (_x1 - suc u), i = u, grecaux1 _K2 _x2 _k2 (_x2 - suc u), i
_G -> _F1 @ (u, grecaux1 _K1 _x1 _k1 (_x1 - suc u), i) = _F2 @ (u, grecaux1 _K2 _x2 _k2 (_x2 - suc u), i)
_G -> \ i, _F1 @ (u, grecaux1 _K1 _x1 _k1 (_x1 - suc u), i) == \ i, _F2 @ (u, grecaux1 _K2 _x2 _k2 (_x2 - suc u), i)
_G -> (\\ u, \ i, _F1 @ (u, grecaux1 _K1 _x1 _k1 (_x1 - suc u), i)) == (\\ u, \ i, _F2 @ (u, grecaux1 _K2 _x2 _k2 (_x2 - suc u), i))
_G -> _n1 = _n2
_G -> recn _z1 (\\ u, \ i, _F1 @ (u, grecaux1 _K1 _x1 _k1 (_x1 - suc u), i)) _n1 = recn _z2 (\\ u, \ i, _F2 @ (u, grecaux1 _K2 _x2 _k2 (_x2 - suc u), i)) _n2
_G -> grecaux2 _z1 _K1 _F1 _x1 _n1 _k1 = grecaux2 _z2 _K2 _F2 _x2 _n2 _k2

Step	Hyp	Ref	Expression
1		hyp _zh	_G -> _z1 = _z2
2		hyp _Fh	_G -> _F1 == _F2
3		eqidd	_G -> u = u
4		hyp _Kh	_G -> _K1 == _K2
5		hyp _xh	_G -> _x1 = _x2
6		hyp _kh	_G -> _k1 = _k2
7		eqidd	_G -> suc u = suc u
8	5, 7	subeqd	_G -> _x1 - suc u = _x2 - suc u
9	4, 5, 6, 8	grecaux1eqd	_G -> grecaux1 _K1 _x1 _k1 (_x1 - suc u) = grecaux1 _K2 _x2 _k2 (_x2 - suc u)
10		eqidd	_G -> i = i
11	9, 10	preqd	_G -> grecaux1 _K1 _x1 _k1 (_x1 - suc u), i = grecaux1 _K2 _x2 _k2 (_x2 - suc u), i
12	3, 11	preqd	_G -> u, grecaux1 _K1 _x1 _k1 (_x1 - suc u), i = u, grecaux1 _K2 _x2 _k2 (_x2 - suc u), i
13	2, 12	appeqd	_G -> _F1 @ (u, grecaux1 _K1 _x1 _k1 (_x1 - suc u), i) = _F2 @ (u, grecaux1 _K2 _x2 _k2 (_x2 - suc u), i)
14	13	lameqd	_G -> \ i, _F1 @ (u, grecaux1 _K1 _x1 _k1 (_x1 - suc u), i) == \ i, _F2 @ (u, grecaux1 _K2 _x2 _k2 (_x2 - suc u), i)
15	14	slameqd	_G -> (\\ u, \ i, _F1 @ (u, grecaux1 _K1 _x1 _k1 (_x1 - suc u), i)) == (\\ u, \ i, _F2 @ (u, grecaux1 _K2 _x2 _k2 (_x2 - suc u), i))
16		hyp _nh	_G -> _n1 = _n2
17	1, 15, 16	recneqd	_G -> recn _z1 (\\ u, \ i, _F1 @ (u, grecaux1 _K1 _x1 _k1 (_x1 - suc u), i)) _n1 = recn _z2 (\\ u, \ i, _F2 @ (u, grecaux1 _K2 _x2 _k2 (_x2 - suc u), i)) _n2
18	17	conv grecaux2	_G -> grecaux2 _z1 _K1 _F1 _x1 _n1 _k1 = grecaux2 _z2 _K2 _F2 _x2 _n2 _k2

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano2, addeq, muleq)