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 -> _K1 == _K2
_G -> _x1 = _x2
_G -> _k1 = _k2
_G -> _x1 - suc u = _x2 - suc u
_G -> grecaux1 _K1 _x1 _k1 (_x1 - suc u) = grecaux1 _K2 _x2 _k2 (_x2 - suc u)
_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		hyp _Kh	_G -> _K1 == _K2
4		hyp _xh	_G -> _x1 = _x2
5		hyp _kh	_G -> _k1 = _k2
6	4	subeq1d	_G -> _x1 - suc u = _x2 - suc u
7	3, 4, 5, 6	grecaux1eqd	_G -> grecaux1 _K1 _x1 _k1 (_x1 - suc u) = grecaux1 _K2 _x2 _k2 (_x2 - suc u)
8	7	preq1d	_G -> grecaux1 _K1 _x1 _k1 (_x1 - suc u), i = grecaux1 _K2 _x2 _k2 (_x2 - suc u), i
9	8	preq2d	_G -> u, grecaux1 _K1 _x1 _k1 (_x1 - suc u), i = u, grecaux1 _K2 _x2 _k2 (_x2 - suc u), i
10	2, 9	appeqd	_G -> _F1 @ (u, grecaux1 _K1 _x1 _k1 (_x1 - suc u), i) = _F2 @ (u, grecaux1 _K2 _x2 _k2 (_x2 - suc u), i)
11	10	lameqd	_G -> \ i, _F1 @ (u, grecaux1 _K1 _x1 _k1 (_x1 - suc u), i) == \ i, _F2 @ (u, grecaux1 _K2 _x2 _k2 (_x2 - suc u), i)
12	11	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))
13		hyp _nh	_G -> _n1 = _n2
14	1, 12, 13	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
15	14	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)