Step
*
1
of Lemma
stream-lex-monotonic
1. T : Type
2. ∀x,y:T. Dec(x = y ∈ T)
3. R : T ⟶ T ⟶ ℙ
4. Trans(T;x,y.x R y)
5. AntiSym(T;x,y.x R y)
6. f : T ⟶ T ⟶ T
7. ∀x,y,u,v:T. ((x R y) ⇒ (u R v) ⇒ ((f x u) R (f y v)))
8. ∀x,y,u,v:T. ((x R y) ⇒ (u R v) ⇒ (¬((x = y ∈ T) ∧ (u = v ∈ T))) ⇒ (¬((f x u) = (f y v) ∈ T)))
9. a : stream(T)
10. b : stream(T)
11. c : stream(T)
12. d : stream(T)
13. a stream-lex(T;R) b
14. c stream-lex(T;R) d
15. ∀R':stream(T) ⟶ stream(T) ⟶ ℙ
(R' => λs1,s2. ((s-hd(s1) R s-hd(s2)) ∧ ((s-hd(s1) = s-hd(s2) ∈ T) ⇒ (s-tl(s1) R' s-tl(s2)))) ⇒ R' => stream-lex\000C(T;R))
⊢ stream-zip(f;a;c) stream-lex(T;R) stream-zip(f;b;d)
BY
{ (InstHyp [⌜λs1,s2. ∃a,b,c,d:stream(T)
((s1 = stream-zip(f;a;c) ∈ stream(T))
∧ (s2 = stream-zip(f;b;d) ∈ stream(T))
∧ (a stream-lex(T;R) b)
∧ (c stream-lex(T;R) d))⌝] (-1)⋅
THEN Auto
) }
1
.....antecedent.....
1. T : Type
2. ∀x,y:T. Dec(x = y ∈ T)
3. R : T ⟶ T ⟶ ℙ
4. Trans(T;x,y.x R y)
5. AntiSym(T;x,y.x R y)
6. f : T ⟶ T ⟶ T
7. ∀x,y,u,v:T. ((x R y) ⇒ (u R v) ⇒ ((f x u) R (f y v)))
8. ∀x,y,u,v:T. ((x R y) ⇒ (u R v) ⇒ (¬((x = y ∈ T) ∧ (u = v ∈ T))) ⇒ (¬((f x u) = (f y v) ∈ T)))
9. a : stream(T)
10. b : stream(T)
11. c : stream(T)
12. d : stream(T)
13. a stream-lex(T;R) b
14. c stream-lex(T;R) d
15. ∀R':stream(T) ⟶ stream(T) ⟶ ℙ
(R' => λs1,s2. ((s-hd(s1) R s-hd(s2)) ∧ ((s-hd(s1) = s-hd(s2) ∈ T) ⇒ (s-tl(s1) R' s-tl(s2)))) ⇒ R' => stream-lex\000C(T;R))
⊢ λs1,s2. ∃a,b,c,d:stream(T)
((s1 = stream-zip(f;a;c) ∈ stream(T))
∧ (s2 = stream-zip(f;b;d) ∈ stream(T))
∧ (a stream-lex(T;R) b)
∧ (c stream-lex(T;R) d)) => λs1,s2. ((s-hd(s1) R s-hd(s2))
∧ ((s-hd(s1) = s-hd(s2) ∈ T)
⇒ (s-tl(s1)
(λs1,s2. ∃a,b,c,d:stream(T)
((s1 = stream-zip(f;a;c) ∈ stream(T))
∧ (s2 = stream-zip(f;b;d) ∈ stream(T))
∧ (a stream-lex(T;R) b)
∧ (c stream-lex(T;R) d)))
s-tl(s2))))
2
1. T : Type
2. ∀x,y:T. Dec(x = y ∈ T)
3. R : T ⟶ T ⟶ ℙ
4. Trans(T;x,y.x R y)
5. AntiSym(T;x,y.x R y)
6. f : T ⟶ T ⟶ T
7. ∀x,y,u,v:T. ((x R y) ⇒ (u R v) ⇒ ((f x u) R (f y v)))
8. ∀x,y,u,v:T. ((x R y) ⇒ (u R v) ⇒ (¬((x = y ∈ T) ∧ (u = v ∈ T))) ⇒ (¬((f x u) = (f y v) ∈ T)))
9. a : stream(T)
10. b : stream(T)
11. c : stream(T)
12. d : stream(T)
13. a stream-lex(T;R) b
14. c stream-lex(T;R) d
15. ∀R':stream(T) ⟶ stream(T) ⟶ ℙ
(R' => λs1,s2. ((s-hd(s1) R s-hd(s2)) ∧ ((s-hd(s1) = s-hd(s2) ∈ T) ⇒ (s-tl(s1) R' s-tl(s2)))) ⇒ R' => stream-lex\000C(T;R))
16. λs1,s2. ∃a,b,c,d:stream(T)
((s1 = stream-zip(f;a;c) ∈ stream(T))
∧ (s2 = stream-zip(f;b;d) ∈ stream(T))
∧ (a stream-lex(T;R) b)
∧ (c stream-lex(T;R) d)) => stream-lex(T;R)
⊢ stream-zip(f;a;c) stream-lex(T;R) stream-zip(f;b;d)
Latex:
Latex:
1. T : Type
2. \mforall{}x,y:T. Dec(x = y)
3. R : T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}
4. Trans(T;x,y.x R y)
5. AntiSym(T;x,y.x R y)
6. f : T {}\mrightarrow{} T {}\mrightarrow{} T
7. \mforall{}x,y,u,v:T. ((x R y) {}\mRightarrow{} (u R v) {}\mRightarrow{} ((f x u) R (f y v)))
8. \mforall{}x,y,u,v:T. ((x R y) {}\mRightarrow{} (u R v) {}\mRightarrow{} (\mneg{}((x = y) \mwedge{} (u = v))) {}\mRightarrow{} (\mneg{}((f x u) = (f y v))))
9. a : stream(T)
10. b : stream(T)
11. c : stream(T)
12. d : stream(T)
13. a stream-lex(T;R) b
14. c stream-lex(T;R) d
15. \mforall{}R':stream(T) {}\mrightarrow{} stream(T) {}\mrightarrow{} \mBbbP{}
(R' => \mlambda{}s1,s2. ((s-hd(s1) R s-hd(s2)) \mwedge{} ((s-hd(s1) = s-hd(s2)) {}\mRightarrow{} (s-tl(s1) R' s-tl(s2))))
{}\mRightarrow{} R' => stream-lex(T;R))
\mvdash{} stream-zip(f;a;c) stream-lex(T;R) stream-zip(f;b;d)
By
Latex:
(InstHyp [\mkleeneopen{}\mlambda{}s1,s2. \mexists{}a,b,c,d:stream(T)
((s1 = stream-zip(f;a;c))
\mwedge{} (s2 = stream-zip(f;b;d))
\mwedge{} (a stream-lex(T;R) b)
\mwedge{} (c stream-lex(T;R) d))\mkleeneclose{}] (-1)\mcdot{}
THEN Auto
)
Home
Index