Step
*
1
1
1
4
1
1
2
of Lemma
face-of-face-pairity
1. k : ℕ
2. a : ℚCube(k)
3. b : ℚCube(k)
4. c : ℚCube(k)
5. 1 < dim(c)
6. immediate-rc-face(k;a;b)
7. immediate-rc-face(k;b;c)
8. i1 : ℕk
9. dim(b i1) = 1 ∈ ℤ
10. ∀j:ℕk. ((¬(j = i1 ∈ ℤ)) ⇒ ((a j) = (b j) ∈ ℚInterval))
11. ((a i1) = [fst((b i1))] ∈ ℚInterval) ∨ ((a i1) = [snd((b i1))] ∈ ℚInterval)
12. i : ℕk
13. dim(c i) = 1 ∈ ℤ
14. ∀j:ℕk. ((¬(j = i ∈ ℤ)) ⇒ ((b j) = (c j) ∈ ℚInterval))
15. ((b i) = [fst((c i))] ∈ ℚInterval) ∨ ((b i) = [snd((c i))] ∈ ℚInterval)
16. dim(a) = (dim(c) - 2) ∈ ℤ
17. ↑Inhabited(a)
18. dim(b) = (dim(c) - 1) ∈ ℤ
19. ↑Inhabited(b)
20. ↑Inhabited(c)
21. λj.if (j =z i1) then a i1 else c j fi ∈ ℚCube(k)
22. ↑Inhabited(λj.if (j =z i1) then a i1 else c j fi )
23. ¬(i1 = i ∈ ℤ)
24. dim(λj.if (j =z i1) then a i1 else c j fi ) = (dim(c) - 1) ∈ ℤ
25. immediate-rc-face(k;a;λj.if (j =z i1) then a i1 else c j fi )
26. immediate-rc-face(k;λj.if (j =z i1) then a i1 else c j fi ;c)
27. ¬((λj.if (j =z i1) then a i1 else c j fi ) = b ∈ ℚCube(k))
28. y : ℚCube(k)
29. immediate-rc-face(k;a;y)
30. immediate-rc-face(k;y;c)
31. ¬(y = b ∈ ℚCube(k))
32. i3 : ℕk
33. dim(y i3) = 1 ∈ ℤ
34. ∀j:ℕk. ((¬(j = i3 ∈ ℤ)) ⇒ ((a j) = (y j) ∈ ℚInterval))
35. ((a i3) = [fst((y i3))] ∈ ℚInterval) ∨ ((a i3) = [snd((y i3))] ∈ ℚInterval)
36. i2 : ℕk
37. dim(c i2) = 1 ∈ ℤ
38. ∀j:ℕk. ((¬(j = i2 ∈ ℤ)) ⇒ ((y j) = (c j) ∈ ℚInterval))
39. ((y i2) = [fst((c i2))] ∈ ℚInterval) ∨ ((y i2) = [snd((c i2))] ∈ ℚInterval)
40. ¬(i2 = i3 ∈ ℤ)
41. ((i2 = i ∈ ℤ) ∨ (i2 = i1 ∈ ℤ)) ∧ ((i3 = i ∈ ℤ) ∨ (i3 = i1 ∈ ℤ))
⊢ y = (λj.if (j =z i1) then a i1 else c j fi ) ∈ ℚCube(k)
BY
{ (D -1
THEN D -2
THEN D -1
THEN ((D -3 THEN Eq) ORELSE (Eliminate ⌜i2⌝⋅ THEN Eliminate ⌜i3⌝⋅ THEN RepeatFor 2 (Thin (-1))))) }
1
1. k : ℕ
2. i1 : ℕk
3. i : ℕk
4. a : ℚCube(k)
5. b : ℚCube(k)
6. c : ℚCube(k)
7. 1 < dim(c)
8. immediate-rc-face(k;a;b)
9. immediate-rc-face(k;b;c)
10. dim(b i1) = 1 ∈ ℤ
11. ∀j:ℕk. ((¬(j = i1 ∈ ℤ)) ⇒ ((a j) = (b j) ∈ ℚInterval))
12. ((a i1) = [fst((b i1))] ∈ ℚInterval) ∨ ((a i1) = [snd((b i1))] ∈ ℚInterval)
13. dim(c i) = 1 ∈ ℤ
14. ∀j:ℕk. ((¬(j = i ∈ ℤ)) ⇒ ((b j) = (c j) ∈ ℚInterval))
15. ((b i) = [fst((c i))] ∈ ℚInterval) ∨ ((b i) = [snd((c i))] ∈ ℚInterval)
16. dim(a) = (dim(c) - 2) ∈ ℤ
17. ↑Inhabited(a)
18. dim(b) = (dim(c) - 1) ∈ ℤ
19. ↑Inhabited(b)
20. ↑Inhabited(c)
21. λj.if (j =z i1) then a i1 else c j fi ∈ ℚCube(k)
22. ↑Inhabited(λj.if (j =z i1) then a i1 else c j fi )
23. ¬(i1 = i ∈ ℤ)
24. dim(λj.if (j =z i1) then a i1 else c j fi ) = (dim(c) - 1) ∈ ℤ
25. immediate-rc-face(k;a;λj.if (j =z i1) then a i1 else c j fi )
26. immediate-rc-face(k;λj.if (j =z i1) then a i1 else c j fi ;c)
27. ¬((λj.if (j =z i1) then a i1 else c j fi ) = b ∈ ℚCube(k))
28. y : ℚCube(k)
29. immediate-rc-face(k;a;y)
30. immediate-rc-face(k;y;c)
31. ¬(y = b ∈ ℚCube(k))
32. i3 : ℕk
33. dim(y i1) = 1 ∈ ℤ
34. ∀j:ℕk. ((¬(j = i1 ∈ ℤ)) ⇒ ((a j) = (y j) ∈ ℚInterval))
35. ((a i1) = [fst((y i1))] ∈ ℚInterval) ∨ ((a i1) = [snd((y i1))] ∈ ℚInterval)
36. i2 : ℕk
37. dim(c i) = 1 ∈ ℤ
38. ∀j:ℕk. ((¬(j = i ∈ ℤ)) ⇒ ((y j) = (c j) ∈ ℚInterval))
39. ((y i) = [fst((c i))] ∈ ℚInterval) ∨ ((y i) = [snd((c i))] ∈ ℚInterval)
40. ¬(i = i1 ∈ ℤ)
⊢ y = (λj.if (j =z i1) then a i1 else c j fi ) ∈ ℚCube(k)
2
1. k : ℕ
2. i : ℕk
3. i1 : ℕk
4. a : ℚCube(k)
5. b : ℚCube(k)
6. c : ℚCube(k)
7. 1 < dim(c)
8. immediate-rc-face(k;a;b)
9. immediate-rc-face(k;b;c)
10. dim(b i1) = 1 ∈ ℤ
11. ∀j:ℕk. ((¬(j = i1 ∈ ℤ)) ⇒ ((a j) = (b j) ∈ ℚInterval))
12. ((a i1) = [fst((b i1))] ∈ ℚInterval) ∨ ((a i1) = [snd((b i1))] ∈ ℚInterval)
13. dim(c i) = 1 ∈ ℤ
14. ∀j:ℕk. ((¬(j = i ∈ ℤ)) ⇒ ((b j) = (c j) ∈ ℚInterval))
15. ((b i) = [fst((c i))] ∈ ℚInterval) ∨ ((b i) = [snd((c i))] ∈ ℚInterval)
16. dim(a) = (dim(c) - 2) ∈ ℤ
17. ↑Inhabited(a)
18. dim(b) = (dim(c) - 1) ∈ ℤ
19. ↑Inhabited(b)
20. ↑Inhabited(c)
21. λj.if (j =z i1) then a i1 else c j fi ∈ ℚCube(k)
22. ↑Inhabited(λj.if (j =z i1) then a i1 else c j fi )
23. ¬(i1 = i ∈ ℤ)
24. dim(λj.if (j =z i1) then a i1 else c j fi ) = (dim(c) - 1) ∈ ℤ
25. immediate-rc-face(k;a;λj.if (j =z i1) then a i1 else c j fi )
26. immediate-rc-face(k;λj.if (j =z i1) then a i1 else c j fi ;c)
27. ¬((λj.if (j =z i1) then a i1 else c j fi ) = b ∈ ℚCube(k))
28. y : ℚCube(k)
29. immediate-rc-face(k;a;y)
30. immediate-rc-face(k;y;c)
31. ¬(y = b ∈ ℚCube(k))
32. i3 : ℕk
33. dim(y i) = 1 ∈ ℤ
34. ∀j:ℕk. ((¬(j = i ∈ ℤ)) ⇒ ((a j) = (y j) ∈ ℚInterval))
35. ((a i) = [fst((y i))] ∈ ℚInterval) ∨ ((a i) = [snd((y i))] ∈ ℚInterval)
36. i2 : ℕk
37. dim(c i1) = 1 ∈ ℤ
38. ∀j:ℕk. ((¬(j = i1 ∈ ℤ)) ⇒ ((y j) = (c j) ∈ ℚInterval))
39. ((y i1) = [fst((c i1))] ∈ ℚInterval) ∨ ((y i1) = [snd((c i1))] ∈ ℚInterval)
40. ¬(i1 = i ∈ ℤ)
⊢ y = (λj.if (j =z i1) then a i1 else c j fi ) ∈ ℚCube(k)
Latex:
Latex:
1. k : \mBbbN{}
2. a : \mBbbQ{}Cube(k)
3. b : \mBbbQ{}Cube(k)
4. c : \mBbbQ{}Cube(k)
5. 1 < dim(c)
6. immediate-rc-face(k;a;b)
7. immediate-rc-face(k;b;c)
8. i1 : \mBbbN{}k
9. dim(b i1) = 1
10. \mforall{}j:\mBbbN{}k. ((\mneg{}(j = i1)) {}\mRightarrow{} ((a j) = (b j)))
11. ((a i1) = [fst((b i1))]) \mvee{} ((a i1) = [snd((b i1))])
12. i : \mBbbN{}k
13. dim(c i) = 1
14. \mforall{}j:\mBbbN{}k. ((\mneg{}(j = i)) {}\mRightarrow{} ((b j) = (c j)))
15. ((b i) = [fst((c i))]) \mvee{} ((b i) = [snd((c i))])
16. dim(a) = (dim(c) - 2)
17. \muparrow{}Inhabited(a)
18. dim(b) = (dim(c) - 1)
19. \muparrow{}Inhabited(b)
20. \muparrow{}Inhabited(c)
21. \mlambda{}j.if (j =\msubz{} i1) then a i1 else c j fi \mmember{} \mBbbQ{}Cube(k)
22. \muparrow{}Inhabited(\mlambda{}j.if (j =\msubz{} i1) then a i1 else c j fi )
23. \mneg{}(i1 = i)
24. dim(\mlambda{}j.if (j =\msubz{} i1) then a i1 else c j fi ) = (dim(c) - 1)
25. immediate-rc-face(k;a;\mlambda{}j.if (j =\msubz{} i1) then a i1 else c j fi )
26. immediate-rc-face(k;\mlambda{}j.if (j =\msubz{} i1) then a i1 else c j fi ;c)
27. \mneg{}((\mlambda{}j.if (j =\msubz{} i1) then a i1 else c j fi ) = b)
28. y : \mBbbQ{}Cube(k)
29. immediate-rc-face(k;a;y)
30. immediate-rc-face(k;y;c)
31. \mneg{}(y = b)
32. i3 : \mBbbN{}k
33. dim(y i3) = 1
34. \mforall{}j:\mBbbN{}k. ((\mneg{}(j = i3)) {}\mRightarrow{} ((a j) = (y j)))
35. ((a i3) = [fst((y i3))]) \mvee{} ((a i3) = [snd((y i3))])
36. i2 : \mBbbN{}k
37. dim(c i2) = 1
38. \mforall{}j:\mBbbN{}k. ((\mneg{}(j = i2)) {}\mRightarrow{} ((y j) = (c j)))
39. ((y i2) = [fst((c i2))]) \mvee{} ((y i2) = [snd((c i2))])
40. \mneg{}(i2 = i3)
41. ((i2 = i) \mvee{} (i2 = i1)) \mwedge{} ((i3 = i) \mvee{} (i3 = i1))
\mvdash{} y = (\mlambda{}j.if (j =\msubz{} i1) then a i1 else c j fi )
By
Latex:
(D -1
THEN D -2
THEN D -1
THEN ((D -3 THEN Eq) ORELSE (Eliminate \mkleeneopen{}i2\mkleeneclose{}\mcdot{} THEN Eliminate \mkleeneopen{}i3\mkleeneclose{}\mcdot{} THEN RepeatFor 2 (Thin (-1)))))
Home
Index