Theorem srecauxeqd ≪ | index | src | ≫ 

theorem srecauxeqd (_G: wff) (_S1 _S2: set) (_n1 _n2: nat):
  $ _G -> _S1 == _S2 $ >
  $ _G -> _n1 = _n2 $ >
  $ _G -> srecaux _S1 _n1 = srecaux _S2 _n2 $;
StepHypRefExpression
1 eqidd 
_G -> 0 = 0
2 eqsidd 
_G -> b == b
3 eqidd 
_G -> a = a
4 hyp _Sh 
_G -> _S1 == _S2
5 eqidd 
_G -> b = b
6 4, 5 appeqd 
_G -> _S1 @ b = _S2 @ b
7 2, 3, 6 writeeqd 
_G -> write b a (_S1 @ b) == write b a (_S2 @ b)
8 7 lowereqd 
_G -> lower (write b a (_S1 @ b)) = lower (write b a (_S2 @ b))
9 8 lameqd 
_G -> \ b, lower (write b a (_S1 @ b)) == \ b, lower (write b a (_S2 @ b))
10 9 slameqd 
_G -> (\\ a, \ b, lower (write b a (_S1 @ b))) == (\\ a, \ b, lower (write b a (_S2 @ b)))
11 hyp _nh 
_G -> _n1 = _n2
12 1, 10, 11 recneqd 
_G -> recn 0 (\\ a, \ b, lower (write b a (_S1 @ b))) _n1 = recn 0 (\\ a, \ b, lower (write b a (_S2 @ b))) _n2
13 12 conv srecaux 
_G -> srecaux _S1 _n1 = srecaux _S2 _n2

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)