Step
*
1
1
1
of Lemma
Q-R-pre-preserving-conditional
1. es : EO@i'
2. [P1] : E ─→ ℙ
3. [P2] : E ─→ ℙ
4. [Q1] : E ─→ E ─→ ℙ
5. [R1] : E ─→ E ─→ ℙ
6. [Q2] : E ─→ E ─→ ℙ
7. [R2] : E ─→ E ─→ ℙ
8. dcd_P1 : e:E ─→ Dec(P1 e)@i
9. f1 : {e:E| P1 e} ─→ E@i
10. f2 : {e:E| P2 e} ─→ E@i
11. ∀e,e':{e:E| P1 e} . (¬(Q2 (f1 e) (f1 e')))
12. ∀e,e':{e:E| P2 e} . (¬(Q1 (f2 e) (f2 e')))
13. ∀e:{e:E| P1 e} . ∀e':{e:E| P2 e} .
((¬(Q1 (f1 e) (f2 e'))) ∧ (¬(Q1 (f2 e') (f1 e))) ∧ (¬(Q2 (f1 e) (f2 e'))) ∧ (¬(Q2 (f2 e') (f1 e))))
14. ∀e,e':{e:E| P1 e} . ((Q1 (f1 e) (f1 e')) ⇒ (R1 e e'))@i
15. ∀e,e':{e:E| P2 e} . ((Q2 (f2 e) (f2 e')) ⇒ (R2 e e'))@i
16. e : {e:E| (P1 e) ∨ (P2 e)} @i
17. e' : {e:E| (P1 e) ∨ (P2 e)} @i
18. (Q1 ∨ Q2) if p:P1 e then f1 e else f2 e fi if p:P1 e' then f1 e' else f2 e' fi @i
⊢ (R1 ∨ R2) e e'
BY
{ RepeatFor 2 (((Branch (-1)) THENA ((D -1 THEN Reduce 0) THEN DSetVars THEN Auto THEN SplitOrHyps THEN Auto))) }
1
1. es : EO@i'
2. [P1] : E ─→ ℙ
3. [P2] : E ─→ ℙ
4. [Q1] : E ─→ E ─→ ℙ
5. [R1] : E ─→ E ─→ ℙ
6. [Q2] : E ─→ E ─→ ℙ
7. [R2] : E ─→ E ─→ ℙ
8. dcd_P1 : e:E ─→ Dec(P1 e)@i
9. f1 : {e:E| P1 e} ─→ E@i
10. f2 : {e:E| P2 e} ─→ E@i
11. ∀e,e':{e:E| P1 e} . (¬(Q2 (f1 e) (f1 e')))
12. ∀e,e':{e:E| P2 e} . (¬(Q1 (f2 e) (f2 e')))
13. ∀e:{e:E| P1 e} . ∀e':{e:E| P2 e} .
((¬(Q1 (f1 e) (f2 e'))) ∧ (¬(Q1 (f2 e') (f1 e))) ∧ (¬(Q2 (f1 e) (f2 e'))) ∧ (¬(Q2 (f2 e') (f1 e))))
14. ∀e,e':{e:E| P1 e} . ((Q1 (f1 e) (f1 e')) ⇒ (R1 e e'))@i
15. ∀e,e':{e:E| P2 e} . ((Q2 (f2 e) (f2 e')) ⇒ (R2 e e'))@i
16. e : {e:E| (P1 e) ∨ (P2 e)} @i
17. e' : {e:E| (P1 e) ∨ (P2 e)} @i
18. x : P1 e
19. (dcd_P1 e) = (inl x) ∈ Dec(P1 e)
20. x1 : P1 e'
21. (dcd_P1 e') = (inl x1) ∈ Dec(P1 e')
22. (Q1 ∨ Q2) (f1 e) (f1 e')
⊢ (R1 ∨ R2) e e'
2
1. es : EO@i'
2. [P1] : E ─→ ℙ
3. [P2] : E ─→ ℙ
4. [Q1] : E ─→ E ─→ ℙ
5. [R1] : E ─→ E ─→ ℙ
6. [Q2] : E ─→ E ─→ ℙ
7. [R2] : E ─→ E ─→ ℙ
8. dcd_P1 : e:E ─→ Dec(P1 e)@i
9. f1 : {e:E| P1 e} ─→ E@i
10. f2 : {e:E| P2 e} ─→ E@i
11. ∀e,e':{e:E| P1 e} . (¬(Q2 (f1 e) (f1 e')))
12. ∀e,e':{e:E| P2 e} . (¬(Q1 (f2 e) (f2 e')))
13. ∀e:{e:E| P1 e} . ∀e':{e:E| P2 e} .
((¬(Q1 (f1 e) (f2 e'))) ∧ (¬(Q1 (f2 e') (f1 e))) ∧ (¬(Q2 (f1 e) (f2 e'))) ∧ (¬(Q2 (f2 e') (f1 e))))
14. ∀e,e':{e:E| P1 e} . ((Q1 (f1 e) (f1 e')) ⇒ (R1 e e'))@i
15. ∀e,e':{e:E| P2 e} . ((Q2 (f2 e) (f2 e')) ⇒ (R2 e e'))@i
16. e : {e:E| (P1 e) ∨ (P2 e)} @i
17. e' : {e:E| (P1 e) ∨ (P2 e)} @i
18. x : P1 e
19. (dcd_P1 e) = (inl x) ∈ Dec(P1 e)
20. y : ¬(P1 e')
21. (dcd_P1 e') = (inr y ) ∈ Dec(P1 e')
22. (Q1 ∨ Q2) (f1 e) (f2 e')
⊢ (R1 ∨ R2) e e'
3
1. es : EO@i'
2. [P1] : E ─→ ℙ
3. [P2] : E ─→ ℙ
4. [Q1] : E ─→ E ─→ ℙ
5. [R1] : E ─→ E ─→ ℙ
6. [Q2] : E ─→ E ─→ ℙ
7. [R2] : E ─→ E ─→ ℙ
8. dcd_P1 : e:E ─→ Dec(P1 e)@i
9. f1 : {e:E| P1 e} ─→ E@i
10. f2 : {e:E| P2 e} ─→ E@i
11. ∀e,e':{e:E| P1 e} . (¬(Q2 (f1 e) (f1 e')))
12. ∀e,e':{e:E| P2 e} . (¬(Q1 (f2 e) (f2 e')))
13. ∀e:{e:E| P1 e} . ∀e':{e:E| P2 e} .
((¬(Q1 (f1 e) (f2 e'))) ∧ (¬(Q1 (f2 e') (f1 e))) ∧ (¬(Q2 (f1 e) (f2 e'))) ∧ (¬(Q2 (f2 e') (f1 e))))
14. ∀e,e':{e:E| P1 e} . ((Q1 (f1 e) (f1 e')) ⇒ (R1 e e'))@i
15. ∀e,e':{e:E| P2 e} . ((Q2 (f2 e) (f2 e')) ⇒ (R2 e e'))@i
16. e : {e:E| (P1 e) ∨ (P2 e)} @i
17. e' : {e:E| (P1 e) ∨ (P2 e)} @i
18. y : ¬(P1 e)
19. (dcd_P1 e) = (inr y ) ∈ Dec(P1 e)
20. x : P1 e'
21. (dcd_P1 e') = (inl x) ∈ Dec(P1 e')
22. (Q1 ∨ Q2) (f2 e) (f1 e')
⊢ (R1 ∨ R2) e e'
4
1. es : EO@i'
2. [P1] : E ─→ ℙ
3. [P2] : E ─→ ℙ
4. [Q1] : E ─→ E ─→ ℙ
5. [R1] : E ─→ E ─→ ℙ
6. [Q2] : E ─→ E ─→ ℙ
7. [R2] : E ─→ E ─→ ℙ
8. dcd_P1 : e:E ─→ Dec(P1 e)@i
9. f1 : {e:E| P1 e} ─→ E@i
10. f2 : {e:E| P2 e} ─→ E@i
11. ∀e,e':{e:E| P1 e} . (¬(Q2 (f1 e) (f1 e')))
12. ∀e,e':{e:E| P2 e} . (¬(Q1 (f2 e) (f2 e')))
13. ∀e:{e:E| P1 e} . ∀e':{e:E| P2 e} .
((¬(Q1 (f1 e) (f2 e'))) ∧ (¬(Q1 (f2 e') (f1 e))) ∧ (¬(Q2 (f1 e) (f2 e'))) ∧ (¬(Q2 (f2 e') (f1 e))))
14. ∀e,e':{e:E| P1 e} . ((Q1 (f1 e) (f1 e')) ⇒ (R1 e e'))@i
15. ∀e,e':{e:E| P2 e} . ((Q2 (f2 e) (f2 e')) ⇒ (R2 e e'))@i
16. e : {e:E| (P1 e) ∨ (P2 e)} @i
17. e' : {e:E| (P1 e) ∨ (P2 e)} @i
18. y : ¬(P1 e)
19. (dcd_P1 e) = (inr y ) ∈ Dec(P1 e)
20. y1 : ¬(P1 e')
21. (dcd_P1 e') = (inr y1 ) ∈ Dec(P1 e')
22. (Q1 ∨ Q2) (f2 e) (f2 e')
⊢ (R1 ∨ R2) e e'
Latex:
1. es : EO@i'
2. [P1] : E {}\mrightarrow{} \mBbbP{}
3. [P2] : E {}\mrightarrow{} \mBbbP{}
4. [Q1] : E {}\mrightarrow{} E {}\mrightarrow{} \mBbbP{}
5. [R1] : E {}\mrightarrow{} E {}\mrightarrow{} \mBbbP{}
6. [Q2] : E {}\mrightarrow{} E {}\mrightarrow{} \mBbbP{}
7. [R2] : E {}\mrightarrow{} E {}\mrightarrow{} \mBbbP{}
8. dcd$_{P1}$ : e:E {}\mrightarrow{} Dec(P1 e)@i
9. f1 : \{e:E| P1 e\} {}\mrightarrow{} E@i
10. f2 : \{e:E| P2 e\} {}\mrightarrow{} E@i
11. \mforall{}e,e':\{e:E| P1 e\} . (\mneg{}(Q2 (f1 e) (f1 e')))
12. \mforall{}e,e':\{e:E| P2 e\} . (\mneg{}(Q1 (f2 e) (f2 e')))
13. \mforall{}e:\{e:E| P1 e\} . \mforall{}e':\{e:E| P2 e\} .
((\mneg{}(Q1 (f1 e) (f2 e')))
\mwedge{} (\mneg{}(Q1 (f2 e') (f1 e)))
\mwedge{} (\mneg{}(Q2 (f1 e) (f2 e')))
\mwedge{} (\mneg{}(Q2 (f2 e') (f1 e))))
14. \mforall{}e,e':\{e:E| P1 e\} . ((Q1 (f1 e) (f1 e')) {}\mRightarrow{} (R1 e e'))@i
15. \mforall{}e,e':\{e:E| P2 e\} . ((Q2 (f2 e) (f2 e')) {}\mRightarrow{} (R2 e e'))@i
16. e : \{e:E| (P1 e) \mvee{} (P2 e)\} @i
17. e' : \{e:E| (P1 e) \mvee{} (P2 e)\} @i
18. (Q1 \mvee{} Q2) if p:P1 e then f1 e else f2 e fi if p:P1 e' then f1 e' else f2 e' fi @i
\mvdash{} (R1 \mvee{} R2) e e'
By
RepeatFor 2 (((Branch (-1))
THENA ((D -1 THEN Reduce 0) THEN DSetVars THEN Auto THEN SplitOrHyps THEN Auto)
))
Home
Index