Nuprl Lemma : matrix+_wf

[n,m:ℤ]. ∀[j:ℕ1]. ∀[r:RngSig]. ∀[M:Matrix(n;m;r)].  (matrix+(r;j;M) ∈ Matrix(n 1;m 1;r))


Proof




Definitions occuring in Statement :  matrix+: matrix+(r;j;M) matrix: Matrix(n;m;r) int_seg: {i..j-} uall: [x:A]. B[x] member: t ∈ T add: m natural_number: $n int: rng_sig: RngSig
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T matrix+: matrix+(r;j;M) so_lambda: λ2y.t[x; y] int_seg: {i..j-} false: False implies:  Q not: ¬A less_than: a < b and: P ∧ Q less_than': less_than'(a;b) true: True squash: T top: Top prop: lelt: i ≤ j < k guard: {T} all: x:A. B[x] decidable: Dec(P) or: P ∨ Q uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] so_apply: x[s1;s2]
Lemmas referenced :  mx_wf rng_one_wf rng_zero_wf less_than_wf matrix-ap_wf subtract_wf int_seg_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermSubtract_wf itermVar_wf intformeq_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_subtract_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_wf decidable__lt intformless_wf itermAdd_wf int_formula_prop_less_lemma int_term_value_add_lemma lelt_wf top_wf int_seg_wf matrix_wf rng_sig_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin addEquality hypothesisEquality natural_numberEquality because_Cache lambdaEquality int_eqEquality setElimination rename hypothesis lessCases independent_pairFormation baseClosed equalityTransitivity equalitySymmetry imageMemberEquality axiomSqEquality isect_memberEquality voidElimination voidEquality lambdaFormation imageElimination productElimination independent_functionElimination dependent_set_memberEquality dependent_functionElimination unionElimination independent_isectElimination approximateComputation dependent_pairFormation intEquality axiomEquality

Latex:
\mforall{}[n,m:\mBbbZ{}].  \mforall{}[j:\mBbbN{}m  +  1].  \mforall{}[r:RngSig].  \mforall{}[M:Matrix(n;m;r)].    (matrix+(r;j;M)  \mmember{}  Matrix(n  +  1;m  +  1;r))



Date html generated: 2019_10_16-AM-11_27_28
Last ObjectModification: 2018_08_20-PM-09_42_13

Theory : matrices


Home Index