Step
*
1
2
2
of Lemma
fixpoint-induction-bottom
1. E : Type
2. S : Type
3. value-type(E)
4. mono(E)
5. ⊥ ∈ S
6. a : Base
7. b : Base
8. c : a = b ∈ (S ⟶ partial(E) × (S ⟶ S))
9. fst(a) ∈ S ⟶ partial(E)
10. fst(b) ∈ S ⟶ partial(E)
11. snd(a) ∈ S ⟶ S
12. snd(b) ∈ S ⟶ S
⊢ ((((fst(a)) fix((snd(a))))↓
⇐⇒ ((fst(b)) fix((snd(b))))↓)
∧ ((fst(a)) fix((snd(a)))) = ((fst(b)) fix((snd(b)))) ∈ E supposing ((fst(a)) fix((snd(a))))↓)
∧ (¬is-exception((fst(a)) fix((snd(a)))))
∧ (¬is-exception((fst(b)) fix((snd(b)))))
BY
{ TACTIC:D 0 }
1
1. E : Type
2. S : Type
3. value-type(E)
4. mono(E)
5. ⊥ ∈ S
6. a : Base
7. b : Base
8. c : a = b ∈ (S ⟶ partial(E) × (S ⟶ S))
9. fst(a) ∈ S ⟶ partial(E)
10. fst(b) ∈ S ⟶ partial(E)
11. snd(a) ∈ S ⟶ S
12. snd(b) ∈ S ⟶ S
⊢ (((fst(a)) fix((snd(a))))↓
⇐⇒ ((fst(b)) fix((snd(b))))↓)
∧ ((fst(a)) fix((snd(a)))) = ((fst(b)) fix((snd(b)))) ∈ E supposing ((fst(a)) fix((snd(a))))↓
2
1. E : Type
2. S : Type
3. value-type(E)
4. mono(E)
5. ⊥ ∈ S
6. a : Base
7. b : Base
8. c : a = b ∈ (S ⟶ partial(E) × (S ⟶ S))
9. fst(a) ∈ S ⟶ partial(E)
10. fst(b) ∈ S ⟶ partial(E)
11. snd(a) ∈ S ⟶ S
12. snd(b) ∈ S ⟶ S
⊢ (¬is-exception((fst(a)) fix((snd(a))))) ∧ (¬is-exception((fst(b)) fix((snd(b)))))
Latex:
Latex:
1. E : Type
2. S : Type
3. value-type(E)
4. mono(E)
5. \mbot{} \mmember{} S
6. a : Base
7. b : Base
8. c : a = b
9. fst(a) \mmember{} S {}\mrightarrow{} partial(E)
10. fst(b) \mmember{} S {}\mrightarrow{} partial(E)
11. snd(a) \mmember{} S {}\mrightarrow{} S
12. snd(b) \mmember{} S {}\mrightarrow{} S
\mvdash{} ((((fst(a)) fix((snd(a))))\mdownarrow{} \mLeftarrow{}{}\mRightarrow{} ((fst(b)) fix((snd(b))))\mdownarrow{})
\mwedge{} ((fst(a)) fix((snd(a)))) = ((fst(b)) fix((snd(b)))) supposing ((fst(a)) fix((snd(a))))\mdownarrow{})
\mwedge{} (\mneg{}is-exception((fst(a)) fix((snd(a)))))
\mwedge{} (\mneg{}is-exception((fst(b)) fix((snd(b)))))
By
Latex:
TACTIC:D 0
Home
Index