Nuprl Definition : geo-extend
extend qa by bc ==
SCO(q;a;a;if M(O;X;a) then if M(a;O;b) then prop2-lemma(e;a;b;c) else prop2-lemma(e;a;O;prop2-lemma(e;O;b;c)) fi
if M(a;X;b) then prop2-lemma(e;a;b;c)
else prop2-lemma(e;a;X;prop2-lemma(e;X;b;c))
fi )
Definitions occuring in Statement :
prop2-lemma: prop2-lemma(e;a;b;c),
geo-X: X,
geo-O: O,
geo-SCO: SCO(a;b;c;d),
geo-M: M(a;b;c),
ifthenelse: if b then t else f fi
Definitions occuring in definition :
geo-SCO: SCO(a;b;c;d),
geo-O: O,
ifthenelse: if b then t else f fi ,
geo-M: M(a;b;c),
prop2-lemma: prop2-lemma(e;a;b;c),
geo-X: X
FDL editor aliases :
geo-extend
geo-extend
geo-extend
Latex:
extend qa by bc ==
SCO(q;a;a;if M(O;X;a)
then if M(a;O;b)
then prop2-lemma(e;a;b;c)
else prop2-lemma(e;a;O;prop2-lemma(e;O;b;c))
fi
if M(a;X;b) then prop2-lemma(e;a;b;c)
else prop2-lemma(e;a;X;prop2-lemma(e;X;b;c))
fi )
Date html generated:
2017_10_02-PM-04_50_26
Last ObjectModification:
2017_08_09-PM-06_38_13
Theory : euclidean!plane!geometry
Home
Index