Nuprl Definition : new-evd-proof
new-evd-proof(exname;sequent;evd)
==r let rule,subevd = NewEvdProofStep(exname;sequent;evd)
in let sr ⟵ <sequent, rule>
in let subgoals ⟵ outl(FOLeffect(sr))
in eval n = ||subgoals|| in
if n=0
then <sr, []>
else let s1 ⟵ subgoals[0]
in let evd1 ⟵ subevd[0]
in eval p1 = new-evd-proof(exname;s1;evd1) in
if n=1
then <sr, [p1]>
else let s2 ⟵ subgoals[1]
in let evd2 ⟵ subevd[1]
in eval p2 = new-evd-proof(exname;s2;evd2) in
if n=2
then <sr, [p1; p2]>
else let LL ⟵ tl(tl(upto(n)))
in eval L = map(λi.new-evd-proof(exname;subgoals[i];subevd[i]);LL) in
<sr, [p1; [p2 / L]]>
new-evd-proof(exname;sequent;evd) ==
fix((λnew-evd-proof,sequent,evd. let rule,subevd = NewEvdProofStep(exname;sequent;evd)
in let sr ⟵ <sequent, rule>
in let subgoals ⟵ outl(FOLeffect(sr))
in eval n = ||subgoals|| in
if n=0
then <sr, []>
else let s1 ⟵ subgoals[0]
in let evd1 ⟵ subevd[0]
in eval p1 = new-evd-proof s1 evd1 in
if n=1
then <sr, [p1]>
else let s2 ⟵ subgoals[1]
in let evd2 ⟵ subevd[1]
in eval p2 = new-evd-proof s2 evd2 in
if n=2
then <sr, [p1; p2]>
else let LL ⟵ tl(tl(upto(n)))
in eval L = map(λi.(new-evd-proof
subgoals[i]
subevd[i]);LL) in
<sr, [p1; [p2 / L]]>))
sequent
evd
Definitions occuring in Statement :
new-evd-proof-step: NewEvdProofStep(exname;sequent;evd),
FOLeffect: FOLeffect(sr),
upto: upto(n),
select: L[n],
length: ||as||,
map: map(f;as),
tl: tl(l),
cons: [a / b],
nil: [],
callbyvalueall: callbyvalueall,
callbyvalue: callbyvalue,
outl: outl(x),
int_eq: if a=b then c else d,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
natural_number: $n
Definitions occuring in definition :
cons: [a / b],
pair: <a, b>,
select: L[n],
apply: f a,
lambda: λx.A[x],
map: map(f;as),
callbyvalue: callbyvalue,
upto: upto(n),
tl: tl(l),
callbyvalueall: callbyvalueall,
nil: [],
natural_number: $n,
int_eq: if a=b then c else d,
length: ||as||,
FOLeffect: FOLeffect(sr),
outl: outl(x),
new-evd-proof-step: NewEvdProofStep(exname;sequent;evd),
spread: spread def,
fix: fix(F)
FDL editor aliases :
new-evd-proof
new-evd-proof
new-evd-proof
new-evd-proof
new-evd-proof
new-evd-proof
Latex:
new-evd-proof(exname;sequent;evd)
==r let rule,subevd = NewEvdProofStep(exname;sequent;evd)
in let sr \mleftarrow{}{} <sequent, rule>
in let subgoals \mleftarrow{}{} outl(FOLeffect(sr))
in eval n = ||subgoals|| in
if n=0
then <sr, []>
else let s1 \mleftarrow{}{} subgoals[0]
in let evd1 \mleftarrow{}{} subevd[0]
in eval p1 = new-evd-proof(exname;s1;evd1) in
if n=1
then <sr, [p1]>
else let s2 \mleftarrow{}{} subgoals[1]
in let evd2 \mleftarrow{}{} subevd[1]
in eval p2 = new-evd-proof(exname;s2;evd2) in
if n=2
then <sr, [p1; p2]>
else let LL \mleftarrow{}{} tl(tl(upto(n)))
in eval L = map(...;LL) in
<sr, [p1; [p2 / L]]>
Latex:
new-evd-proof(exname;sequent;evd) ==
fix((\mlambda{}new-evd-proof,sequent,evd.
let rule,subevd = NewEvdProofStep(exname;sequent;evd)
in let sr \mleftarrow{}{} <sequent, rule>
in let subgoals \mleftarrow{}{} outl(FOLeffect(sr))
in eval n = ||subgoals|| in
if n=0
then <sr, []>
else let s1 \mleftarrow{}{} subgoals[0]
in let evd1 \mleftarrow{}{} subevd[0]
in eval p1 = new-evd-proof s1 evd1 in
if n=1
then <sr, [p1]>
else let s2 \mleftarrow{}{} subgoals[1]
in let evd2 \mleftarrow{}{} subevd[1]
in eval p2 = new-evd-proof s2
evd2 in
if n=2
then <sr, [p1; p2]>
else let LL \mleftarrow{}{}
tl(tl(upto(n)))
in eval L = ... in
<sr
, [p1; [p2 / L]]
>))
sequent
evd
Date html generated:
2017_01_19-PM-02_32_33
Last ObjectModification:
2017_01_19-AM-10_07_46
Theory : minimal-first-order-logic
Home
Index