Step
*
2
1
2
1
2
1
2
of Lemma
es-hist-is-concat
1. [Info] : Type
2. es : EO+(Info)@i'
3. LL : Info List@i
4. L1 : Info List List@i
5. ∀e1,e2:E.
∀L:Info List
(∃f:ℕ||L1|| + 1 ─→ E
((((f 0) = e1 ∈ E) ∧ f ||L1|| ≤loc e2 )
c∧ (∀i:ℕ||L1||. (f i <loc f (i + 1)))
c∧ ((∀i:ℕ||L1||. (es-hist(es;f i;pred(f (i + 1))) = L1[i] ∈ (Info List)))
∧ (es-hist(es;f ||L1||;e2) = L ∈ (Info List))))) supposing
((es-hist(es;e1;e2) = (concat(L1) @ L) ∈ (Info List)) and
(¬(L = [] ∈ (Info List))) and
(∀L∈L1.¬(L = [] ∈ (Info List))))
supposing loc(e1) = loc(e2) ∈ Id@i
6. e1 : E@i
7. e2 : E@i
8. loc(e1) = loc(e2) ∈ Id
9. L : Info List@i
10. (∀L∈[LL / L1].¬(L = [] ∈ (Info List)))
11. ¬(L = [] ∈ (Info List))
12. es-hist(es;e1;e2) = (LL @ concat(L1) @ L) ∈ (Info List)
13. e : E
14. (e1 <loc e)
15. e ≤loc e2
16. es-hist(es;e1;pred(e)) = LL ∈ (Info List)
17. es-hist(es;e;e2) = (concat(L1) @ L) ∈ (Info List)
18. f : ℕ||L1|| + 1 ─→ E
19. (f 0) = e ∈ E
20. f ||L1|| ≤loc e2
21. ∀i:ℕ||L1||. (f i <loc f (i + 1))
22. ∀i:ℕ||L1||. (es-hist(es;f i;pred(f (i + 1))) = L1[i] ∈ (Info List))
23. es-hist(es;f ||L1||;e2) = L ∈ (Info List)
⊢ ((((λx.if (x =z 0) then e1 else f (x - 1) fi ) 0) = e1 ∈ E)
∧ (λx.if (x =z 0) then e1 else f (x - 1) fi ) ||[LL / L1]|| ≤loc e2 )
c∧ (∀i:ℕ||[LL / L1]||
((λx.if (x =z 0) then e1 else f (x - 1) fi ) i <loc (λx.if (x =z 0) then e1 else f (x - 1) fi ) (i + 1)))
c∧ ((∀i:ℕ||[LL / L1]||
(es-hist(es;(λx.if (x =z 0) then e1 else f (x - 1) fi ) i;pred((λx.if (x =z 0) then e1 else f (x - 1) fi )
(i + 1)))
= [LL / L1][i]
∈ (Info List)))
∧ (es-hist(es;(λx.if (x =z 0) then e1 else f (x - 1) fi ) ||[LL / L1]||;e2) = L ∈ (Info List)))
BY
{ Reduce 0 }
1
1. [Info] : Type
2. es : EO+(Info)@i'
3. LL : Info List@i
4. L1 : Info List List@i
5. ∀e1,e2:E.
∀L:Info List
(∃f:ℕ||L1|| + 1 ─→ E
((((f 0) = e1 ∈ E) ∧ f ||L1|| ≤loc e2 )
c∧ (∀i:ℕ||L1||. (f i <loc f (i + 1)))
c∧ ((∀i:ℕ||L1||. (es-hist(es;f i;pred(f (i + 1))) = L1[i] ∈ (Info List)))
∧ (es-hist(es;f ||L1||;e2) = L ∈ (Info List))))) supposing
((es-hist(es;e1;e2) = (concat(L1) @ L) ∈ (Info List)) and
(¬(L = [] ∈ (Info List))) and
(∀L∈L1.¬(L = [] ∈ (Info List))))
supposing loc(e1) = loc(e2) ∈ Id@i
6. e1 : E@i
7. e2 : E@i
8. loc(e1) = loc(e2) ∈ Id
9. L : Info List@i
10. (∀L∈[LL / L1].¬(L = [] ∈ (Info List)))
11. ¬(L = [] ∈ (Info List))
12. es-hist(es;e1;e2) = (LL @ concat(L1) @ L) ∈ (Info List)
13. e : E
14. (e1 <loc e)
15. e ≤loc e2
16. es-hist(es;e1;pred(e)) = LL ∈ (Info List)
17. es-hist(es;e;e2) = (concat(L1) @ L) ∈ (Info List)
18. f : ℕ||L1|| + 1 ─→ E
19. (f 0) = e ∈ E
20. f ||L1|| ≤loc e2
21. ∀i:ℕ||L1||. (f i <loc f (i + 1))
22. ∀i:ℕ||L1||. (es-hist(es;f i;pred(f (i + 1))) = L1[i] ∈ (Info List))
23. es-hist(es;f ||L1||;e2) = L ∈ (Info List)
⊢ ((e1 = e1 ∈ E) ∧ if (||L1|| + 1 =z 0) then e1 else f ((||L1|| + 1) - 1) fi ≤loc e2 )
c∧ (∀i:ℕ||L1|| + 1. (if (i =z 0) then e1 else f (i - 1) fi <loc if (i + 1 =z 0) then e1 else f ((i + 1) - 1) fi ))
c∧ ((∀i:ℕ||L1|| + 1
(es-hist(es;if (i =z 0) then e1 else f (i - 1) fi ;pred(if (i + 1 =z 0) then e1 else f ((i + 1) - 1) fi ))
= [LL / L1][i]
∈ (Info List)))
∧ (es-hist(es;if (||L1|| + 1 =z 0) then e1 else f ((||L1|| + 1) - 1) fi ;e2) = L ∈ (Info List)))
Latex:
1. [Info] : Type
2. es : EO+(Info)@i'
3. LL : Info List@i
4. L1 : Info List List@i
5. \mforall{}e1,e2:E.
\mforall{}L:Info List
(\mexists{}f:\mBbbN{}||L1|| + 1 {}\mrightarrow{} E
((((f 0) = e1) \mwedge{} f ||L1|| \mleq{}loc e2 )
c\mwedge{} (\mforall{}i:\mBbbN{}||L1||. (f i <loc f (i + 1)))
c\mwedge{} ((\mforall{}i:\mBbbN{}||L1||. (es-hist(es;f i;pred(f (i + 1))) = L1[i]))
\mwedge{} (es-hist(es;f ||L1||;e2) = L)))) supposing
((es-hist(es;e1;e2) = (concat(L1) @ L)) and
(\mneg{}(L = [])) and
(\mforall{}L\mmember{}L1.\mneg{}(L = [])))
supposing loc(e1) = loc(e2)@i
6. e1 : E@i
7. e2 : E@i
8. loc(e1) = loc(e2)
9. L : Info List@i
10. (\mforall{}L\mmember{}[LL / L1].\mneg{}(L = []))
11. \mneg{}(L = [])
12. es-hist(es;e1;e2) = (LL @ concat(L1) @ L)
13. e : E
14. (e1 <loc e)
15. e \mleq{}loc e2
16. es-hist(es;e1;pred(e)) = LL
17. es-hist(es;e;e2) = (concat(L1) @ L)
18. f : \mBbbN{}||L1|| + 1 {}\mrightarrow{} E
19. (f 0) = e
20. f ||L1|| \mleq{}loc e2
21. \mforall{}i:\mBbbN{}||L1||. (f i <loc f (i + 1))
22. \mforall{}i:\mBbbN{}||L1||. (es-hist(es;f i;pred(f (i + 1))) = L1[i])
23. es-hist(es;f ||L1||;e2) = L
\mvdash{} ((((\mlambda{}x.if (x =\msubz{} 0) then e1 else f (x - 1) fi ) 0) = e1)
\mwedge{} (\mlambda{}x.if (x =\msubz{} 0) then e1 else f (x - 1) fi ) ||[LL / L1]|| \mleq{}loc e2 )
c\mwedge{} (\mforall{}i:\mBbbN{}||[LL / L1]||
((\mlambda{}x.if (x =\msubz{} 0) then e1 else f (x - 1) fi ) i <loc (\mlambda{}x.if (x =\msubz{} 0)
then e1
else f (x - 1)
fi )
(i + 1)))
c\mwedge{} ((\mforall{}i:\mBbbN{}||[LL / L1]||
(es-hist(es;(\mlambda{}x.if (x =\msubz{} 0) then e1 else f (x - 1) fi ) i;pred((\mlambda{}x.if (x =\msubz{} 0)
then e1
else f (x - 1)
fi )
(i + 1)))
= [LL / L1][i]))
\mwedge{} (es-hist(es;(\mlambda{}x.if (x =\msubz{} 0) then e1 else f (x - 1) fi ) ||[LL / L1]||;e2) = L))
By
Reduce 0
Home
Index