---

Step * of Lemma sp-meet_wf

∀[f,g:Sierpinski].  (f ∧ g ∈ Sierpinski)
BY
{ (Auto
   THEN D 1
   THEN D -1
   THEN Unfold `sp-meet` 0
   THEN EqTypeCD
   THEN Auto
   THEN ((RWO "equal-Sierpinski-bottom" 0 THENA Auto) THEN Reduce 0)
   THEN (RWO "equal-Sierpinski-bottom" (-1) THENA Auto)
   THEN Reduce (-1)
   THEN Auto
   THEN (GenConclTerm ⌜coded-pair(n)⌝⋅ THENA Auto)
   THEN ThinVar `n'
   THEN D -1
   THEN RenameVar `i' (-2)
   THEN RenameVar `j' (-1)
   THEN Reduce 0
   THEN (D 0 THENA Auto)) }

1
1. f : Base
2. f1 : Base
3. f = f1 ∈ (f,g:ℕ ⟶ 𝔹//(f = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹)))
4. f ∈ ℕ ⟶ 𝔹
5. f1 ∈ ℕ ⟶ 𝔹
6. (f = ⊥ ∈ (ℕ ⟶ 𝔹)) ⇒ (f1 = ⊥ ∈ (ℕ ⟶ 𝔹))
7. (f = ⊥ ∈ (ℕ ⟶ 𝔹)) ⇐ f1 = ⊥ ∈ (ℕ ⟶ 𝔹)
8. g : Base
9. g1 : Base
10. g = g1 ∈ (f,g:ℕ ⟶ 𝔹//(f = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹)))
11. g ∈ ℕ ⟶ 𝔹
12. g1 ∈ ℕ ⟶ 𝔹
13. (g = ⊥ ∈ (ℕ ⟶ 𝔹)) ⇒ (g1 = ⊥ ∈ (ℕ ⟶ 𝔹))
14. (g = ⊥ ∈ (ℕ ⟶ 𝔹)) ⇐ g1 = ⊥ ∈ (ℕ ⟶ 𝔹)
15. ∀n:ℕ. (¬↑let x,y = coded-pair(n) in (f x) ∧b (g y))
16. i : ℕ
17. j : ℕ
18. ↑((f1 i) ∧b (g1 j))
⊢ False

2
1. f : Base
2. f1 : Base
3. f = f1 ∈ (f,g:ℕ ⟶ 𝔹//(f = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹)))
4. f ∈ ℕ ⟶ 𝔹
5. f1 ∈ ℕ ⟶ 𝔹
6. (f = ⊥ ∈ (ℕ ⟶ 𝔹)) ⇒ (f1 = ⊥ ∈ (ℕ ⟶ 𝔹))
7. (f = ⊥ ∈ (ℕ ⟶ 𝔹)) ⇐ f1 = ⊥ ∈ (ℕ ⟶ 𝔹)
8. g : Base
9. g1 : Base
10. g = g1 ∈ (f,g:ℕ ⟶ 𝔹//(f = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹)))
11. g ∈ ℕ ⟶ 𝔹
12. g1 ∈ ℕ ⟶ 𝔹
13. (g = ⊥ ∈ (ℕ ⟶ 𝔹)) ⇒ (g1 = ⊥ ∈ (ℕ ⟶ 𝔹))
14. (g = ⊥ ∈ (ℕ ⟶ 𝔹)) ⇐ g1 = ⊥ ∈ (ℕ ⟶ 𝔹)
15. ∀n:ℕ. (¬↑let x,y = coded-pair(n) in (f1 x) ∧b (g1 y))
16. i : ℕ
17. j : ℕ
18. ↑((f i) ∧b (g j))
⊢ False

---

Latex:

---

Latex:
\mforall{}[f,g:Sierpinski].    (f  \mwedge{}  g  \mmember{}  Sierpinski)


By

---

Latex:
(Auto
  THEN  D  1
  THEN  D  -1
  THEN  Unfold  `sp-meet`  0
  THEN  EqTypeCD
  THEN  Auto
  THEN  ((RWO  "equal-Sierpinski-bottom"  0  THENA  Auto)  THEN  Reduce  0)
  THEN  (RWO  "equal-Sierpinski-bottom"  (-1)  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  Auto
  THEN  (GenConclTerm  \mkleeneopen{}coded-pair(n)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVar  `n'
  THEN  D  -1
  THEN  RenameVar  `i'  (-2)
  THEN  RenameVar  `j'  (-1)
  THEN  Reduce  0
  THEN  (D  0  THENA  Auto))

---

Home Index