Step
*
1
1
of Lemma
fpf-normalize-ap
.....equality.....
1. A : Type
2. eq : EqDecider(A)
3. B : A ─→ Type
4. d : A List
5. g1 : x:{x:A| (x ∈ d)} ─→ B[x]
6. x : A
7. ↑x ∈ dom(<d, g1>)
⊢ snd(reduce(λx,f. <[x / filter(λa.(¬b((eqof(eq) x a) ∨bff));fst(f))]
, λa.if (eqof(eq) x a) ∨bff then g1 x else (snd(f)) a fi
>;<[], λx.⋅>;d)) ~ reduce(λx,f,a. if (eqof(eq) x a) ∨bff then g1 x else f a fi ;λx.⋅;d)
BY
{ ((GenConcl ⌈g1 = G ∈ Top⌉⋅ THENA Auto) THEN (Thin (-1))) }
1
1. A : Type
2. eq : EqDecider(A)
3. B : A ─→ Type
4. d : A List
5. g1 : x:{x:A| (x ∈ d)} ─→ B[x]
6. x : A
7. ↑x ∈ dom(<d, g1>)
8. G : Top@i
⊢ snd(reduce(λx,f. <[x / filter(λa.(¬b((eqof(eq) x a) ∨bff));fst(f))]
, λa.if (eqof(eq) x a) ∨bff then G x else (snd(f)) a fi
>;<[], λx.⋅>;d)) ~ reduce(λx,f,a. if (eqof(eq) x a) ∨bff then G x else f a fi ;λx.⋅;d)
Latex:
.....equality.....
1. A : Type
2. eq : EqDecider(A)
3. B : A {}\mrightarrow{} Type
4. d : A List
5. g1 : x:\{x:A| (x \mmember{} d)\} {}\mrightarrow{} B[x]
6. x : A
7. \muparrow{}x \mmember{} dom(<d, g1>)
\mvdash{} snd(reduce(\mlambda{}x,f. <[x / filter(\mlambda{}a.(\mneg{}\msubb{}((eqof(eq) x a) \mvee{}\msubb{}ff));fst(f))]
, \mlambda{}a.if (eqof(eq) x a) \mvee{}\msubb{}ff then g1 x else (snd(f)) a fi
><[], \mlambda{}x.\mcdot{}>d)) \msim{} reduce(\mlambda{}x,f,a. if (eqof(eq) x a) \mvee{}\msubb{}ff then g1 x else f a fi ;\mlambda{}\000Cx.\mcdot{};d)
By
((GenConcl \mkleeneopen{}g1 = G\mkleeneclose{}\mcdot{} THENA Auto) THEN (Thin (-1)))
Home
Index