Theorem listfnS2 ≪ | index | src | ≫ 

theorem listfnS2 (a: nat) {i: nat} (l: nat):
  $ listfn (a : l) =
    \. i e. upto (suc (size (Dom (listfn l)))), if
      (i = 0)
      a
      (listfn l @ (i - 1)) $;
StepHypRefExpression
1 eqtr 
listfn (a : l) =
    (\\ x, \\ z, \ y, \. i e. upto (suc (size (Dom y))), if (i = 0) x (y @ (i - 1))) @
      (a, l, lrec 0 (\\ x, \\ z, \ y, \. i e. upto (suc (size (Dom y))), if (i = 0) x (y @ (i - 1))) l) ->
  (\\ x, \\ z, \ y, \. i e. upto (suc (size (Dom y))), if (i = 0) x (y @ (i - 1))) @
      (a, l, lrec 0 (\\ x, \\ z, \ y, \. i e. upto (suc (size (Dom y))), if (i = 0) x (y @ (i - 1))) l) =
    \. i e. upto (suc (size (Dom (listfn l)))), if (i = 0) a (listfn l @ (i - 1)) ->
  listfn (a : l) = \. i e. upto (suc (size (Dom (listfn l)))), if (i = 0) a (listfn l @ (i - 1))
2 lrecS 
lrec 0 (\\ x, \\ z, \ y, \. i e. upto (suc (size (Dom y))), if (i = 0) x (y @ (i - 1))) (a : l) =
  (\\ x, \\ z, \ y, \. i e. upto (suc (size (Dom y))), if (i = 0) x (y @ (i - 1))) @
    (a, l, lrec 0 (\\ x, \\ z, \ y, \. i e. upto (suc (size (Dom y))), if (i = 0) x (y @ (i - 1))) l)
3 2 conv listfn 
listfn (a : l) =
  (\\ x, \\ z, \ y, \. i e. upto (suc (size (Dom y))), if (i = 0) x (y @ (i - 1))) @
    (a, l, lrec 0 (\\ x, \\ z, \ y, \. i e. upto (suc (size (Dom y))), if (i = 0) x (y @ (i - 1))) l)
4 1, 3 ax_mp 
(\\ x, \\ z, \ y, \. i e. upto (suc (size (Dom y))), if (i = 0) x (y @ (i - 1))) @
      (a, l, lrec 0 (\\ x, \\ z, \ y, \. i e. upto (suc (size (Dom y))), if (i = 0) x (y @ (i - 1))) l) =
    \. i e. upto (suc (size (Dom (listfn l)))), if (i = 0) a (listfn l @ (i - 1)) ->
  listfn (a : l) = \. i e. upto (suc (size (Dom (listfn l)))), if (i = 0) a (listfn l @ (i - 1))
5 biidd 
x = a /\ z = l /\ y = listfn l -> (i = 0 <-> i = 0)
6 anll 
x = a /\ z = l /\ y = listfn l -> x = a
7 anr 
x = a /\ z = l /\ y = listfn l -> y = listfn l
8 7 appneq1d 
x = a /\ z = l /\ y = listfn l -> y @ (i - 1) = listfn l @ (i - 1)
9 5, 6, 8 ifeqd 
x = a /\ z = l /\ y = listfn l -> if (i = 0) x (y @ (i - 1)) = if (i = 0) a (listfn l @ (i - 1))
10 9 lameqd 
x = a /\ z = l /\ y = listfn l -> \ i, if (i = 0) x (y @ (i - 1)) == \ i, if (i = 0) a (listfn l @ (i - 1))
11 7 nseqd 
x = a /\ z = l /\ y = listfn l -> y == listfn l
12 11 dmeqd 
x = a /\ z = l /\ y = listfn l -> Dom y == Dom (listfn l)
13 12 sizeeqd 
x = a /\ z = l /\ y = listfn l -> size (Dom y) = size (Dom (listfn l))
14 13 suceqd 
x = a /\ z = l /\ y = listfn l -> suc (size (Dom y)) = suc (size (Dom (listfn l)))
15 14 uptoeqd 
x = a /\ z = l /\ y = listfn l -> upto (suc (size (Dom y))) = upto (suc (size (Dom (listfn l))))
16 15 nseqd 
x = a /\ z = l /\ y = listfn l -> upto (suc (size (Dom y))) == upto (suc (size (Dom (listfn l))))
17 10, 16 reseqd 
x = a /\ z = l /\ y = listfn l ->
  (\ i, if (i = 0) x (y @ (i - 1))) |` upto (suc (size (Dom y))) == (\ i, if (i = 0) a (listfn l @ (i - 1))) |` upto (suc (size (Dom (listfn l))))
18 17 lowereqd 
x = a /\ z = l /\ y = listfn l ->
  lower ((\ i, if (i = 0) x (y @ (i - 1))) |` upto (suc (size (Dom y)))) =
    lower ((\ i, if (i = 0) a (listfn l @ (i - 1))) |` upto (suc (size (Dom (listfn l)))))
19 18 conv rlam 
x = a /\ z = l /\ y = listfn l ->
  \. i e. upto (suc (size (Dom y))), if (i = 0) x (y @ (i - 1)) = \. i e. upto (suc (size (Dom (listfn l)))), if (i = 0) a (listfn l @ (i - 1))
20 19 applamed 
x = a /\ z = l ->
  (\ y, \. i e. upto (suc (size (Dom y))), if (i = 0) x (y @ (i - 1))) @ listfn l =
    \. i e. upto (suc (size (Dom (listfn l)))), if (i = 0) a (listfn l @ (i - 1))
21 20 appslamed 
x = a ->
  (\\ z, \ y, \. i e. upto (suc (size (Dom y))), if (i = 0) x (y @ (i - 1))) @ (l, listfn l) =
    \. i e. upto (suc (size (Dom (listfn l)))), if (i = 0) a (listfn l @ (i - 1))
22 21 appslame 
(\\ x, \\ z, \ y, \. i e. upto (suc (size (Dom y))), if (i = 0) x (y @ (i - 1))) @ (a, l, listfn l) =
  \. i e. upto (suc (size (Dom (listfn l)))), if (i = 0) a (listfn l @ (i - 1))
23 22 conv listfn 
(\\ x, \\ z, \ y, \. i e. upto (suc (size (Dom y))), if (i = 0) x (y @ (i - 1))) @
    (a, l, lrec 0 (\\ x, \\ z, \ y, \. i e. upto (suc (size (Dom y))), if (i = 0) x (y @ (i - 1))) l) =
  \. i e. upto (suc (size (Dom (listfn l)))), if (i = 0) a (listfn l @ (i - 1))
24 4, 23 ax_mp 
listfn (a : l) = \. i e. upto (suc (size (Dom (listfn l)))), if (i = 0) a (listfn l @ (i - 1))

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)