Theorem sublistAt_id | index | src |

theorem sublistAt_id (L: nat): $ sublistAt 0 L L $;
StepHypRefExpression
1 ian
L = 0 ++ L ++ 0 -> len 0 = 0 -> L = 0 ++ L ++ 0 /\ len 0 = 0
2 eqtr2
0 ++ L ++ 0 = L ++ 0 -> L ++ 0 = L -> L = 0 ++ L ++ 0
3 append0
0 ++ L ++ 0 = L ++ 0
4 2, 3 ax_mp
L ++ 0 = L -> L = 0 ++ L ++ 0
5 append02
L ++ 0 = L
6 4, 5 ax_mp
L = 0 ++ L ++ 0
7 1, 6 ax_mp
len 0 = 0 -> L = 0 ++ L ++ 0 /\ len 0 = 0
8 len0
len 0 = 0
9 7, 8 ax_mp
L = 0 ++ L ++ 0 /\ len 0 = 0
10 eqidd
x = 0 /\ y = 0 -> L = L
11 id
x = 0 -> x = 0
12 11 anwl
x = 0 /\ y = 0 -> x = 0
13 id
y = 0 -> y = 0
14 13 anwr
x = 0 /\ y = 0 -> y = 0
15 10, 14 appendeqd
x = 0 /\ y = 0 -> L ++ y = L ++ 0
16 12, 15 appendeqd
x = 0 /\ y = 0 -> x ++ L ++ y = 0 ++ L ++ 0
17 10, 16 eqeqd
x = 0 /\ y = 0 -> (L = x ++ L ++ y <-> L = 0 ++ L ++ 0)
18 12 leneqd
x = 0 /\ y = 0 -> len x = len 0
19 eqidd
x = 0 /\ y = 0 -> 0 = 0
20 18, 19 eqeqd
x = 0 /\ y = 0 -> (len x = 0 <-> len 0 = 0)
21 17, 20 aneqd
x = 0 /\ y = 0 -> (L = x ++ L ++ y /\ len x = 0 <-> L = 0 ++ L ++ 0 /\ len 0 = 0)
22 9, 21 mpbiri
x = 0 /\ y = 0 -> L = x ++ L ++ y /\ len x = 0
23 22 iexde
x = 0 -> E. y (L = x ++ L ++ y /\ len x = 0)
24 23 iexie
E. x E. y (L = x ++ L ++ y /\ len x = 0)
25 24 conv sublistAt
sublistAt 0 L 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)