Step
*
1
1
2
1
2
2
1
of Lemma
fps-Pascal-iff
1. r : CRng
2. x : Atom
3. y : Atom
4. f : PowerSeries(r)
5. ¬(x = y ∈ Atom)
6. b : bag(Atom)
7. (+r (-r (f ({y} + b))) (+r (-r (f ({x} + b))) (f (({x} + {y}) + b))))
= (+r (-r 0) (+r 0 (+r 0 (+r (-r 0) (-r 0)))))
∈ |r|
⊢ (f (({x} + {y}) + b)) = ((f ({x} + b)) +r (f ({y} + b))) ∈ |r|
BY
{ TACTIC:TACTIC:(Fold `infix_ap` (-1) THEN (RW RngNormC (-1) THENA Auto)) }
1
1. r : CRng
2. x : Atom
3. y : Atom
4. f : PowerSeries(r)
5. ¬(x = y ∈ Atom)
6. b : bag(Atom)
7. ((f (({x} + {y}) + b)) +r ((-r (f ({x} + b))) +r (-r (f ({y} + b))))) = 0 ∈ |r|
⊢ (f (({x} + {y}) + b)) = ((f ({x} + b)) +r (f ({y} + b))) ∈ |r|
Latex:
Latex:
1. r : CRng
2. x : Atom
3. y : Atom
4. f : PowerSeries(r)
5. \mneg{}(x = y)
6. b : bag(Atom)
7. (+r (-r (f (\{y\} + b))) (+r (-r (f (\{x\} + b))) (f ((\{x\} + \{y\}) + b))))
= (+r (-r 0) (+r 0 (+r 0 (+r (-r 0) (-r 0)))))
\mvdash{} (f ((\{x\} + \{y\}) + b)) = ((f (\{x\} + b)) +r (f (\{y\} + b)))
By
Latex:
TACTIC:TACTIC:(Fold `infix\_ap` (-1) THEN (RW RngNormC (-1) THENA Auto))
Home
Index