Step
*
1
1
2
1
1
1
1
1
1
of Lemma
implies-k-1-continuous
1. k : ℕ
2. F : (ℕk ⟶ Type) ⟶ Type
3. ∀[A,B:ℕk ⟶ Type]. F[A] ⊆r F[B] supposing A ⊆ B
4. ∀j:ℕk. ∀Z:ℕk ⟶ Type. Continuous(X.F[λi.if (i =z j) then X else Z i fi ])
5. X : ℕ ⟶ ℕk ⟶ Type
6. ∀n:ℕ. X (n + 1) ⊆ X n
7. j : ℤ
8. 0 < j
9. (⋂n:ℕ. F[X n]) ⊆r (⋂n:ℕ. F[λi.if i <z j - 1 then ⋂n:ℕ. (X n i) else X n i fi ])
10. j ≤ k
11. ∀n:ℕ
((⋂m:ℕ. F[λi.if (i =z j - 1) then X m (j - 1) if i <z j - 1 then ⋂n:ℕ. (X n i) else X n i fi ]) ⊆r F[λi.if i <z j
then ⋂n:ℕ
(X
n
i)
else X n i
fi ])
12. (⋂n,m:ℕ. F[λi.if (i =z j - 1) then X m (j - 1) if i <z j - 1 then ⋂n:ℕ. (X n i) else X n i fi ])
⊆r (⋂n:ℕ. F[λi.if i <z j then ⋂n:ℕ. (X n i) else X n i fi ])
13. x : ⋂n:ℕ. F[λi.if i <z j - 1 then ⋂n:ℕ. (X n i) else X n i fi ]
14. n : ℕ
15. m : ℕ
⊢ x ∈ F[λi.if (i =z j - 1) then X m (j - 1)
if i <z j - 1 then ⋂n:ℕ. (X n i)
else X n i
fi ]
BY
{ ((Assert imax(n;m) ∈ ℕ BY
(RWO "imax_unfold" 0 THEN Auto))
THEN SubsumeC ⌜F[λi.if i <z j - 1 then ⋂n:ℕ. (X n i) else X imax(n;m) i fi ]⌝⋅
) }
1
1. k : ℕ
2. F : (ℕk ⟶ Type) ⟶ Type
3. ∀[A,B:ℕk ⟶ Type]. F[A] ⊆r F[B] supposing A ⊆ B
4. ∀j:ℕk. ∀Z:ℕk ⟶ Type. Continuous(X.F[λi.if (i =z j) then X else Z i fi ])
5. X : ℕ ⟶ ℕk ⟶ Type
6. ∀n:ℕ. X (n + 1) ⊆ X n
7. j : ℤ
8. 0 < j
9. (⋂n:ℕ. F[X n]) ⊆r (⋂n:ℕ. F[λi.if i <z j - 1 then ⋂n:ℕ. (X n i) else X n i fi ])
10. j ≤ k
11. ∀n:ℕ
((⋂m:ℕ. F[λi.if (i =z j - 1) then X m (j - 1) if i <z j - 1 then ⋂n:ℕ. (X n i) else X n i fi ]) ⊆r F[λi.if i <z j
then ⋂n:ℕ
(X
n
i)
else X n i
fi ])
12. (⋂n,m:ℕ. F[λi.if (i =z j - 1) then X m (j - 1) if i <z j - 1 then ⋂n:ℕ. (X n i) else X n i fi ])
⊆r (⋂n:ℕ. F[λi.if i <z j then ⋂n:ℕ. (X n i) else X n i fi ])
13. x : ⋂n:ℕ. F[λi.if i <z j - 1 then ⋂n:ℕ. (X n i) else X n i fi ]
14. n : ℕ
15. m : ℕ
16. imax(n;m) ∈ ℕ
⊢ x ∈ F[λi.if i <z j - 1 then ⋂n:ℕ. (X n i) else X imax(n;m) i fi ]
2
1. k : ℕ
2. F : (ℕk ⟶ Type) ⟶ Type
3. ∀[A,B:ℕk ⟶ Type]. F[A] ⊆r F[B] supposing A ⊆ B
4. ∀j:ℕk. ∀Z:ℕk ⟶ Type. Continuous(X.F[λi.if (i =z j) then X else Z i fi ])
5. X : ℕ ⟶ ℕk ⟶ Type
6. ∀n:ℕ. X (n + 1) ⊆ X n
7. j : ℤ
8. 0 < j
9. (⋂n:ℕ. F[X n]) ⊆r (⋂n:ℕ. F[λi.if i <z j - 1 then ⋂n:ℕ. (X n i) else X n i fi ])
10. j ≤ k
11. ∀n:ℕ
((⋂m:ℕ. F[λi.if (i =z j - 1) then X m (j - 1) if i <z j - 1 then ⋂n:ℕ. (X n i) else X n i fi ]) ⊆r F[λi.if i <z j
then ⋂n:ℕ
(X
n
i)
else X n i
fi ])
12. (⋂n,m:ℕ. F[λi.if (i =z j - 1) then X m (j - 1) if i <z j - 1 then ⋂n:ℕ. (X n i) else X n i fi ])
⊆r (⋂n:ℕ. F[λi.if i <z j then ⋂n:ℕ. (X n i) else X n i fi ])
13. x : ⋂n:ℕ. F[λi.if i <z j - 1 then ⋂n:ℕ. (X n i) else X n i fi ]
14. n : ℕ
15. m : ℕ
16. imax(n;m) ∈ ℕ
17. x = x ∈ F[λi.if i <z j - 1 then ⋂n:ℕ. (X n i) else X imax(n;m) i fi ]
⊢ F[λi.if i <z j - 1 then ⋂n:ℕ. (X n i) else X imax(n;m) i fi ] ⊆r F[λi.if (i =z j - 1) then X m (j - 1)
if i <z j - 1 then ⋂n:ℕ. (X n i)
else X n i
fi ]
Latex:
Latex:
1. k : \mBbbN{}
2. F : (\mBbbN{}k {}\mrightarrow{} Type) {}\mrightarrow{} Type
3. \mforall{}[A,B:\mBbbN{}k {}\mrightarrow{} Type]. F[A] \msubseteq{}r F[B] supposing A \msubseteq{} B
4. \mforall{}j:\mBbbN{}k. \mforall{}Z:\mBbbN{}k {}\mrightarrow{} Type. Continuous(X.F[\mlambda{}i.if (i =\msubz{} j) then X else Z i fi ])
5. X : \mBbbN{} {}\mrightarrow{} \mBbbN{}k {}\mrightarrow{} Type
6. \mforall{}n:\mBbbN{}. X (n + 1) \msubseteq{} X n
7. j : \mBbbZ{}
8. 0 < j
9. (\mcap{}n:\mBbbN{}. F[X n]) \msubseteq{}r (\mcap{}n:\mBbbN{}. F[\mlambda{}i.if i <z j - 1 then \mcap{}n:\mBbbN{}. (X n i) else X n i fi ])
10. j \mleq{} k
11. \mforall{}n:\mBbbN{}
((\mcap{}m:\mBbbN{}
F[\mlambda{}i.if (i =\msubz{} j - 1) then X m (j - 1)
if i <z j - 1 then \mcap{}n:\mBbbN{}. (X n i)
else X n i
fi ]) \msubseteq{}r F[\mlambda{}i.if i <z j then \mcap{}n:\mBbbN{}. (X n i) else X n i fi ])
12. (\mcap{}n,m:\mBbbN{}.
F[\mlambda{}i.if (i =\msubz{} j - 1) then X m (j - 1)
if i <z j - 1 then \mcap{}n:\mBbbN{}. (X n i)
else X n i
fi ]) \msubseteq{}r (\mcap{}n:\mBbbN{}. F[\mlambda{}i.if i <z j then \mcap{}n:\mBbbN{}. (X n i) else X n i fi ])
13. x : \mcap{}n:\mBbbN{}. F[\mlambda{}i.if i <z j - 1 then \mcap{}n:\mBbbN{}. (X n i) else X n i fi ]
14. n : \mBbbN{}
15. m : \mBbbN{}
\mvdash{} x \mmember{} F[\mlambda{}i.if (i =\msubz{} j - 1) then X m (j - 1)
if i <z j - 1 then \mcap{}n:\mBbbN{}. (X n i)
else X n i
fi ]
By
Latex:
((Assert imax(n;m) \mmember{} \mBbbN{} BY
(RWO "imax\_unfold" 0 THEN Auto))
THEN SubsumeC \mkleeneopen{}F[\mlambda{}i.if i <z j - 1 then \mcap{}n:\mBbbN{}. (X n i) else X imax(n;m) i fi ]\mkleeneclose{}\mcdot{}
)
Home
Index