---

Step * 2 1 1 1 1 of Lemma rng-pps_wf


1. r : IntegDom{i}@i'
2. eq : EqDecider(|r|)
3. m : ℕ3 ⟶ |r|@i
4. ¬(m = 0 ∈ (ℕ3 ⟶ |r|))
5. l : ℕ3 ⟶ |r|@i
6. ¬(l = 0 ∈ (ℕ3 ⟶ |r|))
7. p : ℕ3 ⟶ |r|@i
8. ¬(p = 0 ∈ (ℕ3 ⟶ |r|))
9. q : ℕ3 ⟶ |r|@i
10. ¬(q = 0 ∈ (ℕ3 ⟶ |r|))
11. (p . l) = 0 ∈ |r|
12. (q . l) = 0 ∈ |r|
13. (p . m) = 0 ∈ |r|
14. (q . m) = 0 ∈ |r|
15. l1 : ℕ3 ⟶ |r|@i
16. ¬(l1 = 0 ∈ (ℕ3 ⟶ |r|))
17. (p . l1) = 0 ∈ |r|
18. ¬((q . l1) = 0 ∈ |r|)
19. a : ℕ3 ⟶ |r|@i
20. ¬(a = 0 ∈ (ℕ3 ⟶ |r|))
21. (a . l) = 0 ∈ |r|
22. ¬((a . m) = 0 ∈ |r|)
23. ∀x,y:|r|.  Dec(x = y ∈ |r|)
24. ¬((p x q) = 0 ∈ (ℕ3 ⟶ |r|))
25. ¬((l x m) = 0 ∈ (ℕ3 ⟶ |r|))
⊢ False
BY
{ Assert ⌜((l x (p x q)) = 0 ∈ (ℕ3 ⟶ |r|)) ∧ ((m x (p x q)) = 0 ∈ (ℕ3 ⟶ |r|))⌝⋅ }

1
.....assertion..... 
1. r : IntegDom{i}@i'
2. eq : EqDecider(|r|)
3. m : ℕ3 ⟶ |r|@i
4. ¬(m = 0 ∈ (ℕ3 ⟶ |r|))
5. l : ℕ3 ⟶ |r|@i
6. ¬(l = 0 ∈ (ℕ3 ⟶ |r|))
7. p : ℕ3 ⟶ |r|@i
8. ¬(p = 0 ∈ (ℕ3 ⟶ |r|))
9. q : ℕ3 ⟶ |r|@i
10. ¬(q = 0 ∈ (ℕ3 ⟶ |r|))
11. (p . l) = 0 ∈ |r|
12. (q . l) = 0 ∈ |r|
13. (p . m) = 0 ∈ |r|
14. (q . m) = 0 ∈ |r|
15. l1 : ℕ3 ⟶ |r|@i
16. ¬(l1 = 0 ∈ (ℕ3 ⟶ |r|))
17. (p . l1) = 0 ∈ |r|
18. ¬((q . l1) = 0 ∈ |r|)
19. a : ℕ3 ⟶ |r|@i
20. ¬(a = 0 ∈ (ℕ3 ⟶ |r|))
21. (a . l) = 0 ∈ |r|
22. ¬((a . m) = 0 ∈ |r|)
23. ∀x,y:|r|.  Dec(x = y ∈ |r|)
24. ¬((p x q) = 0 ∈ (ℕ3 ⟶ |r|))
25. ¬((l x m) = 0 ∈ (ℕ3 ⟶ |r|))
⊢ ((l x (p x q)) = 0 ∈ (ℕ3 ⟶ |r|)) ∧ ((m x (p x q)) = 0 ∈ (ℕ3 ⟶ |r|))

2
1. r : IntegDom{i}@i'
2. eq : EqDecider(|r|)
3. m : ℕ3 ⟶ |r|@i
4. ¬(m = 0 ∈ (ℕ3 ⟶ |r|))
5. l : ℕ3 ⟶ |r|@i
6. ¬(l = 0 ∈ (ℕ3 ⟶ |r|))
7. p : ℕ3 ⟶ |r|@i
8. ¬(p = 0 ∈ (ℕ3 ⟶ |r|))
9. q : ℕ3 ⟶ |r|@i
10. ¬(q = 0 ∈ (ℕ3 ⟶ |r|))
11. (p . l) = 0 ∈ |r|
12. (q . l) = 0 ∈ |r|
13. (p . m) = 0 ∈ |r|
14. (q . m) = 0 ∈ |r|
15. l1 : ℕ3 ⟶ |r|@i
16. ¬(l1 = 0 ∈ (ℕ3 ⟶ |r|))
17. (p . l1) = 0 ∈ |r|
18. ¬((q . l1) = 0 ∈ |r|)
19. a : ℕ3 ⟶ |r|@i
20. ¬(a = 0 ∈ (ℕ3 ⟶ |r|))
21. (a . l) = 0 ∈ |r|
22. ¬((a . m) = 0 ∈ |r|)
23. ∀x,y:|r|.  Dec(x = y ∈ |r|)
24. ¬((p x q) = 0 ∈ (ℕ3 ⟶ |r|))
25. ¬((l x m) = 0 ∈ (ℕ3 ⟶ |r|))
26. ((l x (p x q)) = 0 ∈ (ℕ3 ⟶ |r|)) ∧ ((m x (p x q)) = 0 ∈ (ℕ3 ⟶ |r|))
⊢ False

---

Latex:

---

Latex:

1.  r  :  IntegDom\{i\}@i'
2.  eq  :  EqDecider(|r|)
3.  m  :  \mBbbN{}3  {}\mrightarrow{}  |r|@i
4.  \mneg{}(m  =  0)
5.  l  :  \mBbbN{}3  {}\mrightarrow{}  |r|@i
6.  \mneg{}(l  =  0)
7.  p  :  \mBbbN{}3  {}\mrightarrow{}  |r|@i
8.  \mneg{}(p  =  0)
9.  q  :  \mBbbN{}3  {}\mrightarrow{}  |r|@i
10.  \mneg{}(q  =  0)
11.  (p  .  l)  =  0
12.  (q  .  l)  =  0
13.  (p  .  m)  =  0
14.  (q  .  m)  =  0
15.  l1  :  \mBbbN{}3  {}\mrightarrow{}  |r|@i
16.  \mneg{}(l1  =  0)
17.  (p  .  l1)  =  0
18.  \mneg{}((q  .  l1)  =  0)
19.  a  :  \mBbbN{}3  {}\mrightarrow{}  |r|@i
20.  \mneg{}(a  =  0)
21.  (a  .  l)  =  0
22.  \mneg{}((a  .  m)  =  0)
23.  \mforall{}x,y:|r|.    Dec(x  =  y)
24.  \mneg{}((p  x  q)  =  0)
25.  \mneg{}((l  x  m)  =  0)
\mvdash{}  False


By

---

Latex:
Assert  \mkleeneopen{}((l  x  (p  x  q))  =  0)  \mwedge{}  ((m  x  (p  x  q))  =  0)\mkleeneclose{}\mcdot{}

---

Home Index