Theorem listfnS ≪ | index | src | ≫

theorem listfnS (a: nat) {i: nat} (l: nat):
  $ listfn (a : l) =
    \. i e. upto (suc (len 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)) ->
  \. i e. upto (suc (size (Dom (listfn l)))), if (i = 0) a (listfn l @ (i - 1)) = \. i e. upto (suc (len l)), if (i = 0) a (listfn l @ (i - 1)) ->
  listfn (a : l) = \. i e. upto (suc (len 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))
\. i e. upto (suc (size (Dom (listfn l)))), if (i = 0) a (listfn l @ (i - 1)) = \. i e. upto (suc (len l)), if (i = 0) a (listfn l @ (i - 1)) ->
  listfn (a : l) = \. i e. upto (suc (len l)), if (i = 0) a (listfn l @ (i - 1))
upto (suc (size (Dom (listfn l)))) = upto (suc (len l)) ->
  \. i e. upto (suc (size (Dom (listfn l)))), if (i = 0) a (listfn l @ (i - 1)) = \. i e. upto (suc (len l)), if (i = 0) a (listfn l @ (i - 1))
suc (size (Dom (listfn l))) = suc (len l) -> upto (suc (size (Dom (listfn l)))) = upto (suc (len l))
size (Dom (listfn l)) = len l -> suc (size (Dom (listfn l))) = suc (len l)
size (Dom (listfn l)) = size (upto (len l)) -> size (upto (len l)) = len l -> size (Dom (listfn l)) = len l
Dom (listfn l) == upto (len l) -> size (Dom (listfn l)) = size (upto (len l))
Dom (listfn l) == upto (len l)
size (Dom (listfn l)) = size (upto (len l))
size (upto (len l)) = len l -> size (Dom (listfn l)) = len l
size (upto (len l)) = len l
size (Dom (listfn l)) = len l
suc (size (Dom (listfn l))) = suc (len l)
upto (suc (size (Dom (listfn l)))) = upto (suc (len l))
\. i e. upto (suc (size (Dom (listfn l)))), if (i = 0) a (listfn l @ (i - 1)) = \. i e. upto (suc (len l)), if (i = 0) a (listfn l @ (i - 1))
listfn (a : l) = \. i e. upto (suc (len l)), if (i = 0) a (listfn l @ (i - 1))

Step	Hyp	Ref	Expression
1		eqtr	listfn (a : l) = \. i e. upto (suc (size (Dom (listfn l)))), if (i = 0) a (listfn l @ (i - 1)) -> \. i e. upto (suc (size (Dom (listfn l)))), if (i = 0) a (listfn l @ (i - 1)) = \. i e. upto (suc (len l)), if (i = 0) a (listfn l @ (i - 1)) -> listfn (a : l) = \. i e. upto (suc (len l)), if (i = 0) a (listfn l @ (i - 1))
2		listfnS2	listfn (a : l) = \. i e. upto (suc (size (Dom (listfn l)))), if (i = 0) a (listfn l @ (i - 1))
3	1, 2	ax_mp	\. i e. upto (suc (size (Dom (listfn l)))), if (i = 0) a (listfn l @ (i - 1)) = \. i e. upto (suc (len l)), if (i = 0) a (listfn l @ (i - 1)) -> listfn (a : l) = \. i e. upto (suc (len l)), if (i = 0) a (listfn l @ (i - 1))
4		rlameq1	upto (suc (size (Dom (listfn l)))) = upto (suc (len l)) -> \. i e. upto (suc (size (Dom (listfn l)))), if (i = 0) a (listfn l @ (i - 1)) = \. i e. upto (suc (len l)), if (i = 0) a (listfn l @ (i - 1))
5		uptoeq	suc (size (Dom (listfn l))) = suc (len l) -> upto (suc (size (Dom (listfn l)))) = upto (suc (len l))
6		suceq	size (Dom (listfn l)) = len l -> suc (size (Dom (listfn l))) = suc (len l)
7		eqtr	size (Dom (listfn l)) = size (upto (len l)) -> size (upto (len l)) = len l -> size (Dom (listfn l)) = len l
8		sizeeq	Dom (listfn l) == upto (len l) -> size (Dom (listfn l)) = size (upto (len l))
9		dmlistfn	Dom (listfn l) == upto (len l)
10	8, 9	ax_mp	size (Dom (listfn l)) = size (upto (len l))
11	7, 10	ax_mp	size (upto (len l)) = len l -> size (Dom (listfn l)) = len l
12		sizeupto	size (upto (len l)) = len l
13	11, 12	ax_mp	size (Dom (listfn l)) = len l
14	6, 13	ax_mp	suc (size (Dom (listfn l))) = suc (len l)
15	5, 14	ax_mp	upto (suc (size (Dom (listfn l)))) = upto (suc (len l))
16	4, 15	ax_mp	\. i e. upto (suc (size (Dom (listfn l)))), if (i = 0) a (listfn l @ (i - 1)) = \. i e. upto (suc (len l)), if (i = 0) a (listfn l @ (i - 1))
17	3, 16	ax_mp	listfn (a : l) = \. i e. upto (suc (len 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)