Nuprl Lemma : ctt-op-meaning_wf
∀[X:?CubicalContext]. ∀[vs:varname() List]. ∀[f:CttOp].
∀[L:{L:CttMeaningTriple List|
vdf-eq(?CubicalContext;ctt-binder-context X vs f;L)
∧ (↑wf-term(λf.ctt-arity(f);λt.ctt-kind(t);mkterm(f;map(λx.(fst(snd(x)));L))))} ].
(ctt-op-meaning{i:l}(X; vs; f; L) ∈ [[X;mkterm(f;map(λx.(fst(snd(x)));L))]])
Proof
Definitions occuring in Statement :
ctt-op-meaning: ctt-op-meaning{i:l}(X; vs; f; L),
ctt-binder-context: ctt-binder-context,
ctt-meaning-triple: CttMeaningTriple,
ctt_meaning: [[ctxt;t]],
ctt-arity: ctt-arity(x),
ctt-kind: ctt-kind(t),
ctt-op: CttOp,
cubical-context: ?CubicalContext,
wf-term: wf-term(arity;sort;t),
mkterm: mkterm(opr;bts),
varname: varname(),
vdf-eq: vdf-eq(A;f;L),
map: map(f;as),
list: T List,
assert: ↑b,
uall: ∀[x:A]. B[x],
pi1: fst(t),
pi2: snd(t),
and: P ∧ Q,
member: t ∈ T,
set: {x:A| B[x]} ,
apply: f a,
lambda: λx.A[x]
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
and: P ∧ Q,
so_lambda: λ2x y.t[x; y],
so_lambda: λ2x.t[x],
so_apply: x[s],
so_apply: x[s1;s2],
ctt-meaning-triple: CttMeaningTriple,
implies: P ⇒ Q,
guard: {T},
all: ∀x:A. B[x],
pi1: fst(t),
pi2: snd(t),
ctt-term: CttTerm,
wfterm: wfterm(opr;sort;arity),
uiff: uiff(P;Q),
uimplies: b supposing a,
prop: ℙ,
ctt-op: CttOp,
sq_type: SQType(T),
subtype_rel: A ⊆r B,
not: ¬A,
false: False,
or: P ∨ Q,
ifthenelse: if b then t else f fi ,
btrue: tt,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
bfalse: ff,
ctt-tokens: ctt-tokens(),
ctt-arity: ctt-arity(x),
eq_atom: x =a y,
ctt-opid-arity: ctt-opid-arity(t),
ctt-op-meaning: ctt-op-meaning{i:l}(X; vs; f; L),
mkterm: mkterm(opr;bts),
ctt_meaning: [[ctxt;t]],
ctt-meaning-type: ctt-meaning-type{i:l}(X;t),
term-opr: term-opr(t),
ctt-op-sort: ctt-op-sort(f),
isvarterm: isvarterm(t),
isl: isl(x),
outr: outr(x),
bor: p ∨bq,
int_seg: {i..j-},
lelt: i ≤ j < k,
decidable: Dec(P),
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
select: L[n],
cons: [a / b],
ctt-binder-context: ctt-binder-context,
provisional-subterm-context: provisional-subterm-context{i:l}(X;f;vs;L),
ctt-opr-is: ctt-opr-is(f;s),
ctt-subterm-context: ctt-subterm-context{i:l}(ctxt;f;n;vs;m),
band: p ∧b q,
int_iseg: {i...j},
cand: A c∧ B,
le: A ≤ B,
less_than': less_than'(a;b),
lt_int: i <z j,
eq_int: (i =z j),
subtract: n - m,
bdd-all: bdd-all(n;i.P[i]),
nat: ℕ,
primrec: primrec(n;b;c),
primtailrec: primtailrec(n;i;b;f),
squash: ↓T,
true: True,
cubical-context: ?CubicalContext,
ctt-level-type: {X ⊢lvl _},
less_than: a < b,
eq0-meaning: eq0-meaning{i:l}(Z),
spreadn: spread3,
eq1-meaning: eq1-meaning{i:l}(Z),
meet-meaning: meet-meaning{i:l}(A; B),
join-meaning: join-meaning{i:l}(A; B),
max-meaning: max-meaning{i:l}(A; B),
min-meaning: min-meaning{i:l}(A; B),
inv-meaning: inv-meaning{i:l}(A),
update-context4: update-context4{i:l}(X;phi),
Glue-meaning: Glue-meaning{i:l}(A; B; C; D),
let: let,
levelsup: levelsup(x;y),
ctt-level-comp: Comp(X;lvl;T),
case-meaning: case-meaning{i:l}(A; B; C; D),
update-context2: update-context2(X;v;t),
sigma-meaning: sigma-meaning{i:l}(A; B),
ge: i ≥ j ,
imax: imax(a;b),
le_int: i ≤z j,
bnot: ¬bb,
composition-structure: Gamma ⊢ Compositon(A),
composition-function: composition-function{j:l,i:l}(Gamma;A),
uniform-comp-function: uniform-comp-function{j:l, i:l}(Gamma; A; comp),
path-meaning: path-meaning{i:l}(A; B; C),
istype: istype(T),
pi-meaning: pi-meaning{i:l}(A; B),
decode-meaning: decode-meaning{i:l}(n; A),
encode-meaning: encode-meaning{i:l}(n; A),
context-ok: context-ok(ctxt),
allowed: allowed(x),
usquash: usquash(T),
bind-provision: bind-provision(x;t.f[t]),
provision: provision(ok; v),
update-cubical-context: ctxt; v:T,
context-set: context-set(ctxt),
allow: allow(x),
update-context-lvl: update-context-lvl(ctxt;lvl;T;v),
cubical_context: CubicalContext,
pathabs-meaning: pathabs-meaning{i:l}(A; B),
cubical-type: {X ⊢ _},
csm-id: 1(X),
csm-ap-type: (AF)s,
cc-fst: p,
interval-0: 0(𝕀),
csm-id-adjoin: [u],
csm-ap: (s)x,
csm-adjoin: (s;u),
interval-1: 1(𝕀),
pathapp-meaning: pathapp-meaning{i:l}(A; B; C),
cubical-path-app: pth @ r,
lambda-meaning: lambda-meaning{i:l}(A; B),
update-context3: update-context3(X;v;t),
apply-meaning: apply-meaning{i:l}(A; B; C),
pair-meaning: pair-meaning{i:l}(A; B; C),
fst-meaning: fst-meaning{i:l}(A; B; C),
snd-meaning: snd-meaning{i:l}(A; B; C),
glue-meaning: glue-meaning{i:l}(A; B; C; D),
constrained-cubical-term: {Gamma ⊢ _:A[phi |⟶ t]},
unglue-meaning: unglue-meaning{i:l}(A; B; C; D; E),
restrict-cubical-context: restrict-cubical-context{i:l}(ctxt;trm),
update-provisional-context-I: X,v:I,
update-cubical-context-I: ctxt,v:I,
provisional-type: Provisional(T),
quotient: x,y:A//B[x; y],
comp-meaning: comp-meaning{i:l}(A; B; C; D),
ctt-type-meaning: cttType(X),
univ-meaning: univ-meaning{i:l}(n),
bool: 𝔹,
unit: Unit,
it: ⋅,
assert: ↑b,
int_upper: {i...}
Lemmas referenced :
vdf-eq-implies2,
cubical-context_wf,
list_wf,
varname_wf,
ctt-term_wf,
ctt_meaning_wf,
pi2_wf,
ctt-binder-context_wf,
assert-wf-mkterm,
ctt-kind_wf,
term_wf,
ctt-arity_wf,
map_wf,
ctt-meaning-triple_wf,
vdf-eq_wf,
istype-assert,
wf-term_wf,
ctt-op_wf,
mkterm_wf,
eq_atom_wf,
subtype_base_sq,
atom_subtype_base,
assert_wf,
bnot_wf,
not_wf,
equal-wf-base,
set_subtype_base,
l_member_wf,
cons_wf,
nil_wf,
istype-atom,
istype-void,
length-map,
bool_cases,
bool_wf,
bool_subtype_base,
eqtt_to_assert,
assert_of_eq_atom,
eqff_to_assert,
iff_transitivity,
iff_weakening_uiff,
assert_of_bnot,
cons_member,
length_of_cons_lemma,
length_of_nil_lemma,
deq_member_cons_lemma,
atomdeq_reduce_lemma,
deq_member_nil_lemma,
decidable__le,
full-omega-unsat,
intformnot_wf,
intformle_wf,
itermConstant_wf,
istype-int,
int_formula_prop_not_lemma,
int_formula_prop_le_lemma,
int_term_value_constant_lemma,
int_formula_prop_wf,
decidable__lt,
length_wf,
intformand_wf,
intformless_wf,
itermVar_wf,
intformeq_wf,
int_formula_prop_and_lemma,
int_formula_prop_less_lemma,
int_term_value_var_lemma,
int_formula_prop_eq_lemma,
istype-le,
istype-less_than,
select-map,
subtype_rel_list,
top_wf,
length_firstn,
istype-false,
bdd_all_zero_lemma,
int_subtype_base,
primrec1_lemma,
select-firstn,
select_wf,
trivial-same-context-set,
ctt-kind-1,
context-ok_wf,
subtype_rel_self,
iff_weakening_equal,
subtype_rel_wf,
squash_wf,
true_wf,
istype-universe,
provisional-type_wf,
ctt-type-meaning_wf,
cubical_set_wf,
ctt-kind-0,
ctt-term-meaning_wf,
subtype_rel_universe1,
le_wf,
length_wf_nat,
pi1_wf_top,
bind-provision_wf,
cubical_context_wf,
provision_wf,
istype-true,
allowed_wf,
allow_wf,
subtype_rel_product,
context-set_wf,
mk_ctt-type-mng_wf,
face-type_wf,
face-comp_wf,
int_seg_wf,
ctt-level-type_wf,
int_seg_properties,
interval-type_wf,
int_seg_subtype_nat,
mk-ctt-term-mng_wf,
interval-0_wf,
interval-1_wf,
ctt-term-type-is_wf,
provisional-subtype,
subtype_rel-equal,
equal_wf,
ctt-term-level_wf,
ctt-level-type-subtype2,
face-zero_wf,
ctt-term-type-is-implies,
face-one_wf,
levelsup_wf,
face-and_wf,
face-or_wf,
interval-join_wf,
interval-meet_wf,
member_singleton,
interval-rev_wf,
context-set-update-context4,
context-subset_wf,
istype-cubical-term,
subtype_rel_transitivity,
ctt-type-type_wf,
cubical-equiv_wf,
ctt-level-type-subtype,
ctt-type-level_wf,
context-subset-subtype-simple,
cubical-term_wf,
cubical-term-eqcd,
update-context4_wf,
imax_ub,
ctt-type-comp_wf,
decidable__equal_int,
gluetype_wf,
int_seg_subtype_special,
int_seg_cases,
glue-comp_wf3,
ctt-level-comp_wf,
face-term-implies_wf,
face-0_wf,
face-1_wf,
case-type-partition,
case-type-comp-partition,
context-set-update-context2,
hd_wf,
cube-context-adjoin_wf-level-type,
update-context2_wf,
cubical-sigma_wf-level-type,
sigma_comp_wf2,
cubical-type-cumulativity,
composition-structure_wf,
cubical-type-cumulativity2,
cube-context-adjoin_wf,
path-type_wf,
cubical-type_wf,
equal_functionality_wrt_subtype_rel2,
path_comp_wf,
cubical-pi_wf-level-type,
pi_comp_wf2,
cubical-universe_wf,
universe-decode_wf,
universe-comp-fun_wf,
less_than_wf,
universe-encode_wf,
comp-fun-to-comp-op_wf,
implies-usquash2,
usquash_wf,
allow_provision_lemma,
allowed_provision_lemma,
csm-ap-type_wf,
cc-fst_wf_interval,
update-cubical-context_wf,
term-to-path_wf,
csm-ap-type_wf-level-type,
cubical-term_wf-level-type,
lelt_wf,
csm-ap-term_wf-level-type,
csm-id-adjoin_wf-interval-0,
csm-id-adjoin_wf-interval-1,
csm-ap-id-type,
pathtype_wf,
ctt-term-type_wf,
ctt-term-term_wf,
cubicalpath-app_wf,
cubical-lambda_wf,
context-set-update-context3,
cubical-pi_wf,
cubical_set_cumulativity-i-j,
update-context3_wf,
cubical-apply_wf,
csm-id-adjoin_wf,
cube_set_map_wf,
cubical-pair_wf,
cubical-sigma_wf,
cubical-fst_wf,
cubical-snd_wf,
cubical-fun_wf,
cubical-app_wf_fun,
ctt-term-meaning-subtype,
context-subset-is-subset,
subset-cubical-term,
glue-term_wf,
glue-type_wf,
unglue-term_wf,
update-provisional-context-I_wf,
restrict-cubical-context_wf,
context-subset-adjoin-subtype,
csm-ap-term_wf,
csm-context-subset-subtype2,
context-subset-term-subtype,
comp_term_wf,
discrete-cubical-type_wf,
discrete_comp_wf,
discrete-cubical-term_wf,
eq_int_wf,
assert_of_eq_int,
nat_properties,
compU_wf,
bool_cases_sqequal,
assert-bnot,
neg_assert_of_eq_int,
upper_subtype_nat,
nequal-le-implies,
zero-add,
int_upper_properties,
upper_subtype_upper
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
cut,
setElimination,
thin,
rename,
sqequalHypSubstitution,
productElimination,
instantiate,
introduction,
extract_by_obid,
isectElimination,
hypothesis,
cumulativity,
productEquality,
sqequalRule,
lambdaEquality_alt,
hypothesisEquality,
inhabitedIsType,
productIsType,
universeIsType,
applyEquality,
independent_functionElimination,
because_Cache,
dependent_functionElimination,
independent_pairEquality,
independent_isectElimination,
setIsType,
closedConclusion,
Error :memTop,
tokenEquality,
equalityTransitivity,
equalitySymmetry,
atomEquality,
baseClosed,
equalityIstype,
sqequalBase,
functionIsType,
unionElimination,
independent_pairFormation,
lambdaFormation_alt,
isect_memberEquality_alt,
dependent_set_memberEquality_alt,
natural_numberEquality,
approximateComputation,
dependent_pairFormation_alt,
voidElimination,
int_eqEquality,
intEquality,
callbyvalueReduce,
sqleReflexivity,
imageElimination,
imageMemberEquality,
universeEquality,
dependent_pairEquality_alt,
applyLambdaEquality,
hyp_replacement,
equalityElimination,
promote_hyp,
inrFormation_alt,
inlFormation_alt,
hypothesis_subsumption,
functionEquality,
setEquality
Latex:
\mforall{}[X:?CubicalContext]. \mforall{}[vs:varname() List]. \mforall{}[f:CttOp].
\mforall{}[L:\{L:CttMeaningTriple List|
vdf-eq(?CubicalContext;ctt-binder-context X vs f;L)
\mwedge{} (\muparrow{}wf-term(\mlambda{}f.ctt-arity(f);\mlambda{}t.ctt-kind(t);mkterm(f;map(\mlambda{}x.(fst(snd(x)));L))))\} ].
(ctt-op-meaning\{i:l\}(X; vs; f; L) \mmember{} [[X;mkterm(f;map(\mlambda{}x.(fst(snd(x)));L))]])
Date html generated:
2020_05_21-AM-10_46_37
Last ObjectModification:
2020_05_18-PM-11_53_12
Theory : cubical!type!theory
Home
Index