---

Step * 2 1 of Lemma sp-join_wf


1. f1 : Base
2. f : Base
3. f1 = f ∈ pertype(λf,g. ((f ∈ ℕ ⟶ 𝔹) ∧ (g ∈ ℕ ⟶ 𝔹) ∧ (f = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹))))
4. f1 ∈ ℕ ⟶ 𝔹
5. f ∈ ℕ ⟶ 𝔹
6. (f1 = ⊥ ∈ (ℕ ⟶ 𝔹)) ⇒ (f = ⊥ ∈ (ℕ ⟶ 𝔹))
7. (f1 = ⊥ ∈ (ℕ ⟶ 𝔹)) ⇐ f = ⊥ ∈ (ℕ ⟶ 𝔹)
8. g1 : Base
9. g : Base
10. g1 = g ∈ pertype(λf,g. ((f ∈ ℕ ⟶ 𝔹) ∧ (g ∈ ℕ ⟶ 𝔹) ∧ (f = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹))))
11. g1 ∈ ℕ ⟶ 𝔹
12. g ∈ ℕ ⟶ 𝔹
13. (g1 = ⊥ ∈ (ℕ ⟶ 𝔹)) ⇒ (g = ⊥ ∈ (ℕ ⟶ 𝔹))
14. (g1 = ⊥ ∈ (ℕ ⟶ 𝔹)) ⇐ g = ⊥ ∈ (ℕ ⟶ 𝔹)
15. (λn.((f n) ∨b(g n))) = ⊥ ∈ (ℕ ⟶ 𝔹)
⊢ (λn.((f1 n) ∨b(g1 n))) = ⊥ ∈ (ℕ ⟶ 𝔹)
BY
{ TACTIC:(Subst' f1 = ⊥ ∈ (ℕ ⟶ 𝔹) 0 THENA Auto) }

1
.....equality..... 
1. f1 : Base
2. f : Base
3. f1 = f ∈ pertype(λf,g. ((f ∈ ℕ ⟶ 𝔹) ∧ (g ∈ ℕ ⟶ 𝔹) ∧ (f = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹))))
4. f1 ∈ ℕ ⟶ 𝔹
5. f ∈ ℕ ⟶ 𝔹
6. (f1 = ⊥ ∈ (ℕ ⟶ 𝔹)) ⇒ (f = ⊥ ∈ (ℕ ⟶ 𝔹))
7. (f1 = ⊥ ∈ (ℕ ⟶ 𝔹)) ⇐ f = ⊥ ∈ (ℕ ⟶ 𝔹)
8. g1 : Base
9. g : Base
10. g1 = g ∈ pertype(λf,g. ((f ∈ ℕ ⟶ 𝔹) ∧ (g ∈ ℕ ⟶ 𝔹) ∧ (f = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹))))
11. g1 ∈ ℕ ⟶ 𝔹
12. g ∈ ℕ ⟶ 𝔹
13. (g1 = ⊥ ∈ (ℕ ⟶ 𝔹)) ⇒ (g = ⊥ ∈ (ℕ ⟶ 𝔹))
14. (g1 = ⊥ ∈ (ℕ ⟶ 𝔹)) ⇐ g = ⊥ ∈ (ℕ ⟶ 𝔹)
15. (λn.((f n) ∨b(g n))) = ⊥ ∈ (ℕ ⟶ 𝔹)
⊢ f1 = ⊥ ∈ (ℕ ⟶ 𝔹)

2
1. f1 : Base
2. f : Base
3. f1 = f ∈ pertype(λf,g. ((f ∈ ℕ ⟶ 𝔹) ∧ (g ∈ ℕ ⟶ 𝔹) ∧ (f = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹))))
4. f1 ∈ ℕ ⟶ 𝔹
5. f ∈ ℕ ⟶ 𝔹
6. (f1 = ⊥ ∈ (ℕ ⟶ 𝔹)) ⇒ (f = ⊥ ∈ (ℕ ⟶ 𝔹))
7. (f1 = ⊥ ∈ (ℕ ⟶ 𝔹)) ⇐ f = ⊥ ∈ (ℕ ⟶ 𝔹)
8. g1 : Base
9. g : Base
10. g1 = g ∈ pertype(λf,g. ((f ∈ ℕ ⟶ 𝔹) ∧ (g ∈ ℕ ⟶ 𝔹) ∧ (f = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹))))
11. g1 ∈ ℕ ⟶ 𝔹
12. g ∈ ℕ ⟶ 𝔹
13. (g1 = ⊥ ∈ (ℕ ⟶ 𝔹)) ⇒ (g = ⊥ ∈ (ℕ ⟶ 𝔹))
14. (g1 = ⊥ ∈ (ℕ ⟶ 𝔹)) ⇐ g = ⊥ ∈ (ℕ ⟶ 𝔹)
15. (λn.((f n) ∨b(g n))) = ⊥ ∈ (ℕ ⟶ 𝔹)
⊢ (λn.((⊥ n) ∨b(g1 n))) = ⊥ ∈ (ℕ ⟶ 𝔹)

---

Latex:

---

Latex:

1.  f1  :  Base
2.  f  :  Base
3.  f1  =  f
4.  f1  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
5.  f  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
6.  (f1  =  \mbot{})  {}\mRightarrow{}  (f  =  \mbot{})
7.  (f1  =  \mbot{})  \mLeftarrow{}{}  f  =  \mbot{}
8.  g1  :  Base
9.  g  :  Base
10.  g1  =  g
11.  g1  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
12.  g  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
13.  (g1  =  \mbot{})  {}\mRightarrow{}  (g  =  \mbot{})
14.  (g1  =  \mbot{})  \mLeftarrow{}{}  g  =  \mbot{}
15.  (\mlambda{}n.((f  n)  \mvee{}\msubb{}(g  n)))  =  \mbot{}
\mvdash{}  (\mlambda{}n.((f1  n)  \mvee{}\msubb{}(g1  n)))  =  \mbot{}


By

---

Latex:
TACTIC:(Subst'  f1  =  \mbot{}  0  THENA  Auto)

---

Home Index