---

Step * 1 of Lemma formal-sum-subtype


1. K : RngSig
2. S : Type
3. T : Type
4. S ⊆r T
5. a : basic-formal-sum(K;S)
6. b : basic-formal-sum(K;S)
7. bfs-equiv(K;S;a;b)
⊢ bfs-equiv(K;T;a;b)
BY
{ (InstLemma `bfs-equiv-implies` [⌜S⌝;⌜K⌝;⌜λa,b. bfs-equiv(K;T;a;b)⌝]⋅ THENA Auto) }

1
1. K : RngSig
2. S : Type
3. T : Type
4. S ⊆r T
5. a : basic-formal-sum(K;S)
6. b : basic-formal-sum(K;S)
7. bfs-equiv(K;S;a;b)
8. x : basic-formal-sum(K;S)
9. y : basic-formal-sum(K;S)
10. bfs-reduce(K;S;x;y)
⊢ (λa,b. bfs-equiv(K;T;a;b)) x y

2
.....antecedent..... 
1. K : RngSig
2. S : Type
3. T : Type
4. S ⊆r T
5. a : basic-formal-sum(K;S)
6. b : basic-formal-sum(K;S)
7. bfs-equiv(K;S;a;b)
⊢ EquivRel(basic-formal-sum(K;S);x,y.(λa,b. bfs-equiv(K;T;a;b)) x y)

3
1. K : RngSig
2. S : Type
3. T : Type
4. S ⊆r T
5. a : basic-formal-sum(K;S)
6. b : basic-formal-sum(K;S)
7. bfs-equiv(K;S;a;b)
8. ∀x,y:basic-formal-sum(K;S).  (bfs-equiv(K;S;x;y) ⇒ ((λa,b. bfs-equiv(K;T;a;b)) x y))
⊢ bfs-equiv(K;T;a;b)

---

Latex:

---

Latex:

1.  K  :  RngSig
2.  S  :  Type
3.  T  :  Type
4.  S  \msubseteq{}r  T
5.  a  :  basic-formal-sum(K;S)
6.  b  :  basic-formal-sum(K;S)
7.  bfs-equiv(K;S;a;b)
\mvdash{}  bfs-equiv(K;T;a;b)


By

---

Latex:
(InstLemma  `bfs-equiv-implies`  [\mkleeneopen{}S\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}\mlambda{}a,b.  bfs-equiv(K;T;a;b)\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index