Nuprl Lemma : dl-ind_wf_definition
∀[A,B:TYPE]. ∀[aprog:x:ℕ ⟶ A]. ∀[comp,choose:x:Prog ⟶ x1:Prog ⟶ A ⟶ A ⟶ A]. ∀[iterate:x:Prog ⟶ A ⟶ A].
∀[test:x:Prop ⟶ B ⟶ A]. ∀[aprop:x:ℕ ⟶ B]. ∀[false:B]. ∀[implies,and,or:x:Prop ⟶ x1:Prop ⟶ B ⟶ B ⟶ B].
∀[box,diamond:x:Prog ⟶ x1:Prop ⟶ A ⟶ B ⟶ B].
(dl-ind(
dl-aprog(x0)⇒ aprog[x0];
dl-comp(x1,x2)⇒ x3,x4.comp[x1;x2;x3;x4];
dl-choose(x5,x6)⇒ x7,x8.choose[x5;x6;x7;x8];
dl-iterate(x9)⇒ x10.iterate[x9;x10];
dl-test(x11)⇒ x12.test[x11;x12];
dl-aprop(x13)⇒ aprop[x13];
dl-false⇒ false;
dl-implies(x14,x15)⇒ x16,x17.implies[x14;x15;x16;x17];
dl-and(x18,x19)⇒ x20,x21.and[x18;x19;x20;x21];
dl-or(x22,x23)⇒ x24,x25.or[x22;x23;x24;x25];
dl-box(x26,x27)⇒ x28,x29.box[x26;x27;x28;x29];
dl-diamond(x30,x31)⇒ x32,x33.diamond[x30;x31;x32;x33]) ∈ d:dl-Obj() ⟶ if dl-kind(d) =a "prog"
then A
else B
fi )
Proof
Definitions occuring in Statement :
dl-ind: dl-ind,
dl-kind: dl-kind(d),
dl-prop: Prop,
dl-prog: Prog,
dl-Obj: dl-Obj(),
nat: ℕ,
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
uall: ∀[x:A]. B[x],
so_apply: x[s1;s2;s3;s4],
so_apply: x[s1;s2],
so_apply: x[s],
member: t ∈ T,
function: x:A ⟶ B[x],
token: "$token"
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
so_lambda: λ2x.t[x],
subtype_rel: A ⊆r B,
all: ∀x:A. B[x],
implies: P ⇒ Q,
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
ifthenelse: if b then t else f fi ,
bfalse: ff,
so_apply: x[s],
eq_atom: x =a y,
dl-kind: dl-kind(d),
mobj-kind: mobj-kind(x),
pi1: fst(t),
dl-prog-obj: prog(x),
so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]),
so_apply: x[s1;s2;s3;s4],
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
dl-prop-obj: prop(x)
Lemmas referenced :
dl-ind_wf,
eq_atom_wf,
dl-kind_wf,
dl-Obj_wf,
istype-nat,
dl-prog_wf,
dl-prop_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
sqequalRule,
lambdaEquality_alt,
hypothesisEquality,
hypothesis,
applyEquality,
because_Cache,
closedConclusion,
tokenEquality,
inhabitedIsType,
lambdaFormation_alt,
unionElimination,
equalityElimination,
equalityIstype,
equalityTransitivity,
equalitySymmetry,
dependent_functionElimination,
independent_functionElimination,
universeIsType,
TYPEMemberIsType,
functionIsType,
TYPEIsType
Latex:
\mforall{}[A,B:TYPE]. \mforall{}[aprog:x:\mBbbN{} {}\mrightarrow{} A]. \mforall{}[comp,choose:x:Prog {}\mrightarrow{} x1:Prog {}\mrightarrow{} A {}\mrightarrow{} A {}\mrightarrow{} A]. \mforall{}[iterate:x:Prog
{}\mrightarrow{} A
{}\mrightarrow{} A].
\mforall{}[test:x:Prop {}\mrightarrow{} B {}\mrightarrow{} A]. \mforall{}[aprop:x:\mBbbN{} {}\mrightarrow{} B]. \mforall{}[false:B]. \mforall{}[implies,and,or:x:Prop
{}\mrightarrow{} x1:Prop
{}\mrightarrow{} B
{}\mrightarrow{} B
{}\mrightarrow{} B].
\mforall{}[box,diamond:x:Prog {}\mrightarrow{} x1:Prop {}\mrightarrow{} A {}\mrightarrow{} B {}\mrightarrow{} B].
(dl-ind(
dl-aprog(x0){}\mRightarrow{} aprog[x0];
dl-comp(x1,x2){}\mRightarrow{} x3,x4.comp[x1;x2;x3;x4];
dl-choose(x5,x6){}\mRightarrow{} x7,x8.choose[x5;x6;x7;x8];
dl-iterate(x9){}\mRightarrow{} x10.iterate[x9;x10];
dl-test(x11){}\mRightarrow{} x12.test[x11;x12];
dl-aprop(x13){}\mRightarrow{} aprop[x13];
dl-false{}\mRightarrow{} false;
dl-implies(x14,x15){}\mRightarrow{} x16,x17.implies[x14;x15;x16;x17];
dl-and(x18,x19){}\mRightarrow{} x20,x21.and[x18;x19;x20;x21];
dl-or(x22,x23){}\mRightarrow{} x24,x25.or[x22;x23;x24;x25];
dl-box(x26,x27){}\mRightarrow{} x28,x29.box[x26;x27;x28;x29];
dl-diamond(x30,x31){}\mRightarrow{} x32,x33.diamond[x30;x31;x32;x33]) \mmember{} d:dl-Obj()
{}\mrightarrow{} if dl-kind(d) =a "prog" then A else B fi )
Date html generated:
2019_10_15-AM-11_41_58
Last ObjectModification:
2019_03_26-AM-11_25_10
Theory : dynamic!logic
Home
Index