Step
*
1
2
of Lemma
one_ideal_wf
.....set predicate.....
1. r : CRng
⊢ λu.True Ideal of r
BY
{ ((Unfold `ideal_p` 0 THEN Reduce 0) THEN Auto) }
1
1. r : CRng
⊢ λu.True SubGrp of r↓+gp
Latex:
Latex:
.....set predicate.....
1. r : CRng
\mvdash{} \mlambda{}u.True Ideal of r
By
Latex:
((Unfold `ideal\_p` 0 THEN Reduce 0) THEN Auto)
Home
Index