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 id 
r = l ++ x -> r = l ++ x
11 10 appendeq1d 
r = l ++ x -> r ++ L2 ++ y = (l ++ x) ++ L2 ++ y
12 11 eqeq2d 
r = l ++ x -> (l ++ L1 = r ++ L2 ++ y <-> l ++ L1 = (l ++ x) ++ L2 ++ y)
13 10 leneqd 
r = l ++ x -> len r = len (l ++ x)
14 13 eqeq1d 
r = l ++ x -> (len r = len l + n <-> len (l ++ x) = len l + n)
15 12, 14 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)
16 15 imeq2d 
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)
17 9, 16 mpbiri 
r = l ++ x -> L1 = x ++ L2 ++ y /\ len x = n -> l ++ L1 = r ++ L2 ++ y /\ len r = len l + n
18 17 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)
19 18 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)
20 19 iexde 
E. y (L1 = x ++ L2 ++ y /\ len x = n) -> E. r E. y (l ++ L1 = r ++ L2 ++ y /\ len r = len l + n)
21 20 conv sublistAt 
E. y (L1 = x ++ L2 ++ y /\ len x = n) -> sublistAt (len l + n) (l ++ L1) L2
22 21 eex 
E. x E. y (L1 = x ++ L2 ++ y /\ len x = n) -> sublistAt (len l + n) (l ++ L1) L2
23 22 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)