---

Step * 1 1 3 of Lemma rng-pps_wf

.....subterm..... T:t
3:n
1. r : IntegDom{i}@i'
2. eq : EqDecider(|r|)
⊢ λa,l,m. if eq (a . m) 0 then inr <a, λnp.(np Ax), λ%6.Ax>  else inl (λ%.Ax) fi  ∈ ∀a:Point. ∀l:{l:Line| 
                                                                                        pgeo-plsep(rng-pp-primitives(r);
                                                                                                   a;
                                                                                                   l)} . ∀m:Line.
                                                                            (pgeo-plsep(rng-pp-primitives(r); a; m)
                                                                            ∨ m ≠ l)
BY
{ (UnfoldpGeoAbbreviations 0
   THEN RepeatFor 3 ((MemCD THENA Auto))
   THEN DSetVars
   THEN BoolCase ⌜eq (a . m) 0⌝⋅
   THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
3:n
1.  r  :  IntegDom\{i\}@i'
2.  eq  :  EqDecider(|r|)
\mvdash{}  \mlambda{}a,l,m.  if  eq  (a  .  m)  0  then  inr  <a,  \mlambda{}np.(np  Ax),  \mlambda{}\%6.Ax>    else  inl  (\mlambda{}\%.Ax)  fi 
    \mmember{}  \mforall{}a:Point.  \mforall{}l:\{l:Line|  pgeo-plsep(rng-pp-primitives(r);  a;  l)\}  .  \mforall{}m:Line.
            (pgeo-plsep(rng-pp-primitives(r);  a;  m)  \mvee{}  m  \mneq{}  l)


By

---

Latex:
(UnfoldpGeoAbbreviations  0
  THEN  RepeatFor  3  ((MemCD  THENA  Auto))
  THEN  DSetVars
  THEN  BoolCase  \mkleeneopen{}eq  (a  .  m)  0\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index