Step
*
of Lemma
seq-normalize-append
∀[n,m:ℕ]. ∀[s1,s2:Top]. (seq-normalize(n + m;seq-append(n;m;s1;s2)) ~ seq-append(n;m;s1;s2))
BY
{ (RepUR ``seq-normalize seq-append`` 0
THEN (UnivCD THENA Auto)
THEN EqCD
THEN SqEqualTopToBase
THEN SqequalSqle
THEN AssumeHasValue
THEN (HasValueD (-1) ORELSE (ExceptionCases (-1) THEN Try (SameException)))) }
1
1. n : ℕ
2. m : ℕ
3. m@0 : Base
4. s2 : Base
5. s1 : Base
6. (if (m@0) < (n + m) then if (m@0) < (n) then s1 m@0 else if (m@0) < (n + m) then s2 (m@0 - n) else ⊥ else ⊥)↓
7. m@0 ∈ ℤ
8. n + m ∈ ℤ
⊢ if (m@0) < (n + m) then if (m@0) < (n) then s1 m@0 else if (m@0) < (n + m) then s2 (m@0 - n) else ⊥ else ⊥
≤ if (m@0) < (n) then s1 m@0 else if (m@0) < (n + m) then s2 (m@0 - n) else ⊥
2
1. n : ℕ
2. m : ℕ
3. m@0 : Base
4. s2 : Base
5. s1 : Base
6. is-exception(if (m@0) < (n + m)
then if (m@0) < (n) then s1 m@0 else if (m@0) < (n + m) then s2 (m@0 - n) else ⊥
else ⊥)
7. m@0 ∈ ℤ
8. n + m ∈ ℤ
⊢ if (m@0) < (n + m) then if (m@0) < (n) then s1 m@0 else if (m@0) < (n + m) then s2 (m@0 - n) else ⊥ else ⊥
≤ if (m@0) < (n) then s1 m@0 else if (m@0) < (n + m) then s2 (m@0 - n) else ⊥
3
1. n : ℕ
2. m : ℕ
3. m@0 : Base
4. s2 : Base
5. s1 : Base
6. is-exception(if (m@0) < (n + m)
then if (m@0) < (n) then s1 m@0 else if (m@0) < (n + m) then s2 (m@0 - n) else ⊥
else ⊥)
7. m@0 ∈ ℤ
8. is-exception(n + m)
⊢ if (m@0) < (n + m) then if (m@0) < (n) then s1 m@0 else if (m@0) < (n + m) then s2 (m@0 - n) else ⊥ else ⊥
≤ if (m@0) < (n) then s1 m@0 else if (m@0) < (n + m) then s2 (m@0 - n) else ⊥
4
1. n : ℕ
2. m : ℕ
3. m@0 : Base
4. s2 : Base
5. s1 : Base
6. (if (m@0) < (n) then s1 m@0 else if (m@0) < (n + m) then s2 (m@0 - n) else ⊥)↓
7. m@0 ∈ ℤ
8. n ∈ ℤ
⊢ if (m@0) < (n) then s1 m@0 else if (m@0) < (n + m) then s2 (m@0 - n) else ⊥ ≤ if (m@0) < (n + m)
then if (m@0) < (n)
then s1 m@0
else if (m@0) < (n + m)
then s2 (m@0 - n)
else ⊥
else ⊥
5
1. n : ℕ
2. m : ℕ
3. m@0 : Base
4. s2 : Base
5. s1 : Base
6. is-exception(if (m@0) < (n) then s1 m@0 else if (m@0) < (n + m) then s2 (m@0 - n) else ⊥)
7. m@0 ∈ ℤ
8. n ∈ ℤ
⊢ if (m@0) < (n) then s1 m@0 else if (m@0) < (n + m) then s2 (m@0 - n) else ⊥ ≤ if (m@0) < (n + m)
then if (m@0) < (n)
then s1 m@0
else if (m@0) < (n + m)
then s2 (m@0 - n)
else ⊥
else ⊥
6
1. n : ℕ
2. m : ℕ
3. m@0 : Base
4. s2 : Base
5. s1 : Base
6. is-exception(if (m@0) < (n) then s1 m@0 else if (m@0) < (n + m) then s2 (m@0 - n) else ⊥)
7. m@0 ∈ ℤ
8. is-exception(n)
⊢ if (m@0) < (n) then s1 m@0 else if (m@0) < (n + m) then s2 (m@0 - n) else ⊥ ≤ if (m@0) < (n + m)
then if (m@0) < (n)
then s1 m@0
else if (m@0) < (n + m)
then s2 (m@0 - n)
else ⊥
else ⊥
Latex:
Latex:
\mforall{}[n,m:\mBbbN{}]. \mforall{}[s1,s2:Top]. (seq-normalize(n + m;seq-append(n;m;s1;s2)) \msim{} seq-append(n;m;s1;s2))
By
Latex:
(RepUR ``seq-normalize seq-append`` 0
THEN (UnivCD THENA Auto)
THEN EqCD
THEN SqEqualTopToBase
THEN SqequalSqle
THEN AssumeHasValue
THEN (HasValueD (-1) ORELSE (ExceptionCases (-1) THEN Try (SameException))))
Home
Index