---

Step * 1 1 2 1 1 1 of Lemma append-finite-nat-seq-1


1. nn : ℕ@i
2. ns : ℕnn ⟶ ℕ@i
3. an : ℕ@i
4. as : ℕan ⟶ ℕ@i
5. bn : ℕ@i
6. bs : ℕbn ⟶ ℕ@i
7. x : ℕ@i
8. (nn + 1) ≤ (an + bn)
9. (λx@0.if (x@0) < (nn)  then ns x@0  else x) = (λx.if (x) < (an)  then as x  else (bs (x - an))) ∈ (ℕnn + 1 ⟶ ℕ)
10. ¬((nn + 1) ≤ an)
⊢ as = ns ∈ (ℕan ⟶ ℕ)
BY
{ ((Ext THENA Auto)
   THEN (Assert ⌜((λx@0.if (x@0) < (nn)  then ns x@0  else x) x1)
                 = ((λx.if (x) < (an)  then as x  else (bs (x - an))) x1)
                 ∈ ℕ⌝⋅
         THENA (HypSubst' (-3) 0 THEN Auto)
         )
   ) }

1
1. nn : ℕ@i
2. ns : ℕnn ⟶ ℕ@i
3. an : ℕ@i
4. as : ℕan ⟶ ℕ@i
5. bn : ℕ@i
6. bs : ℕbn ⟶ ℕ@i
7. x : ℕ@i
8. (nn + 1) ≤ (an + bn)
9. (λx@0.if (x@0) < (nn)  then ns x@0  else x) = (λx.if (x) < (an)  then as x  else (bs (x - an))) ∈ (ℕnn + 1 ⟶ ℕ)
10. ¬((nn + 1) ≤ an)
11. x1 : ℕan
12. ((λx@0.if (x@0) < (nn)  then ns x@0  else x) x1) = ((λx.if (x) < (an)  then as x  else (bs (x - an))) x1) ∈ ℕ
⊢ (as x1) = (ns x1) ∈ ℕ

---

Latex:

---

Latex:

1.  nn  :  \mBbbN{}@i
2.  ns  :  \mBbbN{}nn  {}\mrightarrow{}  \mBbbN{}@i
3.  an  :  \mBbbN{}@i
4.  as  :  \mBbbN{}an  {}\mrightarrow{}  \mBbbN{}@i
5.  bn  :  \mBbbN{}@i
6.  bs  :  \mBbbN{}bn  {}\mrightarrow{}  \mBbbN{}@i
7.  x  :  \mBbbN{}@i
8.  (nn  +  1)  \mleq{}  (an  +  bn)
9.  (\mlambda{}x@0.if  (x@0)  <  (nn)    then  ns  x@0    else  x)  =  (\mlambda{}x.if  (x)  <  (an)    then  as  x    else  (bs  (x  -  an)))
10.  \mneg{}((nn  +  1)  \mleq{}  an)
\mvdash{}  as  =  ns


By

---

Latex:
((Ext  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}((\mlambda{}x@0.if  (x@0)  <  (nn)    then  ns  x@0    else  x)  x1)
                              =  ((\mlambda{}x.if  (x)  <  (an)    then  as  x    else  (bs  (x  -  an)))  x1)\mkleeneclose{}\mcdot{}
              THENA  (HypSubst'  (-3)  0  THEN  Auto)
              )
  )

---

Home Index