---

Step * of Lemma seq-append1-assoc

∀[n,n1:ℕ]. ∀[s,s1,t:Top].
  (λm.if m=n + n1 then t else (seq-append(n;n1;s;s1) m) ~ seq-append(n;n1 + 1;s;λm.if m=n1 then t else (s1 m)))
BY
{ (RepUR ``seq-append`` 0
   THEN (UnivCD THENA Auto)
   THEN EqCD
   THEN SqEqualTopToBase
   THEN SqequalSqle
   THEN AssumeHasValue
   THEN (HasValueD (-1) ORELSE (ExceptionCases (-1) THEN Try (SameException)))
   THEN Try ((FLemma `exception-not-value` [-1] THEN Complete (Auto)))
   THEN (Decide ⌜m < n⌝⋅ THENA Auto)
   THEN (All Reduce THENW Auto)
   THEN (Decide ⌜m = (n + n1) ∈ ℤ⌝⋅ THENA Auto)
   THEN (All Reduce THENW Auto)
   THEN Try (Complete (SqLeCD))
   THEN (Complete ((WeakAutoSplit THEN Auto')) ORELSE Auto')) }

---

Latex:

---

Latex:
\mforall{}[n,n1:\mBbbN{}].  \mforall{}[s,s1,t:Top].
    (\mlambda{}m.if  m=n  +  n1  then  t  else  (seq-append(n;n1;s;s1)  m)  \msim{}  seq-append(n;n1  +  1;s;\mlambda{}m.if  m=n1
                                                                                                                                                                      then  t
                                                                                                                                                                      else  (s1  m)))


By

---

Latex:
(RepUR  ``seq-append``  0
  THEN  (UnivCD  THENA  Auto)
  THEN  EqCD
  THEN  SqEqualTopToBase
  THEN  SqequalSqle
  THEN  AssumeHasValue
  THEN  (HasValueD  (-1)  ORELSE  (ExceptionCases  (-1)  THEN  Try  (SameException)))
  THEN  Try  ((FLemma  `exception-not-value`  [-1]  THEN  Complete  (Auto)))
  THEN  (Decide  \mkleeneopen{}m  <  n\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (All  Reduce  THENW  Auto)
  THEN  (Decide  \mkleeneopen{}m  =  (n  +  n1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (All  Reduce  THENW  Auto)
  THEN  Try  (Complete  (SqLeCD))
  THEN  (Complete  ((WeakAutoSplit  THEN  Auto'))  ORELSE  Auto'))

---

Home Index