---

Step * 1 of Lemma subtype_rel_tuple-type


1. u : Type
2. v : Type List
3. ¬(v = [] ∈ (Type List))
4. ∀[Bs:Type List]. tuple-type(v) ⊆r tuple-type(Bs) supposing (||v|| = ||Bs|| ∈ ℤ) ∧ (∀i:ℕ||v||. (v[i] ⊆r Bs[i]))
5. u1 : Type
6. v1 : Type List
7. ¬(v1 = [] ∈ (Type List))
8. tuple-type([u / v]) ⊆r tuple-type(v1) supposing (||[u / v]|| = ||v1|| ∈ ℤ) ∧ (∀i:ℕ||[u / v]||. ([u / v][i] ⊆r v1[i]))
9. ||[u / v]|| = ||[u1 / v1]|| ∈ ℤ
10. ∀i:ℕ||[u / v]||. ([u / v][i] ⊆r [u1 / v1][i])
11. u ⊆r u1
⊢ (u × tuple-type(v)) ⊆r (u1 × tuple-type(v1))
BY
{ (SubtypeReasoning THEN Auto THEN BackThruSomeHyp THEN Auto) }

1
1. u : Type
2. v : Type List
3. ¬(v = [] ∈ (Type List))
4. ∀[Bs:Type List]. tuple-type(v) ⊆r tuple-type(Bs) supposing (||v|| = ||Bs|| ∈ ℤ) ∧ (∀i:ℕ||v||. (v[i] ⊆r Bs[i]))
5. u1 : Type
6. v1 : Type List
7. ¬(v1 = [] ∈ (Type List))
8. tuple-type([u / v]) ⊆r tuple-type(v1) supposing (||[u / v]|| = ||v1|| ∈ ℤ) ∧ (∀i:ℕ||[u / v]||. ([u / v][i] ⊆r v1[i]))
9. ||[u / v]|| = ||[u1 / v1]|| ∈ ℤ
10. ∀i:ℕ||[u / v]||. ([u / v][i] ⊆r [u1 / v1][i])
11. u ⊆r u1
12. u
⊢ ||v|| = ||v1|| ∈ ℤ

2
1. u : Type
2. v : Type List
3. ¬(v = [] ∈ (Type List))
4. ∀[Bs:Type List]. tuple-type(v) ⊆r tuple-type(Bs) supposing (||v|| = ||Bs|| ∈ ℤ) ∧ (∀i:ℕ||v||. (v[i] ⊆r Bs[i]))
5. u1 : Type
6. v1 : Type List
7. ¬(v1 = [] ∈ (Type List))
8. tuple-type([u / v]) ⊆r tuple-type(v1) supposing (||[u / v]|| = ||v1|| ∈ ℤ) ∧ (∀i:ℕ||[u / v]||. ([u / v][i] ⊆r v1[i]))
9. ||[u / v]|| = ||[u1 / v1]|| ∈ ℤ
10. ∀i:ℕ||[u / v]||. ([u / v][i] ⊆r [u1 / v1][i])
11. u ⊆r u1
12. u
13. ||v|| = ||v1|| ∈ ℤ
14. i : ℕ||v||
⊢ v[i] ⊆r v1[i]

---

Latex:

---

Latex:

1.  u  :  Type
2.  v  :  Type  List
3.  \mneg{}(v  =  [])
4.  \mforall{}[Bs:Type  List]
          tuple-type(v)  \msubseteq{}r  tuple-type(Bs)  supposing  (||v||  =  ||Bs||)  \mwedge{}  (\mforall{}i:\mBbbN{}||v||.  (v[i]  \msubseteq{}r  Bs[i]))
5.  u1  :  Type
6.  v1  :  Type  List
7.  \mneg{}(v1  =  [])
8.  tuple-type([u  /  v])  \msubseteq{}r  tuple-type(v1) 
      supposing  (||[u  /  v]||  =  ||v1||)  \mwedge{}  (\mforall{}i:\mBbbN{}||[u  /  v]||.  ([u  /  v][i]  \msubseteq{}r  v1[i]))
9.  ||[u  /  v]||  =  ||[u1  /  v1]||
10.  \mforall{}i:\mBbbN{}||[u  /  v]||.  ([u  /  v][i]  \msubseteq{}r  [u1  /  v1][i])
11.  u  \msubseteq{}r  u1
\mvdash{}  (u  \mtimes{}  tuple-type(v))  \msubseteq{}r  (u1  \mtimes{}  tuple-type(v1))


By

---

Latex:
(SubtypeReasoning  THEN  Auto  THEN  BackThruSomeHyp  THEN  Auto)

---

Home Index