Nuprl Definition : FOLeffect

FOLeffect(sr) ==
  let s,r = sr
  in let hyps,concl = s
     in case(r)
        andI => let a,b = dest-"and"(concl) in
                inl [<hyps, a>; <hyps, b>]
        impI => let a,b = dest-"imp"(concl) in
                inl [<[a / hyps], b>]

        allI with v => if ¬_bv ∈_b mFOL-sequent-freevars(<hyps, concl>) then let x,b = dest-all(concl); in inl [<hyps, b[v\000C/x]>] else inr ⋅  fi

        existsI with v => if v ∈_b mFOL-sequent-freevars(<hyps, concl>) then let x,b = dest-exists(concl); in inl [<hyps,\000C b[v/x]>] else inr ⋅  fi

        orI (left?x) => let a,b = dest-"or"(concl) in
                        inl [<hyps, if x then a else b fi >]
        hyp => if concl ∈_b hyps then inl [] else inr ⋅  fi

        andE @i => if i <z ||hyps|| then let a,b = dest-"and"(hyps[i]) in inl [<[a; [b / hyps]], concl>] else inr ⋅  fi

        orE @i => if i <z ||hyps|| then let a,b = dest-"or"(hyps[i]) in inl [<[a / hyps], concl>; <[b / hyps], concl>] e\000Clse inr ⋅  fi

        impE @i => if i <z ||hyps|| then let a,b = dest-"imp"(hyps[i]) in inl [<hyps, a>; <[b / hyps], concl>] else inr \000C⋅  fi

        allE @i with v => if i <z ||hyps|| ∧_b v ∈_b mFOL-sequent-freevars(<hyps, concl>)
                          then let x,b = dest-all(hyps[i]); in
                                inl [<[b[v/x] / hyps], concl>]
                          else inr ⋅
                          fi

        existsE @i with v => if i <z ||hyps|| ∧_b (¬_bv ∈_b mFOL-sequent-freevars(<hyps, concl>))

                             then let x,b = dest-exists(hyps[i]); in
                                   inl [<[b[v/x] / hyps], concl>]
                             else inr ⋅
                             fi
        falseE @i => if i <z ||hyps||
                     then let n,vars = dest-atomic(hyps[i]) in

                          if n =a "false" ∧_b null(vars) then inl [] else inr ⋅  fi

else inr ⋅
fi

Definitions occuring in Statement : mFOL-sequent-freevars: mFOL-sequent-freevars(s), FOLRule_ind: FOLRule_ind, FOL-subst: fmla[nw/old], deq-mFO: deq-mFO(), mFO-dest-quantifier: mFO-dest-quantifier, mFO-dest-connective: mFO-dest-connective, mFO-dest-atomic: mFO-dest-atomic, select: L[n], length: ||as||, null: null(as), deq-member: x ∈_b L, cons: [a / b], nil: [], int-deq: IntDeq, band: p ∧_b q, bnot: ¬_bb, ifthenelse: if b then t else f fi , eq_atom: x =a y, lt_int: i <z j, bfalse: ff, btrue: tt, it: ⋅, spread: spread def, pair: <a, b>, inr: inr x , inl: inl x, token: "$token"
Definitions occuring in definition : cons: [a / b], pair: <a, b>, inl: inl x, token: "$token", select: L[n], mFO-dest-connective: mFO-dest-connective, length: ||as||, lt_int: i <z j, ifthenelse: if b then t else f fi , it: ⋅, inr: inr x , nil: [], deq-mFO: deq-mFO(), deq-member: x ∈_b L, FOL-subst: fmla[nw/old], bfalse: ff, mFO-dest-quantifier: mFO-dest-quantifier, mFOL-sequent-freevars: mFOL-sequent-freevars(s), int-deq: IntDeq, btrue: tt, bnot: ¬_bb, FOLRule_ind: FOLRule_ind, spread: spread def, band: p ∧_b q, mFO-dest-atomic: mFO-dest-atomic, eq_atom: x =a y, null: null(as)
FDL editor aliases : FOLeffect

Latex:
FOLeffect(sr) == let s,r = sr in let hyps,concl = s in case(r) andI => let a,b = dest-"and"(concl) in inl [<hyps, a> <hyps, b>] impI => let a,b = dest-"imp"(concl) in inl [<[a / hyps], b>] allI with v => if \mneg{}\msubb{}v \mmember{}\msubb{} mFOL-sequent-freevars(<hyps, concl>) then let x,b = dest-all(concl)\000C; in inl [<hyps, b[v/x]>] else inr \mcdot{} fi existsI with v => if v \mmember{}\msubb{} mFOL-sequent-freevars(<hyps, concl>) then let x,b = dest-exists(concl); in inl [<hyps, b[v/x]>] else inr \mcdot{} fi orI (left?x) => let a,b = dest-"or"(concl) in inl [<hyps, if x then a else b fi >] hyp => if concl \mmember{}\msubb{} hyps then inl [] else inr \mcdot{} fi andE @i => if i <z ||hyps|| then let a,b = dest-"and"(hyps[i]) in inl [<[a; [b / hyps]], concl>] else inr \mcdot{} fi orE @i => if i <z ||hyps|| then let a,b = dest-"or"(hyps[i]) in inl [<[a / hyps], concl> <[b / hyps], concl>] else inr \mcdot{} fi impE @i => if i <z ||hyps|| then let a,b = dest-"imp"(hyps[i]) in inl [<hyps, a> <[b / hyps], concl>] else inr \mcdot{} fi allE @i with v => if i <z ||hyps|| \mwedge{}\msubb{} v \mmember{}\msubb{} mFOL-sequent-freevars(<hyps, concl>) then let x,b = dest-all(hyps[i]); in inl [<[b[v/x] / hyps], concl>] else inr \mcdot{} fi existsE @i with v => if i <z ||hyps|| \mwedge{}\msubb{} (\mneg{}\msubb{}v \mmember{}\msubb{} mFOL-sequent-freevars(<hyps, concl>)) then let x,b = dest-exists(hyps[i]); in inl [<[b[v/x] / hyps], concl>] else inr \mcdot{} fi falseE @i => if i <z ||hyps|| then let n,vars = dest-atomic(hyps[i]) in if n =a "false" \mwedge{}\msubb{} null(vars) then inl [] else inr \mcdot{} fi else inr \mcdot{} fi Date html generated: 2016_05_15-PM-10_28_05 Last ObjectModification: 2015_09_23-AM-08_25_40 Theory : minimal-first-order-logic Home Index