Theorem sublistAt_right ≪ | index | src | ≫ 

theorem sublistAt_right (L1 L2 l n: nat):
  $ sublistAt n L1 L2 -> sublistAt (len l + n) (l ++ L1) L2 $;
StepHypRefExpression
1 anim 
(L1 = x ++ L2 ++ y -> l ++ L1 = (l ++ x) ++ L2 ++ y) ->
  (len x = n -> len (l ++ x) = len l + n) ->
  L1 = x ++ L2 ++ y /\ len x = n ->
  l ++ L1 = (l ++ x) ++ L2 ++ y /\ len (l ++ x) = len l + n
2 appendass 
(l ++ x) ++ L2 ++ y = l ++ x ++ L2 ++ y
3 appendeq2 
L1 = x ++ L2 ++ y -> l ++ L1 = l ++ x ++ L2 ++ y
4 2, 3 syl6eqr 
L1 = x ++ L2 ++ y -> l ++ L1 = (l ++ x) ++ L2 ++ y
5 1, 4 ax_mp 
(len x = n -> len (l ++ x) = len l + n) -> L1 = x ++ L2 ++ y /\ len x = n -> l ++ L1 = (l ++ x) ++ L2 ++ y /\ len (l ++ x) = len l + n
6 appendlen 
len (l ++ x) = len l + len x
7 addeq2 
len x = n -> len l + len x = len l + n
8 6, 7 syl5eq 
len x = n -> len (l ++ x) = len l + n
9 5, 8 ax_mp 
L1 = x ++ L2 ++ y /\ len x = n -> l ++ L1 = (l ++ x) ++ L2 ++ y /\ len (l ++ x) = len l + n
10 biidd 
r = l ++ x -> (L1 = x ++ L2 ++ y /\ len x = n <-> L1 = x ++ L2 ++ y /\ len x = n)
11 eqidd 
r = l ++ x -> l ++ L1 = l ++ L1
12 id 
r = l ++ x -> r = l ++ x
13 eqidd 
r = l ++ x -> L2 ++ y = L2 ++ y
14 12, 13 appendeqd 
r = l ++ x -> r ++ L2 ++ y = (l ++ x) ++ L2 ++ y
15 11, 14 eqeqd 
r = l ++ x -> (l ++ L1 = r ++ L2 ++ y <-> l ++ L1 = (l ++ x) ++ L2 ++ y)
16 12 leneqd 
r = l ++ x -> len r = len (l ++ x)
17 eqidd 
r = l ++ x -> len l + n = len l + n
18 16, 17 eqeqd 
r = l ++ x -> (len r = len l + n <-> len (l ++ x) = len l + n)
19 15, 18 aneqd 
r = l ++ x -> (l ++ L1 = r ++ L2 ++ y /\ len r = len l + n <-> l ++ L1 = (l ++ x) ++ L2 ++ y /\ len (l ++ x) = len l + n)
20 10, 19 imeqd 
r = l ++ x ->
  (L1 = x ++ L2 ++ y /\ len x = n -> l ++ L1 = r ++ L2 ++ y /\ len r = len l + n <->
    L1 = x ++ L2 ++ y /\ len x = n -> l ++ L1 = (l ++ x) ++ L2 ++ y /\ len (l ++ x) = len l + n)
21 9, 20 mpbiri 
r = l ++ x -> L1 = x ++ L2 ++ y /\ len x = n -> l ++ L1 = r ++ L2 ++ y /\ len r = len l + n
22 21 eximd 
r = l ++ x -> E. y (L1 = x ++ L2 ++ y /\ len x = n) -> E. y (l ++ L1 = r ++ L2 ++ y /\ len r = len l + n)
23 22 impcom 
E. y (L1 = x ++ L2 ++ y /\ len x = n) /\ r = l ++ x -> E. y (l ++ L1 = r ++ L2 ++ y /\ len r = len l + n)
24 23 iexde 
E. y (L1 = x ++ L2 ++ y /\ len x = n) -> E. r E. y (l ++ L1 = r ++ L2 ++ y /\ len r = len l + n)
25 24 conv sublistAt 
E. y (L1 = x ++ L2 ++ y /\ len x = n) -> sublistAt (len l + n) (l ++ L1) L2
26 25 eex 
E. x E. y (L1 = x ++ L2 ++ y /\ len x = n) -> sublistAt (len l + n) (l ++ L1) L2
27 26 conv sublistAt 
sublistAt n L1 L2 -> sublistAt (len l + n) (l ++ L1) L2

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)