Theorem nztailsS ≪ | index | src | ≫ 

theorem nztailsS (l L: nat): $ nztails (l : L) = (l, L) : nztails L $;
StepHypRefExpression
1 eqtr 
nztails (l : L) = (\\ a1, \\ a2, \ a3, (a1, a2) : a3) @ (l, L, nztails L) ->
  (\\ a1, \\ a2, \ a3, (a1, a2) : a3) @ (l, L, nztails L) = (l, L) : nztails L ->
  nztails (l : L) = (l, L) : nztails L
2 lrecS 
lrec 0 (\\ a1, \\ a2, \ a3, (a1, a2) : a3) (l : L) = (\\ a1, \\ a2, \ a3, (a1, a2) : a3) @ (l, L, lrec 0 (\\ a1, \\ a2, \ a3, (a1, a2) : a3) L)
3 2 conv nztails 
nztails (l : L) = (\\ a1, \\ a2, \ a3, (a1, a2) : a3) @ (l, L, nztails L)
4 1, 3 ax_mp 
(\\ a1, \\ a2, \ a3, (a1, a2) : a3) @ (l, L, nztails L) = (l, L) : nztails L -> nztails (l : L) = (l, L) : nztails L
5 anll 
a1 = l /\ a2 = L /\ a3 = nztails L -> a1 = l
6 anlr 
a1 = l /\ a2 = L /\ a3 = nztails L -> a2 = L
7 5, 6 preqd 
a1 = l /\ a2 = L /\ a3 = nztails L -> a1, a2 = l, L
8 anr 
a1 = l /\ a2 = L /\ a3 = nztails L -> a3 = nztails L
9 7, 8 conseqd 
a1 = l /\ a2 = L /\ a3 = nztails L -> (a1, a2) : a3 = (l, L) : nztails L
10 9 applamed 
a1 = l /\ a2 = L -> (\ a3, (a1, a2) : a3) @ nztails L = (l, L) : nztails L
11 10 appslamed 
a1 = l -> (\\ a2, \ a3, (a1, a2) : a3) @ (L, nztails L) = (l, L) : nztails L
12 11 appslame 
(\\ a1, \\ a2, \ a3, (a1, a2) : a3) @ (l, L, nztails L) = (l, L) : nztails L
13 4, 12 ax_mp 
nztails (l : L) = (l, L) : nztails L

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 (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)